A Proof-Theoretic Assessment of Runtime Type Errors

AT&T Bell Laboratories Technical Memo 11261-921230-43TM

November 1993

Carl A. Gunter AT&T Bell Laboratories and the University of Pennsylvania

Didier Rémy INRIA, Rocquencourt

Abstract

We analyze the way in which a result concerning the absence of runtime type errors can be expressed when the semantics of a language is described using proof rules in what is sometimes called a natural semantics. We argue that the usual way of expressing such results has conceptual short-comings when compared with similar results for other methods of describing semantics. These short-comings are addressed through a form of operational semantics based on proof rules in what we call a partial proof semantics. A partial proof semantics represents steps of evaluation using proofs with logic variables and subgoals. Such a semantics allows a prooftheoretic expression of the absence of runtime type errors that addresses the problems with such results for natural semantics. We demonstrate that there is a close correspondence between partial proof semantics and a form of structural operational semantics that uses a grammar to describe evaluation contexts and rules for the evaluation of redexes that may appear in such contexts. Indeed, partial proof semantics can be seen as an intermediary between such a description and one using natural semantics. Our study is based on a case treatment for a language called RAVL for Records And Variants Language, which has a polymorphic type system that supports flexible programming with records and variants.

1 Runtime Type Errors in Natural Semantics

One of the primary purposes for imposing a type discipline on a programming language is to ensure the absence of certain forms of data incompatibilities that might occur at runtime in the evaluation of an ill-typed program. A characterisitic instance of such a problem occurs when a procedure call is made on an actual parameter that fails to have the proper form demanded of the formal parameter of the procedure. Such a guarantee of runtime safety can often be expressed precisely and proved rigorously for a clean language design. One of the earliest examples of such a treatment appeared in Milner’s paper [Mil78] introducing the type system that forms the basis for the Standard Meta-Language (SML) [MTH90, MT91]. Similar results have been stated and proved for many subsequent language designs involving types and semantic specifications. The goal of this paper is to study some of the relationships between various approaches to such results and use this perspective as a basis for describing a new form of operational specification for which it is possible to provide a proof-theoretic expression of the guarantees obtained from the type correctness of a program.

A paper by Wright and Felleisen [WF91], which surveys some of the literature on results about runtime type errors, can be taken as a background for our discussion in this paper, which focuses on the form of such results for a semantics like the one given for the SML in [MTH90]. The term natural semantics is sometimes used for this form of specification, which is based on rules that look like those of natural deduction (see the survey in [Gun91] for further discussion). For example, the following natural semantics rules describe call-by-value evaluation and the evaluation of local definitions (‘let’ bindings):

\overline{fun x M ↓ fun x M}  (Arrow)

\frac{M ↓ fun x L  N ↓ V  [V/x]L ↓ U}{M N ↓ U}  (App)

\frac{M ↓ V  [V/x]N ↓ U}{let x = M in N ↓ U}  (Let)

Basic judgements have the form M ↓ U where M is a term (program) and U is a value (typically defined as a term in a normal form) where U is to be viewed as the result of evaluating M. This binary relation is defined to be the least relation satisfying a collection of rules such as those above. For example, the App rule can be viewed as asserting that the result of applying M to N is U provided three other judgments hold: M evaluates to a value fun x L and N to a value V such that the result [V/x]L of substituting V for x in L evaluates to U. For sequential languages specified in this way it is possible to show that if M ↓ U and M ↓ V, then U and V are the same.

Given a semantics expressed in this form, a theorem about runtime type errors can be expressed by providing rules illustrating when such errors arise and showing that type-correct programs do not raise type errors (this approach is used in [ACPP91] for example). Such rules have two forms that might be termed error origination and propogation rules. Here are typical examples:

\frac{M ↓ U  U is not a procedure}{M N ↓ error}  (ErrOrig)

\frac{M ↓ fun x L  N ↓ error}{M N ↓ error}  (ErrProp)

where error is a distinguished value which does not have a type. The rule ErrOrig indicates that an error is raised (originated) if the operator M in an application M N is evaluated to a term that fails to have the form M ↓ fun x L for some L. The rule ErrProp indicates that if the evaluation of an argument of a procedure raises an error, then the application also raises (propogates) an error. One proves that a type-correct program does not raise a runtime error by showing that subject reduction holds: that is, if M ↓ U and M has type σ, then U also has type σ. From this it follows that U is not error because error cannot have type σ.

Although this approach does directly express the errors that are being avoided due to the type correctness of a program, it does so in an ad hoc manner. To see what we mean by this, note that the particular choice of error rules determines exactly what the theorem indicating the absence of runtime errors actually means. For example, the rule

\frac{N ↓ error}{M N ↓ error}  (ErrProp-1)

