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 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.
Download full text files
-
Version 1 ; 15 August 2007
-
Version 2 ; 10. September 2007
Export metadata
Additional Services
| Author: | Manfred Schmidt-Schauß, Matthias Mann |
|---|---|
| URN: | urn:nbn:de:hebis:30-50344 |
| 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): | 22.10.2007 |
| Year of first Publication: | 2007 |
| Publishing Institution: | Univ.-Bibliothek Frankfurt am Main |
| HeBIS PPN: | 19395740X |
| Institutes: | Informatik |
| Dewey Decimal Classification: | 004 Datenverarbeitung; Informatik |
| Sammlungen: | Universitätspublikationen |
| Note: | Version 1: 15. August 2007 + Version 2 (revised version): 10. September 2007 |
| Licence (German): |  Veröffentlichungsvertrag für Publikationen ohne Print on Demand |
