Simply-typed Underdeterminism

Ewen Denney^{∗}

LFCS, Department of Computer Science, University of Edinburgh Kings Buildings, Edinburgh EH9 3JZ, Scotland

                        Email : ewd@dcs.ed.ac.uk

February 26, 1998

Abstract We study an extension of the simply-typed lambda calculus with constructs for expressing a notion we call underdeterminism. This allows us to interpret notions of stub and skeleton used in top-down program development. We axiomatise a simple notion of program refinement, and give a semantics, for which the calculus is proved sound and complete.

1 Introduction

When programmers write programs they often use a mixture of top-down and bottom-up development. Central to the method of top-down development is the idea of a stub. Suppose we are writing some program, the main body of which needs to use a sorting function on lists. We prefer to get the structure of the main body correct first before writing the sorting function, but in order to get the program to compile, or even to type-check, we must at least declare the sorting function, and give it a dummy body — a stub.

                                   fun Sort l = nil;

Any use of the function elsewhere is now well-defined

                                  l′ = Sort some list;

Conceptually, however, it is inelegant to use dummy code. Practically, although the program will compile and will run, the programmer must always bear in mind that this is not ‘true’ code. When testing the behaviour of the partially written program this must be taken into account. One way of avoiding this would be to use some kind of error, or exception mechanism as a stub. This is not entirely satisfactory however, since the programmer might forget that various stubs are left throughout the program. It would be better to have a language construct that allows the programmer to write what we might call true stubs. The sorting function would be written as

                                  fun Sort l =?_{int list};

The idea is that ?_{int list} stands for some unwritten code of type int list. This can then be typechecked and the system would give a warning message to the effect that certain lines of code still remain to be implemented. We would like to be able to compile and run such partially written programs. In general, this is not possible since our program might just be one big stub. However, we would like an understanding of programs with stubs which lets us do this whenever possible.

∗Research supported by a grant from the Engineering and Physical Sciences Research Council

A similar concept used in program development is that of program skeletons. These are templates of code expressing useful algorithm schemes, such as divide-and-conquer. Using the ?_{τ} construct, it is possible to define a simple notion of skeleton^{1} within the language, rather than as some kind of metaentity. As explained below, we cannot in general express stubs and skeletons using parameterisation, since parameters cannot range over code which can contain local variables.

In this paper, we study an extension of the simply-typed lambda calculus, λ^{×→}, with constructs ?_{τ} for each type τ, giving a calculus λ_{?}. We give an equational theory for λ_{?} and we study the natural notion of refinement induced by this.

We can compile pure functional programming languages into the simply-typed lambda calculus and, similarly, can compile a language with true stubs into λ_{?}. The theory of λ_{?} could be used to prove the correctness of transformations carried out by a compiler.

It is possible to extend the calculus to a full refinement calculus, in which stubs contain logical assumptions. An equational theory is also necessary in order to give a full program logic for this extended language. This is carried out in the author’s forthcoming PhD thesis. However, we believe it is worthwhile to study this simpler system, for both theoretical interest and for the practical applications described above.

2 Overview

We introduce an extension of the simply-typed lambda calculus (λ^{×→}) with constructs for expressing a notion we call underdeterminism. Consider the term λx : σ.⟨2, x⟩ of type σ → nat × σ. This term is determined in the sense that we have complete knowledge about it. Suppose now, we know that some term of the same type always returns pairs of which the left component is 2, but we know nothing about the right component. We might write this as λx : σ.⟨2,?_{σ}⟩, where ?_{σ} means ‘some term of type σ’. We allow ?_{σ} to stand for any subterm which is well-formed in the local context, so these unknowns can contain the variable x. This is in contrast to the use of variables as indeterminates. If, instead of the stub ?_{σ}, we use a free variable y of type σ as a parameter, writing the above term as λx : σ.⟨2, y⟩, then we can substitute any term for y which is well-formed in the global context. The point is, though, that because of variable capture, we cannot substitute x to get λx : σ.⟨2, x⟩. This, of course, is crucial to the use of stubs.

Now, a less determined term would be λx : σ.⟨?_{nat},?_{σ}⟩. This is a term of type σ → (nat × σ) which returns … what? Evaluation does not make sense in general for such partially constructed terms anyway, but our intuition tells us that the term λx : σ.⟨?_{nat},?_{σ}⟩ carries the same information as λx : σ.?_{nat×σ} and ?_{σ→(nat×σ)}. We would like to prove equivalences such as this, and in general consider a specialisation ordering at each type, such that

?_{σ→(nat×σ)} ⊑ λx : σ.⟨2,?_{σ}⟩ ⊑ λx : σ.⟨2, x⟩

Moreover, we would like to study how underdeterminism interacts with the usual equational rules of λ^{×→}. Our interest in such a calculus of refinement comes from our belief that this is a fundamental aspect of program development. The refinement methodology of program development consists of writing a term meaning ‘a program which satisfies specification ϕ’, and transforming it step by step into an actual program satisfying the specification ϕ. We view types as rudimentary specifications, and defer study of the logic to a separate report [2]. We believe it is worthwhile to study underdeterminism in isolation from logic, as much of the difficulty in reasoning in refinement calculi is in understanding how underdeterminism interacts with the programming features.

In Section 3 we describe the language and its refinement rules. The equational theory is then studied as part of a simple logic. We give a simple denotational semantics in Section 4 as a class of set-theoretic models, and show that our calculus is complete for proving the refinements valid in this class of models.

1A full account of skeletons would make reference to software architecture and is outside the scope of this paper. The simple characterisation given here seems a reasonable starting point though.

In Section 5 we describe a first-order logic of refinement and give its semantics. The logic is also proven sound and complete. Finally, we draw some brief conclusions in Section 6.

Related Work

The study of indefinite descriptions — ‘some x such that P ’ — goes right back to the earliest work on modern logic (e.g. [9]) but the idea there is that a description ranges over semantic values. Similarly, Hermida and Jacobs’ study of indeterminates in the lambda calculus [4] does not account for substitution allowing variable capture.

Although much work has been published on refinement calculi, there seem to be no fully axiomatised systems. [8] describes the classical refinement calculus of Back, Morgan and Morris. This is an imperative language extended with specification constructs. Their system however, uses nondeterminism to express specification constructs. We believe this to be a mistake, as nondeterminism is a computational phenomenon distinct from our view of underdeterminism as a specificational phenomenon, at a level above the programming language. Moreover, we might want to consider a combination of nondeterminism and underdeterminism, for example when developing a logic program.

Proof development systems, such as Lego [5], allow users to interactively construct a proof by refinement. Intermediate states in a proof development may be modelled as underdetermined terms. The notion of metavariable or logical or existential variable is similar to our ? terms.

The concept of underdeterminism also arises in linguistics (with the name ‘underspecification’), where semantically ambiguous statements such as “every student is ?_{noun phrase}” are studied. [1] for example, considers a language with metavariables for representing such statements.

3 The Calculus

We give the syntax of the language and the classes of judgements. Then we give some syntactic results and a short example of refinement.

3.1 Syntax

We extend the simply-typed lambda calculus with an underdeterminism construct, ?_{τ}, meaning ‘some term with type τ’. We view the type τ as a rudimentary specification and refer to terms with such ‘holes’ for programs to be supplied later, as refinement terms. Here “simply-typed lambda calculus” means with finite products and an applied theory of ground types γ and constants k. The types, preterms and environments are

τ ::= 1 | γ | τ × τ | τ → τ

r ::= x | k(r_{1}, …, r_{n}) | ∗ | ⟨r, r′⟩ | λx : τ.r | ?_{τ} | π_{1}(r) | π_{2}(r) | rr′ | let x : τ be r in r′

Γ ::= ⟨⟩ | Γ, x : τ

We say that a term is determined if it contains no stubs, that is, subterms of the form ?_{τ}. Otherwise, we call a term underdetermined. We use the metavariable t to range over determined terms, and r over arbitrary underdetermined terms. Note that primitive constants are determined. In fact, each term of the simply-typed lambda calculus is determined. The converse does not hold, however, since we allow let x : σ be t in t′ to be determined. We will see, though, that by eliminating let’s, every determined term is provably equal to an ordinary term of the simply-typed lambda calculus. This is since let x : σ be t in t′ equals t′[t/x].

We use the notation r[t/x] to indicate the (capture avoiding) substitution of t for each free occurrence of variable x in r. We sometimes write r[x] to distinguish all the free occurrences of variable x in term r. This does not mean that x is the only free variable, nor that it actually appears free in r. When writing r[x], we can use r[t] to indicate the substitution r[t/x].

We assume throughout some fixed signature of types and constants.

Definition 3.1 A λ_{?}-signature consists of a collection of ground types γ and constants k, each of which is assigned some sort τ_{1}, …, τ_{n} → τ.

We write k : τ_{1}, …, τ_{n} → τ to indicate that constant k has sort τ_{1}, …, τ_{n} → τ. This does not mean that k itself is a well-typed term, but that with n arguments, r_{1} : τ_{1}, …, r_{n} : τ_{n}, the term k(r_{1}, …, r_{n}) has type τ.

Intuitively, we can think of a term r as being a kind of description or specification of determined terms, so for example, ⟨2,?_{nat}⟩ is a term which specifies pairs of naturals ⟨2, t⟩, where t is any natural. Conversely, we say that ⟨2, t⟩ satisfies ⟨2,?_{nat}⟩.

