{-# OPTIONS -W #-} {-# LANGUAGE NoMonomorphismRestriction #-} -- Here we encode the ``target language'', the language -- to express denotations (or, meanings) -- We use the same technique to embed a formal language -- as the one we used before to embed a fraghment of -- English (cf. Montague's famous quote). -- To warm-up, we start with the language of -- classical propositional logic (without equality) -- Formula simplification (the interpreter P below) -- is much easier to explain in the propositional case. module Prop where import qualified Data.Set as S -- Embedding of the language of propositional logic class Prop lrepr where -- Propositional letters pretty' :: lrepr quiet' :: lrepr raining' :: lrepr -- (more can be added later) true :: lrepr neg :: lrepr -> lrepr conj :: lrepr -> lrepr -> lrepr -- sample formulas fml1 = neg (conj (neg (neg true)) (neg true)) fml2 = quiet' `conj` raining' fml3 = pretty' `conj` neg raining' `conj` true `conj` pretty' -- Ex: Where is false and disjunction? -- How to write TRUE AND (FALSE == (TRUE OR P)) -- Abbreviations -- They are not part of Prop (not part of the language) -- Consider them as `abbreviations', of `macros' false = neg true disj x y = neg (conj (neg x) (neg y)) fml4 = true `conj` (false `disj` pretty') -- I still haven't written the exercise. It remains -- an exercise. We need to add implication and -- equivalence. -- ------------------------------------------------------------------------ -- Models -- First model: the domain is Bool (Boolean algebra with two -- constants, True and False) data R = R { unR :: Bool } instance Prop R where -- One particular interpretation function -- interpreting prop letters pretty' = R True quiet' = R True raining' = R False -- Logical part of the model true = R True neg (R True) = R False neg (R False) = R True conj (R True) (R True) = R True conj _ _ = R False -- Evaluate our examples in the model fml1R = unR fml1 fml2R = unR fml2 fml3R = unR fml3 fml4R = unR fml4 -- Exercise (adv): the instance R has the interpretation -- of propositional letters wired-in. -- If we wish to try a different interpretation function, -- we have to re-write the instance, repeating -- neg and conj (which stay constant) -- Re-write R so that the interpretation of propositional -- letters (I) is a parameter, to be specified by the user. -- We can give another model: the standard set-theoretical -- one, in a richer Boolean algebra (posets) -- Ex: What are the deriving Eq and Ord, and why we need them? data Event = PP | PQ | PR deriving (Eq, Ord, Show) -- Ex: What is the meaning of the following? s_top = S.fromList [PP,PQ,PR] data RS = RS{unRS :: S.Set Event} instance Prop RS where -- One particular interpretation function -- interpreting prop letters pretty' = RS (S.singleton PP) quiet' = RS (S.singleton PQ) raining' = RS (S.singleton PR) -- Logical part of the model true = RS s_top neg (RS s) = RS (S.difference s_top s) conj (RS s1) (RS s2) = RS (S.intersection s1 s2) fml1RS = unRS fml1 fml2RS = unRS fml2 fml3RS = unRS fml3 fml4RS = unRS fml4 -- Compare fml3RS vs fml3R and the same for fml4 -- See the difference? Why? -- fml1R and fml3R were the same; but fml1RS and fml3RS are not -- Some models are more discriminating... -- Is it possible to build a model that is even more discriminating? -- And yet another `model'. Why do we need it? -- Is it a real model? data C = C { unC :: String } instance Prop C where pretty' = C "P" quiet' = C "Q" raining' = C "R" true = C "T" neg (C x) = C ("-" ++ x) conj (C x) (C y) = C ("(" ++ x ++ " & " ++ y ++ ")") fml1C = unC fml1 fml2C = unC fml2 fml3C = unC fml3 fml4C = unC fml4 -- ------------------------------------------------------------------------ -- Simplification: (very) simple inference -- an instance of a language _transformation_ -- data P0 lrepr = P0{unP0 :: lrepr} data P0 lrepr = P0 lrepr unP0 (P0 x) = x instance (Prop lrepr) => Prop (P0 lrepr) where -- is there a weird self-reference in here? -- how could this possibly work? pretty' = P0 pretty' quiet' = P0 quiet' raining' = P0 raining' true = P0 true neg (P0 x) = P0 (neg x) conj (P0 xs) (P0 ys) = P0 (conj xs ys) -- How to use P0? fml1P0C = unC . unP0 \$ fml1 fml1P0C' = unC (unP0 fml1) -- Isn't this stupid? -- What possible use could be for P0? -- (if it isn't a rhetorical question, it should be) -- What is the intended meaning for known? data P lrepr = P { unP :: lrepr, known :: Maybe Bool } instance (Prop lrepr) => Prop (P lrepr) where pretty' = P pretty' Nothing quiet' = P quiet' Nothing raining' = P raining' Nothing true = P true (Just True) neg (P _ (Just False)) = true neg (P _ (Just True)) = P (neg true) (Just False) -- Why not to put false on the right-hand side of the above? neg (P x _) = P (neg x) Nothing conj (P _ (Just True)) y = y conj x (P _ (Just True)) = x conj (P _ (Just False)) _ = false conj _ (P _ (Just False)) = false conj (P x _) (P y _) = P (conj x y) Nothing fml1PC = unC . unP \$ fml1 fml2PC = unC . unP \$ fml2 fml3PC = unC . unP \$ fml3 fml4PC = unC . unP \$ fml4 -- It is good. Still we can do better. -- Can we simplify double-negation and repeated -- occurrences of the same literal? -- Does this remind you of normalization?