Логика предикатов в Haskell

Question

Логика предикатов в Haskell

Я использовал следующую структуру данных для представления логики высказываний в Haskell:

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

Любые комментарии к этой структуре приветствуются.

Однако теперь я хочу расширить свои алгоритмы для обработки FOL - логика предикатов. Каков был бы хороший способ представить FOL в Haskell?

Я видел версии, которые являются - в значительной степени - расширение вышеупомянутого и версии, которые основаны на более классических контекстно-свободных грамматиках. Есть ли какая-либо литература по этому, которое могло быть рекомендовано?

25

haskell data-structures context-free-grammar first-order-logic

задан wen 12 July 2010 в 13:14

1 ответ

Другие вопросы по тегам:

haskell data-structures context-free-grammar first-order-logic

Похожие вопросы:

score 29 · Accepted Answer

Это известно как абстрактный синтаксис высшего порядка.

Первое решение: Использовать лямбды Хаскеля. Тип данных может выглядеть так:

data Prop 
    = Not   Prop
    | And   Prop Prop
    | Or    Prop Prop
    | Impl  Prop Prop
    | Equiv Prop Prop
    | Equals Obj Obj
    | ForAll (Obj -> Prop)
    | Exists (Obj -> Prop)
    deriving (Eq, Ord)

data Obj
    = Num Integer
    | Add Obj Obj
    | Mul Obj Obj
    deriving (Eq, Ord)

Вы можете написать формулу так:

ForAll (\x -> Exists (\y -> Equals (Add x y) (Mul x y))))

Это подробно описано в статье The Monad Reader. Очень рекомендую.

Второе решение:

Используйте строки типа

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

data Obj
    = Num Integer
    | Var String
    | Add Obj Obj
    | Mul Obj Obj
    deriving (Eq, Ord)

Тогда вы можете написать формулу типа

ForAll "x" (Exists "y" (Equals (Add (Var "x") (Var "y")))
                               (Mul (Var "x") (Var "y"))))))

Преимущество в том, что вы можете легко показать формулу (трудно показать функцию Obj -> Prop). Недостаток в том, что вам придется писать меняющиеся имена при столкновении (~альфа-преобразование) и подстановке (~бета-преобразование). В обоих решениях вместо двух типов данных можно использовать GADT:

 data FOL a where
    True :: FOL Bool
    False :: FOL Bool
    Not :: FOL Bool -> FOL Bool
    And :: FOL Bool -> FOL Bool -> FOL Bool
    ...
     -- first solution
    Exists :: (FOL Integer -> FOL Bool) -> FOL Bool
    ForAll :: (FOL Integer -> FOL Bool) -> FOL Bool
    -- second solution
    Exists :: String -> FOL Bool -> FOL Bool
    ForAll :: String -> FOL Bool -> FOL Bool
    Var :: String -> FOL Integer
    -- operations in the universe
    Num :: Integer -> FOL Integer
    Add :: FOL Integer -> FOL Integer -> FOL Integer
    ...

Третье решение: Используйте цифры для обозначения границы переменной, где нижняя означает более глубокую. Например, в ForAll (Exists (Equals (Num 0) (Num 1))) первая переменная будет связана с Exists, а вторая - с ForAll. Это известно как числительные де Бройна. См. Я не число - я свободная переменная.