The abstraction λx : τ.r should be thought of as describing the collection of determined functions λx : τ.t, such that for all determined arguments t′ of type τ, t[t′/x] satisfies r[t′/x], and not as a nondeterministic function which takes an argument t′ and returns a term r[t′/x].

We want to regard variables as ranging over determined terms, in order to retain the familiar rules of λ^{×→} for determined terms. Since only determined terms can be substituted for variables, we use an axiomatisation of let expressions, let x : τ be r in r′, as in the computational lambda calculus [7], as a way of discharging an arbitrary underdetermined term r, without substituting directly for a variable x. The idea is that let x : τ be r in r′ delays the substitution of r for x until r can be refined into some determined t, but still lets us reason about the substitution. The expression let x : τ be r in r′ then, can be satisfied by t′, when t satisfies r′[t/x] for some t which satisfies r.

Although we do not assume that all types are inhabited, for various statements below we will make this restriction. This is a natural assumption when types are used in programming and avoids certain semantic complications (see [6]). The reader may assume though that this assumption means that our calculus is of no interest in studying program specification, where in traditional type-theoretic approaches, specifications are viewed as possibly empty types. However, the idea in [2] is not to use types themselves as specifications, but that a specification (which may be unsatisfiable) is something ‘over’ an ordinary program type. e.g. The specification (n : nat)even(n) (in the notation of [2]) is over

nat.

3.2 Judgements

We axiomatise an equational theory with judgements

Typing  Γ ⊢ r : τ
Refinement  Γ ⊢ r ⊑_{τ} r′

where Γ is a context of variable assumptions. As is usual with lambda calculi, (in)equations are at a type, which we sometimes drop when not significant. We write the refinement of r to r′ (at τ) as r ⊑_{τ} r′, to indicate that r′ is more determined than r. Note that some authors use ⊒ for refinement.

We take equality to be a derived notion, defined as mutual refinement. This is reasonable because, as we show by a semantic argument below, the calculus is a conservative extension of the simply-typed lambda calculus, i.e. determined terms are mutually refinable if and only if they are provably equal in λ^{×→}.

Contexts are well-formed

                                        ⊢ Γ wf

when they contain distinct variables. We adopt the convention that in writing a judgement we assume its context to be well-formed.

We assume throughout some fixed applied theory given (with respect to a signature) as a set of well-typed equations in context between determined terms.

Definition 3.2 A λ_{?}-theory consists of a λ_{?}-signature, and a collection of equations in context, Γ ⊢ t =_{τ} t′, well-typed with respect to the signature.

We write Ax ▷ Γ ⊢ t =_{τ} t′ to indicate that an equation is an axiom in the applied theory.

Example 3.1 We give an axiomatisation of booleans, as an example of an applied theory. There is one ground type

                                       γ ::= bool

and three constant symbols

                                     true : bool
                                     false : bool
                            if  then  else : bool, τ, τ → τ

Strictly speaking, there are separate conditionals for each type τ but we ignore this.

The axioms are given in a schematic form for arbitrary contexts :

Γ ⊢ iftruethen x else y =_{τ} x (x : τ, y : τ ∈ Γ)
Γ ⊢ iffalsethen x else y =_{τ} y (x : τ, y : τ ∈ Γ)

         Γ ⊢ f(b) =_{τ} if b then f(true) else f(false)  (f : bool → τ, b : bool ∈ Γ)

The equations are between determined terms. Refinements follow from the rules of the calculus.

3.3 Rules of the equational calculus

The typing judgement Γ ⊢ r : τ is axiomatised in Figure 1. This just extends the rules of the simplytyped lambda calculus with typing rules for the ? and let constructs.

The equality rules in Figure 2 are just those of λ^{×→}, and should be read as mutual refinements. The rules are given for determined terms. Although we show below various generalisations of these to arbitrary underdetermined terms, we prefer to give the axioms of the calculus in this minimal form as it more clearly shows that refinement is an axiomatisation on top of the underlying equational theory.

Figure 3 axiomatises how underdeterminism combines with program constructs via the let expressions. Most of these rules are borrowed from the computational lambda calculus. The exception is (LET-ABS-EQ), which makes explicit the ‘hidden dependency’ of specifications on variables in the context. In view of (LET-ASSOC-EQ), we use let x_{1} : σ_{1}, x_{2} : σ_{2} be r_{1}, r_{2} in r as an abbreviation of the nested let expression let x_{1} : σ_{1} be r_{1} in (let x_{2} : σ_{2} be r_{2} in r). Note that because of the assumption of well-formedness of contexts, we can omit side-conditions on the occurrence of variables. For example, in (LET-ASSOC-EQ), since Γ, y : τ is well-formed, y is not in Γ and so y is not in r′′.

Figures 4 and 5 axiomatise the refinement relation. The intuition behind the refinement relation is that it should correspond to an increase in information, and a decrease in the possible programs which could satisfy a refinement term. There are top-down rules for decomposing a specification by refinement into a combination of simpler ones. We also have a weakening rule (LET-WEAKEN-REF) which may be thought of as claiming an auxiliary lemma, and a congruence rule (LET-ξ-REF) for let expressions, which lets us derive the corresponding rules for pairs, applications and projections. Sequent style bottom-up rules for making use of the context are derived below.

The following lemma provides some insight into underdeterminism. It says that in any term, all the underdeterminism can be moved to the outside, so the term can be viewed as a simple combination of program and specification. For example, λx : σ.⟨2,?_{nat}⟩ is equal to let f : σ → natbe ?_{σ→nat} in λx : σ.⟨2, fx⟩.

Lemma 3.1 For all terms in context Γ ⊢ r : τ, there exists a context x_{1} : σ_{1}, …, x_{n} : σ_{n} and a determined term Γ, x_{1} : σ_{1}, …, x_{n} : σ_{n} ⊢ t : τ such that each x_{i} appears exactly once in t, and Γ ⊢ let x_{1} : σ_{1}, …, x_{n} : σ_{n} be ?_{σ_{1}}, …,?_{σ_{n}} in t =_{τ} r.

Proof: Use let rules to move the underdeterminism outwards, (LET-ABS-EQ) handling the abstractions.

Γ, x : σ, Γ′ ⊢ x : σ  (VAR-TYPE)

{Γ ⊢ r_{i} : τ_{i} (i = 1, …, n) \atop Γ ⊢ k(r_{1}, …, r_{n}) : τ} (k : τ_{1}, …, τ_{n} → τ)  (CONST-TYPE)

Γ ⊢ ∗ : 1  (UNIT-TYPE)

Γ ⊢ ?_{σ} : σ  (SPEC-TYPE)

\begin{matrix}Γ ⊢ r : σ & Γ ⊢ r′ : τ \\ Γ ⊢ ⟨r, r′⟩ : σ × τ \end{matrix}  (PAIR-TYPE)

{Γ, x : σ ⊢ r : τ \atop Γ ⊢ λx : σ.r : σ → τ}  (ABS-TYPE)

{Γ ⊢ r : σ × τ \atop Γ ⊢ π_{1}(r) : σ}  (PROJ1-TYPE)

{Γ ⊢ r : σ × τ \atop Γ ⊢ π_{2}(r) : τ}  (PROJ2-TYPE)

\begin{matrix}Γ ⊢ r : σ → τ & Γ ⊢ r′ : σ \\ Γ ⊢ rr′ : τ \end{matrix}  (APP-TYPE)
Γ ⊢ r : τ Γ, x : τ ⊢ r′ : τ′
Γ ⊢ let x : τ be r in r′ : τ′ (LET-TYPE)

Figure 1: Typing Rules

Note the linearity – each stub counts exactly once, so ⟨?_{σ},?_{σ}⟩ becomes let x : σ, y : σ be ?_{σ},?_{σ} in ⟨x, y⟩ and not let z : σ be ?_{σ} in ⟨z, z⟩ (to which it refines though). We will not, however, use the linearity in appeals to the lemma below. Note also that such canonical forms need not be unique. We sometimes use the useful abbreviation let x_{1} : σ_{1}, …, x_{n} : σ_{n} in t for this canonical form. So, for example, λx : σ.⟨2,?_{nat}⟩ is equal to let f : σ → natin λx : σ.⟨2, fx⟩. In fact, by repeated pairing, we can always express terms in the simpler form let x : σ in t.

It is often convenient to write let x_{1} : σ_{1}, …, x_{n} : σ_{n} in t as let Γ in t, where Γ stands for the local context x_{1} : σ_{1}, …, x_{n} : σ_{n}. We also write t[Γ] as informal notation for t[x_{1} : σ_{1}, …, x_{n} : σ_{n}].

By expressing terms in canonical form, we can prove a few results about let expressions. None of these results hold in the computational lambda calculus.

Lemma 3.2 The following rules are derived :

1. (let-commutativity)

Γ ⊢ r : τ  Γ ⊢ r′ : τ′  Γ, x : τ, y : τ′ ⊢ r′′ : τ′′
Γ ⊢ let x : τ, y : τ′ be r, r′ in r′′ =_{τ′′} let y : τ′, x : τ be r′, r in r′′

