证明Standard Reduction Theory

Standard Reduction Theory主要讲的是当->>能推导出Value时，一定存在一种计算方法，使得|->推出该Value，
这里的主要想法是当M->>Value时，对于递归情况会有M->P->>Value,我们在P->>Value上递归，可以得到M->P,P |->Q,Q->> Value‘,Value‘->> Value,然后我证明了一个引理可以将P |->> Value‘中的一个|->过程“移动”出来，得到M |-> P‘,P->Q,
这里其实使用->>上的Church-Rosser定理会更好证明一些。

;M ->>v N
;1 M ->v N => M ->>v N, 2 M ->>v M, 3 M ->>v P, P ->>v N => M ->>v N

;M ->v N
;1 M v N => M ->v N , 2 M ->v M‘ => (λX.M) ->v (λX.M‘) , 3 M ->v M‘ => (M N) ->v (M‘ N) , 4 N ->v N‘ => (M N) ->v (M N‘)

;(λX.M) N v M[X<-N]

;E = [] | (E N) | (V E)

;M v M‘ => E[M] |->v E[M‘]

;M ->>v U <=> M |->>v V, V->>v U, M != Value, V ,U = Value
(lambda (M ->>v U)
(cond
((M ->v U)
(cond
((M v U) ; M = (λX.M1) M2, U = M1[X<-M2]
(M l->v U))))
((M ->>v P, P ->>v U))))

;M ->v P, P ->>v U => M |->>v P‘, P‘ ->>v U ,
(lambda (M ->v P, P ->>v U)
; M ->>v P
(cond
((M ->v P)
(cond
((M v P) ; M = (λX.M1) M2, P = M1[X<-M2]
=> M l->>v P, P ->>v U)
((M = (M1 M2) , P = (M1‘ M2) , M1 ->v M1‘)
; P ->>v U
(cond
((P ->v U)
(cond
((P v U) ; P = ((λY.M1‘‘) M2), U = M1‘‘[X<- M2]
;M1 ->v (λY.M1‘‘)
(cond
((M1 v (λX.M1‘‘)) ;M1 v M1‘ => M l->v P M1 = (λZ.M11) M12, M1 v M11[Z<-M12] = (λY.M1‘‘), M = ( ((λZ.M11) M12) M2) , P = ((λX.M1‘‘) M2) , U = M1‘‘[X<-M2]
(M l->v P, P->>v U))
((M1=(λX.M1‘) , M1‘=(λX.M1‘‘), M1‘->v M1‘‘ => M1 ->v M1‘);M=((λX.M1‘) M2) , P =((λX.M1‘‘) M2) , U =M1‘‘[X<-M2]
;P‘ = M1‘[X<-M2] , M1‘ ->v M1‘‘ => P‘ -> U
(P->>U M1‘[X<-M2] M1‘‘[X<- M2]) => P‘->U
M l->v P‘, P‘ -> U)
((P -> Q, Q ->> U)
P l-> Q‘, Q‘ ->> U))))))))) ; M -> P ,P l-> Q‘ ,Q‘ ->> U
))
;M -> P ,P l-> Q => M l-> P‘ ,P‘ -> Q
(lambda1 (M -> P ,P l-> Q)
; M -> P
(cond ((M v P) ; M = (λX.M1) M2, P = M1[X<-M2]
M l->v P, P -> Q)
((M = (M1 M2),P = (P1 P2),M1 -> P1)
; P l-> Q => P = E[P1‘] , Q = E[Q1‘] , P1‘ v Q1‘
;E
(cond ((E = []); P = P1‘ = (P1 P2)=((λX.P1‘1) P2) , Q = Q1‘ =P1‘1[X<-P2]
;M1 -> P1
(cond ((M1 v P1)
M l->v P , P -> Q)
((M1 = (λX.M1‘),P1 = (λX.P1‘1), M =((λX.M1‘) M2),P=((λX.P1‘1) P2),M1‘->P1‘1)
M=((λX.M1‘) M2) v M1[X<-M2] = M1[X<-P2] -> P1‘1[X<-P2] = Q)
))
((E=(E M));P=(E[P1‘] M2),Q=(E[Q1‘] M2),P1‘ v Q1‘,M=(M1 M2),P=(P1 M2),M1->P1
(lambda1 M1->P1,P1 l-> Q1)=>M1 l-> P11,P11 -> Q1
M1 l-> P11 => (M1 M2) l-> (P1 M2)
P11 -> Q1 => (P1 M2) -> (Q1 M2))
)
))
)
;given P‘ ,U ,find the path from P‘ -> U
(define P‘->U
(lambda ( P‘ = M1‘[X<-M2],U = M1‘‘[X<-M2], M1‘->v M1‘‘)
;M1‘ ->v M1‘‘
(cond
((M1‘ v M1‘‘) ; => M1‘ = ((λY.M1‘1) M1‘2) , M1‘‘ = M1‘1[Y<-M1‘2],
;P‘ = ((λY.M1‘1) M1‘2)[X<-M2] = ((λY.M1‘1[X<-M2]) M1‘2[X<-M2]),
;U = M1‘1[Y<-M1‘2][X<-M2] = M1‘1[X<-M2][Y<-M1‘2[X<-M2]]
;P‘ v M1‘1[X<-M2][Y<-M1‘2[X<-M2]]
P‘ v U)
((M1‘ = (λX.M1‘‘), M1‘‘ = (λX.M1‘‘‘), M1‘‘ ->v M1‘‘‘)
;P‘=(λX.M1‘‘)[X<-M2] = (λX.M1‘‘[X<-M2])
;U=(λX.M1‘‘‘)[X<-M2] = (λX.M1‘‘‘[X<-M2])
(P‘->U M1‘‘[X<-M2] M1‘‘‘[X<-M2] => M1‘‘[X<-M2] -> M1‘‘‘[X<-M2])
=> P‘ -> U)
((M1‘ = (M1‘1 M1‘2), M1‘‘ = (M1‘‘1 M1‘‘2), M1‘1 ->v M1‘‘1)
(P‘->U M1‘1[X<-M2] M1‘‘1[X<-M2]) => M1‘1[X<-M2] -> M1‘‘1[X<-M2]
=> P‘ -> U))))