On equivalences and standardization in a non-deterministic call-by-need lambda calculus

The goal of this report is to prove correctness of a considerable subset of transformations w.r.t. contextual equivalence in a an extended lambda-calculus with case, constructors, seq, let, and choice, with a simple set 
The goal of this report is to prove correctness of a considerable subset of transformations w.r.t. contextual equivalence in a an extended lambda-calculus 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, case-reduction and seq-reductions that use variablebinding chains. This complex calculus has well-behaved diagrams and allows a proof that of correctness of transformations, and also that the simple calculus defines an equivalent contextual order.
show moreshow less

Download full text files

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

    Share in Twitter Search Google Scholar
Metadaten
Author:Manfred Schmidt-Schauß, Matthias Mann
URN:urn:nbn:de:hebis:30-50344
URL:http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank31-approxcalc.pdf
Parent Title (English):Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 31
Series (Serial Number):Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (31)
Publisher:Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology
Place of publication:Frankfurt [am Main]
Document Type:Working Paper
Language:English
Date of Publication (online):2007/08/15
Date of first Publication:2007/08/15
Publishing Institution:Univ.-Bibliothek Frankfurt am Main
Release Date:2007/10/22
Issue:Version: 15 August 2007
Pagenumber:26
Last Page:26
HeBIS PPN:19395740X
Institutes:Informatik
Dewey Decimal Classification:004 Datenverarbeitung; Informatik
Sammlungen:Universitätspublikationen
Licence (German):License Logo Veröffentlichungsvertrag für Publikationen

$Rev: 11761 $