Two-level languages for program optimization.
Two-level languages incorporate binding time information inside types, that is, whether a piece of code is completely known at compile-time, or needs some more inputs and can be evaluated only at run-time. We consider the use of 2-level languages in the framework of partial evaluation, and use a 2-level version of the simply typed lambda calculus with recursion. We give an operational semantics, an equational theory and a denotational semantics, that give an account of the distinction between compilation and execution phases. An adequacy theorem is given to relate the two semantics, showing in particular how they agree on non-termination at compile time. We finally give a more refined model using functor categories.
Introduction
Partial evaluation is an attempt to ll the gap between interpreting and compil-
ing. In the rst case we obtain an easy-to-prove correctness and good
exibility
to modications. Unfortunately, we usually get also a poor run-time behaviour,
often an order of magnitude slower than the non-interpretative counterpart. On
the other hand, compiled code is comparatively hard to understand, and prove
correct.
The aim of partial evaluation is to take a program as input and produce
a new program that gives the same output as the original one. But constant
evaluations are performed just once, during the program generation process.
This new program will incorporate all the data that remains constant, and is
called a specialized version of the old one. The following picture illustrates the
process:
Program
compile-time - Residual
run-time - Value
In this view, it is essential to distinguish between the computations that can be
performed at compile-time, called static, and the computations that need some
more data to be executed, that are called dynamic: the process of making this
distinction is called binding time analysis.
A classical example is the function power, that takes two integers x and y,
and computes y x , the x-th power of y. This function could be dened as follows
Research partially supported by MURST
Suppose that we know at compile-time that x is the number 3. Then x is a static
variable and y dynamic, and we can produce a residual program
y  y  y
This program is typically more e-cient than f 3 y.
There are various ways to perform a binding time analysis, but a promising
technique is to use a 2-level language: a language that incorporates binding time
information inside its types. Usually these languages have two versions of each
data type constructor, one for static and one for dynamic types. 2-level languages
were originally introduced in [12], and have been studied extensively in [18], but
their use for partial evaluation is more recent. Some examples can be found in
[4] and [11].
In this paper we study the semantics of a 2-level language, and give an operational
semantics and a denotational model. The basic idea of the semantics is
to evaluate all the static components of a program during compilation, obtaining
a residual program, that is a specialized version of the original one, and execute
it at run-time.
In the second section we introduce a 2-level language, essentially a 2-level
variant of the call-by-name language PCF [19], and give an operational semantics
that gives an account of the distinction between the compilation and the
execution phases. This distinction is made clear on showing that all the dynamic
operations can be postponed until after the static ones have been performed. We
study equivalences between terms, and show how an unrestricted -rule is not
valid for dynamic terms, although both levels of the language are purely call-
by-name if taken in isolation. This makes it more di-cult to give an abstract
model, because two kinds of undenedness are required, one for each level, and
it is not clear at rst how to generalize it to higher types.
In the third section we relate the operational semantics and the denotational
model given, and show an adequacy theorem asserting that the model not only
gives the same results, but also preserves the phase distinction from the operational
semantics.
The last section shows that, although adequate, the model contains some
junk, that is, some basic elements that are not denable within the language.
We suggest a better solution using a slightly more complex machinery.
The purpose of this work is to provide some insight in how to prove correctness
of partial evaluation, that is to prove the equivalence between the semantics of
the original program and the semantics of the specialized one. Both [11] and [4]
give a partial evaluator for a 2-level language but leave a correctness proof for
further work, while [18] gives a dynamic semantics parametrised on a xed static
semantics, but does not consider partial evaluation. A model is given in [18] but
no connection to operational notions is made. In our view, this connection is
crucial for understanding the link between the semantics and implementation
issues, especially for partial evaluation.
Proving correctness of partial evaluators is di-cult, and often error prone,
as shown in [8], where partial evaluation for an untyped language is considered.
An alternative solution is given in [16], and the correctness of the original model
is proved in [7], which also provides a correctness proof of the partial evaluator
of [4].
Existing models ([8, 7, 16]) give a syntactic interpretation of dynamic types,
namely as collections of open terms of the language, while our approach is more
abstract and similar to a standard treatment of PCF. The novelty of our approach
is the interpretation of both the compilation and execution phases in the
same framework, allowing to study their interaction with respect to computational
eects like non-termination.
2 A simple 2-level language
In this section we introduce a simple language, 2-level PCF, obtained from PCF
by augmenting each construct with a dynamic counterpart. First we explain the
syntax of the language and the type formation rules; then we give an operational
semantics, an equational theory and a denotational model.
2.1 2-level PCF
2-level PCF is a language obtained from PCF by adding dynamic types and
dynamic terms. The intended use of the language is to evaluate the static components
at compile-time, and execute the remaining part - the residual program -
at run-time. The base types are the usual natural numbers, nat , and the dynamic
numbers, nat . The higher types are constructed with static arrows, !, and dynamic
ones, ! . There are well-formedness rules on dynamic types, introduced
originally in [18]: a dynamic arrow must have dynamic types on either side. These
rules are motivated by the consideration that dynamic functions should not depend
on static computations, because at run-time the static computations have
already been performed. For the base case, there is no reason to allow dynamic
functions to take static naturals as inputs, because there is a construct - lift -
that embeds terms of type nat in dynamic terms. Moreover, these constraints
give interesting properties that allow to postpone all the dynamic evaluations
after the static ones in the operational semantics.
The types of 2-level PCF are given by the following grammar:
where s are the static types and d are the dynamic ones. We will use t;
as
The terms and type rules are structured in a similar way: essentially two copies
of every construct.
Terms:
pred (M)
pred (M)
Here succ is the successor function over numbers, ifz is the conditional whose
guard checks if the rst argument is zero, x is the recursion operator, and lift
embeds a static expression of type nat in a dynamic expression: note that this
is possible only for the base type. The purpose of lift is to insert a static value
into the residual program.
A type assignment , written is a nite set of variable/type
pairs, where all the x i are distinct. indicates the extension of with the
Type formation rules:
Note that the dynamic if-then-else requires all the arguments to be dynamic;
this is to avoid, for example, static terms like
whose evaluation would depend on the evaluation of the dynamic term D. This
would be a problem especially if we consider the possibility of non-termination:
if D does not terminate at run-time, this cannot in
uence the value of the whole
term at compile-time.
2.2 Operational Semantics
In this section we give an operational semantics for 2-level PCF. The basic idea
is to give two reduction relations: ! s for static reduction and ! d for dynamic
reduction. The intended constraint is that static reduction must always be performed
before the dynamic one.
Operational semantics:
pred lift(n) ! d lift(n 0 1)
where static contexts C s and dynamic contexts C d are dened as follows:
pred [
pred [
pred [
The notation indicates the subtraction of natural numbers extended
with Each relation is dened in an analogous way to the usual
reductions for PCF, where M [N=x] indicates the capture-free substitution of N
for x in the term M . In particular ! s is exactly the one of PCF, while ! d is
the obvious dynamic counterpart. Note the use of lift to form basic constants of
are in fact the canonical forms of dynamic numbers, i.e. the form
that a terminating computation is expected to reach.
Consider the static term sund dened as follows.
sund  x x:x : nat
We will use sund as a canonical term to represent static undenedness at base
type. Clearly its evaluation will fail to terminate already during the compilation
phase. On the other hand, consider the dynamic term dund :
dund  x x:x : nat
This new term is evaluated to itself during compilation. In fact, it cannot be
reduced statically, but an attempt to execute it at run-time will lead to non-termination

The need for the constraints on the interleaving of static and dynamic reductions
can be explained with a few examples. Consider the following term:
In principle it is possible to use dynamic reduction to yield a result: M ! d
. But a careful analysis of M reveals the presence of a sub-term, sund ,
that does not terminate at compile-time, and because we are in the setting of
partial evaluation we should try to reduce it, causing non-termination during
the compilation of M . Conversely, the term
can be statically reduced to 0, although it has an innite reduction sequence.
The discussion above suggests that a term can be reduced dynamically only if
it can be compiled; in other words terms that do not have a terminating static
reduction should not be reduced dynamically. The simplest way to ensure that
a term can be run safely is to require it to be in Static Normal Form (SNF).
Denition 1 A term M is in SNF if there is no M 0 such that M ! s M 0 .
We can now put the two relations together.
Denition 2 Given a well-typed term M , M ! sd M 0 if
1.
2. M is in SNF and M ! d M 0 .
The following lemma is crucial, in the sense that it shows how all the static
reductions can be performed before the dynamic ones, obtaining a complete
separation between the two phases.
Lemma 3 Postponent
Given a well-typed term M , M !
sd M 0 if and only if there is a term M 00 such
that
Proof. We show that if M is in SNF and M ! d M 0 , then M 0 is in SNF.
The only interesting part is the rule
are in SNF, hence the only problem is if M 1 contains a
sub-term of the form (x N) for some N , but this is not possible because x must
have dynamic type due to the type formation rules. ut
If we relax the condition that M must be well-typed, the previous lemma is
no longer valid. Consider the ill-typed term
Clearly M is in SNF, but M ! d ((x:x)
We conclude this section with a complete example of partial evaluation: the
power function discussed in the introduction. Let POW : nat!nat!nat be the
x f: n:x:ifz nthen lift(1) else x  (f (n 1) x)
where is the static subtraction, and  is the dynamic product, both denable in
the obvious way. The reduction has the eect of compiling the program yielding
an optimized version:
sd x: x  x  lift(1)
If all the arguments are given to POW , also the execution phase is performed:
sd lift(49)
From the example, it should be clear that the operational semantics gives information
about both compilation and execution of programs.
2.3 Equational Theory
In this section we consider the  and  rules familiar from type theory, and state
which versions of them are valid in this setting. Two versions of each rule can
be expressed in the language, and only one of the four combinations is invalid.
The following rules are valid
x:(M @
The  and  rules are valid because the static fragment of the language is purely
call-by-name. The  rule does not aect the static behaviour of the term, and
purely dynamic terms behave in a call-by-name fashion.
The  rule is not valid:
In fact, consider the term (x:lift(0)) @ lift(sund). It cannot be equal to lift(0),
because the term sund does not terminate at compile-time, thus the code lift(0)
is never produced. Borrowing the ideas from operational semantics, we can give
a special rule
is in SNF
The remarks in this section will be veried after introducing the denotational
model.
2.4 Denotational Semantics
A CPO (complete partial order) is a partially ordered set with a least element
and all least upper bounds of !-chains, and a function between CPOs is said to
be continuous if it preserves least upper bounds of !-chains (hence is monotone).
In this section we give a model of the language interpreting types as CPOs and
terms as continuous functions between CPOs. We write N? for the
at CPO
of natural numbers (with ? n for each number n), and in general X? for the
CPO obtained from the CPO X by adding a new least element. X!Y indicates
the CPO of continuous functions between X and Y , and - is for function composition

Interpretation of types:
The interpretation of static types is the usual one from call-by-name PCF, while
the dynamic types deserve an explanation. We have seen that there are two kinds
of undenedness: at compile-time and at run-time. In this view, the type nat
contains two elements apart from natural numbers: ? is intended to interpret
terms like lift(sund) and indicate failure during the compilation phase, while
? is intended to interpret terms like dund that do not terminate when exe-
cuted. Normally [[nat would be written (N? ) ? , but we use ? as a notational
convenience to denote the inner ?.
For the dynamic arrow, the idea is that a dynamic function can either not
terminate at compile-time, or behave in a usual call-by-name fashion at run-
time. Thus the semantics of dynamic types turns out to be the lifting of the
semantics of the corresponding static types obtained removing underlines.
From the semantics of types one might have expected  to be valid and
invalid, because looks like in lazy -calculus. But we will see that just
the reverse is true.
For each CPO X we consider a function up : X!X? that embeds x 2 X in X? ,
that is the identity on X extended by sending ? to the least
element of X . The two following functions will be essential to give the semantics
of dynamic terms:
otherwise.
The function dyn is used to transform a static arrow between dynamic types
into a dynamic arrow, and corresponds to the type formation rule
The idea behind the denition of dyn is that a static function between dynamic
types is either undened or is dened for each dened argument. That
is, the failure to compile the function, once applied, does not depend on the
dynamic argument passed to it, unless the argument itself fails to be compiled.
The dapp operator is used to interpret dynamic application, and has the
purpose of propagating the undenedness of terms in a call-by-value style. Note
that both levels are essentially call-by-name if taken in isolation, but the dynamic
level behaves like call-by-value with respect to static undenedness.
Given a type assignment  , an environment  is a function
Given a judgement ' M : t,
we write [[M for the interpretation of M in the environment . Figure 1 denes
the interpretation of the terms of the language.
The static components of the language are interpreted as in call-by-name PCF.
The use of the functions dyn and dapp has already been explained, and the other
constructs are interpreted in a very natural way: propagating static undened-
ness in case of non-termination, using a standard interpretation otherwise.
Now we reconsider the rules introduced in the equational theory section, and
show that they are valid in the model. To see that  is not valid, consider the
terms
[[pred M
[[pred M
F
Fig. 1. Denotational Semantics
From the denotational rules we have
For the  rule, we have
First note that [[M since x is not free in M by assumption.
If since dyn(c 7!?) =?. Otherwise, there
exists an f such that [[M
The  rule is trivial, and in order to prove the other rules we need a fundamental
lemma.
Lemma 4 Substitution Lemma
for each
Proof. The proof is by induction on M. We indicate with  0 the environment
[x 7! [[N ]]], and will consider only two important cases.
Case
Case M  y:M 0 ,
Exploiting this result, it is easy to see that  rule is valid. Note that the failure
of the  rule is not due to a fail in the Substitution Lemma, but to the fact that
in general
The validity of the  0 rule follows easily from a result of the next section: if N
is in static normal form, then [[N
3 Adequacy
So far we have seen an operational semantics and a denotational model of 2-level
PCF. Now it is time to relate the two semantics and prove an adequacy result.
This is achieved using two dierent logical relations dened by induction on the
structure of types. The rst one is used to obtain a static adequacy result, and
gives a semantic counterpart to the syntactic result of phase distinction between
static and dynamic evaluation. The second is easier and shows how the purely
dynamic fragment behaves exactly like call-by-name PCF, because there is no
way to introduce static undenedness.
3.1 Adequacy Theorems
We state below two adequacy theorems, leaving the proofs to the end of each
section.
Theorem 5 Static Adequacy
Let M be a closed term of type nat , then M !
The Dynamic Adequacy Theorem states that a term of type nat can be compiled
if and only if its denotation is not ?; moreover, if it can be compiled then it
terminates at run-time if and only if its denotation is not ?.
This is a crucial result, because it shows that the operational distinction
between static and dynamic evaluation is respected in the model; in particular,
the way how the two relations ! s and ! d are combined is re
ected.
Theorem 6 Dynamic Adequacy
Let M be a closed term of type nat , then
s D for some dynamic value D.
Moreover,
d lift(n).
3.2 Proof of Static Adequacy
In this section we prove the Static Adequacy Theorem. A logical relation is given
to relate the operational semantics and the denotational model in a way that
ignores the denotational semantics of dynamic terms.
The following lemma states the independence of static reduction from dynamic
terms.
t, and N : u.
If
s M 00 for some term M 00 .
Proof. It is enough to observe that a static rewriting can only discard or duplicate
a dynamic sub-term, but does not depend on its shape, that is if M [N=x] ! s
We now introduce the notion of value: a shape that a term can reach through
static reduction if the compilation succeeds. The values V are divided into static
The following two lemmas give a characterization of values and a con
uence
property.
Lemma 8 A term M is a value if and only if either it is an abstraction or it is
in SNF.
Lemma 9 If M !
equality up to -
equivalence is considered.
Denition Logical Relation . t .
Dene a family of relations . t between elements of closed terms of type
t. For any d 2 closed
1 d =?, or
exists V such that M !
up(n) . nat n
d . nat V 0 , for each V 0
c . t 1
d . d1
This relation will be used to prove that if the semantics of a term is not unde-
ned, then it can be statically reduced to a value. This is very important for
dynamic terms, because we can show that all their static sub-terms are completely
evaluated and discarded during compilation. Note how the relation is
essentially independent from the actual interpretation of dynamic constructs,
since it only checks if the interpretation is dened.
Lemma
Proof. The trivial case is when c =?. If c 6=?, then there exists a unique (by
Lemma
Lemma 12 The relation . t is monotone and complete: for each type t and
closed t, the following hold.
is an !-chain and c i . t M for each i 2 !, then
F
Proof. The only interesting case is point 2 when t is of the form t 1 !t 2 .
If F
there is nothing to prove. Otherwise there exists k 2 ! such that
s V for some (unique by Lemma
such that a . t 1
U . By denition for each i 2 !, c i (a) . t 2
induction hypothesis (
F
F
The following lemma is valid in general for open terms, but in the particular
case of closed terms it states that the interpretation of a term is related with the
term itself. The proof of the various cases is developed in quite a natural way
from the previous lemmas. The only exception is the  case, where some eort
is required.
Lemma
t. If c i 2
Proof. By induction on the structure of M . Let  be the substitution [
and let  be the environment [ We consider only some important cases:
Case M  x:M
Let f be [[x:M 0 ]]. If f =?, the conclusion is immediate.
Otherwise, since x:M 0 is a value, we have to show, for each c 2 [[t 0
Taken any such c and N , the induction hypothesis gives
by an
application of the  rule, Lemma 11 implies f(c) . t 00
Case M  (L N ).
Suppose that be [[L]], and a be [[N ]]. We have
to prove that f(a) . t 00 (L N ). If f(a) =?, the conclusion is immediate.
Otherwise, also f 6=?, and by induction hypothesis (L)
induction hypothesis a . t 0 (N ), so f(a) . t 00 (x:L 0 (N )). By operational
rules (L
gives the
result.
Case M  x:M
Let f be c 7! =?, the proof
is immediate. Otherwise, by denition of dyn , for each c 6=?, f(c) 6=?. We
have to show that there exists a value V such that (x:M 0
Because
d 0 is a dynamic type, it can be written as d 1 !    ! dn ! nat . Consider the
It is easy to show that [[Z d 0
By induction hypothesis on M 0 ,
there exists a value V
such that [x 7! Z d 0 ](M
using Lemma 7 we obtain (M
s
Case M  xx:M t.
Let f be c 7! [[M 0 ]][x 7! c], let e 0 =? and e
F
induction hypothesis on
M 0 we have e
By the operational semantics of x ,
Lemma 11 we obtain e i+1 . t (M ). We have shown that, for each i 2 !,
F
Lemma 14 Static soundness
Given a closed term M , if
Proof. The proof is a simple case analysis, involving the Substitution Lemma.
ut
Proof of Theorem 5
Consider a closed term M of type nat .
By Lemma 13, [[M
s n.
Conversely, if M !
3.3 Proof of Dynamic Adequacy
In this section we prove how the interpretation of purely dynamic terms is essentially
the same as that of call-by-name PCF. We dene a translation between
2-level PCF and standard PCF, a relation between the two denotational seman-
tics, and conclude with the proof of the Dynamic Adequacy Theorem.
From now on we will refer to dynamic terms and dynamic types simply as terms
and types, and introduce a new notation: indicates the interpretation
of terms of 2-level PCF and the usual interpretation of terms of
call-by-name PCF, i.e. the continuous function model over N? given in [19].
We dene a translation p q from dynamic values of 2-level PCF to terms of
standard PCF. The translation of types simply removes the annotations.
The translation of type assignments is point-wise, and the denition for terms
is the following.
plift(n)q
pred pV q
px x:V q
To understand the following logical relation, note that the semantics of a
dynamic type d is the lift of the corresponding static type:
Denition Logical relation R.
For each dynamic type d, dene a logical relation R d between
f R d1 ! d2 g, if for all b and c, b R d1 c implies dapp(f; b) R d2 g(c)
The relation is intended to be used on purely dynamic terms, i.e. terms that
compile to themselves, hence are always dened. Thus ? in 2LPCF is not in
relation with anything, and at the upper levels, the relation is essentially one-
to-one.
Lemma For each type d, b R d c if and only if equivalently,
Lemma t. If b i R t i
c i for each i, then
Proof. By induction on the structure of D. Let  be the environment [x i 7!
and let  0 be the environment [x i 7! c i ]. We consider only some key cases:
Case D  x:D
Let f be b 7! [[D 0 let g be c 7! [[pD 0
Suppose by denition of dyn , there exists a 2 [[d 1
such that a 6=? and f(a) =?, but a R d1 down(a) by Lemma 16, hence
by induction hypothesis on D 0 we have f(a) R d2 g(down(a)). By Lemma
=?. This is a contradiction, hence we
conclude that dyn(f) 6=?.
We have to show dyn(f) R d1 ! d2 g. Suppose b R d1 c, then we have to show
that dapp(dyn(f); b) R d2 g(c).
By induction hypothesis on D 0 , f(b) R d2 g(c). But dyn(f) 6=? and b 6=?,
since f(b). We have shown
that dyn(f) R d1 ! d2 g.
Case D  x
Let f be [[x:D 0 and g be [[x:pD 0
From the  case, dyn(f) R d ! d g, so b R d c implies dapp(dyn(f); b) R d g(c);
but from Lemma 16,
hence up(
F
F
Proof of Theorem 6
Take a closed term M of type nat .
If
s D for some dynamic value D.
Conversely if M !
s D, by Lemma 14 [[M
Suppose now that [[M
up(n), hence by adequacy of PCF D !
d lift(n).
Conversely if D !
d lift(n), then by soundness of PCF we have
up(n), and by Lemma 17
4 A Model in CPO !
In this nal section we introduce a new model for 2-level PCF, showing the
advantages of this on the previous one. Then we show the limits of the new
model and outline what an ideal model would be.
So far we have seen how to interpret 2-level PCF in the category CPO of
complete partial orders and continuous functions. We have seen a function dyn
to interpret dynamic types, and its denition was not completely natural. The
use of CPO ! allows to give a more natural interpretation.
Denition The category CPO ! is dened as follows
Objects are triples (X; A; p) where X and A are CPOs, and
a continuous function.
Morphisms between (X; A; p) and (Y; B; q) are pairs hf; gi such that the
following diagram commutes
A
f
The identity on (X; A; p) is the pair hid A ; id X i.
Composition is point-wise: hh; li - hf;
The category CPO ! is cartesian closed, where the product is dened point-wise,
and the exponential object (X; A; p) ) (Y; B; q) is
where  1 is the rst projection, and the order in the upper CPO is dened as
the conjunction of the two orders between functions.
We use additional notation: ! is the unique morphism X!1, where 1 is the
CPO with one element;  is the element above ? in 1? ; if f : X!Y is a continuous
function, then f? : X?!Y? is the extension of f that maps ? to ?; (!)
indicates the exponential in CPO and ( ) ) the exponential in CPO ! .
With this machinery we can give another model of 2-level PCF. The types are
interpreted as follows
id
Y?
The ! that CPO ! uses for parametrisation can be visualized as
static
compile - dynamic:
In the model the top CPO represents the information before compilation, while
the bottom one represents the information after compilation. In the nat case,
the bottom part says whether the program can be compiled or not.
To give a characterization of the interpretation of dynamic types, consider
the notation in 2
? (X), given a CPO X , for
Then the interpretation of each dynamic type d has the following property:
We can now dene a family of morphisms dyn 0 , used to interpret dynamic
terms.
Denition 19 For each pair of CPOs X and Y , dene
In diagrams this is
For the nature of the objects involved, it is enough to give the upper function
of the morphism, because the lower one is determined by the other.
Note that if f =?, then also g =?. If
We will not give the formal interpretation of terms, since it is very similar to
the CPO case. Note that considering global elements, i.e. morphisms from 1 to
A, the interpretations of base types and of dynamic types in CPO ! are order-
isomorphic to the interpretations in CPO, hence the interpretation of dynamic
terms and of most of the static constructs is given essentially in the same way. In
particular, a type assignment is interpreted as the product of the interpretations
of its types, and static -abstraction and application are interpreted in the usual
way using the cartesian closed structure of CPO ! . The remaining cases are
the dynamic -abstraction that is interpreted like the CPO case but using dyn 0
instead of dyn, and the static x point is interpreted using the CPO-enrichment
of CPO ! .
Another example illustrates how the model in CPO ! is an improvement
of the previous one. Consider the type u  nat!nat . By denition
while the intuition from the operational semantics suggests that the
only denable functions of that type should be the constant ones, because there
is no way for a dynamic sub-term to in
uence the compilation of a static term.
On the other side, the elements of
are pairs hf; gi such that the following
diagram commutes
f
id
If f(?) 6=?, then g is a constant function; otherwise g maps ? to ? and is
constant on the remaining elements.
4.1 Limits of the Model
We have seen how the introduction of the CPO ! model eliminates some junk
present in the CPO one. But the new model is not completely satisfactory, as
will be clear from the following example.
Consider the simple language where the only base types are booleans; the
interpretation of the type bool!bool will contain the pairs hf; gi such that
f
commutes, where B is the set ftrue; falseg.
In particular we can have
Clearly this is not denable, because a term would be required able to distinguish
between failure at compile-time and at run-time of its argument. This shows that
not all the elements of the model are denable.
As a nal remark, we make a case-study of what an optimal interpretation
should be for an even easier type. Consider the type unit , whose only constant
is ; we want to study the denable functions of type unit!unit . To do so
we consider the global elements of [[unit!unit
and say which ones are
denable.
f
There are the following cases:
Case f =?. Then also g =? and is dened by x:lift(sund).
Case Then g has a component
dened by x:((y:dund) @ x);
dened by x:x;
dened by x:((y:lift()) @ x).
Case has a component
dened by x:dund ;
dened by x:lift().
In summary there are 6 denable functions of type unit!unit , the CPO ! interpretation
contains 8 functions, and the CPO one contains 10 functions.
5 Conclusion
In this work we presented an operational and denotational semantics of a 2-level
language. Both dynamic and static operational semantics were call-by-name. The
denotational model, however, was a bit unusual; the model of the static part is
standard, while the model of the dynamic part is the lift of the standard call-by-
name model. This lifting was used to capture the interplay between static and
dynamic evaluation. The adequacy theorem conrms the accuracy of the model
in this regard.
The model, although adequate, is not very precise, because it contains some
junk. For example the type nat!nat is interpreted as the CPO N? ? !N? ? ,
while the actual denable functions are either undened or send each dened
element to a dened result.
In conclusion, the relation between static and dynamic is subtle and we do
not understand it perfectly yet from a semantic point of view. In particular, the
nature of it is not the cartesian closed arrow, nor it is
the usual interpretation in call-by-value or lazy -calculus. A future work would
be to clarify its meaning from a categorical point of view.
Another area of further work is the choice of evaluation strategies: we have
chosen call-by-name at both static and dynamic levels for simplicity, but we
expect the same could work for call-by-value or lazy -calculus.

Acknowledgements

.
I want to thank Peter O'Hearn for the many fruitful discussions. I am also
grateful to Eugenio Moggi and the anonymous referees for their useful comments
on an early draft of this paper.
Paul Taylor's macros for diagrams have been used.



--R

Handbook of logic in computer science.
A Mixed Linear and Non-Linear Logic: Proofs
What is a Categorical Model of Intuitionistic Linear Logic?

Pragmatics of Type-Directed Partial Evaluation

A Semantic Account of Type-Directed Partial Evaluation
A partial evaluator for the untyped lambda cal- culus
Semantics of Programming Languages: Structures and Techniques.
Polymorphic binding-time analysis
Type specialization for the lambda calculus.

Leeuwen, editor. Handbook of Theoretical Computer Science.
Projection Factorisations in Partial Evaluation.
A categorical account of two-level languages
Functor categories and two-level languages


LCF as a programming language.

--TR
An experiment in partial evaluation: the generation of a compiler generator
Projection factorisations in partial evaluation
Two-level functional languages
Semantics of programming languages
Handbook of logic in computer science (vol. 2)
Type-directed partial evaluation
Handbook of Theoretical Computer Science
Partial Evaluation
Polymorphic Binding-Time Analysis
A Semantic Account of Type-Directed Partial Evaluation
Functor Categories and Two-Level Languages
Multi-Level Lambda-Calculi
Pragmatics of Type-Directed Partial Evaluation
Type Specialisation for the lambda-Calculus; or, A New Paradigm for Partial Evaluation Based on Type Inference
program generation;partial evaluation;semantics