Technical report Frank / JohannWolfgangGoetheUniversität, Fachbereich Informatik und Mathematik, Institut für Informatik
1 search hit
 31

On equivalences and standardization in a nondeterministic callbyneed lambda calculus
(2007)

Manfred SchmidtSchauß
Matthias Mann
 The goal of this report is to prove correctness of a considerable subset of transformations w.r.t. contextual equivalence in a an extended lambdacalculus with case, constructors, seq, let, and choice, with a simple set of reduction rules. Unfortunately, a direct proof appears to be impossible. The correctness proof is by defining another calculus comprising the complex variants of copy, casereduction and seqreductions that use variablebinding chains. This complex calculus has wellbehaved diagrams and allows a proof that of correctness of transformations, and also that the simple calculus defines an equivalent contextual order.