{-# OPTIONS -fglasgow-exts #-} {- Using GADTs to encode normalizable and non-normalizable terms in the lambda calculus. For definitions of normalizable and de Bruin indices, I used: Christian Urban and Stefan Berghofer - A Head-to-Head Comparison of de Bruijn Indices and Names. In Proceedings of the International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2006). Seattle, USA. ENTCS. Pages 46-59 http://www4.in.tum.de/~urbanc/Publications/lfmtp-06.ps @incollection{ pierce97foundational, author = "Benjamin Pierce", title = "Foundational Calculi for Programming Languages", booktitle = "The Computer Science and Engineering Handbook", publisher = "CRC Press", address = "Boca Raton, FL", editor = "Allen B. Tucker", year = "1997", url = "citeseer.ist.psu.edu/pierce95foundational.html" } -} module Terminating where -- Terms in the untyped lambda-calculus with the de Bruijn representation data Term t where Var :: Nat n -> Term (Var n) Lambda :: Term t -> Term (Lambda t) Apply :: Term t1 -> Term t2 -> Term (Apply t1 t2) -- Natural numbers data Nat n where Zero :: Nat Z Succ :: Nat n -> Nat (S n) data Z data S n data Var t data Lambda t data Apply t1 t2 data Less n m where LessZero :: Less Z (S n) LessSucc :: Less n m -> Less (S n) (S m) data Equal a b where Equal :: Equal a a data Plus a b c where PlusZero :: Plus Z b b PlusSucc :: Plus a b c -> Plus (S a) b (S c) {- We can reduce a term by function application, reduction under the lambda, or reduction of either side of an application. We don't need this full power, since we could get by with normal-order evaluation, but that required a more complicated datatype for Reduce. -} data Reduce t1 t2 where ReduceSimple :: Replace Z t1 t2 t3 -> Reduce (Apply (Lambda t1) t2) t3 ReduceLambda :: Reduce t1 t2 -> Reduce (Lambda t1) (Lambda t2) ReduceApplyLeft :: Reduce t1 t2 -> Reduce (Apply t1 t3) (Apply t2 t3) ReduceApplyRight :: Reduce t1 t2 -> Reduce (Apply t3 t1) (Apply t3 t2) {- Lift and Replace use the de Bruijn operations as expressed in the Urban and Berghofer paper. -} data Lift n k t1 t2 where LiftVarLess :: Less i k -> Lift n k (Var i) (Var i) LiftVarGTE :: Either (Equal i k) (Less k i) -> Plus i n r -> Lift n k (Var i) (Var r) LiftApply :: Lift n k t1 t1' -> Lift n k t2 t2' -> Lift n k (Apply t1 t2) (Apply t1' t2') LiftLambda :: Lift n (S k) t1 t2 -> Lift n k (Lambda t1) (Lambda t2) data Replace k t n r where ReplaceVarLess :: Less i k -> Replace k (Var i) n (Var i) ReplaceVarEq :: Equal i k -> Lift k Z n r -> Replace k (Var i) n r ReplaceVarMore :: Less k (S i) -> Replace k (Var (S i)) n (Var i) ReplaceApply :: Replace k t1 n r1 -> Replace k t2 n r2 -> Replace k (Apply t1 t2) n (Apply r1 r2) ReplaceLambda :: Replace (S k) t n r -> Replace k (Lambda t) n (Lambda r) {- Reflexive transitive closure of the reduction relation. -} data ReduceEventually t1 t2 where ReduceZero :: ReduceEventually t1 t1 ReduceSucc :: Reduce t1 t2 -> ReduceEventually t2 t3 -> ReduceEventually t1 t3 -- Definition of normal form: nothing with a lambda term applied to anything. data Normal t where NormalVar :: Normal (Var n) NormalLambda :: Normal t -> Normal (Lambda t) NormalApplyVar :: Normal t -> Normal (Apply (Var i) t) NormalApplyApply :: Normal (Apply t1 t2) -> Normal t3 -> Normal (Apply (Apply t1 t2) t3) -- Something is terminating when it reduces to something normal data Terminating where Terminating :: Term t -> ReduceEventually t t' -> Normal t' -> Terminating {- We can also encode terms that are non-terminating. -} data Reducible t1 where Reducible :: Reduce t1 t2 -> Reducible t1 -- A term is non-normalizable if, no matter how many reductions you have applied, -- you can still apply one more. type Infinite t1 = forall t2 . ReduceEventually t1 t2 -> Reducible t2 data NonTerminating where NonTerminating :: Term t -> Infinite t -> NonTerminating -- x test1 :: Terminating test1 = Terminating (Var Zero) ReduceZero NormalVar -- (\x . x)@y test2 :: Terminating test2 = Terminating (Apply (Lambda (Var Zero))(Var Zero)) (ReduceSucc (ReduceSimple (ReplaceVarEq Equal (LiftVarGTE (Left Equal) PlusZero))) ReduceZero) NormalVar -- omega = \x.x@x type Omega = Lambda (Apply (Var Z) (Var Z)) omega = Lambda (Apply (Var Zero) (Var Zero)) -- (\x . \y . y)@(\z.z@z) test3 :: Terminating test3 = Terminating (Apply (Lambda (Lambda (Var Zero))) omega) (ReduceSucc (ReduceSimple (ReplaceLambda (ReplaceVarLess LessZero))) ReduceZero) (NormalLambda NormalVar) -- (\x.x@x)(\x.x@x) test4 :: NonTerminating test4 = NonTerminating (Apply omega omega) help3 help1 :: Reducible (Apply Omega Omega) help1 = Reducible (ReduceSimple (ReplaceApply (ReplaceVarEq Equal (LiftLambda (LiftApply (LiftVarLess LessZero) (LiftVarLess LessZero)))) (ReplaceVarEq Equal (LiftLambda (LiftApply (LiftVarLess LessZero) (LiftVarLess LessZero)))))) help2 :: ReduceEventually (Apply Omega Omega) t -> Equal (Apply Omega Omega) t help2 ReduceZero = Equal help2 (ReduceSucc (ReduceSimple (ReplaceApply (ReplaceVarEq _ (LiftLambda (LiftApply (LiftVarLess _) (LiftVarLess _)))) (ReplaceVarEq _ (LiftLambda (LiftApply (LiftVarLess _) (LiftVarLess _)))))) y) = case help2 y of Equal -> Equal help3 :: Infinite (Apply Omega Omega) help3 x = case help2 x of Equal -> help1 {- Meng Wang Hello, Jim. I have been looking at the termination of lambda calculus example you posted on Haskell Mailing list. However, I don't understand how ReduceApply works. It seems Apply is tree-shaped; yet the multiple-step reduction ReduceEventually is linear. I could not figure out how to perform multiple-step reductions on both branches of Apply. Specifically, is it possible to encode (\x.x \x.x) (\x.x \x.x)? Thanks. Regards, Meng -} -- (\x.x)@(\x.x) test5 :: Terminating test5 = Terminating (Apply (Lambda (Var Zero)) (Lambda (Var Zero))) (ReduceSucc (ReduceSimple (ReplaceVarEq Equal (LiftLambda (LiftVarLess LessZero)))) ReduceZero) (NormalLambda NormalVar) -- ((\x.x)@(\x.x))@((\x.x)@(\x.x)) test6 :: Terminating test6 = Terminating (Apply (Apply (Lambda (Var Zero)) (Lambda (Var Zero))) (Apply (Lambda (Var Zero)) (Lambda (Var Zero)))) (ReduceSucc (ReduceApplyLeft (ReduceSimple (ReplaceVarEq Equal (LiftLambda (LiftVarLess LessZero))))) (ReduceSucc (ReduceApplyRight (ReduceSimple (ReplaceVarEq Equal (LiftLambda (LiftVarLess LessZero))))) (ReduceSucc (ReduceSimple (ReplaceVarEq Equal (LiftLambda (LiftVarLess LessZero)))) ReduceZero))) (NormalLambda NormalVar) test7 = ReduceSimple (ReplaceVarEq Equal (LiftLambda (LiftVarLess LessZero))) test8 = ReduceSucc (ReduceApplyLeft (ReduceApplyLeft test7)) (ReduceSucc (ReduceApplyLeft (ReduceApplyRight test7)) (ReduceSucc (ReduceApplyLeft test7) (ReduceSucc (ReduceApplyRight test7) (ReduceSucc test7 ReduceZero))))