\begin{matrix}Γ, x : σ ⊢ t : τ & Γ ⊢ t′ : σ \\ Γ ⊢ (λx : σ.t)t′ =_{τ} t[t′/x] \end{matrix}  (ABS-β-EQ)
{Γ ⊢ t : σ → τ \atop Γ ⊢ λx : σ.(tx) =_{σ→τ} t}  (ABS-η-EQ)
\begin{matrix}Γ ⊢ t_{1} : σ_{1} & Γ ⊢ t_{2} : σ_{2} \\ Γ ⊢ π_{i}⟨t_{1}, t_{2}⟩ =_{σ_{i}} t_{i} \end{matrix} (i = 1, 2)  (PAIR-β-EQ)
{Γ ⊢ t : σ × τ \atop Γ ⊢ ⟨π_{1}(t), π_{2}(t)⟩ =_{σ×τ} t}  (PAIR-η-EQ)
{Γ ⊢ t : 1 \atop Γ ⊢ t =_{1} ∗}  (UNIT-η-EQ)
Γ ⊢ t =_{τ} t′  (Ax ▷ Γ ⊢ t =_{τ} t′) (AXIOM-EQ)

Figure 2: Equality rules for determined terms

Γ ⊢ t : τ Γ, x : τ ⊢ r : τ′

Γ ⊢ let x : τ be t in r[x] =_{τ′} r[t] (LET-β-EQ)

Γ ⊢ r : τ

Γ ⊢ let x : τ be r in x =_{τ} r (LET-η-EQ)

Γ ⊢ r : τ Γ, y : τ ⊢ r′ : τ′ Γ, x : τ′ ⊢ r′′ : τ′′

Γ ⊢ let x : τ′ be (let y : τ be r in r′[y]) in r′′[x] =_{τ′′} let y : τ be r in (let x : τ′ be r′[y] in r′′[x])

(LET-ASSOC-EQ)

Γ ⊢ r_{i} : τ_{i} Γ ⊢ let x_{1} : τ_{1}, …, x_{n} : τ_{n} be r_{1}, …, r_{n} in k(x_{1}, …, x_{n}) =_{τ} k(r_{1}, …, r_{n}) (k : τ_{1}, …, τ_{n} → τ) (LET-CONST-EQ)
Γ ⊢ r : σ → τ Γ ⊢ r′ : σ

Γ ⊢ let x : σ → τ, x′ : σ be r, r′ in xx′ =_{τ} rr′ (LET-APP-EQ)

Γ ⊢ r : τ Γ ⊢ r′ : τ′

Γ ⊢ let x : τ, x′ : τ′ be r, r′ in ⟨x, x′⟩ =_{τ×τ′} ⟨r, r′⟩ (LET-PAIR-EQ)

Γ ⊢ r : τ_{1} × τ_{2}

Γ ⊢ let x : τ_{1} × τ_{2} be r in π_{i}(x) =_{τ_{i}} π_{i}(r) (LET-PROJi-EQ)

Γ, x : σ, y : τ ⊢ r[x, y] : τ′

Γ ⊢ let z : σ → τ be ?_{σ→τ} in λx : σ.r[x, zx] =_{σ→τ′} λx : σ.(let y : τ be ?_{τ} in r[x, y])

(LET-ABS-EQ)

Figure 3: let equalities

Γ, x : σ, Γ′ ⊢ ?_{σ} ⊑_{σ} x  (VAR-REF)

Γ ⊢ ?_{τ} ⊑_{τ} k(?_{τ_{1}}, …,?_{τ_{n}}) (k : τ_{1}, …, τ_{n} → τ) (CONST-REF)

Γ ⊢ ?_{1} ⊑_{1} ∗  (UNIT-REF)

Γ ⊢ ?_{σ×τ} ⊑_{σ×τ} ⟨?_{σ},?_{τ} ⟩  (PAIR-REF)

Γ ⊢ ?_{σ→τ} ⊑_{σ→τ} λx : σ.?_{τ}  (ABS-REF)

Figure 4: Top-down refinement rules

Γ ⊢ r_{1} ⊑_{τ_{1}} r′_{1} Γ, x : τ_{1} ⊢ r_{2} ⊑_{τ_{2}} r′_{2}

Γ ⊢ let x : τ_{1} be r_{1} in r_{2} ⊑_{τ_{2}} let x : τ_{1} be r′_{1} in r′_{2} (LET-ξ-REF)

{Γ, x : σ ⊢ r ⊑_{τ} r′ \atop Γ ⊢ λx : σ.r ⊑_{σ→τ} λx : σ.r′}  (ABS-ξ-REF)

{Γ ⊢ r : τ \atop Γ ⊢ r ⊑_{τ} r}  (REFL-REF)

\begin{matrix}Γ ⊢ r ⊑_{τ} r′ & Γ ⊢ r′ ⊑_{τ} r′′ \\ Γ ⊢ r ⊑_{τ} r′′ \end{matrix}  (TRANS-REF)

Γ ⊢ r′ : τ Γ ⊢ r : σ Γ ⊢ r′ ⊑_{τ} let x : σ be r in r′ x ∉ r′  (LET-WEAKEN-REF)

Figure 5: Other refinement rules 2. (let-contraction)

Γ ⊢ r : σ  Γ, x : σ, y : σ ⊢ r′ : τ
Γ ⊢ let x : σ, y : σ be r, r in r′ ⊑_{τ} let z : σ be r in r′[z/x, z/y]

3. (Strengthen local context)

For x ∉ r′,

Γ ⊢ r′ : τ′  Γ, x : τ, y : τ′ ⊢ r : τ′′
Γ ⊢ λx : τ.(let y : τ′ be r′ in r) ⊑_{τ→τ′′} let y : τ′ be r′ in λx : τ.r

Proof: We prove (3). First we show that

λx : σ.let y : τ in r[y] ⊑ let y : τ in λx : σ.r[y]  (4)

This is :

λx : τ.let y : τ′ in r[y]

= let z : τ → τ′ in λx : τ.r[zx]  (LET-ABS-EQ)
⊑ let y : τ′ inlet z : τ → τ′ in λx : τ.r[zx]  (LET-WEAKEN-REF)
⊑ let y : τ′ in  (y : τ′ ⊢ ?_{τ→τ′} ⊑ λx : τ.y,
let z : τ → τ′ be λx : τ.y in λx : τ.r[zx]  and LET-ξ-REF)
= let y : τ′ in λx : τ.r[y]  (LET-ξ-EQ)

Then :

λx : τ.let y : τ′ be r′ in r[x, y]

= λx : τ.let y : τ′ be (let z : σ in t) in r[x, y] (Lemma 3.1; can.form)
= λx : τ.let z : σ in (let y : τ′ be t in r[x, y])  (LET-ASSOC-EQ)
⊑ let z : σ in λx : τ.(let y : τ′ be t in r[x, y])  (4)
= let z : σ inlet y : τ′ be t in λx : τ.r[x, y]  (LET-β-EQ)
= let y : τ′ be (let z : σ in t) in λx : τ.r[x, y]  (LET-ASSOC-EQ)
= let y : τ′ be r′ in λx : τ.r[x, y]  (can.form)

The proofs of (1) and (2) are carried out similarly, by expressing terms in canonical form.

Commutativity of let’s corresponds to the idea that it does not matter what order we solve subproblems in (so long as they do not depend on each other), and contraction of let’s says that we can solve two identical problems by just solving the problem once and using the solution twice. The third rule illustrates the dependence of underdeterminism on the context. There are more determined terms which satisfy the term on the left, since x can be used in refining r′, but this is not possible when r′ is outside the bound variable on the right.

If all types are inhabited then, in fact, all terms are satisfiable. That is, every r refines to some determined t. Because of this, the rule (LET-WEAKEN-REF) can be strengthened to an equality, i.e. for x ∉ r′, we have r′ = let x : σ be r in r′. We use this fact to derive strengthened forms of (PAIR-β-EQ) and (UNIT-η-EQ) for arbitrary underdetermined terms (of appropriate type).

Proposition 3.1 If all types are inhabited :

1. \begin{matrix}Γ ⊢ r_{1} : τ_{1} & Γ ⊢ r_{2} : τ_{2} \\ Γ ⊢ π_{i}⟨r_{1}, r_{2}⟩ =_{τ_{i}} r_{i} \end{matrix} (i = 1, 2)
2. {Γ ⊢ r : 1 \atop Γ ⊢ r =_{1} ∗}

Proof:

1. The first is derived as :

π_{1}⟨r_{1}, r_{2}⟩ = π_{1}⟨let x : σ in t_{1}, let y : τ in t_{2}⟩
= let x : σ, y : τ in π_{1}⟨t_{1}, t_{2}⟩
= let x : σ, y : τ in t_{1}
= let x : σ in t_{1}
= r_{1}

The ⊑ of the second last equality is by refining with some determined term of type τ, and the ⊒ is an instnace of (LET-WEAKEN-REF).

2. Suppose r has type 1. Now r has canonical form let x : σ in t, say, where t has type 1. By (UNIT-η-EQ) we can prove x : σ ⊢ t =_{1} ∗ and so let x : σ in t =_{1} let x : σ in ∗, which since σ is inhabited, equals ∗.

We can strengthen (ABS-β-EQ), without the assumption of nonemptiness.

Proposition 3.2 The following can be derived :

\begin{matrix}Γ, x : σ ⊢ r : τ & Γ ⊢ t : σ \\ Γ ⊢ (λx : σ.r)t =_{τ} r[t/x] \end{matrix}

Proof: We use the auxiliary result that for any t of type σ

let f : σ → τ in r[ft/x] = let x : τ in r

Then,

(λx : σ.r)t = (λx : σ.let z : τ′ in t′)t
= let f : σ → τ′ in (λx : σ.t′[fx/z])t
= let f : σ → τ′ in t′[ft/z, t/x]
= let z : τ′ in t′[t/x]
= r[t/x]

