TY  - UNPD
A1  - Mann, Matthias
A1  - Schmidt-Schauß, Manfred
T1  - How to prove similarity a precongruence in non-deterministic call-by-need lambda calculi
T2  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 22
N2  - 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.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 22 
KW  - similarity
KW  - precongruence
KW  - contextual equivalence
KW  - non-determinism
KW  - call-by-need lambda calculus
Y1  - 2006
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/2835
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30-25743
UR  - http://www.ki.informatik.uni-frankfurt.de/papers/mann/pc_sim_ndnd_IB200106.pdf
EP  - 31
PB  - Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology
CY  - Frankfurt [am Main]
ER  -