25

Haskellで命題論理を表現するために次のデータ構造を使用しています。

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

この構造に関するコメントは大歓迎です。

ただし、ここで、アルゴリズムを拡張してFOL（述語論理）を処理したいと思います。HaskellでFOLを表現する良い方法は何でしょうか？

上記の拡張版であるバージョンと、より古典的な文脈自由文法に基づくバージョンを見てきました。これに関する文献はありますか、それは推奨される可能性がありますか？

4

2 に答える 2

29

これは、高次抽象構文として知られています。

最初の解決策： 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))))

これについては、 MonadReaderの記事で詳しく説明されています。強くお勧めします。

2番目の解決策：

次のような文字列を使用します

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です）。欠点は、衝突（〜alpha変換）と置換（〜beta変換）で名前を変更する必要があることです。どちらのソリューションでも、2つのデータ型の代わりに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
    ...

3番目の解決策：数字を使用して変数がバインドされている場所を表します。低いほど深いことを意味します。たとえば、ForAll（Exists（Equals（Num 0）（Num 1）））では、最初の変数はExistsにバインドされ、2番目はForAllにバインドされます。これはdeBruijn数字として知られています。私は数ではありません-私は自由変数です。

于 2010-07-12T14:54:54.177 に答える
4

ICFP 2013で発表され、Chiusanoがブログで簡単に説明した、AxelssonとClaessenによる、高次構文の循環プログラムを使用した機能的な真珠について言及するために、ここに回答を追加するのが適切と思われます。

このソリューションは、Haskellの構文（@sdcvvcの最初のソリューション）の適切な使用法と、数式を簡単に印刷する機能（@sdcvvcの2番目のソリューション）をうまく組み合わせています。

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])
于 2015-03-28T12:49:28.790 に答える