call-by-value semantics, etc. (248 lines)

Date: Wed, 2 Aug 89 23:23:46 -0400

We have followed with interest the recent types discussion about the
semantics of call-by-value.  It happens that we have been working on
the operational semantics of a call-by-value version of PCF extended
to a type system with multiple inheritance.  That the lifted function
space semantics (or, if you prefer, partial function semantics) of
call-by-value PCF is computationally adequate is a consequence of our
similar result for the multiple inheritance extension we have studied.

We append below a LaTeX source for the introduction to an extended
abstract entitled COMPUTING WITH COERCIONS which we have just
completed.  As a side note on this research, our objective was to
prove a syntactic result about the relationship between two views of
the operational semantics.  Although it is interesting in its own
right, we proved a computational adequacy result primarily because it
was a useful tool in showing our central syntactic result.

   Val Breazu-Tannen
   Carl Gunter
   Andre Scedrov

============================== cut here ===============================

\documentstyle{article}
\def\baselinestretch{1.2}

\begin{document}

\begin{center}

{\LARGE
{\bf COMPUTING WITH COERCIONS}}\\[5pt]
{\large {\it (Extended Abstract)}}

\vspace{.5cm}

{\large {\em \hfill V.~Breazu-Tannen\hfill C.~A.~Gunter\hfill
A.~Scedrov \hfill}}

\vspace{.5cm}

University of Pennsylvania

\end{center}

\vspace{.5cm}

\begin{quote} {\small {\bf Abstract.} This paper relates two views
of the operational semantics of a language with multiple inheritance.
It is shown that the introduction of explicit coercions as an interpretation
for the implicit coercion of inheritance does not affect the evaluation
of a program in an essential way.  The result is proved by semantic
means using a denotational model and a computational adequacy result
to relate the operational and denotational semantics. } \end{quote}

