A fully abstract semantics for concurrent graph reduction

This paper presents a fully abstract semantics for a variant of the untyped λ-calculus with recursive [Bdeclarations. We first present a summary of existing work on full abstraction for the untyped λ-calculus, concentrating on S. Abramsky (1989) and C.H.L. Ong (1988) work on the lazy λ-calculus. Abramsky and Ong´s work is based on leftmost outermost reduction without sharing. This is notably inefficient, and many implementations model share by reducing syntax graphs rather than syntax trees. Here we present a concurrent graph reduction algorithm for the λ-calculus with recursive declarations, in a style similar to G. Berry and G. Boudol´s chemical abstract machine. We adapt Abramsky and Ong´s techniques, and present a program logic and denotational semantics for the λ-calculus with recursive declarations, and show that the three semantics are equivalent