विधेय तर्क हास्केल

Question

में मैं हास्केल में प्रोपोज़िशनल तर्क के प्रतिनिधित्व के लिए निम्न डेटा संरचना का उपयोग किया गया है:

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

इस संरचना पर किसी भी टिप्पणी का स्वागत है।

हालांकि, अब मैं एफओएल - भविष्यवाणी तर्क को संभालने के लिए अपने एल्गोरिदम का विस्तार करना चाहता हूं। हास्केल में एफओएल का प्रतिनिधित्व करने का एक अच्छा तरीका क्या होगा?

मैंने संस्करणों को देखा है - बहुत अधिक - उपर्युक्त का विस्तार, और संस्करण जो अधिक क्लासिक संदर्भ-मुक्त व्याकरण पर आधारित हैं। क्या इस पर कोई साहित्य है, इसकी सिफारिश की जा सकती है?

Answer 1

इसे higher-order abstract syntax के रूप में जाना जाता है।

पहला समाधान: हास्केल के लैम्ब्डा का उपयोग करें। एक डेटाप्रकार दिखाई दे सकता है जैसे:

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 (Obj -> Prop) 
    | Exists (Obj -> Prop) 
    deriving (Eq, Ord) 

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

के रूप में आप एक सूत्र लिख सकते हैं। अत्यधिक सिफारिशित।

दूसरा समाधान:

उपयोग तार

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 में (मौजूद (बराबर (संख्या 0) (संख्या 1))) पहला चर मौजूदियों से जुड़ जाएगा, और दूसरा FORAll। इसे डी Bruijn अंकों के रूप में जाना जाता है। I am not a number - I am a free variable देखें।

Answer 2

आईसीएफपी 2013 में प्रस्तुत किए गए एक्सेलसन और क्लेसेन द्वारा कार्यात्मक मोती Using Circular Programs for Higher-Order Syntax का उल्लेख करने के लिए यहां एक उत्तर जोड़ने के लिए उचित लगता है, और briefly described by Chiusano on his blog।

यह समाधान आसानी से फॉर्मूला (@ 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])