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

March 1987
Technical Report 87/90

(This work was later described in: L. Allison, Direct semantics and exceptions define jumps and coroutines, Inf. Proc. Lett., vol.31, pp.327-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[ γ₁; γ₂ ] ρ σ = ((C[γ₂]ρ)o(C[γ₁]ρ)) σ

This simple equation does not work if γ₁ can be a sequencer such as a goto. The second command, γ₂, is still involved in the meaning of goto φ; γ₂ 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 γ₂. 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[ γ₁; γ₂ ] ρ θ σ = C[γ₁] ρ {C[γ₂]ρθ} σ

 

C[ goto φ ] ρ θ σ = ρ[φ] σ

 

C[ begin φ_i:γ_i end ] ρ θ σ = θ₁ σ, i=1..n

  where θ_i = C[γ_i] ρ' θ_i+1, for_all i=1..n

  and θ_n+1 = θ

  and ρ' = ρ[θ_i/φ_i], 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[ γ₁; γ₂ ] ρ σ = ((C[γ₂]ρ) o (C[γ₁]ρ)) σ

 

τ :Tag

exception jump : (Tag × Cont) × S

newtag :S --> (Tag × S)

 

C[ begin φ_i:γ_i end ] ρ σ = G θ₁ σ', i=1..n

  where G θ σ = (θ σ) handle jump with <τ',θ'>,σ"

  => if τ'=τ then G θ' σ" else raise jump with <τ',θ'>,σ",

  and θ_i = C[γ_i;..;γ_n]ρ', for_all i=1..n,

  and ρ' = ρ[<τ,θ_i>/φ_i], for_all i=1..n,

  and τ,σ' = newtag σ

 

C[ goto φ ] ρ σ = raise jump with (ρ[φ]),σ

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[ γ₁; γ₂ ] ρ = (C[γ₂]ρ) o (C[γ₁]ρ)

 

C[ resume ξ ] ρ σ = raise res with ρ[ξ],(λx.x),σ

 

C[ cobegin ξ_i=γ_i end] ρ σ = R ι₁ σ', i=1..n

  where R ι σ = (let θ=σ ι in θ σ) handle res with ι',θ,σ"

  => if ι' in [ι₁..ι_n] then R ι' σ"[θ/ι] else raise res with ι',Rι,σ"[θ/ι],

  and ρ' = ρ[ ι_i/ξ_i ], for_all i=1..n,

  and <ι₁,..,ι_n>,σ' = reserve n <C[γ₁]ρ',..,C[γ_n]ρ'> σ

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:

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)].