Because of Proposition 3.2, we can β-reduce applications with arbitrary function bodies. This is significant as it means that underdetermined terms can be executed, up to a point, as ordinary programs. In general, this is not possible as evaluation can not proceed when a stub is encountered. For example, π_{1}(?_{σ×τ}) cannot be reduced. This observation forms the basis for a single-step operational semantics, although this is not investigated further here.

At this point, we pause to review our motivation for studying this calculus. Program refinement is a stepwise decomposition of logical specifications and their gradual replacment with code. The calculus which we are studying here formalises refinement for a limited form of specification, with no logic, and is a fragment of a larger calculus studied in the author’s thesis.

The statement corresponding to Proposition 3.2 does not hold in the full system, as the auxiliary result fails. That is, in the presence of logic, we cannot β-reduce with arbitrary function bodies. We believe that this is motivation for studying this subcalculus of a full logical refinement calculus.

Now, Propositions 3.1 and 3.2 show that we can deduce general forms of β, although the axioms for pairs and abstractions are given for determined terms. We do not, however, have η equalities for arbitrary pairs and abstractions.

To see this for abstractions, first note, that as in the computational lambda-calculus, application distributes over let’s :

    (let x be r in r′)t = let x_{1} be (let x be r in r′) in x_{1}t
                     = let x be r in (let x_{1} be r′ in x_{1}t)
                     = let x be r in r′t

Now we show that we not have λx : σ.rx =_{σ→τ} r for arbitrary underdetermined r, by proving that for r_{1} ≡ let b : boolin λx : σ.b and r_{2} ≡ λx : σ.?bool, we have λx : σ.r_{1}x =_{σ→τ} r_{2}. λx : σ.(let b : boolbe ?_{bool} in λx : σ.b)x

= λx : σ.let b : boolbe ?_{bool} in (λx : σ.b)x
= λx : σ.?_{bool}

Finally, recall that the intuition is that terms describe a set of values, and that refinement is a reduction of this set. Based on this intuition, we do not want r_{1} to equal r_{2}. A more formal justification must await the presentation of the semantics in the next section.

We can derive inequalities, though.

Proposition 3.3 For well-typed, r, we can derive λx : σ.rx ⊑_{σ→τ} r and ⟨π_{1}r, π_{2}r⟩ ⊑_{σ×τ} r.

Proof: We sketch the proof of the first statement. By Lemma 3.1, r has canonical form let y : σ′ in t. Then, λx : σ.(let y : σ′ in t)x = λx : σ.let y : σ′ in tx, by the distribution of application over let’s. By Lemma 3.2(3), this refines to let y : σ′ in λx : σ.tx, which by (ABS-η-EQ) and (LET-ξ-REF), equals let y : σ′ in t, that is, r.

The next lemma says that our refinement rules are complete, in the sense that they allow us to construct by refinement any program which satisfies a specification.

Lemma 3.3 If Γ ⊢ t : σ then Γ ⊢ ?_{σ} ⊑_{σ} t.

Proof: By Proposition 3.2, ?_{σ} = (λx : σ.?_{σ})t. Then (λx : σ.?_{σ})t ⊑ (λx : σ.x)t = t. The fact that this can be proven trivially motivates restricted calculi better suited to proof search, where construction must be on the structure of t. This is work in progress.

Remark 3.1 Using booleans, we can define a form of binary choice on terms. For r, r′ : σ, define

                        r ⫾ r′ ≜ let b : boolin (if b then r else r′)

We can prove that ⫾ is commutative, associative, and idempotent, and so is a reasonable notion of choice. This definition is useful because it helps to illustrate the differences between underdeterminism and nondeterminism. If the reader is unfamiliar with nondeterminism, then this remark can be safely ignored.

We compare our axiomatisation of underdeterminism with a notion of external nondeterminism, that is, where the nondeterminism arises from the environment making the choice. In particular, we compare a nondeterministic choice operator, +, with ⫾. For example, we would intuitively expect to have λx : nat.2 + 3 = λx : nat.2 + λx : nat.3 (using some constants for naturals). This contrasts with the properties of ⫾ under a binding, since 2 ⫾ 3 can refine to anything well-formed in the local context. For example, 2 ⫾ 3 ⊑ if x > 3 then 2 else 3, so λx : nat.2 ⫾ 3 ⊑ λx : nat.if x > 3 then 2 else 3.

Another difference is between nondeterministic failure terms and the analagous idea for underdeterminism — unsatisfiable terms. Suppose the type τ is uninhabited. Then there are unsatisfiable terms at every type. Any term of the form let x : τ in r, where r is any term of type σ, will be unsatisfiable. Now, for nondeterministic failure, we expect r + 0 = r. However, if the term empty_{σ} is unsatisfiable, then r ⫾ empty_{σ} is also unsatisfiable. Informally, ‘r ⫾ empty_{σ} = empty_{σ}’.

We can prove the equivalences mentioned in the introduction and say that ‘underdeterminism commutes with determinism’, in the sense that underdeterminism at a particular type can be expressed at a lower type using the relevant term constructor. This offers some conceptual justification for regarding underdeterminism as being a feature at a level above a programming language. There is no substantial interaction with computation.

Proposition 3.4 The following are derivable

1. ?_{σ×τ} = ⟨?_{σ},?_{τ} ⟩

2. ⟨π_{1}(?_{σ×τ}), π_{2}(?_{σ×τ})⟩ = ?_{σ×τ} 3. If τ is inhabited, then π_{1}(?_{σ×τ}) = ?_{σ}, and if σ is inhabited, then π_{2}(?_{σ×τ}) = ?_{τ}.

4. ?_{σ→τ} = λx : σ.?_{τ} and ?_{σ→τ} r =_{τ} ?_{τ} for all satisfiable r : σ.

Proof: We prove (1), that ?_{σ×τ} =_{σ×τ} ⟨?_{σ},?_{τ} ⟩. Clearly, (PAIR-REF) lets us refine from left to right. We prove the other direction.

⟨?_{σ},?_{τ} ⟩ = let x : σ, y : τ be ?_{σ},?_{τ} in ⟨x, y⟩
⊑ let z : σ × τ be ?_{σ×τ} in
let x : σ, y : τ be ?_{σ},?_{τ} in ⟨x, y⟩
⊑ let z : σ × τ be ?_{σ×τ} in
let x : σ, y : τ be π_{1}z, π_{2}z in ⟨x, y⟩
= let z : σ × τ be ?_{σ×τ} in ⟨π_{1}z, π_{2}z⟩
= ?_{σ×τ}

The proofs of the other statements are carried out in a similar way, by expressing the terms in canonical form, and using the let-axioms and Lemma 3.2 to manipulate the terms.

We can derive some useful refinement rules. There are bottom-up style refinement rules, complementing the top-down rules given as primitive, and various congruence rules.

Proposition 3.5 The following are derivable :

Bottom-up refinement :

\begin{matrix}Γ ⊢ t : τ & Γ, x : τ′ ⊢ r ⊑_{σ} r′[x] \\ Γ, y : τ → τ′ ⊢ r ⊑_{σ} r′[yt] \end{matrix} x ∉ r (APP-REF)

{Γ, x : τ ⊢ r ⊑_{σ} r′[x] \atop Γ, z : τ × τ′ ⊢ r ⊑_{σ} r′[π_{1}z]} x ∉ r (PROJ1-REF)  {Γ, y : τ′ ⊢ r ⊑_{σ} r′[y] \atop Γ, z : τ × τ′ ⊢ r ⊑_{σ} r′[π_{2}z]} y ∉ r (PROJ2-REF)

Congruence :

\begin{matrix}Γ ⊢ r_{1} ⊑_{σ} r′_{1} & Γ ⊢ r_{2} ⊑_{τ} r′_{2} \\ Γ ⊢ ⟨r_{1}, r_{2}⟩ ⊑_{σ×τ} ⟨r′_{1}, r′_{2}⟩ \end{matrix}  (PAIR-ξ-REF) {Γ ⊢ r_{i} ⊑_{τ_{i}} r′_{i} (i = 1, …, n) \atop Γ ⊢ k(r_{1}, …, r_{n}) ⊑_{τ} k(r′_{1}, …, r′_{n})} (CONST-ξ-REF)

{Γ ⊢ r ⊑_{τ_{1}×τ_{2}} r′ \atop Γ ⊢ π_{i}(r) ⊑_{τ_{i}} π_{i}(r′)} (i = 1, 2) (PROJ-ξ-REF) \begin{matrix}Γ ⊢ r_{1} ⊑_{σ→τ} r′_{1} & Γ ⊢ r_{2} ⊑_{σ} r′_{2} \\ Γ ⊢ r_{1}r_{2} ⊑_{τ} r′_{1}r′_{2} \end{matrix}  (APP-ξ-REF)

Proof: The bottom-up refinement rules are obtained by cutting. (PROJ1-REF), for example, is derived as :

{Γ, x : τ ⊢ r ⊑_{σ} r′[x] \atop Γ ⊢ λx : τ.r ⊑_{τ→σ} λx : τ.r′[x]} ; Γ, z : τ × τ′ ⊢ (λx : τ.r)π_{1}z ⊑_{σ} (λx : τ.r′[x])π_{1}z ; Γ, z : τ × τ′ ⊢ r ⊑_{σ} r′[π_{1}z]

