A syntactic theory of sequential control (Q1101435): Difference between revisions

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.