Technical report Frank / JohannWolfgangGoetheUniversität, Fachbereich Informatik und Mathematik, Institut für Informatik
2 search hits
 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.
 31 [v.2]

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 an extended lambdacalculus LS with case, constructors, seq, let, and choice, with a simple set of reduction rules; and to argue that an approximation calculus LA is equivalent to LS w.r.t. the contextual preorder, which enables the proof tool of simulation. Unfortunately, a direct proof appears to be impossible The correctness proof is by defining another calculus L comprising the complex variants of copy, casereduction and seqreductions that use variablebinding chains. This complex calculus has wellbehaved diagrams and allows a proof of correctness of transformations, and that the simple calculus LS, the calculus L, and the calculus LA all have an equivalent contextual preorder.