The congruence rules all follow from (LET-ξ-REF). For example, (PAIR-ξ-REF) follows since ⟨r_{1}, r_{2}⟩ equals let x_{1} : τ_{1}, x_{2} : τ_{2} be r_{1}, r_{2} in ⟨x_{1}, x_{2}⟩. Then using (LET-ξ-REF), this refines to let x_{1} : τ_{1}, x_{2} : τ_{2} be r′_{1}, r′_{2} in ⟨x_{1}, x_{2}⟩, which equals ⟨r′_{1}, r′_{2}⟩.

We make a similar point here to that made after Lemma 3.3. In a search-directed refinement calculus these rules would be primitive. Our intention here, though, was to give a system complete for proving arbitrary refinements of the form r ⊑_{τ} r′, and not goal-directed refinements r ⊑_{τ} t.

Example 3.2 We can use let weakening (or contraction) to combine two equivalent problems into one

⟨?_{σ},?_{σ}⟩ ⊑ let z : σ be ?_{σ} in ⟨?_{σ},?_{σ}⟩ ⊑ let z : σ be ?_{σ} in ⟨z, z⟩

The first step uses (LET-WEAKEN-REF), and the second uses (VAR-REF), (REFL-REF), (PAIR-REF) and (LET-ξ-REF).

Example 3.3 We give a short example, using refinement to derive a swap function. Transitivity of refinement means that we can often present much of a refinement derivation as equational reasoning. Here there are two main steps.

?_{σ×τ→τ×σ} ⊑ λz : σ × τ.?_{τ×σ} ⊑ λz : σ × τ.⟨π_{2}z, π_{1}z⟩

Formally, this is

\begin{matrix}⊢ ?_{σ×τ→τ×σ} ⊑ λz : σ × τ.?_{τ×σ} ^{ABS-REF} & ⊢ λz : σ × τ.?_{τ×σ} ⊑ λz : σ × τ.⟨π_{2}z, π_{1}z⟩ \\ ⊢ ?_{σ×τ→τ×σ} ⊑ λz : σ × τ.⟨π_{2}z, π_{1}z⟩ \end{matrix} ^{TRANS-REF}

The first hypothesis follows from (ABS-REF), and the second is derived as

z : σ × τ ⊢ ?_{τ×σ} ⊑ ⟨?_{τ} ,?_{σ}⟩ ^{PAIR-REF}

y : τ ⊢ ?_{τ} ⊑ y ^{VAR-REF} z : σ × τ ⊢ ?_{τ} ⊑ π_{2}z

PROJ2-REF

x : σ ⊢ ?_{σ} ⊑ x ^{VAR-REF} z : σ × τ ⊢ ?_{σ} ⊑ π_{1}z

PROJ1-REF

z : σ × τ ⊢ ⟨?_{τ} ,?_{σ}⟩ ⊑ ⟨π_{2}z, π_{1}z⟩ PAIR-ξ-REF

z : σ × τ ⊢ ?_{τ×σ} ⊑ ⟨π_{2}z, π_{1}z⟩ TRANS-REF

⊢ λz : σ × τ.?_{τ×σ} ⊑ λz : σ × τ.⟨π_{2}z, π_{1}z⟩ ABS-ξ-REF

4 Models

We can interpret the calculus using a simple generalisation of Henkin models [3]. A Henkin model (with products) is an applicative structure, that is, a tuple of families of sets and type-indexed mappings

⟨{A^{σ}}, {Proj_{1}^{σ,τ} }, {Proj_{2}^{σ,τ} }, {App^{σ,τ} }, Const⟩

which is also extensional and satisfies the environment model condition. See [6] for details. It is extensionality which allows us to interpret abstractions, pairs and the unit uniquely, and the environment model condition which gives us enough elements. To each type σ we ascribe the set A^{σ}, and use Const to map constants into the appropriate sets. This much is needed for a model of the simply-typed lambda calculus. We will use the same apparatus, but interpret our underdetermined terms as subsets of the A^{σ}, rather than elements^{2}.

We make one additional assumption of our models. We require that the function sets be ‘closed under factoring’. Let f′ ∈ A^{τ→τ′}, f ∈ A^{σ→τ′}. If for all b ∈ A^{τ}, there exists an a ∈ A^{σ} such that App(f′, b) = App(f, a), then there exists an element g ∈ A^{τ→σ} such that for all b ∈ A^{τ}, App(f′, b) = App(f, App(g, b)). In other words, writing f̄ for the function associated with f ∈ A^{σ→τ}, that is, (a ∈ A^{σ} ↦ App(f, a)) : if there exists a function h : A^{τ} → A^{σ} such that f̄′ = h; f̄, then there exists an element g ∈ A^{τ→σ} such that f̄′ = ḡ; f̄. Note that we do not require ḡ = h. The factoring condition is essentially a form of choice axiom.

Before proceeding further, we give an example of a Henkin model with the factoring condition.

2We need to interpret Γ ⊢ r : τ at Γ → P(A^{τ}) rather than P(A^{Γ} → A^{τ}), to capture the fact that underdeterminism depends on the context. For example, there are only two elements in P(A1 → A1), but in context b : bool, each of ∗, 0 and if b then ∗ elseempty_{1}, where empty_{1} is an empty term of type 1, should have different interpretations.

Example 4.1 (Full set-theoretic function hierarchy) The sets of the full set-theoretic function hierarchy for a given signature are defined inductively as

A^{γ} = any set
A^{1} = {∗}
A^{σ×τ} = A^{σ} × A^{τ}
A^{σ→τ} = A^{σ} → A^{τ}

The projection and application maps are the usual set-theoretic maps, and Const is any mapping into the appropriate sets.

We will see below that the open term model is another example. Now we interpret Γ ⊢ r : τ inductively on the structure of the typing derivation. This is given in Figure 6.

⟦Γ, x : σ, Γ′ ⊢ x : σ⟧⟨g, a, g′⟩ = {a}

{⟦Γ ⊢ r_{i}⟧ = m_{i} \atop ⟦Γ ⊢ k(r_{1}, …, r_{n}) : τ⟧(g) = \{Const(k)(a_{1}, … a_{n}) | a_{i} ∈ m_{i}(g)\}}

⟦Γ ⊢ ∗ : 1⟧(g) = A^{1}
⟦Γ ⊢ r : σ⟧ = m ⟦Γ ⊢ r′ : τ⟧ = m′

⟦Γ ⊢ ⟨r, r′⟩ : σ × τ⟧(g) = {a ∈ A^{σ×τ} | Proj_{1}^{σ,τ} (a) ∈ mg, Proj_{2}^{σ,τ} (a) ∈ m′g}

{⟦Γ, x : σ ⊢ r : τ⟧ = m \atop ⟦Γ ⊢ λx : σ.r : σ → τ⟧(g) = \{f ∈ A^{σ→τ} | ∀a ∈ A^{σ}.App(f, a) ∈ m⟨g, a⟩\}}

⟦Γ ⊢ ?_{σ} : σ⟧(g) = A^{σ}

{⟦Γ ⊢ r : τ × τ′⟧ = m \atop ⟦Γ ⊢ π_{1}(r) : τ⟧(g) = \{Proj_{1}^{τ,τ′}(a) | a ∈ mg\}}

{⟦Γ ⊢ r : τ × τ′⟧ = m \atop ⟦Γ ⊢ π_{2}(r) : τ⟧(g) = \{Proj_{2}^{τ,τ′}(a) | a ∈ mg\}}

\begin{matrix}⟦Γ ⊢ r : σ → τ⟧ = m & ⟦Γ ⊢ r′ : σ⟧ = m′ \\ ⟦Γ ⊢ rr′ : τ⟧(g) = \{App(f, a) | f ∈ mg, a ∈ m′g\} \end{matrix}

⟦Γ ⊢ r : σ⟧ = m ⟦Γ, x : σ ⊢ r′ : τ⟧ = m′

⟦Γ ⊢ let x : σ be r in r′ : τ⟧(g) = ⋃_{a∈mg} m′⟨g, a⟩

Figure 6: Interpretation of well-formed terms

We take an environment g for context Γ to be a tuple of elements in the appropriate sets, written g ⊨ Γ. It is easily seen that we have soundness of typing, that is, if g ⊨ Γ, then ⟦Γ ⊢ r : τ⟧(g) ⊆ A^{τ}.

We say that a refinement is valid, Γ ⊨ r ⊑_{τ} r′, when for all Henkin models which satisfy the equations in the signature, for all g ⊨ Γ, ⟦Γ ⊢ r : τ⟧(g) ⊇ ⟦Γ ⊢ r′ : τ⟧(g).

We will prove soundness below, but first, it is easy to see that for determined t, the interpretation ⟦Γ ⊢ t : τ⟧(g) is a singleton set. Now we prove a standard lemma.

Lemma 4.1 (Substitution Lemma) For well-formed terms in context x_{1} : τ_{1}, … x_{n} : τ_{n} ⊢ r : τ and Γ ⊢ t_{i} : τ_{i} (i = 1, …, n), we have

⟦x_{1} : τ_{1}, … x_{n} : τ_{n} ⊢ r : τ⟧⟨a_{1}, …, a_{n}⟩ = ⟦Γ ⊢ r[t_{i}/x_{i}]⟧(g)

where a_{i} is the unique inhabitant of ⟦Γ ⊢ t_{i} : τ_{i}⟧(g).

