|Deletions are marked like this.||Additions are marked like this.|
|Line 1:||Line 1:|
. | (subst B x N) -nor-> B'
. M N -cbn-> B' |
. | M N -nor-> B' |
4) M -cbn-> (M' =/= (\x.B)) | M-cbn->(M' =/= (\x.B)), M'-nor-> M,
. | N -nor-> N'
. M N -cbn-> M'N |
. | M N -cbn-> M' N'
. Then it follows inductively on the structure of the derivation that nor is absorbent to cbn. For the rules 1) 2) and 4) this is direct. For the rule 3) we use the induction hpothesis. Every other possible pair of subsidiary and hybrid orders leads to the same inductive proof. The substitution is what makes the proof hard, but both the hybrid and the subsidiary evaluation orders use the same evaluation order for |op1|. For the evaluation of the substitution the hypothesis is enough.
This theorem induces us to think that the following definitions for nor are equivalent:
> -- la op1 ar1 op2 ar2 >
. > cbn = eval return cbn return cbn return > nor = eval nor cbn return (cbn >=> nor) nor > nor' = eval nor' cbn return nor' nor'
because we know that (cbn >=> nor) T = nor T. But this does not have to be generally true, because in the definitions above nor =/= nor', as they are different fix points. It is possible true but further poorf regarding fix point issues must be done.
We expect that the hybridation operation and the absorption theorem can be extended to the case where the evaluation orders being hybridated are not uniform and simplified. This requires to extend the definition of the weaker-than realtion to the infinite space induced by multiple-step recursion definitions and extend the proof as well.
|EVALUATION OF THE LAMBDA-CALCULUS - GENERIC EVALUATORS
by Alvaro Garcia Perez
October 23th 2009
EVALUATION OF THE LAMBDA-CALCULUS - GENERIC EVALUATORS by Alvaro Garcia Perez October 23th 2009