Predicate logic trong Haskell

Question

Tôi đã sử dụng các cấu trúc dữ liệu sau đây cho các đại diện của logic mệnh đề trong Haskell:

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

Bất kỳ ý kiến ​​về cấu trúc này được hoan nghênh.

Tuy nhiên, bây giờ tôi muốn mở rộng thuật toán của mình để xử lý FOL - vị ngữ logic. Điều gì sẽ là một cách tốt để đại diện cho FOL trong Haskell?

Tôi đã xem các phiên bản - khá nhiều - một phần mở rộng của các phiên bản ở trên và các phiên bản dựa trên ngữ pháp ngữ cảnh cổ điển hơn. Có bất kỳ tài liệu nào về điều này, có thể được đề nghị không?

Answer 1

Điều này được gọi là higher-order abstract syntax.

Giải pháp đầu tiên: Sử dụng lambda của Haskell. Một datatype có thể trông giống như:

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) 

Bạn có thể viết một công thức như sau:

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

này được mô tả chi tiết trong trong The Monad Reader bài viết. Rat khuyen khich.

giải pháp thứ hai:

Sử dụng chuỗi như

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) 

Sau đó, bạn có thể viết một công thức như

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

Ưu điểm là bạn có thể hiển thị công thức một cách dễ dàng (thật khó để hiển thị hàm Obj -> Prop). Điểm bất lợi là bạn phải viết tên thay đổi khi va chạm (~ chuyển đổi alpha) và thay thế (~ beta conversion). Trong cả hai giải pháp, bạn có thể sử dụng GADT thay vì hai kiểu dữ liệu:

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 
    ... 

giải pháp thứ ba: Sử dụng chữ số để đại diện cho nơi biến được ràng buộc, nơi phương tiện thấp sâu hơn. Ví dụ, trong ForAll (Exists (bằng (Num 0) (Num 1))) biến đầu tiên sẽ liên kết với Exists, và thứ hai là ForAll. Điều này được gọi là chữ số de Bruijn. Xem I am not a number - I am a free variable.

Answer 2

Có vẻ như thích hợp để thêm câu trả lời vào đây để đề cập đến hàm ngọc trai chức năng Using Circular Programs for Higher-Order Syntax, bởi Axelsson và Claessen, được trình bày tại ICFP 2013 và briefly described by Chiusano on his blog.

Giải pháp này gọn gàng kết hợp việc sử dụng gọn gàng cú pháp của Haskell (giải pháp đầu tiên của @ sdcvvc) với khả năng in công thức dễ dàng (giải pháp thứ hai của @ 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 

Giải pháp này sẽ sử dụng một kiểu dữ liệu như:

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) 

Nhưng cho phép bạn viết công thức như sau:

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