-- Martin Escardo, 21 Feb 2008
--
-- We write a lambda-evaluator to prove that the
-- selection monad is a monad and that the claimed
-- morphism into the continuation monad is a morphism.
--
-- Reason: the proof by hand gets rather complicated.
-- We print the "proof by hand" in the function main.
--
-- This is intended to be simple rather than efficient.

type N = Int
type Variable = (String,N)

-- Lambda terms. 
-- (Our examples are typeable, but the evaluator is untyped.)

data T = V Variable
       | L Variable T
       | A T T
     deriving (Eq)

free :: Variable -> T -> Bool
free x (V y) = x == y
free x (L y t) = x /= y && free x t
free x (A t u) = free x t || free x u

-- The following is used to manufacture fresh variables. 
-- For user-friendliness, we don't come up with new variables names.
-- We instead change the index of the variable that has to be
-- renamed. The following function helps us to do that:

order :: String -> T -> N
order a (V(b,n)) = if a == b then n else -1
order a (L(b,n) t) = max n (order a t)
order a (A t u) = max(order a t)(order a u)

-- With this we can do substitution.
-- The expression (subst x t u) substitutes t for x in u,
-- delivering the term u[x:=t].

subst :: Variable -> T -> T -> T
subst x t (V y)   = if x == y then t else V y
subst x t (L y s) | x == y    = L y s 
                  | free y t = let (a,n) = y
                                   n' = 1 + max(order a t)(order a s)
                                   y' = (a,n')
                                   s' = subst y (V y') s
                               in L y' (subst x t s')
                  | otherwise = L y (subst x t s)
subst x t (A u v) = A (subst x t u) (subst x t v)

-- We need an environment env to hold the global declarations.
-- This is to be defined in the applications of this program.
-- One is given below. 

-- We consider eta-redexes as well, but this can be disabled.
-- Only one equation needs eta (see below).

wantEtaReduction = True

hasredex :: T -> Bool
hasredex (V x) = env(V x) /= V x
hasredex (L x t) = if wantEtaReduction
                   then case t of
                          A u (V y) -> (x == y && not(free x u)) || hasredex t
                          otherwise -> hasredex t
                   else hasredex t
hasredex (A (V x) u) = env(V x) /= V x || hasredex u
hasredex (A (L x t) u) = True
hasredex (A t u) = hasredex t || hasredex u

normal :: T -> Bool
normal = not.hasredex

step :: T -> T
step (V x) = env(V x)
step (L x t) = if wantEtaReduction 
               then case t of
                      A u (V y) -> if x == y && not(free x u) then u else L x (step t)
                      otherwise -> L x (step t)
               else L x (step t)
step (A (V x) u) = if env(V x) == V x 
                   then A (V x) (step u)
                   else A (env(V x)) u
step (A (L x t) u) = subst x u t
step (A t u) = if hasredex t then A (step t) u else A t (step u)


steps :: T -> [T]
steps t = takeUntil normal (iterate step t)

takeUntil p [] = []
takeUntil p (x:l) = x : if p x then [] else takeUntil p l

-- Normal form:

nf :: T -> T
nf = last.steps

-- Another feature for the user:

data Redex = NameExpansion Variable | Beta T | Eta T | None

redex :: T -> Redex
redex (V x) = if env(V x) /= V x then NameExpansion x else None
redex (L x t) = if wantEtaReduction
                   then case t of
                          A u (V y) -> if x == y && not(free x u)
                                       then Eta(L x t)
                                       else redex t
                          otherwise -> redex t
                   else redex t
redex (A (V x) u) = if env(V x) /= V x then NameExpansion x else redex u
redex (A (L x t) u) = Beta(A (L x t) u)
redex (A t u) = if hasredex t then redex t else redex u

redexes :: T -> [Redex]
redexes t = map redex (steps t)

-- alpha-equivalence.
-- We use De Bruijn indices for this.