is not a consequence of ErrProp and adding it would therefore result in a stronger theorem asserting that a type-correct program does not evaluate to error.^{1} In formulating an assertion about what runtime errors are avoided as a result of type correctness, attention must therefore be paid to whether important origination or propogation rules may have been omitted; it is unclear how such rules could be chosen mechanically. Similar decisions must also be made in the kind of semantic formulation used by Milner [Mil78] and others.

This can be contrasted with the kind of result one may assert when a structural operational semantics (SOS) is used to describe the operational semantics of programs. Under such a semantics, there is a sequence of steps of evaluation (transitions)

M → M_{1} → ⋯ → M_{n}

and M is said to evaluate to M_{n} just in case M_{n} is a value (one also shows that if U is a value, then there is no N such that U → N). In such a formulation, a theorem asserting that type correct programs do not have runtime type errors says that if a sequence of relations such as those above holds and M is type correct, then either M_{n} → M_{n+1} for some term M_{n+1}, or M_{n} is a value. This means that either the evaluation sequence can be extended, or it cannot be extended and the last term in the sequence is a normal form. In this way one rules out, for example, the possibility that M_{n} has the form V L where V is a value that is not a procedure because M_{n} would then be a non-value to which no rule applies.

Intuitively, type correctness of a term under a natural semantics assures that there is some rule that can be applied to the term in searching for the value to which it evaluates. More generally, if we are given a term M and a search is made for a proof of a proposition M ↓ U for some value U, then an analogy with SOS suggests that the type correctness of M implies that the proof search is never ‘blocked’ on any of its subgoals. In the remaining sections of this paper we describe how this can be viewed as the proper analogy to the case for a transition system by formalizing the sense in which the search for a proof in natural semantics is like a transition semantics on ‘partially completed’ proofs, in a system we call a partial proof semantics. The absence of runtime type errors in this setting is then described proof-theoretically by saying that a (legitimately formed) partial proof of the evaluation of a well-typed program M is either total (that is, a proof that M has a value U) or it can be developed further by applying additional proof steps to its subgoals. We will illustrate how partial proof semantics can be viewed as an intermediary between natural semantics—with which it shares the characteristic that computation is viewed as the search for a proof—and a form of SOS that is defined by combining rules for the reduction of redexes with a grammar for evaluation contexts.

Our treatment of partial proof semantics is done through a case illustration based on a language called RAVL, which has a polymorphic type system that supports flexible programming with records and variants. This language is typical of new language proposals for which the absence of runtime type errors is a key design issue. In RAVL, as in most similar languages for record calculi, the type system is intended to ensure that a type-correct field selection from a record does not raise a runtime error due to the absence of the field and ensure that a case analysis of a variant value covers all of its possible cases.

1This rule also has the operational significance that an error is reported even if the evaluation of the operator M diverges. If a similar propogation rule for the operator M is given, then the operational semantics for programs would appear to be non-sequential.

2 RAVL: A Language for Programming with Records and Variants

There has been considerable interest in developing programming languages with strong static typechecking that provide a better treatment of programming with records than languages developed in the 1970’s. Seminal research of John Reynolds [Rey80] and Luca Cardelli [Car84, Car88] showed a way to achieve this to a substantial degree using a subtyping relation on types. A more recent paper of Mitchell Wand [Wan87] proposed another pleasing calculus for the manipulation of records. His system used parametric polymorphism and the concept of a row variable to provide the desired flexibility and also offered the prospect of type inference. Subsequently there have been several proposals for similar systems including the Machiavelli language of Atsushi Ohori [OBBT89], the system of Didier Rémy [Rém89] and the ML^{++} language of Jategaonkar and Mitchell [JM88]. RAVL, the language introduced in this paper, is similar to languages studied in [Rém89, Rém90, Rém93].

The new language is the Records And Variants Language—RAVL. Some of the basic design goals of RAVL can be summarized as follows:

1. RAVL is ‘upwards compatible’ with the functional core fragment of ML,

2. RAVL has a statically inferred polymorphic typing system,

3. type safety properties of RAVL are similar to those that hold for ML,

4. RAVL provides intuitive and flexible constructs for the manipulation of records and variants.

As presented in this paper, RAVL is a theoretical language in the spirit of languages such as the those studied by Cardelli and Milner. Nevertheless, RAVL can be implemented efficiently and we believe that an acceptable concrete syntax for it is also possible.

Syntax of types and terms.

We are given a collection of symbols L called labels which will be used as tags (in variants) and field names (in records). We use the symbols a and b for labels and L for finite sets of labels. The typing system of RAVL is composed of four syntax classes: types, rows, attendances, and schemes. The symbols used for the syntax classes can be summarized as follows:

