|
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., 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 ] ρ σ
= ((C[γ2]ρ)o(C[γ1]ρ)) σ
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 ] ρ θ σ
= C[γ1] ρ {C[γ2]ρθ} σ
-
- C[ goto φ ] ρ θ σ = ρ[φ] σ
-
- C[ begin φi:γi end ] ρ θ σ
= θ1 σ, 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[ γ1; γ2 ] ρ σ
= ((C[γ2]ρ) o (C[γ1]ρ)) σ
-
- τ :Tag
- exception jump : (Tag × Cont) × S
- newtag :S --> (Tag × S)
-
- C[ begin φi:γi end ] ρ σ
= G θ1 σ', 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 (ρ[φ]),σ
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 ] ρ
= (C[γ2]ρ) o (C[γ1]ρ)
-
- C[ resume ξ ] ρ σ
= raise res with ρ[ξ],(λx.x),σ
-
- C[ cobegin ξi=γi end] ρ σ
= R ι1 σ', i=1..n
- where R ι σ
= (let θ=σ ι in θ σ)
handle res with ι',θ,σ"
- => if ι' in [ι1..ιn]
then R ι' σ"[θ/ι]
else raise res with ι',Rι,σ"[θ/ι],
- and ρ' = ρ[ ιi/ξi ], for_all i=1..n,
- and <ι1,..,ιn>,σ'
= reserve n <C[γ1]ρ',..,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)].
|
|