data B = Vb Variable             
       | Ib N             
       | Lb B
       | Ab B B
     deriving (Show,Eq)

-- Lambda abstraction algorithm.
-- We abstract the varible x from the de Bruijn term t
-- (then it disappears from t).

lam :: Variable -> B -> B
lam x t = Lb (h 0 t)
 where h n (Vb y) = if x == y then Ib n else Vb y
       h n (Ib i) = Ib i
       h n (Lb t) = Lb (h (n+1) t)
       h n (Ab t u) = Ab (h n t) (h n u)

-- alpha is a quotient with alpha-equivalence as its kernel:

alpha :: T -> B
alpha (V x) = Vb x
alpha (L x t) = lam x (alpha t)
alpha (A t u) = Ab (alpha t) (alpha u)

-- eta-beta-alpha equivalence:

same :: T -> T -> Bool
same t u = alpha(nf t) == alpha(nf u)

-- Output functions

ssteps :: T -> IO ()
ssteps t = interact(\s -> concat (map (++"\n") (map show (steps t))))

sredexes :: T -> IO()
sredexes t = interact(\s -> concat (map (++"\n") (map show (redexes t))))

instance Show T where
  show = unparse

shown (a,n) = a ++ if n == 0 then "" else show n

unparse (V x) = shown x
unparse (L x t) = "\\" ++ shown x ++ "." ++ unparse t
unparse (A s t) = unparsel s ++ " " ++ unparser t

unparsel (V x) = shown x
unparsel (L x t) = "(\\" ++ shown x ++ "." ++ unparse t ++ ")"
unparsel (A s t) = unparsel s ++ " " ++ unparser t

unparser (V x) = shown x
unparser (L x t) = "(\\" ++ shown x ++ "." ++ unparse t ++ ")"
unparser (A s t) = "(" ++ unparsel s ++ " " ++ unparser t ++ ")"

instance Show Redex where
   show (NameExpansion x) = "Name redex: " ++ shown x
   show (Beta t) = "Beta redex: " ++ show t
   show (Eta t) = "Eta  redex:" ++ show t
   show None = ""

-- Proof of the selection monad properties.
-- (The proof is printed, but we can also get a yes/no
--  answer if we wish.)

-- First define variable names:

a = V("a",0)
x = V("x",0)
y = V("y",0)
z = V("z",0)
f = V("f",0)
g = V("g",0)
h = V("h",0)
e = V("e",0)
bige = V("E",0)
bigphi = V("Phi",0)
phi = V("phi",0)
bigu = V("U",0)
bigp = V("P",0)
bigq = V("Q",0)
p = V("p",0)
q = V("q",0)

la = L("a",0)
lx = L("x",0)
ly = L("y",0)
lz = L("z",0)
lf = L("f",0)
lg = L("g",0)
lh = L("h",0)
le = L("e",0)
lbige = L("E",0)
lbigphi = L("Phi",0)
lphi = L("phi",0)
lbigu = L("U",0)
lp = L("p",0)
lq = L("q",0)

s = V("s",0)
eta = V("eta",0)
mu = V("mu",0)
t = V("t",0)
qeta = V("qeta",0)
qmu = V("qmu",0)
forsome = V("forsome",0)

-- Now define the environment with names for the terms we want to study:

env (V(name,n)) = en name
 where -- selection monad
       en "s" = lf (le (lq (A f (A e (la (A q (A f a)))))))
       en "eta" = lx (lp x)
       en "mu" = lbige (lp (A (A bige (le (A p (A e p)))) p))
       -- continuation monad
       en "t" = lf (lphi(lp (A phi(lx (A p(A f x))))))
       en "qeta" = lx(lp (A p x))
       en "qmu" = lbigphi(lbigu (A bigphi(lphi(A phi bigu))))
       -- morphism from the first to the second monad
       en "forsome" = le(lp(A p(A e p)))
       en _  = V(name,n)