In a previous paper [Breazu-Tannen, Coquand, Gunter and Scedrov,
LICS'89], we proposed a novel semantic paradigm for understanding
inheritance subtyping in object-oriented programming languages.

Our paradigm applies to some of the languages that try to capture the
flexibility of object-oriented programming [Goldberg and Robson 83] in
a setting which maintains the reliability, and sometimes increased
efficiency, of statically type-checkable programs. The type discipline
of these languages relies on an {\em inheritance relationship} between
types which was first proposed in [Reynolds, LNCS 94, 1980]. Such a
typed language is proposed in [Cardelli, LNCS 173, 1984 and Cardelli,
I\&C, 1988], and an extension that incorporates parametric
polymorphism, called Fun, appears in [Cardelli and Wegner, Comp Surv,
1985].

The essence of our semantic paradigm is to think of the inheritance
relationship as an implicit coercion, and to interpret it by an
explicit coercion which, moreover, is already definable in the
inheritance-free fragment of the language.  In [BCGS89], we
demonstrate this idea on the language Fun of Cardelli and Wegner,
extended with recursive types. The paper proves the {\em denotational
coherence} of our interpretation, a result which shows how to make a
model of the inheritance-free fragment of the language into a model of
the whole language. Quite pleasantly, denotational coherence holds
true of a large class of models.

We regard denotational coherence only as the first step in proving the
robustness of our interpretation. In the present paper we supply even
more convincing evidence, in the form of a result that relates our
interpretation to the {\em operational semantics} of the languages.

We choose a simpler language than Fun to illustrate this kind of
result.  In particular, we drop polymorphism and we replace recursive
types with just plain recursion, believing that the results can be
extended to include these dropped features, at the price of some
technical complications. What we have can be described as a double
extension of Plotkin's illustrative language PCF [Plotkin, TCS, 1977].
We get one extension, PCF+, by adding record and variant types, and a
further extension, PCF++, by adding inheritance. This is essentially
the language studied by Cardelli in [LNCS 173, 1984] and [I\&C, 1988]
(plus some arithmetic, for definiteness).

Applying our semantic paradigm to PCF++, we translate its programs
into PCF+ programs, essentially by inserting explicit coercion terms
wherever inheritance is used in type-checking. In anticipation of an
exact definition of this translation, here is
an example. PCF++ type-checks the program $P \equiv G(F)$ where
\begin{eqnarray*}
G & \equiv & 
    \lambda f : \{l:{\bf int}\}\rightarrow{\bf int} .\ 
\{k_1=f(\{l={\bf 0},l_1={\bf 1}\}),k_2=f(\{l={\bf 2},l_2={\bf false}\})\}\\
F & \equiv & \lambda x:\{l:{\bf int}\}.\ x.l
\end{eqnarray*}
Note that $G$ will not type-check in PCF+ because of the different types
of the two arguments to which $f$ is applied.

The translation to PCF+ depends on the way $P$ is type-checked.
One possible translation is $P' \equiv G'(F)$ where
$$G' \equiv \lambda f : \{l:{\bf int}\}\rightarrow{\bf int} . \ 
\{k_1=f(\xi_1(\{l={\bf 0},l_1={\bf 1}\})),
  k_2=f(\xi_2(\{l={\bf 2},l_2={\bf false}\}))\}$$ 
where $\xi_1$ and $\xi_2$ are the following {\em coercion terms}
$$\xi_1 \equiv \lambda x_1 : \{l:{\bf int},l_1:{\bf int}\}.\ \{l=x_1.l\} 
\;\;\;\;\;
  \xi_2 \equiv \lambda x_2 : \{l:{\bf int},l_2:{\bf bool}\}.\ \{l=x_2.l\}\ .$$
Another possible translation is $P'' \equiv G''(F)$ where
$$G'' \equiv \lambda f : \{l:{\bf int}\}\rightarrow{\bf int} . \ 
\{k_1=\zeta_1(f)(\{l={\bf 0},l_1={\bf 1}\}),
  k_2=\zeta_2(f)(\{l={\bf 2},l_2={\bf false}\})\}$$ 
where 
$$\zeta_1 \equiv 
  \lambda f_1 : \{l:{\bf int}\}\rightarrow{\bf int}.\ 
     \lambda x_1 : \{l={\bf int},l_1={\bf int}\}.\  f_1(\xi_1(x_1))$$
and
$$\zeta_2 \equiv 
  \lambda f_2 : \{l:{\bf int}\}\rightarrow{\bf int}.\ 
     \lambda x_2 : \{l={\bf int},l_2={\bf bool}\}.\  f_2(\xi_2(x_2))$$  

The fact that the translation (more generally, the meaning) depends on
the type-checking derivation entails the need for denotational
coherence results [BCGS89]. In this paper, however, we
will examine the computational (operational) aspects of this
translation. Notice that the ``execution'' of both $P'$ and $P''$
yields the same result 
$$\{k_1={\bf 0},k_2={\bf 2}\}$$ 
 More importantly, so does the direct execution of $P$.  The
``direct'' operational semantics for PCF++ that we have in mind is
just the same as that of PCF+. It is a simple but crucial observation
that the same evaluation rules work on programs allowed by the more
permissive type discipline of PCF++.  Not surprisingly, this is the
natural way to implement such languages (Luca Cardelli, personal
communication about Quest).  Although it is
probably not useful to fully translate a term before executing it, it
is reasonable to ask whether translation would affect the evaluation.
Since coercions remove the ``junk'' in a term, they may play a useful
role in efficient implementation.  However, our primary interest is in
the abstract specification of the language and not the details of its
efficient implementation.

Our {\em main result} relates the direct execution of a PCF++ program
phrase $e$ to the execution of {\em any} of its PCF+ translations, $e^*$.
We prove that
\begin{center}
$e$ terminates if and only if $e^*$ terminates.
\end{center}
If both $e$ and $e^*$ terminate, what can we say about the
relationship between the results of the two computations? Of course,
we are able to show that if the type of $e$ is {\em ground}, (integer
or boolean) then the results are the exactly the same.  In this
language we are also interested in computing with more complex
objects, such as records/variants of records/variants of ground data
(this is particularly consistent with the way things are viewed in
object-oriented database programming applications
[Ohori, Buneman, and Breazu-Tannen, SIGMOD'89]
for example).  We call the types of such data {\em observable types}.
Now, the philosophy of PCF++ is that the type of program phrases is
part of them, i.e., user-supplied in some sense.  (This is in contrast
with the approaches based on type inference; see for
example [Wand, LICS'89].) At observable types, we show that the results
of the two computations have the same {\em components} in those record
fields which appear in the prescribed type of the program phrase.
This is the best we can hope for, since the introduction of coercions
yields computations which may remove ``junk'' fields, namely the
fields not occuring in the prescribed type. Moral: if you specify a
type for your program, don't expect to observe more than what the type
allows.  Anyway, our conclusion is that coercions {\it make no
essential difference} to the computation.

In this paper, we have chosen to focus on an eager (call-by-value)
operational semantics since this is the most common style of
implementation for the languages we are studying and because it offers
a change of pace from our earlier results [BCGS89] where
we focused on models in which the unrestricted $\beta$ axiom holds.
In particular, we must avoid translating a record such as $\{l={\bf
1},k=e\}:\{l:int\}$ by simply truncating the field $k$ which is not
specified in the explicitly given type to get the record $\{l={\bf
1}\}:\{l:int\}$.  This would lead to a substantial difference between
the operational semantics of the original term and the operational
semantics of the translation in the case in which the evaluation of
the expression $e$ diverges.  Instead, we translate the judgment
$\{l={\bf 1},k=e\}:\{l:int\}$ as $\xi(\{l={\bf 1},k=e\}):\{l:int\}$
where $\xi$ is the obvious coercion of type $\{l:int,k:s\}\rightarrow
\{l:int\}$ where $s$ is the type of $e$.  Since function application
is call-by-value, the $k$ field of the record will now be evaluated
before the coercion is applied; this will yield the desired
correspondence between the operational behavior of the the translated
and untranslated terms.  We expect that results such as the ones we
are proving in this paper could be formulated for a call-by-name
operational semantics, although this would call for some changes in
our concept of observability.  An important issue is the proper
translation of eagerly evaluated records.

While the main result of this paper relates our translation to the
operational semantics, it can also be used for {\em transfer of
computational adequacy}.  Consider a denotational semantics ${\cal
D}^+$ of PCF+ for which our translation is coherent. This yields a
denotational semantics ${\cal D}^{++}$ for PCF++ where a term is
interpreted by first translating it into PCF+ and then taking the
${\cal D}^+$-meaning of the translation. Under some reasonable
assumptions about ${\cal D}^+$, our main result implies that if ${\cal
D}^+$ is computationally adequate ({\it i.e.} the meaning of a term
$e$ is non-bottom iff the evaluation of $e$ terminates) for the
operational semantics of PCF+ then ${\cal D}^{++}$ is computationally
adequate for the operational semantics of PCF++.

An interesting methodological twist is that our proof of the main
result actually uses a specific denotational semantics $[[
{\cdot}]]^+$ which is computationally adequate for PCF+ and for which
this transfer can be done! As it is, we show directly that $[[
{\cdot}]]^{++}$ is computationally adequate for PCF++ and we derive
our main result from this. We regard this as a nice example of the use
of a domain-theoretic semantics for obtaining an essentially syntactic
result.

In section 2 we begin by introducing the syntax of PCF++ as an
extension of PCF+. Then we describe the translation back, from PCF++
to PCF+. Finally we give the call-by-value operational semantics and
state our main theorem. In section 3 we give a domain-theoretic
denotational semantics of PCF+ for which our translation is coherent
and for which the operational semantics of PCF+ is sound and
computationally adequate. We prove that the operational semantics of
PCF++ is sound and computationally adequate for the induced
denotational semantics and then we show how to derive from this our
main theorem. The paper ends with a section of conclusions and ideas
for more work.

\end{document}