A fully abstract semantics for concurrent graph reduction

Author

Jeffrey, Alan

Author_Institution

Sch. of Cognitive & Comput. Sci., Sussex Univ., Brighton, UK

fYear

1994

fDate

4-7 Jul 1994

Firstpage

82

Lastpage

91

Abstract

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

Keywords

formal logic; lambda calculus; programming theory; chemical abstract machine; concurrent graph reduction; denotational semantics; fully abstract semantics; leftmost outermost reduction; program logic; recursive declarations; syntax graphs; syntax trees; untyped lambda calculus; Chemicals; Computer languages; Computer science; Convergence; Functional programming; Logic; Testing; Trademarks; Tree graphs;

fLanguage

English

Publisher

ieee

Conference_Titel

Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on

Conference_Location

Paris

Print_ISBN

0-8186-6310-3

Type

conf

DOI

10.1109/LICS.1994.316084

Filename

316084