-- Macros. Warning: assume that "x" is not free in u and v for composition.

comp u v = lx(A u (A v x))
sfunctor u = A s u
tfunctor u = A t u

-- Now the equations we want to verify:

functorial1 = lg(lf(comp (sfunctor g) (sfunctor f))) 
functorial2 = lg(lf(sfunctor (comp g f)))
naturaleta1 = lf(comp (sfunctor f) eta)
naturaleta2 = lf(comp eta f)
naturalmu1 = lf(comp (sfunctor f) mu)
naturalmu2 = lf(comp mu (sfunctor (sfunctor f)))
unit1 =  comp mu (sfunctor eta)
unit2 =  comp mu eta
identity = lx x
assoc1 = comp mu (sfunctor mu)
assoc2 = comp mu mu


-- No need to verify the next chunk, as this is well known:

qfunctorial1 = lg(lf(comp (tfunctor f) (tfunctor g))) 
qfunctorial2 = lg(lf(tfunctor (comp f g)))
qnaturaleta1 = lf(comp (tfunctor f) qeta)
qnaturaleta2 = lf(comp qeta f)
qnaturalmu1 = lf(comp (tfunctor f) qmu)
qnaturalmu2 = lf(comp qmu (tfunctor(tfunctor f)))
qunit1 = comp qmu (tfunctor qeta)
qunit2 = comp qmu qeta
qassoc1 = comp qmu (tfunctor qmu)
qassoc2 = comp qmu qmu

-- But we need to check this:

naturalforsome1 = lf(comp forsome (sfunctor f))
naturalforsome2 = lf(comp (tfunctor f) forsome)
morphismeta1 = comp forsome eta
morphismeta2 = qeta
morphismmu1 = comp qmu (comp forsome (sfunctor forsome))
morphismmu2 = comp forsome mu

equations =  [ (functorial1, functorial2),         -- (s,eta,mu) is a monad
               (naturaleta1, naturaleta2),        
               (naturalmu1, naturalmu2),
               (unit1, unit2),                     -- only this one requires eta-reduction
               (unit2, identity),                        
               (assoc1, assoc2), 
               -- (qfunctorial1, qfunctorial2),       -- (t,qeta,qmu) is a monad
               -- (qnaturaleta1, qnaturaleta2),
               -- (qnaturalmu1, qnaturalmu2),
               -- (qunit1, qunit2),
               -- (qassoc1, qassoc2), 
               (naturalforsome1, naturalforsome2), -- forsome is a morphism s->t
               (morphismeta1, morphismeta2),
               (morphismmu1, morphismmu2) ]

verification :: Bool
verification = and [same t1 t2 | (t1,t2) <- equations]

terms =  [     functorial1, functorial2,         
               naturaleta1, naturaleta2,        
               naturalmu1, naturalmu2,
               unit1, unit2,                 
               assoc1, assoc2,
               -- qfunctorial1, qfunctorial2,   
               -- qnaturaleta1, qnaturaleta2,
               -- qnaturalmu1, qnaturalmu2,
               -- qunit1, qunit2,
               -- qassoc1, qassoc2, 
               naturalforsome1, naturalforsome2,
               morphismeta1, morphismeta2,
               morphismmu1, morphismmu2 
         ]

derivations = [ (steps t, redexes t) | t <- terms]

textderivations :: String
textderivations = concat [ concat(map (++ "\n") (map show (steps t))) ++ "\n" ++
                           concat(map (++ "\n") (map show (redexes t))) ++ "\n\n" 
                              | t <- terms]

-- This prints the derivation of all the equations:

main = interact(\s -> textderivations)

-- This only works with eta reduction enabled:

{- Result of the verification

*Main> verification
True

Here is a detailed step-by-step verification of one of the equations:

*Main> ssteps assoc1
\x.mu (s mu x)
\x.(\E.\p.E (\e.p (e p)) p) (s mu x)
\x.\p.s mu x (\e.p (e p)) p
\x.\p.(\f.\e.\q.f (e (\a.q (f a)))) mu x (\e.p (e p)) p
\x.\p.(\e.\q.mu (e (\a.q (mu a)))) x (\e.p (e p)) p
\x.\p.(\q.mu (x (\a.q (mu a)))) (\e.p (e p)) p
\x.\p.mu (x (\a.(\e.p (e p)) (mu a))) p
\x.\p.(\E.\p.E (\e.p (e p)) p) (x (\a.(\e.p (e p)) (mu a))) p
\x.\p.(\p1.x (\a.(\e.p (e p)) (mu a)) (\e.p1 (e p1)) p1) p
\x.\p.x (\a.(\e.p (e p)) (mu a)) (\e.p (e p)) p
\x.\p.x (\a.p (mu a p)) (\e.p (e p)) p
\x.\p.x (\a.p ((\E.\p.E (\e.p (e p)) p) a p)) (\e.p (e p)) p
\x.\p.x (\a.p ((\p.a (\e.p (e p)) p) p)) (\e.p (e p)) p
\x.\p.x (\a.p (a (\e.p (e p)) p)) (\e.p (e p)) p

*Main> :r -- needed reinstate the handle. This is a ghci I/O bug.
Ok, modules loaded: Main.

*Main> ssteps assoc2
\x.mu (mu x)
\x.(\E.\p.E (\e.p (e p)) p) (mu x)
\x.\p.mu x (\e.p (e p)) p
\x.\p.(\E.\p.E (\e.p (e p)) p) x (\e.p (e p)) p
\x.\p.(\p.x (\e.p (e p)) p) (\e.p (e p)) p
\x.\p.x (\e.(\e.p (e p)) (e (\e.p (e p)))) (\e.p (e p)) p
\x.\p.x (\e.p (e (\e.p (e p)) p)) (\e.p (e p)) p

Here is another example:

*Main> ssteps morphismmu1
\x.qmu ((\x.forsome (s forsome x)) x)
\x.(\Phi.\U.Phi (\phi.phi U)) ((\x.forsome (s forsome x)) x)
\x.\U.(\x.forsome (s forsome x)) x (\phi.phi U)
\x.\U.forsome (s forsome x) (\phi.phi U)
\x.\U.(\e.\p.p (e p)) (s forsome x) (\phi.phi U)
\x.\U.(\p.p (s forsome x p)) (\phi.phi U)
\x.\U.(\phi.phi U) (s forsome x (\phi.phi U))
\x.\U.s forsome x (\phi.phi U) U
\x.\U.(\f.\e.\q.f (e (\a.q (f a)))) forsome x (\phi.phi U) U
\x.\U.(\e.\q.forsome (e (\a.q (forsome a)))) x (\phi.phi U) U
\x.\U.(\q.forsome (x (\a.q (forsome a)))) (\phi.phi U) U
\x.\U.forsome (x (\a.(\phi.phi U) (forsome a))) U
\x.\U.(\e.\p.p (e p)) (x (\a.(\phi.phi U) (forsome a))) U
\x.\U.(\p.p (x (\a.(\phi.phi U) (forsome a)) p)) U
\x.\U.U (x (\a.(\phi.phi U) (forsome a)) U)
\x.\U.U (x (\a.forsome a U) U)
\x.\U.U (x (\a.(\e.\p.p (e p)) a U) U)
\x.\U.U (x (\a.(\p.p (a p)) U) U)
\x.\U.U (x (\a.U (a U)) U)

*Main> length(steps morphismmu1)
19

*Main> ssteps morphismmu2
\x.forsome (mu x)
\x.(\e.\p.p (e p)) (mu x)
\x.\p.p (mu x p)
\x.\p.p ((\E.\p.E (\e.p (e p)) p) x p)
\x.\p.p ((\p.x (\e.p (e p)) p) p)
\x.\p.p (x (\e.p (e p)) p)

We can see which redexes were reduced above:

*Main> sredexes morphismmu1
Name redex: qmu
Beta redex: (\Phi.\U.Phi (\phi.phi U)) ((\x.forsome (s forsome x)) x)
Beta redex: (\x.forsome (s forsome x)) x
Name redex: forsome
Beta redex: (\e.\p.p (e p)) (s forsome x)
Beta redex: (\p.p (s forsome x p)) (\phi.phi U)
Beta redex: (\phi.phi U) (s forsome x (\phi.phi U))
Name redex: s
Beta redex: (\f.\e.\q.f (e (\a.q (f a)))) forsome
Beta redex: (\e.\q.forsome (e (\a.q (forsome a)))) x
Beta redex: (\q.forsome (x (\a.q (forsome a)))) (\phi.phi U)
Name redex: forsome
Beta redex: (\e.\p.p (e p)) (x (\a.(\phi.phi U) (forsome a)))
Beta redex: (\p.p (x (\a.(\phi.phi U) (forsome a)) p)) U
Beta redex: (\phi.phi U) (forsome a)
Name redex: forsome
Beta redex: (\e.\p.p (e p)) a
Beta redex: (\p.p (a p)) U

Another example (only one in which eta-reduction is used):

*Main> ssteps unit1
\x.mu (s eta x)
\x.(\E.\p.E (\e.p (e p)) p) (s eta x)
\x.\p.s eta x (\e.p (e p)) p
\x.\p.(\f.\e.\q.f (e (\a.q (f a)))) eta x (\e.p (e p)) p
\x.\p.(\e.\q.eta (e (\a.q (eta a)))) x (\e.p (e p)) p
\x.\p.(\q.eta (x (\a.q (eta a)))) (\e.p (e p)) p
\x.\p.eta (x (\a.(\e.p (e p)) (eta a))) p
\x.\p.(\x.\p.x) (x (\a.(\e.p (e p)) (eta a))) p
\x.\p.(\p1.x (\a.(\e.p (e p)) (eta a))) p
\x.\p.x (\a.(\e.p (e p)) (eta a))
\x.\p.x (\a.p (eta a p))
\x.\p.x (\a.p ((\x.\p.x) a p))
\x.\p.x (\a.p ((\p.a) p))
\x.\p.x (\a.p a)
\x.\p.x p
\x.x

*Main> sredexes unit1
Name redex: mu
Beta redex: (\E.\p.E (\e.p (e p)) p) (s eta x)
Name redex: s
Beta redex: (\f.\e.\q.f (e (\a.q (f a)))) eta
Beta redex: (\e.\q.eta (e (\a.q (eta a)))) x
Beta redex: (\q.eta (x (\a.q (eta a)))) (\e.p (e p))
Name redex: eta
Beta redex: (\x.\p.x) (x (\a.(\e.p (e p)) (eta a)))
Beta redex: (\p1.x (\a.(\e.p (e p)) (eta a))) p
Beta redex: (\e.p (e p)) (eta a)
Name redex: eta
Beta redex: (\x.\p.x) a
Beta redex: (\p.a) p
Eta  redex:\a.p a
Eta  redex:\p.x p

*Main> ssteps unit2
\x.mu (eta x)
\x.(\E.\p.E (\e.p (e p)) p) (eta x)
\x.\p.eta x (\e.p (e p)) p
\x.\p.(\x.\p.x) x (\e.p (e p)) p
\x.\p.(\p.x) (\e.p (e p)) p
\x.\p.x p
\x.x

*Main> sredexes unit2
Name redex: mu
Beta redex: (\E.\p.E (\e.p (e p)) p) (eta x)
Name redex: eta
Beta redex: (\x.\p.x) x
Beta redex: (\p.x) (\e.p (e p))
Eta  redex:\p.x p

 -}