• σ and τ range over types and α, β, γ over type variables,

• ρ^{L} ranges over rows and π^{L} over row variables,

• φ and ψ range over attendances and χ over attendance variables.

Types are defined inductively, based on a given collection F_{1}, ..., F_{n} of operators. These operators have a signature indicating the number of arguments of each operator and the sorts of the arguments, where sorts are of types, rows and attendances.

• a type variable α is a type expression,

• σ → τ is a type expression if σ and τ are type expressions,

• Πρ^{∅} is a type expression, • Σρ^{∅} is a type expression,

• F_{i}(σ̄_{i}, ρ̄_{i}, φ̄_{i}) is a type expression where F_{i} is a type operator taking type arguments σ̄, row

arguments ρ̄, and attendance arguments φ̄ where

σ̄_{i} ≡ σ_{1}, …, σ_{l_{i}} and ρ̄_{i} ≡ ρ_{1}, …, ρ_{m_{i}} and φ̄_{i} ≡ φ_{1}, …, φ_{n_{i}}

Rows have the following definition:

• a row variable π^{L} is a row,

• abs^{L} is a row,

• a: φ; ρ^{L∪{a}} is a row if a ∉ L, φ is an attendance and π^{L} is a row. Attendances have the following definition:

• an attendance variable χ is an attendance,

• abs is an attendance,

• pre(σ) is an attendance if σ is a type.

The definition of RAVL is relative to a given collection of recursive type equations:

F_{1}(ᾱ_{1}, π̄_{1}, χ̄_{1})  = F_{1}(ᾱ_{1}, π̄_{1}, χ̄_{1})
⋮
F_{m}(ᾱ_{m}, π̄_{m}, χ̄_{m}) = F_{m}(ᾱ_{m}, π̄_{m}, χ̄_{m})

where F_{i}(ᾱ_{i}, π̄_{i}, χ̄_{i}) is a type whose free variables lie among ᾱ_{i}, π̄_{i}, χ̄_{i}. We write F_{i}(σ̄_{i}, ρ̄_{i}, φ̄_{i}) for the type obtained by simultaneously substituting types σ̄_{i}, ρ̄_{i}, φ̄_{i} for variables ᾱ_{i}, π̄_{i}, χ̄_{i} respectively in this expression. As usual, a type scheme is either a type or a quantified variable followed by a type scheme. The syntax of types is summarized in a pseudo-BNF grammar in Table 1.

Table 1: Syntax of RAVL types

σ ::= α | σ → σ | Πρ^{∅} | Σρ^{∅} | F_{i}(σ_{i}, r0_{i}, f0_{i})
ρ^{L} ::= π^{L} | abs^{L} | a: φ; ρ^{L∪{a}}  a ∉ L
φ ::= χ | abs | pre(σ)
s ::= σ | ∀ α. s | ∀ χ. s | ∀ π. s

The rows are defined by a rule scheme in which L can be instantiated by any finite set of labels. Because of the labels, the grammar for the language is context sensitive. The superscripts in row expressions are intended to exclude expressions such as Π (a: χ; a: χ′; π^{L}) in which a field is defined twice or Π (a: χ; π^{L}) → Π (π^{L}) in which L must be both ∅ and {a}. All occurrences of a given row variable should be preceded by the same set of labels (possibly in various different orders). The labels on the inside of a row can be omitted when the outermost superscript is given.

In particular, this is the case for any row expression embedded in a type expression. Hence it will be convenient to write Π (a: χ; π), for example, rather than writing Π (a: χ; π^{{a}}). Another way of expressing the rules concerning the formation of such expressions is to treat the types as a sorted algebra as in [Rém93]. Expressions for rows are taken modulo left commutativity,

(a: φ; b: ψ; ρ^{({a,b}∪L)}) = (b: ψ; a: φ; ρ^{({a,b}∪L)})

and distributivity,

abs^{L} = (a: abs ; abs^{L∪{a}})

Ordinarily we omit the labels on such expressions and write,

(a: φ; b: ψ; ρ) = (b: ψ; a: φ; ρ)

and abs = a: abs ; abs

The language of expressions is defined by the BNF grammar in Table 2. The typing judgments

Table 2: Syntax of RAVL terms.

M ::= x | fun x M | M M | let x = M in M | intro [F_{i}] M | elim [F_{i}] M
| {} | {M with a = M} | M \ a | M.a
| a tag M | lastcase M of a tag x ⇒ M | case M of a tag x ⇒ M else x ⇒ M

have the form H ⊢ M : s where H is a list of assertions x : s. The full list of rules is given in Appendix A. The rules listed there fall into three groups. First of all, there are the rules for the Damas-Milner type inference of ML. Second there are rules for the MacQueen-Sethi treatment of recursive types using introduction and elimination constructors. And third there are rules for records and variants that are special to RAVL.

