{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-} -- Copied from module LambdaCalc where import Data.List import Data.Typeable import Control.Monad import GHC.Generics import Test.QuickCheck import Test.SmartCheck type Sym = String data Expr = Var Sym | App Expr Expr | Lam Sym Expr deriving (Eq, Read, Show, Typeable, Generic) freeVars :: Expr -> [Sym] freeVars (Var v) = [v] freeVars (App f a) = freeVars f `union` freeVars a freeVars (Lam i e) = freeVars e \\ [i] subst :: Sym -> Expr -> Expr -> Expr subst v x b = sub b where sub e@(Var i) = if i == v then x else e sub (App f a) = App (sub f) (sub a) sub (Lam i e) = if v == i then Lam i e else if i `elem` fvx then let i' = cloneSym e i e' = substVar i i' e in Lam i' (sub e') else Lam i (sub e) fvx = freeVars x cloneSym e i = loop i where loop i' = if i' `elem` vs then loop (i ++ "'") else i' vs = fvx ++ freeVars e substVar :: Sym -> Sym -> Expr -> Expr substVar v v' e = subst v (Var v') e alphaEq :: Expr -> Expr -> Bool alphaEq (Var v) (Var v') = v == v' alphaEq (App f a) (App f' a') = alphaEq f f' && alphaEq a a' alphaEq (Lam v e) (Lam v' e') = alphaEq e (substVar v' v e') alphaEq _ _ = False nf :: Expr -> Expr nf ee = spine ee [] where spine (App f a) as = spine f (a:as) spine (Lam v e) [] = Lam v (nf e) spine (Lam v e) (a:as) = spine (subst v a e) as spine f as = app f as app f as = foldl App f (map nf as) betaEq :: Expr -> Expr -> Bool betaEq e1 e2 = alphaEq (nf e1) (nf e2) z,s,m,n :: Expr [z,s,m,n] = map (Var . (:[])) "zsmn" app2 :: Expr -> Expr -> Expr -> Expr app2 f x y = App (App f x) y zero, one, two, three, plus :: Expr zero = Lam "s" $ Lam "z" z one = Lam "s" $ Lam "z" $ App s z two = Lam "s" $ Lam "z" $ App s $ App s z three = Lam "s" $ Lam "z" $ App s $ App s $ App s z plus = Lam "m" $ Lam "n" $ Lam "s" $ Lam "z" $ app2 m s (app2 n s z) test0 :: Bool test0 = betaEq (app2 plus one two) three --------------------------------------------------------------------------------- instance SubTypes Expr instance SubTypes Pr --------------------------------------------------------------------------------- data Pr = Pr Expr Expr deriving (Read, Show, Typeable, Generic) instance Arbitrary Expr where arbitrary = sized mkE where mkE 0 = liftM Var vars mkE x = oneof [ liftM2 App (liftM2 Lam vars mkE') mkE' , liftM2 Lam vars mkE' ] where mkE' = mkE =<< choose (0, x-1) vars :: Gen [Char] vars = oneof $ map return ["x", "y", "z"] instance Arbitrary Pr where arbitrary = do expr <- arbitrary return $ Pr expr expr --------------------------------------------------------------------------------- -- prop0 :: Pr -> Property -- prop0 (Pr (e0, e1)) = alphaEq e0 e1 ==> betaEq e0 e1 -- if you do a beta reduction to nf -- prop1 :: Pr -> ScProperty -- prop1 (Pr e0 e1) = -- Timeout due to possible non-termination -- within 1000 $ alphaEq e0 e1 --> betaEq e0 (substVar "x" "y" e1) -- lambdaTest :: IO () -- lambdaTest = smartCheck args prop1 -- where args = scStdArgs { qcArgs = stdArgs { maxSuccess = 100 -- , maxSize = 100 -- } -- } --------------------------------------------------------------------------------- -- Cruft {- nonDet = App x x where x = Lam "x" (App (Var "x") (Var "x")) xx = (App (Lam "`" (App (Lam "\SI" (Var "f")) (App (Lam "" (Var "O\172")) (Var "3UC"))))) aa (Pr a b) = alphaEq a b -}