{-# 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))))