Although RAVL is more expressive than ML, it is still possible to perform ML-style type inference on terms. We omit details here; the result can be obtained from arguments in [Rém93] and [Rém90].

Natural semantics.

A natural semantics presents the evaluation of a language through a set of rules for inferring a binary relation between programs and values. This is often an intuitive and flexible way to describe an abstract evaluator for a language; in particular, such rules were used to provide the formal definition of the ML Standard [MTH90]. We now sketch how one might describe a natural semantics for RAVL. The goal is to define a binary relation M ↓ U between terms M and a special class of terms U called values. Values are defined by the grammar in Table 3. We indicated in the right column the name of the set of values of the corresponding shape. Letters U, V and W range over values.

Table 3: Syntax of values

U ::= A | I | R | B  normal values  U
A ::= fun x M  function values A
I ::= intro [F] U intro values I
R ::= {} | {R with a = U} record values  R
B ::= a tag U  variant values  B

The (non-error) rules given in the first section can be taken as rules for the semantics of RAVL. Some further examples for the record part of the language would look as follows:

\frac{M ↓ \{R with a = U\}}{M.a ↓ U}  (Project-1)

\frac{M ↓ \{R with b = V \}  R.a ↓ U}{M.a ↓ U}  (Project-2)

\frac{M ↓ R  N ↓ U}{\{M with a = N\} ↓ \{R with a = U\}}  (Extend)

3 Type Errors and SOS

As mentioned earlier, it is possible to formulate a good theorem concerning the absence of runtime errors for a transition semantics of the right kind. Let us now look at an SOS for RAVL in the style urged by Wright and Felleisen [WF91]. It can be seen as an instance of term rewriting in which a grammar of evaluation contexts is used to control the order in which redexes in a term are to be reduced. For RAVL, the evaluation contexts are listed in Table 4. (Our evaluation contexts are slightly more general than left-to-right or right-to-left evaluation of application, but they do describe call-by-value evaluation.) The SOS of RAVL is obtained by connecting these evaluation contexts with reduction rules for redexes as given in Table 5 via the following rule:

\frac{M ⟶ N}{E[M] ⟶ E[N]}

which asserts that a term M′ evaluates to N′ (in one step) if there is an evaluation context E such that M′, N′ have the forms E[M], E[N] respectively for terms M and N such that M ⟶ N.

It is possible to show that the resulting reduction system is deterministic in the following sense. Suppose ⟶^{∗} is the transitive closure of ⟶.

Theorem 1 If M ⟶^{∗} U and M ⟶^{∗} V for values U and V, then U and V are the same (up to renaming of bound variables).

This result is proved by demonstrating local confluence. (The result is not difficult because evaluation contexts cannot be ‘embedded’ within one another.) The following theorem states precisely the desired property.

Theorem 2 If ⊢ M : σ and M ⟶^{∗} N and there is no term N′ such that N ⟶ N′, then N is a value.

Table 4: Evaluation Contexts

E ::= [ ]
| E M | M E | let x = E in M | intro [F_{i}] E | elim [F_{i}] E
| {E with a = M} | {M with a = E} | E \ a | E.a
| a tag E | case E of a tag x ⇒ M else x ⇒ M | lastcase E of a tag x ⇒ M

Table 5: Redex Rules

(fun x M) V ⟶[V/x]M
let x = V in M ⟶[V/x]M
elim [F_{i}] intro [F_{i}] V ⟶ V
{V with a = U}.a ⟶ U
{V with b = U}.a ⟶ V.a
{V with a = U} \ a ⟶ V
{V with b = U} \ a ⟶{V \ a with b = U}
case a tag V of a tag x ⇒ M else y ⇒ N ⟶[V/x]M
case b tag V of a tag x ⇒ M else y ⇒ N ⟶[V/y]N
lastcase a tag V of a tag x ⇒ M ⟶[V/x]M

It can be viewed as a guarantee of safety from runtime errors of type correct programs and proved by demonstrating that subject reduction holds.

The more reduction contexts are permitted the stronger the Subject Reduction Lemma is, since safe evaluation is an easy consequence of the reduction lemma. Thus it is interesting to prove the subject reduction for a general semantics, even a non-deterministic one: the result for any deterministic semantics is then obtained by restricting the evaluation contexts will be a corollary, and the safe evaluation theorem will follow easily. For RAVL, we could have proved the subject reduction lemma for the full calculus where all contexts are admissible.

4 Partial Proof Semantics

