Haskell - реализация логических выражений первого порядка

Я пытаюсь реализовать FOL с помощью Haskell. Логика первого порядка может быть в форме предложений, связанных между собой связками, такими как And и Or. Существуют также квантификаторы, которые имеют ограниченную область действия в выражении.

Что я сделал до сих пор:

импортировать Data.List

data Prop 
    = Not Prop
    | Prop And Prop
    | Prop Or Prop
    | Prop Impl Prop
    | Prop Equiv Prop
    | ForAll String Prop
    | Exists String Prop
    deriving (Eq, Ord)

Но я получаю эту ошибку:

 Multiple declarations of ‘Prop’

haskell ghci first-order-logic
person SalmaFG    schedule 25.11.2014    source источник
comment
Имейте в виду, что вы включаете квантификаторы, такие как ForAll, но не включаете какой-либо способ использования количественных переменных, то есть предикатов. Я бы добавил Pred String [Term] для предикатов, где data Term = Var String | App String [Term]. Вы также можете добавить равенство.   -  person chi    schedule 25.11.2014
comment
Да, это была моя первая мысль: единственный способ получить значение типа Prop прямо сейчас - это что-то сумасшедшее, например let a = Not b; b = Not a in ..., потому что в этой формуле отсутствуют примитивы.   -  person CR Drost    schedule 25.11.2014

Ответы (3)


arrow_upward
6
arrow_downward

Когда вы объявляете алгебраический тип данных, правая часть объявления представляет собой «список» возможных конструкторов для этого типа. Однако конструкторы - это просто функции, то есть они используются в префиксной нотации. Вы пытаетесь использовать, например, And инфиксный конструктор, который не работает.

Следующий код работает хорошо:

data Prop
    = Not Prop
    | And Prop Prop
    | Or Prop Prop
    | Impl Prop Prop
    | Equiv Prop Prop
    | ForAll String Prop
    | Exists String Prop
    deriving (Eq, Ord)

Однако вы можете определять функции, имитирующие конструкторы, например -

propAnd :: Prop -> Prop -> Prop
propAnd a b = And a b

и используйте их инфиксным способом, используя обратные кавычки: a `propAnd` b. Как предлагается в комментариях, в этом нет необходимости, поскольку And уже можно использовать в инфиксном виде: a `And` b

Другой вариант - определить сами конструкторы инфиксным способом:

data Prop
    = Not Prop
    | Prop `And` Prop
    | Prop `Or` Prop
    | Prop `Impl` Prop
    | Prop `Equiv` Prop
    | ForAll String Prop
    | Exists String Prop
    deriving (Eq, Ord)

а затем работают и a `And` b, и And a b.

Примечание: ваш тип данных бесконечен, поскольку все конструкторы занимают один или несколько Prop. Я думаю, вам следует также включить некоторые «атомарные» конструкторы.

person zegkljan    schedule 25.11.2014
comment
Вы правы насчет атомарных констант, поэтому я попытался добавить их как таковые: data Prop = Not Prop | Опора And Опора | Obj And Obj | Prop And Obj | Obj And Prop | Опора Or Опора | Obj Or Obj | Prop Or Obj | Obj Or Prop | Опора Impl Опора | Obj Impl Obj | Prop Impl Obj | Obj Impl Prop | Опора Equiv Опора | Obj Equiv Obj | Prop Equiv Obj | Obj Equiv Prop | ForAll String Prop | Exists String Prop, производные (Eq, Ord) данные Obj = Var String | Pred String [Prop] deeding (Eq, Ord) Но в нем говорится, что я делаю несколько объявлений. - person SalmaFG; 25.11.2014
comment
propAnd на самом деле избыточен: даже если конструктор And был объявлен не-инфиксным способом, конструктор все равно можно использовать инфиксно, используя обратные кавычки, как в a `And` b. - person chi; 25.11.2014
comment
@SalmaFG Теперь вы используете And (и все остальные конструкторы) несколько раз. Я не знаю, что вы думаете о дизайне вашего программного обеспечения, поэтому не знаю, что мне предложить. На самом деле, я знаю - задайте новый вопрос о том, с чем вы боретесь. - person zegkljan; 25.11.2014

arrow_upward
6
arrow_downward

Вы пытаетесь использовать Prop в качестве имени конструктора несколько раз (первое слово всегда является именем конструктора). Похоже, вы хотите использовать инфиксные конструкторы для And, Or и других. Чтобы написать их инфиксным, вам нужно поместить имена конструкторов в обратные кавычки.

data Prop
    = Not Prop
    | Prop `And` Prop
    ...
person Helmut Grohne    schedule 25.11.2014
comment
Что именно означает эта обратная кавычка? Делает ли это And строкой? - person SalmaFG; 25.11.2014
comment
@SalmaFG Обратный апостроф превращает обычное имя в инфиксный оператор. - person MathematicalOrchid; 25.11.2014

arrow_upward
3
arrow_downward

Вы сказали

...
| Prop And Prop
...

Вам нужно сказать

...
| And Prop Prop
...

(И так же для всех остальных). Имя конструктора должно быть первым.

person MathematicalOrchid    schedule 25.11.2014