A syntactic theory of sequential control (Q1101435): Difference between revisions
From MaRDI portal
Removed claim: reviewed by (P1447): Item:Q1188836 |
Changed an Item |
||
Property / reviewed by | |||
Property / reviewed by: Jiří Zlatuška / rank | |||
Normal rank |
Revision as of 15:05, 22 February 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A syntactic theory of sequential control |
scientific article |
Statements
A syntactic theory of sequential control (English)
0 references
1987
0 references
The paper presents an exposition of a theory of syntactic control in a lambda-calculus based programming language. First deficiencies of the lambda-calculus as a programming language are discussed and relevant literature reviewed. Although the control problem can be solved in a general setting using continuations, the authors seek to enrich the lambda-calculus by control operators rather than to model these operators within the standard calculus, and to provide a syntactic theory for these operators. The language \(\Lambda_ c\) contains two control operators, one of them giving its argument complete control over the current continuation, and the other representing on abort operation terminating the program and yielding the value of its argument. Operational semantics for the language is defined, and programming in this language is compared with programming in the traditional lambda- calculus. For the new calculus, notions of reduction and computation are defined, and their fundamental properties are proved. It is shown that the extended calculus satisfies the diamond property and contains a Church-Rosser subcalculus (i.e. the interpretation of control operators is to a certain degree independent of a specific evaluation strategy). A standardization theorem is proved and the correctness of the calculus is demonstrated by showing its correspondence with the original machine semantics. As far as reasoning with the calculus is concerned, its soundness is proved, but it is shown that the calculus is incomplete.
0 references
functional programs
0 references
Church-Rosser property
0 references
denotational semantics
0 references
reduction machine
0 references
compiler optimizations
0 references
lambda-calculus
0 references
control operators
0 references