--#include "Prelude.agda" --#include "Confluence.agda" --#include "Term.agda" ---------------------------------------------------------------------------- -- beta reduction relation idata Beta (|X::Set) :: Term X -> Term X -> Set where BetaBase (!M::Term (Maybe X)) (!N::Term X) :: Beta (App (Lam M) N) (instantiate N M) BetaAppL (|M,|M'::Term X) (!p::Beta M M') (!N::Term X) :: Beta (App M N) (App M' N) BetaAppR (!M::Term X) (|N,|N'::Term X) (!p::Beta N N') :: Beta (App M N) (App M N') BetaLam (|M::Term (Maybe X)) (|M'::Term (Maybe X)) (!p::Beta M M') :: Beta (Lam M) (Lam M') ---------------------------------------------------------------------------- -- reflexive transitive closure of beta reduction. BetasApp (X::Set) (M,M',N,N'::Term X) :: RList Beta M M' -> RList Beta N N' -> RList Beta (App M N) (App M' N') BetasApp r1 r2 = let f (M,M',N::Term X) :: RList Beta M M' -> RList Beta (App M N) (App M' N) f p = case p of (RNil x )-> RNil (App M N) (RCons x y z r1 r2)-> RCons (BetaAppL r1 N) (f r2) g (M,N,N'::Term X) :: RList Beta N N' -> RList Beta (App M N) (App M N') g p = case p of (RNil x )-> RNil (App M N) (RCons x y z r1 r2)-> RCons (BetaAppR M r1) (g r2) in rappend (f r1) (g r2) BetasLam (X::Set) (M,M'::Term (Maybe X)) :: RList Beta M M' -> RList Beta (Lam M) (Lam M') BetasLam p = case p of (RNil x )-> RNil (Lam x) (RCons x y z r1 r2)-> RCons (BetaLam r1) (BetasLam r2) ---------------------------------------------------------------------------- -- parallel reduction relation idata Par (|X::Set) :: Term X -> Term X -> Set where ParVar (!x::X) :: Par (Var x) (Var x) ParApp (|M1,|M1'::Term X) (!p1::Par M1 M1') (|M2,|M2'::Term X) (!p2::Par M2 M2') :: Par (App M1 M2) (App M1' M2') ParLam (|M,|M'::Term (Maybe X)) (!p::Par M M') :: Par (Lam M) (Lam M') ParBeta (|M1,|M1'::Term (Maybe X)) (!p1::Par M1 M1') (|M2,|M2'::Term X) (!q::Par M2 M2') :: Par (App (Lam M1) M2) (instantiate M2' M1') parRefl (X::Set) :: Reflexive (Par |X) parRefl M = case M of (Var x )-> ParVar x (App M N)-> ParApp (parRefl M) (parRefl N) (Lam M )-> ParLam (parRefl M) prop_5_5_a (X::Set) (M,M'::Term X) :: Beta M M' -> Par M M' prop_5_5_a p = case p of (BetaBase M N )-> ParBeta (parRefl M) (parRefl N) (BetaAppL M M' p N)-> ParApp (prop_5_5_a p) (parRefl N) (BetaAppR M N N' p)-> ParApp (parRefl M) (prop_5_5_a p) (BetaLam M M' p )-> ParLam (prop_5_5_a p) prop_5_5_b (X::Set) (M,M'::Term X) :: Par M M' -> RList Beta M M' prop_5_5_b p = case p of (ParVar x )-> RNil (Var x) (ParApp M M' p N N' q )-> BetasApp (prop_5_5_b p) (prop_5_5_b q) (ParLam M M' p )-> BetasLam (prop_5_5_b p) (ParBeta M M' p N N' q)-> let r1 :: RList Beta (App (Lam M) N) (App (Lam M') N') r1 = BetasApp (BetasLam (prop_5_5_b p)) (prop_5_5_b q) r2 :: RList Beta (App (Lam M') N') (instantiate N' M') r2 = runit (BetaBase M' N') in rappend r1 r2 fmapPar (A,B::Set) :: (f::A->B) -> (M1,M2::Term A) |-> Par M1 M2 -> Par (fmap f M1) (fmap f M2) fmapPar f |M1 |M2 p = case p of (ParVar x )-> ParVar (f x) (ParApp M M' p N N' q )-> ParApp (fmapPar f p) (fmapPar f q) (ParLam M M' p )-> ParLam (fmapPar (fmap f) p) (ParBeta M M' p N N' q)-> let lem :: Par (App (Lam (fmap (fmap f) M)) (fmap f N)) (instantiate (fmap f N') (fmap (fmap f) M')) lem = ParBeta (fmapPar (fmap f) p) (fmapPar f q) in substId (\(x::Term B) -> Par (App (Lam (fmap (fmap f) M)) (fmap f N)) x) (instantiate_lemma2 f N' M') lem ---------------------------------------------------------------------------- target (X::Set) :: Term X -> Term X target M = case M of (Var x )-> Var x (Lam M )-> Lam (target M) (App M N)-> case M of (Lam M' )-> instantiate (target N) (target M') (Var x )-> App (target M) (target N) (App M0 M1)-> App (target M) (target N) weakenPar (X::Set) (M1,M2::Term X) :: Par M1 M2 -> Par (weaken M1) (weaken M2) weakenPar = fmapPar Just prop_5_7 (X::Set) (N,N'::Term X) (L, L'::Term (Maybe X)) :: Par N N' -> Par L L' -> Par (instantiate N L) (instantiate N' L') prop_5_7 r2 r1 = case r1 of (ParVar x )-> case x of (Nothing)-> r2 (Just x')-> ParVar x' (ParApp M1 M1' p M2 M2' q )-> ParApp (prop_5_7 r2 p) (prop_5_7 r2 q) (ParLam M M' p )-> let q :: Par (fmap swap M) (fmap swap M') q = fmapPar swap p r2' :: Par (weaken N) (weaken N') r2' = weakenPar r2 lem1 :: Par (instantiate (weaken N) (fmap swap M)) (instantiate (weaken N') (fmap swap M')) lem1 = prop_5_7 r2' q lem2 :: Par (ext (tmap (inst N)) M) (instantiate (weaken N') (fmap swap M')) lem2 = substId (\(m::Term (Maybe X)) -> Par m (instantiate (weaken N') (fmap swap M'))) (instantiate_lemma3 N M) lem1 lem3 :: Par (ext (tmap (inst N)) M) (ext (tmap (inst N')) M') lem3 = substId (\(m::Term (Maybe X)) -> Par (ext (tmap (inst N)) M) m) (instantiate_lemma3 N' M') lem2 lem4 :: Par (instantiate N (Lam M)) (instantiate N' (Lam M')) lem4 = ParLam lem3 in lem4 (ParBeta M1 M1' p M2 M2' q)-> let lem1 :: Par (instantiate (weaken N) (fmap swap M1)) (instantiate (weaken N') (fmap swap M1')) lem1 = prop_5_7 (weakenPar r2) (fmapPar swap p) lem2 :: Par (instantiate N M2) (instantiate N' M2'); lem2 = prop_5_7 r2 q lem3 :: Par (App (Lam (instantiate (weaken N) (fmap swap M1))) (instantiate N M2)) (instantiate (instantiate N' M2') (instantiate (weaken N') (fmap swap M1'))) lem3 = ParBeta |X lem1 lem2 lem4 :: Par (App (Lam (instantiate (weaken N) (fmap swap M1))) (instantiate N M2)) (instantiate N' (instantiate M2' M1')) lem4 = substId (\(z::Term X) -> Par (App (Lam (instantiate (weaken N) (fmap swap M1))) (instantiate N M2)) z) (instantiate_lemma' M1' M2' N') lem3 lem6 :: Id (App (Lam (instantiate (weaken N) (fmap swap M1))) (instantiate N M2)) (instantiate N (App (Lam M1) M2)) lem6 = AppId (LamId (instantiate_lemma3 N M1)) (refId (ext (inst N) M2)) lem5 :: Par (instantiate N (App (Lam M1) M2)) (instantiate N' (instantiate M2' M1')) lem5 = substId (\(x::Term X) -> Par x (instantiate N' (instantiate M2' M1'))) lem6 lem4 in lem5 lemma_5_6 (X::Set) (M,M'::Term X) :: Par M M' -> Par M' (target M) lemma_5_6 p_ = case p_ of (ParVar x )-> ParVar x (ParLam M1 M1' p1 )-> ParLam (lemma_5_6 p1) (ParBeta M1 M1' p1 N2 N2' p2)-> prop_5_7 (lemma_5_6 p2) (lemma_5_6 p1) (ParApp M1 M1' p1 M2 M2' p2 )-> let lem :: Par (App M1' M2') (App (target M1) (target M2)) lem = ParApp (lemma_5_6 p1) (lemma_5_6 p2) in case p1 of (ParVar x )-> lem (ParApp _M1 _M1' _p _M2 _M2' _q )-> lem (ParBeta _M1 _M1' _p _M2 _M2' _q)-> lem (ParLam M0 M0' p0 )-> ParBeta (lemma_5_6 p0) (lemma_5_6 p2) ParConfluence (X::Set) :: Confluence (Par |X) ParConfluence |M1 |M2 span = struct c :: Term X c = target span.c fst :: Par M1 c fst = lemma_5_6 span.fst snd :: Par M2 c snd = lemma_5_6 span.snd manyParConfluence (X::Set) :: Confluence (RList (Par |X)) manyParConfluence = rliftConf (ParConfluence |_) ChurchRosserTheorem (X::Set) :: Confluence (RList (Beta |X)) ChurchRosserTheorem |M1 |M2 span = let f (M,M'::Term X) :: RList Beta M M' -> RList Par M M' f = rmap (prop_5_5_a |_) g (M,M'::Term X) :: RList Par M M' -> RList Beta M M' g x = rconcat (rmap (prop_5_5_b |_) x) span' :: Span (RList Par) (RList Par) M1 M2 span' = struct c :: Term X c = span.c fst :: RList Par c M1 fst = f span.fst snd :: RList Par c M2 snd = f span.snd cospan :: CoSpan (RList Par) (RList Par) M1 M2 cospan = manyParConfluence span' in struct c :: Term X c = cospan.c fst :: RList Beta M1 c fst = g cospan.fst snd :: RList Beta M2 c snd = g cospan.snd ----------------------------------------------------------------------------