Proof: The proof is a straightforward induction over the typing judgement x_{1} : τ_{1}, … x_{n} : τ_{n} ⊢ r : τ.

Theorem 4.1 (Soundness) If Γ ⊢ r ⊑_{τ} r′ then Γ ⊨ r ⊑_{τ} r′.

Proof: The proof is by induction on the derivation of the judgement. Most cases are straightforward. We prove two key cases.

• (LET-β-EQ)

The interpretation ⟦Γ ⊢ let x : τ be t in r : τ′⟧(g) is defined to be ⋃_{a∈⟦Γ⊢t:τ⟧(g)}⟦Γ, x : τ ⊢ r⟧⟨g, a⟩. Since t is determined, this is ⟦Γ, x : τ ⊢ r : τ′⟧⟨g, a⟩ where a is the unique member of ⟦Γ ⊢ t : τ⟧(g), so by the substitution lemma, the interpretation is ⟦Γ ⊢ r[t/x] : τ′⟧(g).

• (LET-ABS-EQ). To prove the soundness of LET-ABS-EQ, we show first that the axiom follows from the simpler

Γ, x : σ, y : τ ⊢ t[x, y] : τ′

Γ ⊢ let z : σ → τ in λx : σ.t[x, zx] =_{σ→τ′} λx : σ.(let y : τ in t[x, y]) (5)

where the term t is determined. The first step is to show, by induction over terms, that (5) is sufficient to prove that all terms have a canonical form. For the abstraction case, we have λx : σ.r = λx : σ.let y : τ in t[x, y], by induction, and using (5) we get let f : σ → τ in λx : σ.t[x, fx]. Now we prove the full axiom, (LET-ABS-EQ). Assume λx : σ.let y : τ in r : σ → τ′′.

λx : σ.let y : τ in r[x, y] = λx : σ.let y : τ, z : τ′ in t[y, z]
= λx : σ.let p : τ × τ′ in t[π_{1}p, π_{2}p]
= let f′′ : σ → τ × τ′ in λx : σ.t[π_{1}(f′′x), π_{2}(f′′x)]
= let f : σ → τ, f′ : σ → τ′ in λx : σ.t[fx, f′x]
= let f : σ → τ in λx : σ.let z : τ′ in t[fx, z]
= let f : σ → τ in λx : σ.r[x, fx]

Now we prove that (5) is sound.

Let g ⊨ Γ. Now f ∈ ⟦Γ ⊢ let z : σ → τ be ?_{σ→τ} in λx : σ.t[x, zx] : σ → τ′⟧(g), that is, ⋃_{a∈A^{σ→τ}} ⟦Γ, z : σ → τ ⊢ λx : σ.t[x, zx] : σ → τ′⟧⟨g, a⟩, when

∃a ∈ A^{σ→τ} such that ∀b ∈ A^{σ}, fb ∈ ⟦Γ, z : σ → τ, x : σ ⊢ t[x, zx] : τ′⟧⟨g, a, b⟩  (6)

and f ∈ ⟦Γ ⊢ λx : σ.(let y : τ be ?_{τ} in t[x, y]) : σ → τ′⟧(g), when

∀b ∈ A^{σ}, ∃a_{b} ∈ A^{τ} such that fb ∈ ⟦Γ, x : σ, y : τ ⊢ t[x, y] : τ′⟧⟨g, b, a_{b}⟩  (7)

We must prove (6) and (7) are equivalent. Suppose (6). Now let b ∈ A^{σ}. We can define a_{b} as App(a, b). We have fb ∈ ⟦Γ, z : σ → τ, x : σ ⊢ t[x, zx] : τ′⟧⟨g, a, b⟩ = ⟦Γ, x : σ, y : τ ⊢ t[x, y] : τ′⟧⟨g, b, a_{b}⟩, so (7) holds.

Now suppose (7). Define a′ : A^{σ} → A^{τ} as (b ∈ A^{σ} ↦ a_{b} ∈ A^{τ}), and h : A^{σ} → A^{σ×τ} to be (b ∈ A^{σ} ↦ ⟨b, a(b)⟩). Then (7) can be read as h; f̄′ = f̄ where f′ : A^{σ×τ→τ′} is the unique inhabitant of ⟦Γ ⊢ λp : σ × τ.t[π_{1}p, π_{2}p] : σ × τ → τ′⟧(g).

By the factoring condition, there exists an element g ∈ A^{σ→σ×τ} such that ḡ; f̄′ = h̄. Now define a = App(App(comp, g), p_{2}) ∈ A^{σ→τ}, where the elements comp = ⟦λf : σ → σ × τ.λg : σ × τ → τ.λx : σ.g(fx)⟧ and p_{2} = ⟦λp : σ × τ.π_{2}(p)⟧ exist by the environment model condition, and so a ∈ A^{σ→τ}.

We now prove (6). Let b ∈ A^{σ}. Then, by assumption, fb ∈ ⟦Γ, x : σ, y : τ ⊢ t[x, y] : τ′⟧⟨g, b, a_{b}⟩ which, by the substitution lemma, is ⟦Γ, z : σ → τ, x : σ ⊢ t[x, zx] : τ′⟧⟨g, a, b⟩, so (6) holds.

Since we have nontrivial models, soundness implies that the calculus is consistent. More significantly, however, we have completeness of the equational theory of simply-typed underdeterminism with respect to the class of Henkin models with factoring. This implies the system is a conservative extension of the simply-typed lambda calculus.

We will need the following lemmas. The first says that all auxiliary claims made using let weakening can be immediately satisfied.

Lemma 4.2 If Γ ⊢ let z : σ be r in r′ ⊑_{τ} t′ then there exists a determined term Γ ⊢ t : σ such that Γ ⊢ r ⊑_{σ} t and Γ ⊢ r′[t/z] ⊑_{τ} t′.

The lemma follows from

Lemma 4.3 Suppose Γ ⊢ r ⊑_{τ} t′, and r has the form t[?_{σ_{1}}^{Γ_{1}}, …,?_{σ_{n}}^{Γ_{n}}], where ?_{σ_{i}}^{Γ_{i}} means that the subterm ?_{σ_{i}} appears in ‘local context’ (of let’s and λ’s) Γ_{i}. Note also that each such subterm appears exactly once.

Then for each i = 1 … n, there exists Γ, Γ_{i} ⊢ t_{i} : σ_{i}, such that Γ ⊢ t[t_{1}, …, t_{n}] =_{τ} t′.

Proof: We can prove the lemma by induction on the derivation of refinement. Write Γ ⊢ r ⇝ t′ if there exists a standard refinement sequence given by immediately refining the specifications in r ≡ t[?_{σ_{1}}^{Γ_{1}}, …,?_{σ_{n}}^{Γ_{n}}] as Γ, Γ_{i} ⊢ ?_{σ_{i}} ⊑ u_{i}. The inductive case involves showing that the standard sequence can be extended back along each rule. We consider two cases. The reasoning is similar for the others.

• (LET-WEAKEN-REF)

Suppose Γ ⊢ r ⊑ let x : σ be r′ in r ⇝ t′′, where r ≡ t_{1}[?_{σ_{1}}^{Γ_{1}}, …,?_{σ_{n}}^{Γ_{n}}]. By the inductive hypothesis, there exists a t′ and t_{2}[x] such that Γ ⊢ r′ ⊑ t′ (the details of this refinement do not matter), and Γ, x : σ ⊢ r ⇝ t_{2}[x] with Γ ⊢ let x : σ be t′ in t_{2} = t′′, so Γ ⊢ t_{2}[t′] = t′′. Now the standard refinement of r gives terms Γ, x : σ, Γ_{i} ⊢ u_{i} : σ_{i} for each i = 1 … n, and so Γ, Γ_{i} ⊢ u_{i}[t′/x] : σ_{i}.

Hence, Γ ⊢ r ⇝ t_{2}[t′] = t′′, by refining ?_{σ_{i}}^{Γ_{i}} to u_{i}[t_{i}/x].

• (LET-ABS-EQ)

Since this rule is given as an equation, we must consider the two directions of refinement separately. Suppose

Γ ⊢ let z : σ → τ in λx : σ.t′[?_{σ_{i}}^{Γ_{i}}, x, zx] ⊑ λx : σ.(let y : τ in t′[?_{σ_{i}}^{Γ_{i}}, x, y]) ⇝ t

For clarity, we just indicate the one specification ?_{σ_{i}}. Here Γ_{i} records the context in t′.

