module Equational_Logic where {- Implement the "..." below and check that at least all PROPERTY equations hold. -} {--- Term datatype: either a function symbol applied to sub-terms, or a variable. ---} data Term = App String [Term] | Var String deriving (Show, Read, Eq) {--- Substitutions are represented as Haskell functions ---} type Subst = String -> Term no_subst :: Subst no_subst n = Var n replace :: String -> Term -> Subst -> Subst replace n t s n' = if n == n' then t else s n' {--- The substitution { x |-> f(a, b), y |-> z } is written as replace "x" (App "f" [App "a" [], App "b" []]) \$ replace "y" (Var "z") \$ no_subst ---} {--- A proof either failed: "None", or states the equality btw. a ~ b: "Some (a, b)" ---} type Proof = Maybe (Term, Term) {--- HOMEWORK: Implement the following rules ---} {- compute substitute s(t): -} subst :: Subst -> Term -> Term subst s t = ... {- There is no signature, so we do not need to check for it. -} axiomP :: Term -> Term -> Proof axiomP s t = ... reflP :: Term -> Proof reflP t = ... symmP :: Proof -> Proof symmP p = ... tranP :: Proof -> Proof -> Proof tranP l r = ... substP :: Subst -> Proof -> Proof substP s p = ... congP :: String -> [Proof] -> Proof congP c ps = ... {--- Now some example proofs, or failures ---} sig = [("f", 2), ("i", 1), ("e", 0)] f a b = App "f" [a, b] i a = App "i" [a] e = App "e" [] x = Var "x" y = Var "y" z = Var "z" assocP = axiomP (f x (f y z)) (f (f x y) z) leftUnitP = axiomP (f e x) x rightUnitP = axiomP (f x e) x inverseP = axiomP (f x (i x)) e prf = foldl1 tranP [ symmP (substP (replace "x" (i (i x)) \$ no_subst) leftUnitP), congP "f" [symmP inverseP, reflP (i (i x))], symmP (substP (replace "y" (i x) \$ replace "z" (i (i x)) \$ no_subst) assocP), congP "f" [reflP x, substP (replace "x" (i x) \$ no_subst) inverseP], rightUnitP ] {- PROPERTY: prf == Just (i (i x), x) -} flr = tranP leftUnitP rightUnitP {- PROPERTY: flr == Nothing -} flr2 = tranP (symmP leftUnitP) rightUnitP {- PROPERTY: flr2 == Nothing -} prf2 = tranP leftUnitP (symmP rightUnitP) {- PROPERTY: prf2 == Just (f e x, f x e) -}