Let us turn now to the question of how a result such as 2 can be expressed for a system based on proof rules (as opposed to transitions). To get the intuition for what we will capture rigorously, consider how one might calculate the result of evaluating a program in a language described using natural semantics. If, for example, an application M N is to be evaluated, then the last step of the evaluation may come from an application of the rule App. This means that it is necessary to calculate the values of M and N, then combine these into a term obtained from a substitution involving these values, and then evaluate this term. The calculation therefore involves a subgoal M ↓ X where X is a variable whose value must be found, and a subgoal N ↓ Y. This essentially corresponds to the clause in the grammar for evaluation contexts (given in Table 4) of the form E ::= ⋯ | E M | M E | ⋯ Once values have been found for X and Y, we may view the situation as that of a redex analogous to the β-reduction rule at the beginning of Table 5. In the semantics we are about to describe, there are two relations written M ↓ u and M ⇓ u. The first of these is analogous to the clauses of the grammar for evaluation in SOS, and we call the rules that apply to it search rules. The second is analogous to the rules for redex reduction in SOS and we call these the redex rules. There are some rules for how the search and redex rules are combined. We call this style of semantic description a Partial Proof Semantics (PPS).

As an example, let us consider the rules associated with application in a partial proof semantics for RAVL. Here are the search and redex rules respectively:

\frac{M ↓ v  N ↓ w  v w ⇓ u}{M N ↓ u}  (App-S)

\frac{[V/x]M ↓ u}{(fun x M) V ⇓ u}  (App-R)

The variables u, v, w range over a syntax class of partial values that consists either of values U (as given by the grammar in Table 3) or logic variables X. The idea being that a logic variable represents an unknown value which will be determined through the resolution of subgoals of the proof. A rule of the form

\overline{V ⇓ V}  (Value)

indicates that a value is related to itself. Two additional rules apply to the formation of subgoals, which are leaves of a partial evaluation tree in which the result of evaluation is a variable:

\overline{M ↓ X}  \overline{M ⇓ X}  (Subgoal)

The full set of PPS rules for RAVL is given in the appendix. Some definitions are needed to make the rules clear. The grammar of terms for RAVL is expanded to include a new syntax class of logic variables which are denoted by X, Y, Z. Here is an example of a program in the expanded grammar

{X with a = Y }

A term with no logic variables is said to be a total program; these are the ones whose semantics particularly interests us. Similarly, let us refer to values as defined in Table 3 as total values. Recall that letters U, V and W range over total values. As in the table, letters such as A, I, R, B range over specific shapes of values. It can be shown that types and values match with one another: values of function types are function values, values of recursive types are intro values, and so on. Logic variables are drawn from a new syntax class; letters X, Y and Z range over logic variables. A Partial value is a total value or logic variable:

u ::= X | U

Total values are partial values that do not contain any logic variables.

A partial proof is viewed as a way of representing intermediate steps in the search for a proof ▽ of a relation of the form M ⇓ V where ▽ has no logic variables. A proof is said to be total if it has no logic variables; otherwise it is said to be partial. It can be shown that the conclusion of a proof ▽ has the form M ↓ V or M ⇓ U where U is a total value if, and only if, ▽ has no logic variables. A subgoal is a leaf of the form M ↓ X or M ⇓ X where M is total; it can also be shown that a proof has subgoals if, and only if, it has logic variables. In PPS, the search for a proof can be viewed as a sequence of proofs:

▽_{1} ⟶ ▽_{2} ⟶ ⋯ ⟶ ▽_{n}

where ▽_{1} is a partial proof of the form

\overline{M ⇓ X}

and each ▽_{i+1} can be obtained by resolving or extending subgoals in ▽_{i}. The search is to be viewed as complete (terminated) if the proof ▽_{n} is total; its conclusion will have the form M ⇓ U where U is a (total) value.

Some examples may help to illustrate the idea. The following is a partial proof with two logic variables:

\frac{\{\{\} with a = fun x x\} ↓ X X.a ⇓ Y}{\{\{\} with a = fun x x\}.a ↓ Y}

A refinement of this partial proof can be obtained by carrying out further steps on the left subgoal:

\frac{▽ \{\{\} with a = fun x x\}.a ⇓ Y}{\{\{\} with a = fun x x\}.a ↓ Y}

where ▽ is

\frac{\{\} ↓ \{\} fun x x ↓ fun x x \{\{\} with a = fun x x\} ⇓ \{\{\} with a = fun x x\}}{\{\{\} with a = fun x x\} ↓ \{\{\} with a = fun x x\}}

When the logic variable Y is replaced by the total value fun x x in accordance with redex rule Project-R-1, then the proof becomes total.

By constrast, let us consider the search for a proof of a program that is not type correct. The first step in the partial evaluation of {} (fun x x) is the following partial proof:

