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
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.
show moreshow less

Download full text files

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

    Share in Twitter Search Google Scholar
Metadaten
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):2006/04/19
Year of first Publication:2006
Publishing Institution:Univ.-Bibliothek Frankfurt am Main
Release Date:2006/04/19
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):License Logo Veröffentlichungsvertrag für Publikationen

$Rev: 11761 $