By induction, there exist terms Γ, x : σ, y : τ, Γ_{i} ⊢ u_{i}[x, y] : σ_{i} and Γ, x : σ ⊢ u[x] : τ such that Γ ⊢ λx : σ.(let y : τ be u in t′[u_{i}, x, y] = t, that is, Γ ⊢ λx : σ.t′[u_{i}[x, u], x, u] = t.

Then we have Γ ⊢ λx : σ.u[x] : σ → τ and Γ, z : σ → τ, x : σ, Γ_{i} ⊢ u_{i}[x, zx] : σ_{i} so we can refine the left term to Γ ⊢ let z : σ → τ be λx : σ.u[x] in λx : σ.t′[u_{i}[x, zx], x, zx], which equals λx : σ.t′[u_{i}[x, u[x]], x, u[x]], and this equals t.

Now we consider the reverse refinement. Suppose

Γ ⊢ λx : σ.(let y : τ in t′[?_{σ_{i}}^{Γ_{i}}, x, y]) ⊑ let z : σ → τ in λx : σ.t′[?_{σ_{i}}^{Γ_{i}}, x, zx] ⇝ t

By induction, we have terms Γ ⊢ u : σ → τ and Γ, z : σ → τ, x : σ, Γ_{i} ⊢ u_{i}[z, x] : σ_{i} such that

Γ ⊢ let z : σ → τ be u in λx : σ.t′[u_{i}[z, x], x, zx] = t

so Γ ⊢ λx : σ.t′[u_{i}[u, x], x, ux] = t.

Hence we have terms

Γ, x : σ ⊢ ux : τ
Γ, x : σ, y : τ, Γ_{i} ⊢ u_{i}[u, x] : σ_{i}

for which

Γ ⊢ λx : σ.(let y : τ be ux in t′[u_{i}[u, x], x, y]) = t

and so we can refine the left term in a standard sequence.

This lemma tells us that if a refinement is possible, then there exists a ‘standard refinement sequence’ of this form.

Remark 4.1 Note that this lemma only holds if the axioms of applied theories only involve determined equations, t =_{τ} t′. If a theory has constants k_{1}, k_{2}, k_{3} : τ and axiom let b : boolin (if b then k_{1} else k_{2}) ⊑_{τ} k_{3}, then we cannot find a specific t : bool such that if t then k_{1} else k_{2} =_{τ} k_{3}.

Theorem 4.2 (Completeness of equational system) If all types are inhabited, then Γ ⊢ r ⊑_{τ} r′ iff Γ ⊨ r ⊑_{τ} r′

Proof : We give a sketch of the proof. The idea is to construct a minimal term model for our signature of ground types, constants and equational assumptions (with no empty types).

1. Fix an infinite context Γ_{∞} with an infinite number of variables at each type. We use Γ_{∞} in judgements to mean some finite Γ′ ⊆ Γ_{∞}.

2. Define A^{τ} as the set of =_{τ} -equivalence classes of open determined terms of type τ, that is, A^{τ} = {[t]^{τ} | Γ_{∞} ⊢ t : τ}. The projection, application and constant interpretation mappings are interpreted syntactically. Since provable equality is a logical equivalence relation, this forms a Henkin model [6]. A^{τ} is nonempty since we have variables at each type.

To see that the model satisfies the factoring condition, suppose h; f̄ = f̄′, where f = [x : σ ⊢ t[x] : τ′] and f′ = [y : τ ⊢ t′[y] : τ′]. This says that for all terms u′ : τ there exists a term h(u′) : σ such that t[h(u′)] = t′[u′]. In particular then, for the variable y : τ, there exists some term u[y] : σ such that t[u[y]] = t′[y]. We can define g to be λy : τ.u[y], and then ḡ; f̄ = f̄′.

3. Prove that ⟦Γ ⊢ r : τ⟧(g) = {[t]^{τ} | Γ_{∞} ⊢ r[g/Γ] ⊑_{τ} t}, where r[g/Γ] has the obvious meaning. The ?_{σ} case uses Lemma 3.3. We prove the let z : σ be r in r′ case.

The interpretation is

⟦Γ ⊢ let z : σ be r in r′⟧(g) = ⋃_{a∈⟦Γ⊢r:σ⟧(g)}⟦Γ, z : σ ⊢ r′⟧⟨g, a⟩
= ⋃_{a∈{[t]|r[g/Γ]⊑t}}{[t′] | r′[g/Γ, a/z] ⊑ t′}

Now t′ is in the set when there exists a t such that r[g/Γ] ⊑ t and r′[g/Γ, t/z] ⊑ t′. Hence (let z : σ be r in r′)[g/Γ] ⊑ t′.

Conversely, if let z : σ be r[g/Γ] in r′[g/Γ] ⊑ t′, then by Lemma 4.2, there exists a t such that r[g/Γ] ⊑ t and r′[g/Γ, t/z] ⊑ t′.

4. Prove that Γ ⊨ r ⊑_{τ} r′ iff Γ ⊢ r ⊑_{τ} r′.

The first three steps are standard in completeness proofs; the fourth is particular to our calculus. To prove it, we first define an ordering r ≲_{τ} r′, for well-formed open terms r : τ, r′ : τ, to mean for all determined open terms t : τ, Γ_{∞} ⊢ r′ ⊑_{τ} t ⇒ Γ_{∞} ⊢ r ⊑_{τ} t. Note that Γ ⊨ r ⊑_{τ} r′, is equivalent to r ≲_{τ} r′. Clearly r ⊑_{τ} r′ ⇒ r ≲_{τ} r′. To get completeness, we need to prove the converse. The crucial step uses the canonical form of refinement terms :

Lemma 4.4 (Refinement mappings) If

let x_{1} : σ_{1}, …, x_{n} : σ_{n} in t ≲_{τ} let y_{1} : τ_{1}, …, y_{m} : τ_{m} in t′

then letting Γ ≡ y_{1} : τ_{1}, …, y_{m} : τ_{m}, for all i = 1 … n, there exists Γ ⊢ t_{i} : σ_{i}, such that Γ ⊢ t[t_{1}/x_{1}, …, t_{n}/x_{n}] =_{τ} t′.

Proof: First of all, note that this can be reduced by repeated pairing to the one variable case. Now if let x : σ in t ≲_{υ} let y : τ in t′, then since let y : τ in t′ ⊑ t′[y], we have let x : σ in t ⊑ t′[y], so by Lemma 4.2, there must exist a term u[y] such that t[u[y]] =_{υ} t′.

Now we can finish the proof of completeness. Suppose r ≲_{τ} r′. We can express this using canonical forms as

let x_{1} : σ, …, x_{n} : σ_{n} in t ≲_{τ} let y_{1} : τ_{1}, …, y_{m} : τ_{m} in t′

so assume r ≡ let x_{1} : σ, …, x_{n} : σ_{n} in t and r′ ≡ let y_{1} : τ_{1}, …, y_{m} : τ_{m} in t. By LET-WEAKEN-REF, r ⊑_{τ} let y_{1} : τ_{1}, …, y_{m} : τ_{m} in r and this refines to let y_{1} : τ_{1}, …, y_{m} : τ_{m} in t[t_{1}/x_{1}, …, t_{n}/x_{n}] using Lemma 4.4. Again by Lemma 4.4, this is equal to let y_{1} : τ_{1}, …, y_{m} : τ_{m} in t′ which equals r′. Hence Γ_{∞} ⊢ r ⊑_{τ} r′, and since types are nonempty we get Γ ⊢ r ⊑_{τ} r′.

Corollary 4.1 If Γ ⊢ r : σ then Γ ⊢ ?_{σ} ⊑_{σ} r.

Corollary 4.2 λ_{?} is a conservative extension of λ^{×→}.

Proof: Both calculi are complete for Henkin models (with the factoring condition), and the determined equation Γ ⊢ t =_{τ} t′ has the same interpretation.

5 Logic

We can consider an auxiliary logic built on top of the equational theory, with judgements

Δ ⊢_{Γ} P

where Δ is a list of propositions, and P a proposition. The meaning is : for all variables in Γ, if each proposition in Δ is true, then P is true.

This combination of logic and refinement is not the same as was mentioned in the brief discussion at the end of Section 1. The idea discussed there is to internalise logic into the stubs themselves. In this section we present an ‘external’ logic for reasoning about refinement.

We should regard the logic as being orthogonal to refinement. Here we use classical first order logic with refinements r ⊑_{τ} r′ as atomic propositions. The propositions of the logic are

P ::= false | P ⊃ P′ | ∀x : τ.P | r ⊑_{τ} r′

These are sufficient to define ∧, ∨, ∃ and ¬. In addition to the rules for refinement, we assume a signature of (extralogical) axioms, which we can take, without loss of generality, to be closed propositions. We write Ax ▷ P when P is in this collection. We only allow equations between determined terms, t =_{τ} t′ (that is, t ⊑_{τ} t′ ∧ t′ ⊑_{τ} t) as axioms. This is a natural restriction, given our intuition of constructing a refinement theory on top of an applied λ^{×→} theory.

The natural deduction rules for the judgement Δ ⊢_{Γ} P of first order logic are given in the appendix. Only the rules for ⊃, ∀ and false are necessary, but we give the derived rules for the other connectives as well. We must also add a rule

{Γ ⊢ r ⊑_{τ} r′ \atop Δ ⊢_{Γ} r ⊑_{τ} r′} (REF)

so that the equational theory is subsumed by the logic.

There are also well-formedness judgements

Γ ⊢ P wf
Γ ⊢ Δ wf

which we omit here.

The interest in studying the logic is that it is complete over the same class of models as the equational theory. After giving a semantics and proving completeness below, we will be able to conclude that refinement can be encoded in the logic using just equality. This does not mean that the notion of refinement is superfluous. Rather, we can consider r ⊑_{τ} r′ to be a useful high-level notation for some proposition with quantifiers.

In Figure 7 we give the interpretation for the propositions. We interpret a proposition in context

⟦Γ ⊢ false⟧ = ∅
⟦Γ ⊢ P ⊃ P′⟧ = {g ⊨ Γ . g ∉ ⟦Γ ⊢ P ⟧ or g ∈ ⟦Γ ⊢ P′⟧
⟦Γ ⊢ ∀x : σ.P ⟧ = {g ⊨ Γ | ∀a ∈ A^{σ}.⟨g, a⟩ ∈ ⟦Γ, x : σ ⊢ P ⟧}
⟦Γ ⊢ r ⊑_{σ} r′⟧ = {g ⊨ Γ | ⟦Γ ⊢ r : σ⟧(g) ⊇ ⟦Γ ⊢ r′ : σ⟧(g)}

Figure 7: Interpretation of well-formed propositions

Γ ⊢ P as the set of environments g ⊨ Γ in which P holds. We say that Δ ⊨_{Γ} P in some model, if for all g ⊨ Γ, if g ⊨ A for each A in Δ, then g ⊨ P. Completeness is with respect to the class of Henkin models (of the applied theory) with the factoring condition.

Theorem 5.1 (Soundness and Completeness of logical system) Δ ⊢_{Γ} P iff Δ ⊨_{Γ} P

Proof: Soundness is straightforward to prove. As for completeness, we do not have a minimal (Henkin) model for the logical system, but nevertheless, we can still use a term model in order to prove deductive completeness, by showing that any consistent theory is satisfiable. For a theory with axioms Ax, we want to show that Δ ⊢_{Γ} P iff Δ ⊨_{Γ} P in all Henkin models of Ax with the factoring condition. We can restrict our attention to closed propositions. We do not assume that types are nonempty.

1. Given Ax, Δ ⊬ P we want to find a Henkin model A such that A ⊨ Ax ∪ Δ ∪ {¬P }.

2. Construct a maximal consistent Henkin theory Δ_{∞} such that Ax ∪ Δ ∪ {¬P } ⊆ Δ_{∞}.

A Henkin^{3} theory, T, is a collection of propositions closed under derivation, such that if the proposition ∃x : τ.P is in T, then P [t/x] is in T for some t : τ. See [10].

Here we extend the definition of Henkin theory with the further condition that if the proposition let x : τ in t ⊑_{σ} let x′ : τ′ in t′ is in T, then there exists a term t′′ : τ′ → τ such that ∀x′ : τ′.t[t′′x′/x] =_{σ} t′ is in T.

The construction of the Henkin theory involves adding constants k_{P} : τ, and axioms P [k_{P}], for each proposition P, for which ∃x : τ.P is in T, and constants f : τ′ → τ and the corresponding axiom, ∀x′ : τ′.t[fx′/x] =_{σ} t′, for every let x : τ in t ⊑_{σ} let x′ : τ′ in t′ in T.

3Nothing to do with Henkin models.

The existence of a maximal consistent Henkin extension of Ax∪Δ∪{¬P } follows using a standard argument from Zorn’s Lemma. See [10] for details. Note that for a maximal consistent theory T and well-formed proposition P, exactly one of P, ¬P is in T.

3. Define an infinite context Γ_{∞} consisting of an infinite number of variables x_{i} : σ for each type σ for which the proposition ∃x : σ.true is in Δ_{∞}.

4. Define a family of relations on open determined terms R_{Δ_{∞}}^{σ}(t, t′) ⟺ Δ_{∞} ⊢_{Γ_{∞}} t =_{σ} t′ and prove it is a logical equivalence relation. See [6] for details.

5. Construct the term model T of the calculus, and prove that ⟦Γ ⊢ r : τ⟧_{T} (g) = {[t]^{τ} | Γ_{∞} ⊢ r[g/Γ] ⊑_{τ} t}.

6. Construct the quotient model A = T /R where A^{τ} is the set of R_{Δ_{∞}}^{τ}-classes, and show that ⟦Γ ⊢ r : τ⟧_{A}(g) = {[t]_{R}^{τ} | Δ_{∞} ⊢_{Γ_{∞}} r[g/Γ] ⊑_{τ} t}. This requires the generalisation of Lemma 4.3 to logical contexts. In contrast with Remark 4.1, this holds because of the construction of the Henkin theory Δ_{∞}.

A is a Henkin model with the factoring condition.

7. Prove that A ⊨ P iff P ∈ Δ_{∞}. The crucial cases are ∃x : τ.P and r ⊑_{τ} r′, which go through by virtue of Δ_{∞} being a Henkin theory. The r ⊑_{σ} r′ case is proven as in Theorem 4.2, with the observation that the appropriate generalisation of Lemma 4.3 holds.

The use of canonical forms in the proof of Theorem 4.2 suggests that we can translate refinement into first order logic, just using equality of determined terms. If we let r^{∘} denote the canonical form of open term r, then if r^{∘} = let x_{1} : σ_{1}, …, x_{n} : σ_{n} in t, and r^{′∘} = let y_{1} : τ_{1}, …, y_{m} : τ_{m} in t′, define (r ⊑_{υ} r′)^{∘} to be ∀y_{1} : τ_{1}, …, y_{m} : τ_{m}.∃x_{1} : σ_{1}, …, x_{n} : σ_{n}.t =_{υ} t′. Then the logical system is a conservative extension of the equational system (which, in turn, is a conservative extension of the simply-typed lambda calculus). Moreover, we have

Corollary 5.1 If all types are inhabited, then Γ ⊢ r ⊑_{τ} r′ iff ⟨⟩ ⊢_{Γ} r ⊑_{τ} r′ iff ⟨⟩ ⊢_{Γ} (r ⊑_{τ} r′)^{∘}.

Proof : Both systems are complete with respect to Henkin models (with the factoring condition), and the statements have the same interpretation.

6 Conclusion

As far as we know, this is the first proof of completeness of any refinement calculus. Though the language we study is very simple, we believe that it captures the essence of program refinement. We plan to extend this to more complicated type theories, the polymorphic lambda calculus offering particular promise as a way of combining data refinement and type theory. We are currently combining the calculus with the calculus of specifications in [2]. This gives a calculus expressive enough to study program development, but still conceptually simple. Another area for development is in restricted calculi more suitable for automation.

We would also be interested to see how this calculus might be usefully combined with work on logical frameworks. The use of logical variables there is an example of underdeterminism.

That the concept of underdeterminism arises both in computing science and in linguistics strengthens our belief that it is an important concept in the study of general informatics.

Acknowledgements

This work has benefited from discussions with my supervisors : Gordon Plotkin, John Power and Marcelo Fiore. The presentation was improved by a number of suggestions from the anonymous referee. Álvaro Moreira made useful comments on drafts.

References

[1] J. Bos. Predicate logic unplugged. In Tenth Amsterdam Colloquium, 1995.

[2] E. Denney. Refinement Types for Specification. In IFIP Working Conference on Programming Concepts and Methods (PROCOMET ’98), Shelter Island, New York, USA, 1998. To appear.

[3] L. Henkin. Completeness in the theory of types. Journal of Symbolic Logic, 15(2), 1950.

[4] C. Hermida and B. Jacobs. Fibrations with indeterminates : Contextual and functional completeness for polymorphic lambda calculi. Mathematical Structures in Computer Science, 5(4), 1995.

[5] Z. Luo and R. Pollack. LEGO Proof Development System : User’s Manual. Technical Report ECS-LFCS-92-211, Department of Computer Science, University of Edinburgh, 1992.

[6] J. Mitchell. Foundations for Programming Languages. Foundations of Computing Series. MIT Press, 1996.

[7] E. Moggi. Notions of computation and monads. Information and Computation, 1, 1991.

[8] C. Morgan. Programming from Specifications. Prentice Hall, 1994.

[9] B. Rosser. On the Consistency of Quine’s New Foundations for Mathematical Logic. Journal of Symbolic Logic, 4, 1939.

[10] D. van Dalen. Logic and Structure. Springer-Verlag, 1994.

A RULES FOR THE LOGIC 22

A Rules for the Logic

Δ ⊢_{Γ} P  (Ax ▷ P)  (AXIOM)
Δ, P ⊢_{Γ} P  (HYP)
\begin{matrix}Δ ⊢_{Γ} P & Δ ⊢_{Γ} Q \\ Δ ⊢_{Γ} P ∧ Q \end{matrix}  (∧-INTRO)
{Δ ⊢_{Γ} P ∧ Q \atop Δ ⊢_{Γ} P}  (∧-ELIM1)
{Δ ⊢_{Γ} P ∧ Q \atop Δ ⊢_{Γ} Q}  (∧-ELIM2)
{Δ ⊢_{Γ} P \atop Δ ⊢_{Γ}⊢ P ∨ Q}  (∨-INTRO1)
{Δ ⊢_{Γ} Q \atop Δ ⊢_{Γ} P ∨ Q}  (∨-INTRO2)
Δ ⊢_{Γ} P ∨ Q Δ, P ⊢_{Γ} R Δ, Q ⊢_{Γ} R

Δ ⊢_{Γ} R (∨-ELIM)

{Δ, P ⊢_{Γ} Q \atop Δ ⊢_{Γ} P ⊃ Q}  (⊃-INTRO)
\begin{aligned}Δ ⊢_{Γ} P & Δ ⊢_{Γ} P ⊃ Q \\ & Δ ⊢_{Γ} Q \end{aligned}  (⊃-ELIM)
\begin{matrix}Δ ⊢_{Γ} ∀x : σ.P & Γ ⊢ t : σ \\ Δ ⊢_{Γ} P [t/x] \end{matrix}  (∀-ELIM)
{Δ ⊢_{Γ,x:σ} P \atop Δ ⊢_{Γ} ∀x : σ.P} x ∉ Δ  (∀-INTRO)
Δ, false ⊢_{Γ} P  (false-ELIM)

Δ, ¬P ⊢_{Γ} false

Δ ⊢_{Γ} P (¬-ELIM) Figure 8: Natural Deduction rules for classical first-order logic