\frac{\{\} ↓ X  fun x x ↓ Y  X Y ⇓ Z}{M N ↓ Z}

This can be extended to:

\frac{\{\} ↓ \{\}  fun x x ↓ fun x x  \{\} (fun x x) ⇓ Z}{M N ↓ Z}

Although this proof is not total, its remaining subgoal does not match any of the rules; there is no way of refining further to a total proof or even continuing the effort to resolve the subgoal. The theorem asserting absence of runtime errors for PPS says that this situation does not occur for type-correct programs.

Some care must be taken about the names of logic variables in subgoals when stating the desired result about the resolution of subgoals in a partial proof involving a type-correct program. There is a problem that can occur if the same variable is used in two different subgoals. For example, a partial proof that has the form

\frac{M ↓ X  N ↓ X  X X ⇓ Z}{M N ↓ Z}

is an instance of APP-S, but an unwanted connection is made between the results of evaluating M and N. A simple technical restriction resolves this problem. A partial proof is said to be linear if the logic variables appearing in its subgoals are all distinct. Putting this another way, linear proofs are those in which each logic variable appears in exactly one subgoal. The following lemmas and theorem now express the desired conclusion in a manner similar to that used for SOS.

Lemma 1 (Confluence) Let M be a RAVL term and suppose tere are proofs

\frac{▽}{M ↓ U} \frac{^{▽′}}{M ↓ U′} ,

Then U = U′ and ▽ = ▽′.

This is stronger in some sense that the equivalent lemma for SOS approach, since the proofs are also identified. Different choices of reduction order are expressed as different ways in which parts of the proof are completed. Local confluence could be proved for the full calculus, but the proof would be more difficult than that for SOS since redexes can be embbeded. Local confluence and determinism are not required for type safety, but they are useful properties of the semantics. The operational semantics of RAVL does not specifiy the order of evaluation between the argument and the function, but the Confluence Lemma says it is still deterministic. For languages with states or concurrency, leaving the order of evaluation unspecified would make the semantics nondeterministic: a program in such a language could return several answers.

The two central results are the following:

Lemma 2 (Subject reduction) If M : σ and \frac{▽}{M ↓ u}, then all of the total programs in ▽ are

well-typed. Also, if u is total, then u : σ.

Theorem 3 (Safe evaluation) Suppose ⊢ M : σ and \frac{▽}{M ↓ u} is linear. If there is no ▽′ that

extends ▽ such that \frac{^{▽′}}{M : u′} , then ▽ is total (which implies that u is also total).

5 Discussion and Acknowledgements

Of course, it can be shown that the SOS and PPS specifications of RAVL are equivalent. The primary difference between them is that PPS rules derive an evaluation relation while SOS describes the evaluation relation as the transitive closure of the ‘redex reduction’ relation. It is possible to modify the SOS description so that rules are used to serve the role of evaluation contexts. For example, the following pair of rules would suffice in place of the clause E ::= ⋯ | E M | M E | ⋯ from Table 4:

\frac{M ⟶ M′}{M N ⟶ M′ N}  \frac{N ⟶ N′}{M N ⟶ M N′}

The resulting formulation would then be more like the ones in [Plo81]; the connection between SOS rules and those of PPS would be less clear, however.

The primary significance of PPS comes from the ability to express intermediate stages in the search for a proof of an evaluation relation M ⇓ U. PPS proofs are similar in spirit to the goal stack structures in goal-directed theorem proving; they differ in allowing only a very restricted form of proposition and in the fact that the theorem to be proved is not known before the proof is complete (because the result of evaluation is constructed along with the proof). Ideally we would have prefered to retain the natural semantics rules and simply introduce logic variables and subgoals for them, but technical difficulties force the distinction between search and redex rules. To see where the problem arises, suppose we had expressed the App-S as follows:

\frac{M ↓ v  N ↓ w  v w ↓ u}{M N ↓ u}  (App-S’)

Then the same rule would again be applicable to its right-most hypothesis v w ↓ u allowing an infinite regress of partial resolutions of the application into subgoals. This would permit an infinite proof search that does not arise from a divergent evaluation and invalidate the property that a total proofs are uniquely determined by their conclusions.

Some of the basic ideas in PPS have appeared in other work on programming languages and their semantics. A paper by Howe [How91] studies the meta-theory of natural semantic proofs. His work includes the notion of a logic variables in natural semantics and the linearity restriction. Howe also makes a restriction on proof search that has basically the same effect as our use of two relations ↓ and ⇓. A somewhat similar idea is embodied in logic programming constructs such as the freeze, constrain, and in wait declarations [Nai85]. These constructs restrain the use of a clause until logic variables have been instantiated.

