How to prove similarity a precongruence in non-deterministic call-by-need lambda calculi
Extending the method of Howe, we establish a large class of untyped higher-order calculi, in particular such with call-by-need evaluation, where similarity, also called applicative simulation, can be used as a proof tool for showing contextual preorder. The paper also demonstrates that Mann’s approach using an intermediate “approximation” calculus scales up well from a basic call-by-need non-deterministic lambdacalculus to more expressive lambda calculi. I.e., it is demonstrated, that after transferring the contextual preorder of a non-deterministic call-byneed lambda calculus to its corresponding approximation calculus, it is possible to apply Howe’s method to show that similarity is a precongruence. The transfer is not treated in this paper. The paper also proposes an optimization of the similarity-test by cutting off redundant computations. Our results also applies to deterministic or non-deterministic call-by-value lambda-calculi, and improves upon previous work insofar as it is proved that only closed values are required as arguments for similaritytesting instead of all closed expressions.
| Author: | Matthias Mann, Manfred Schmidt-Schauß |
|---|---|
| URN: | urn:nbn:de:hebis:30-25743 |
| Series (Serial Number) | Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (22) |
| 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): | 19.04.2006 |
| Year of first Publication: | 2006 |
| Publishing Institution: | Univ.-Bibliothek Frankfurt am Main |
| Tag: | call-by-need lambda calculus; contextual equivalence ; non-determinism ; precongruence; similarity |
| Source: | Technical Report Frank 22, Institut für Informatik, Johann Wolfgang Goethe-Universität Frankfurt am Main |
| HeBIS PPN: | 190341882 |
| Institutes: | Informatik |
| Dewey Decimal Classification: | 004 Datenverarbeitung; Informatik |
| Sammlungen: | Universitätspublikationen |
| Licence (German): | Veröffentlichungsvertrag für Publikationen ohne Print on Demand |





