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

Question

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

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

Answer 1

Это называется higher-order abstract syntax.

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

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. Это называется цифрами Брюйна. См. I am not a number - I am a free variable.

Answer 2

Кажется уместным добавить ответ здесь, чтобы упомянуть функциональную жемчужину Using Circular Programs for Higher-Order Syntax от Axelsson и Claessen, которая была представлена ​​на ICFP 2013 и briefly described by Chiusano on his blog.

Это решение аккуратно сочетает в себе аккуратное использование синтаксиса 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])