Exceptions, a mathematical semantics for handling full jumps
(This work was later described in:
Abstract: The direct semantics flavour of denotational semantics is simpler and easier to use than the continuation semantics flavour. Unfortunately the former cannot define sequencers and coroutines. However with the use of exceptions direct semantics can define these language features. This avoids the complications of continuations. Exceptions add to the expressive power of direct semantics but they can be defined in terms of the λ-calculus without exceptions so their use does not require any extensions to the foundations of semantics.
Conventional direct semantics cannot define the semantics of sequencers and of coroutines. By introducing continuations, continuation semantics can define them. However continuations are a complex mechanism and are introduced even in those commands that have nothing to do with jumps. This paper shows that by using exceptions, direct semantics can define sequencers and coroutines while restricting changes to the semantics to simple additions for these features.
Direct semantics is the simpler flavour of denotational semantics. It expresses the meaning of a compound command directly as the functional composition of the meaning of its parts:
This simple equation does not work if γ1 can be a sequencer such as a goto. The second command, γ2, is still involved in the meaning of goto φ; γ2 because of the composition operator, `o'.
The more complex continuation semantics introduces functions, called continuations, to stand for following computations. The continuation for goto φ above will include γ2. This continuation is passed to (the meaning of) goto φ which can choose not to execute it. Instead the goto executes whichever continuation the label φ denotes:
Each label in a block is bound to a continuation which is the computation that follows from the label. A goto discards the continuation standing for the computation that statically follows it.
Coroutines can also be defined by continuation semantics. Within coroutine A, resume B is much like a goto, a jump into coroutine B. The difference is that the continuation of the resume must be kept, not discarded, as it may in turn be resumed later.
In the following section, it will be shown how the use of exceptions allows the semantics of sequencers and of coroutines to be defined in direct semantics. For clarity type checking will be omitted from the semantics. For example it will be assumed that a goto is always jumping to a label and not to an integer variable.
The notation used for exceptions is based on standard ML. This form is chosen because ML is a freely available system with this feature, not because it is the only form of exceptions. An exception is declared and obeys the usual scope rules for identifiers. It has a type, which is the type of a value that may be returned when the exception is raised.
An exception can be handled or caught and appropriate action, usually remedial action, taken:
If an exception returns a value, it is bound to the var_id in the handler.
Exceptions can be defined in the λ-calculus without exceptions. Loosely, each expression returns a pair consisting of a flag and a conventional value. If the flag is 1, normal evaluation continues. Otherwise the flag represents an exception and evaluation returns until a matching handler is found. The value of the handler is then used.
Using exceptions it is possible to add the semantics of labels and of goto to the direct semantics of a language:
Note that while the θi are technically continuations, Cont is used here in the sense of a computation S-->S. It is the simple type of C that is the hallmark of direct semantics. The definition of jumps requires only the clauses for goto and for begin end; no other clauses require continuations or are altered in any way.
The addition of other sequencers, such as return from a procedure is straightforward:
Coroutines are only a little harder to define than jumps. The continuation of a resume must be preserved for later use; in this way the computation denoted by a coroutine identifier changes and must be placed in the store. If sequential execution is defined by composition, g o f, f has no information on what follows it, g. Only the operator `o' can access both f and g. By redefining `o', the continuation to a function that raises an exception can be obtained:
In a new environment ρ' each coroutine identifier ξi is bound to a location ιi. The locations are reserved from the store and initialised to the respective coroutine bodies C[γi]ρ'. A resume raises a res exception, returning the location bound to the label, the remaining computation θ and the state. The exception is handled by the appropriate cobegin. It binds the remaining computation to the location associated with the suspending coroutine and resumes the new one.
Note the else part in the definition of R. This is to permit nested coroutines as in the following example:
The statements one, two and three are executed in that order.
Exceptions can be added to the λ-calculus and defined in terms of existing mechanisms, thus the semantics of exceptions is well defined. Using exceptions the semantics of sequencers such as goto and of coroutines can be defined within direct semantics. This avoids the use of continuations. The resulting semantics are easy to use and can be grafted onto the semantics of a language that does not have sequencers without major changes.
Also see: L. Allison, A Practical Introduction to Denotational Semantics, CUP, Cambridge Computer Science Texts V23, 1986, (click).