What is the merit of PPS relative to the other approaches to the semantics of programming languages? We have stressed that PPS provides a link between natural semantics and SOS for RAVL, but more work will be necessary to determine its robustness as a specification technique for other kinds of languages. For example, the presentation of SOS using evaluation contexts is convenient for describing the semantics of control features: does PPS share or lack this property? What about the semantics of state or concurrency? These are questions that will occupy our future investigations of PPS as a specification formalism.

We would like to acknowledge some remarks of Val Breazu-Tannen that inspired us to think about the problem of expressing freedom from runtime errors in natural semantics style and useful conversations with Amy Felty, Elsa Gunter, Doug Howe, Myra VanInwegen, Xavier Leroy, Luc Maranget, and Fernando Pereira. Gunter’s research was partially supported by NSF grant INT-8819598 and by an ONR Young Investigator grant.

References

[ACPP91] M. Abadi, L. Cardelli, B. Pierce, and G. D. Plotkin. Dynamic typing in a statically typed language. Transactions on Programming Languages and Systems, 13(2):237– 268, April 1991. Preliminary version in Proceedings of the Sixteenth Annual ACM Symposium on Principles of Programming Languages (Austin, TX), January, 1989.

[Car84] L. Cardelli. A semantics of multiple inheritance. In G. Kahn, D. B. MacQueen, and G. D. Plotkin, editors, Semantics of Data Types, pages 51–67. Lecture Notes in Computer Science vol. 173, Springer, 1984.

[Car88] L. Cardelli. A semantics of multiple inheritance. Information and Computation, 76:138– 164, 1988.

[Gun91] C. A. Gunter. Forms of semantic specification. Bulletin of the European Association for Theoretical Computer Science, 45:98–113, 1991.

[How91] Douglas J. Howe. On computational open-endedness in Martin-Löf’s type theory. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science, pages 162– 172. IEEE Computer Society, 1991.

[JM88] L. Jategaonkar and J. C. Mitchell. ML with extended pattern matching and subtypes. In R. Cartwright, editor, Symposium on LISP and Functional Programming, pages 198– 211. ACM, 1988.

[Mil78] R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, 1978.

[MT91] R. Milner and M. Tofte. Commentary on Standard ML. The MIT Press, 1991.

[MTH90] R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. The MIT Press, 1990.

[Nai85] L. Naish. Negation and Control in Prolog, volume 238 of Lecture Notes in Computer Science. Springer, 1985.

[OBBT89] A. Ohori, P. Buneman, and V. Breazu-Tannen. Datbase programming in Machiavelli — a polymorphic language with static type inference. In SIGMOD Conference on the Management of Data, pages 46–57. ACM, 1989.

[Plo81] G. D. Plotkin. A structural approach to operational semantics. Technical Report FN-19, Computer Science Department, Aarhus University, Ny Munkegade—DK 8000 Aarhus C—Denmark, 1981.

[Rém89] Didier Rémy. Records and variants as a natural extension of ML. In Sixteenth Annual Symposium on Principles Of Programming Languages, 1989.

[Rém90] Didier Rémy. Algèbres Touffues. Application au Typage Polymorphe des Objects Enregistrements dans les Langages Fonctionnels. Thèse de doctorat, Université de Paris 7, 1990.

[Rém93] Didier Rémy. Type inference for records in a natural extension of ML. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects Of Object-Oriented Programming. Types, Semantics and Language Design. MIT Press, 1993.

[Rey80] J. C. Reynolds. Using category theory to design implicit conversions and generic operators. In N. D. Jones, editor, Semantics-Directed Compiler Generation, pages 211–258. Lecture Notes in Computer Science vol. 94, Springer, 1980.

[Wan87] Mitchell Wand. Complete type inference for simple objects. In D. Gries, editor, Second Symposium on Logic In Computer Science, pages 207–276, Ithaca, New York, June 1987. IEEE Computer Society Press.

[WF91] A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Technical Report COMP TR91-160, Department of Computer, Rice University, 1991.

A Typing Rules for RAVL

\frac{H ⊢ M : s}{H ⊢ M : ∀ α. s}  \frac{H ⊢ M : s}{H ⊢ M : ∀ χ. s}  \frac{H ⊢ M : s}{H ⊢ M : ∀ π. s}  (All-Intro) α, χ, π ∉ H
\frac{H ⊢ M : ∀ α. s}{H ⊢ M : [σ/α]s}  \frac{H ⊢ M : ∀ χ. s}{H ⊢ M : [φ/χ]s}  \frac{H ⊢ M : ∀ π. s}{H ⊢ M : [ρ/π]s}  (All-Elim)
\overline{(Var)} ; H ⊢ x : H(x)  H[x : σ] ⊢ M : τ ; \overline{(Fun)} ; H ⊢ fun x M : σ → τ  H ⊢ M : σ → τ  H ⊢ N : σ ; \overline{(App)} ; H ⊢ M N : τ

