Предикатная логика в Хаскеле - PullRequest
Новая
       15

Предикатная логика в Хаскеле

25 голосов
/ 12 июля 2010

Я использовал следующую структуру данных для представления логики высказываний в 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?

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

Ответы [ 2 ]

29 голосов
/ 12 июля 2010

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

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

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.Это известно как цифры де Брюин.См. Я не число - я свободная переменная .

4 голосов
/ 28 марта 2015

Представляется целесообразным добавить здесь ответ, чтобы упомянуть функциональную жемчужину Использование циркулярных программ для синтаксиса высшего порядка от Axelsson и Claessen, которая была представлена ​​на ICFP 2013, и , кратко описаннуюКьюзано в своем блоге .

Это решение аккуратно сочетает аккуратное использование синтаксиса Haskell (первое решение @ sdcvvc) со способностью легко печатать формулы (второе решение @ sdcvvc). 

forAll :: (Prop -> Prop) -> Prop
forAll f = ForAll n body
  where body = f (Var n)
        n    = maxBV body + 1

bot :: Name
bot = 0

-- Computes the maximum bound variable in the given expression
maxBV :: Prop -> Name
maxBV (Var _  ) = bot
maxBV (App f a) = maxBV f `max` maxBV a
maxBV (Lam n _) = n

Это решение будет использовать тип данных, такой как: 

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

Но позволяет записывать формулы как: 

forAll (\x -> Pred "P" [x] `Impl` Pred "Q" [x])
...