Exceptions, a mathematical semantics for handling full jumps

Lloyd Allison, Department of Computer Science, Monash University, Clayton, Victoria 3168, Australia.

March 1987
Technical Report 87/90

home1 home2
 Bib
 Algorithms
 Bioinfo
 FP
 Logic
 MML
 Prog.Lang
and the
 Book

Semantics

book

(This work was later described in: L. Allison, Direct semantics and exceptions define jumps and coroutines, Inf. Proc. Lett., V31, pp327-330, 1989.)

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.

Introduction

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[1]. It expresses the meaning of a compound command directly as the functional composition of the meaning of its parts:

γ :Cmd
ξ :Ide
ρ :Env = Ide --> Dv
σ :S = Loc --> Sv
 
C :Cmd --> Env --> S --> S
 
C[ γ1; γ2 ] ρ σ = ((C2]ρ)o(C1]ρ)) σ

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[3] 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:

θ :Cont = S --> S
C :Cmd --> Env --> Cont --> S --> S
 
C[ γ1; γ2 ] ρ θ σ = C1] ρ {C2]ρθ} σ
 
C[ goto φ ] ρ θ σ = ρ[φ] σ
 
C[ begin φii end ] ρ θ σ = θ1 σ, i=1..n
  where θi = Ci] ρ' θi+1, for_all i=1..n
  and θn+1 = θ
  and ρ' = ρ[θii], for_all i=1..n

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.

Exceptions

The notation used for exceptions is based on standard ML[2]. 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.

<decln> ::= exception <exception_id> {: <type>}

An exception can be handled or caught and appropriate action, usually remedial action, taken:

<expression> ::= raise <exception_id> {with <expression>} |
<expression> handle <exception_id> {with <var_id>} => <expression> |
<decln>; <expression> | ...

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.

E : Exp --> Env --> (Flag × Value)
newex : Env --> (Flag × Env)
 
E[ exception ξ; ε ]ρ = let n,ρ'=newex ρ in E[ε]ρ'[n/ξ]
 
E[ raise ξ with ε ]ρ = let f,v=E[ε]ρ in if f=1 then <ρ[ξ],v> else <f,v>
 
E[ ε handle ξ with ξ' => ε' ]ρ = let f,v=E[ε]ρ in if f=ρ[ξ] then E[ε']ρ[v/ξ'] else <f,v>
 
E[ ε ε' ]ρ =
  let f,v = E[ε]ρ in
  if f=1 then let f',v'=E[ε']ρ in if f'=1 then apply v v' else <f',v'>
  else <f,v>

Jumps

Using exceptions it is possible to add the semantics of labels and of goto to the direct semantics of a language:

C :Cmd --> Env --> S --> S
 
C[ γ1; γ2 ] ρ σ = ((C2]ρ) o (C1]ρ)) σ
 
τ :Tag
exception jump : (Tag × Cont) × S
newtag :S --> (Tag × S)
 
C[ begin φii end ] ρ σ = G θ1 σ', i=1..n
  where G θ σ = (θ σ) handle jump with <τ',θ'>,σ"
  => if τ'=τ then G θ' σ" else raise jump with <τ',θ'>,σ",
  and θi = Ci;..;γn]ρ', for_all i=1..n,
  and ρ' = ρ[<τ,θi>/φi], for_all i=1..n,
  and τ,σ' = newtag σ
 
C[ goto φ ] ρ σ = raise jump with (ρ[φ]),σ
In the new environment ρ' within a block, each label stands for a tag and a computation from the label to the end of the block. The tag is something to uniquely identify a block invocation; it could for example be the free storage counter of the state if function newtag also increments this. A goto raises a jump exception, returning the tag and computation that the label denotes and a store. The exception is handled by the meaning of the block. If the label is non-local to the block, it is raised again until the appropriate block handles it. The tag is needed because the language being defined may contain procedures. The scope of a label reflects the static layout of a program but exceptions are handled dynamically and the tag ensures that the exception raised by a goto is caught by the correct block.

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:

δ :Dec
D :Dec --> Env --> S --> (Env × S)
 
exception ret :S
D[ proc ξ=γ ]ρσ = <ρ',σ>
  where ρ'=ρ[p/ξ],
  and p = λσ'.C[γ]ρ'σ' handle ret with σ" => σ"
 
C[ δ; γ ]ρσ = let ρ',σ'=D[δ]ρσ in C[γ]ρ'σ'
 
C[ call ξ ]ρσ = let p=ρ[ξ] in pσ
 
C[ return ]ρσ = raise ret with σ

Coroutines

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:

C :Cmd --> Env --> S --> S
 
ι :Loc
exception res :Loc × Cont × S
f o g = λ σ. f((g σ) handle res with ι,θ,σ' => raise res with ι,f o θ,σ')
 
C[ γ1; γ2 ] ρ = (C2]ρ) o (C1]ρ)
 
C[ resume ξ ] ρ σ = raise res with ρ[ξ],(λx.x),σ
 
C[ cobegin ξii end] ρ σ = R ι1 σ', i=1..n
  where R ι σ = (let θ=σ ι in θ σ) handle res with ι',θ,σ"
  => if ι' in1..ιn] then R ι' σ"[θ/ι] else raise res with ι',Rι,σ"[θ/ι],
  and ρ' = ρ[ ιii ], for_all i=1..n,
  and <ι1,..,ιn>,σ' = reserve n <C1]ρ',..,Cn]ρ'> σ

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 Ci]ρ'. 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:

cobegin
  A=cobegin
      A1=begin one; resume B; three;... end;
      A2=begin ... end
    end;
  B=begin two; resume A; ... end
end

The statements one, two and three are executed in that order.

Conclusions

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.

References.

[1] R.Milne, C.Strachey. A Theory of Programming Language Semantics, Chapman and Hall (2vols) 1976.
[2] R.Milner. The standard ML core language, Edinburgh University 1986
[3] C.Strachey, C.P.Wadsworth. Continuations: a mathematical semantics for handling full jumps, PRG-11 Oxford University Programming Research Group 1974

Also see: L. Allison, A Practical Introduction to Denotational Semantics, CUP, Cambridge Computer Science Texts V23, 1986, (click).

Coding Ockham's Razor, L. Allison, Springer

A Practical Introduction to Denotational Semantics, L. Allison, CUP

Linux
 Ubuntu
free op. sys.
OpenOffice
free office suite
The GIMP
~ free photoshop
Firefox
web browser

© L. Allison   http://www.allisons.org/ll/   (or as otherwise indicated),
Faculty of Information Technology (Clayton), Monash University, Australia 3800 (6/'05 was School of Computer Science and Software Engineering, Fac. Info. Tech., Monash University,
was Department of Computer Science, Fac. Comp. & Info. Tech., '89 was Department of Computer Science, Fac. Sci., '68-'71 was Department of Information Science, Fac. Sci.)
Created with "vi (Linux + Solaris)",  charset=iso-8859-1,  fetched Thursday, 28-Mar-2024 22:52:53 AEDT.