H ⊢ M : s H[x : s] ⊢ N : σ \overline{(Let)}

H ⊢ let x = M in N : σ

H ⊢ M : σ σ = τ ; \overline{(Equal)} ; H ⊢ M : τ

H ⊢ M : F_{i}(σ̄_{i}, ρ̄_{i}, φ̄_{i}) \overline{(Rec-I)}

H ⊢ intro [F_{i}] M : F_{i}(σ̄_{i}, ρ̄_{i}, φ̄_{i})

H ⊢ M : F_{i}(σ̄_{i}, ρ̄_{i}, φ̄_{i}) \overline{(Rec-E)}

H ⊢ elim [F_{i}] M : F_{i}(σ̄_{i}, ρ̄_{i}, φ̄_{i})

\overline{(Empty)}

H ⊢ {} : Π (abs)

H ⊢ M : Π (a: abs ; ρ) H ⊢ N : σ
\overline{(Extend)}
H ⊢ {M with a = N} : Π (a: pre(σ) ; ρ)

H ⊢ M : Π (a: σ; ρ)

\overline{(Restrict)}

H ⊢ M \ a : Π (a: abs ; ρ)

H ⊢ M : Π (a: pre(σ) ; ρ)
\overline{(Project)}
H ⊢ M.a : σ

H ⊢ M : σ \overline{(Tag)}

H ⊢ a tag M : Σ(a: pre(σ) ; ρ)

H ⊢ L : Σ(a: pre(σ) ; abs) H[x : σ] ⊢ M : τ
\overline{(Lastcase)}
H ⊢ lastcase L of a tag x ⇒ M : τ

H ⊢ L : Σ(a: pre(σ) ; ρ) H[x : σ] ⊢ M : τ H[y : Σ(a: φ; ρ)] ⊢ N : τ

\overline{(Case)}
H ⊢ case L of a tag x ⇒ M else y ⇒ N : τ

B Partial Proof Semantics for RAVL

B.1 Search rules

fun x M ⇓ w ; \overline{(Fun-S)} ; fun x M ↓ w M ↓ v  N ↓ w  v w ⇓ u ; \overline{(App-S)} ; M N ↓ u M ↓ v let x = v in N ⇓ u \overline{(Let-S)}

let x = M in N ↓ u

M ↓ v intro [F_{i}] v ⇓ w

\overline{(Intro-S)}

intro [F_{i}] M ↓ w

M ↓ v elim [F_{i}] v ⇓ u \overline{(Elim-S)}

elim [F_{i}] M ↓ u

\{\} ⇓ w ; \overline{(Empty-S)} ; \{\} ↓ w M ↓ u  N ↓ v  {u with a = v} ⇓ w \overline{(Extend-S)}

{M with a = N} ↓ w

M ↓ v v \ a ⇓ u

(Restrict-S)

M \ a ↓ u

M ↓ v v.a ⇓ u \overline{(Project-S)}

M.a ↓ u

M ↓ v a tag v ⇓ w \overline{(Tag-S)}

a tag M ↓ w

L ↓ v case v of a tag x ⇒ M else y ⇒ N ⇓ u
\overline{(Case-S)}
case L of a tag x ⇒ M else y ⇒ N ↓ u
L ↓ v lastcase v of a tag x ⇒ M ⇓ u

(Lastcase-S)

lastcase L of a tag x ⇒ M ↓ u

B.2 Redex rules

[V/x]M ↓ u ; \overline{(App-R)} ; (fun x M) V ⇓ u [V/x]M ↓ u \overline{(Let-R)}

let x = V in M ⇓ u

\overline{(Elim-R)}

elim [F_{i}] (intro [F_{i}] U) ⇓ U

{V with a = U}.a ⇓ U

V.a ⇓ u

(Project-R)

{V with b = U}.a ⇓ u

{} \ a ⇓ {} {V with a = U} \ a ⇓ V

V \ a ⇓ v {v with b = U} ⇓ w

(Restrict-R)

{V with b = U} \ a ⇓ w

\frac{[V/x]M ↓ u}{case a tag V of a tag x ⇒ M else y ⇒ N ⇓ u} (Case-R)

a ≠ b

\frac{[b tag V/y]N ↓ u}{case b tag V of a tag x ⇒ M else y ⇒ N ⇓ u} \frac{[V/x]M ↓ u}{lastcase a tag V of a tag x ⇒ M ⇓ u} (Lastcase-R)

B.3 Other rules

\overline{(Subgoal-S)} ; M ↓ X

(Subgoal-R) M ⇓ X

\overline{(Value)} ; V ⇓ V