Practical Foundations for Programming Languages

(1)

Practical Foundations for Programming Languages

Robert Harper

Carnegie Mellon University Spring, 2009

[Draft of October 16, 2009 at 18:42.]

(2)

Copyright c2009 by Robert Harper.

The electronic version of this work is licensed under the Cre- ative Commons Attribution-Noncommercial-No Derivative Works 3.0 United States License. To view a copy of this license, visit

http://creativecommons.org/licenses/by-nc-nd/3.0/us/

or send a letter to Creative Commons, 171 Second Street, Suite 300, San Francisco, California, 94105, USA.

(3)

Preface

This is a working draft of a book on the foundations of programming languages. The central organizing principle of the book is that programming language features may be seen as manifestations of an underlying type structure that governs its syntax and semantics. The emphasis, therefore, is on the concept oftype, which codifies and organizes the computational universe in much the same way that the concept ofset may be seen as an organizing principle for the mathematical universe. The purpose of this book is to explain this remark.

This is very much a work in progress, with major revisions made nearly every day. This means that there may be internal inconsistencies as revisions to one part of the book invalidate material at another part. Please bear this in mind!

Corrections, comments, and suggestions are most welcome, and should be sent to the author [email protected].

(4)

(5)

Judgements and Rules

(18)

(19)

Chapter 1

Inductive Definitions

Inductive definitions are an indispensable tool in the study of programming languages. In this chapter we will develop the basic framework of inductive definitions, and give some examples of their use.

1.1 Objects and Judgements

We start with the notion of ajudgement, orassertion, about anobjectof study.

We shall make use of many forms of judgement, including examples such as these:

nnat nis a natural number n= n₁+n₂ nis the sum ofn₁andn₂ aast ais an abstract syntax tree τtype τis a type

e :τ expressionehas typeτ e ⇓v expressionehas valuev

A judgement states that one or more objects have a property or stand in some relation to one another. The property or relation itself is called ajudgement form, and the judgement that an object or objects have that property or stand in that relation is said to be an instanceof that judgement form.

A judgement form is also called apredicate, and the objects constituting an instance are itssubjects.

We will use the meta-variablePto stand for an unspecified judgement form, and the meta-variables a, b, and c to stand for unspecified objects.

We write a Pfor the judgement asserting that Pholds ofa. When it is not important to stress the subject of the judgement, we write J to stand for

(20)

4 1.2 Inference Rules an unspecified judgement. For particular judgement forms, we freely use prefix, infix, or mixfix notation, as illustrated by the above examples, in order to enhance readability.

We are being intentionally vague about the universe of objects that may be involved in an inductive definition. The rough-and-ready rule is that any sort of finite construction of objects from other objects is permissible.

In particular, we shall make frequent use of the construction of compos- ite objects of the form o(a₁, . . . ,a_n), where a₁, . . . , a_n are objects and o is ann-argument operator. This construction includes as a special case the formation ofn-tuples,(a₁, . . . ,a_n), in which the tupling operator is left im- plicit. (In Chapters 6 and 7 we will formalize these and richer forms of objects, called abstract syntax trees.)

1.2 Inference Rules

Aninductive definitionof a judgement form consists of a collection ofrules of the form

J₁ . . . J_k

J (1.1)

in whichJ andJ₁, . . . , J_k are all judgements of the form being defined. The judgements above the horizontal line are called the premises of the rule, and the judgement below the line is called itsconclusion. If a rule has no premises (that is, whenkis zero), the rule is called anaxiom; otherwise it is called aproper rule.

An inference rule may be read as stating that the premises are suffi- cientfor the conclusion: to show J, it is enough to show J₁, . . . ,J_k. When k is zero, a rule states that its conclusion holds unconditionally. Bear in mind that there may be, in general, many rules with the same conclusion, each specifying sufficient conditions for the conclusion. Consequently, if the conclusion of a rule holds, then it is not necessary that the premises hold, for it might have been derived by another rule.

For example, the following rules constitute an inductive definition of the judgementanat:

zeronat (1.2a)

anat

succ(a)nat (1.2b)

These rules specify that a nat holds whenever either a is zero, or a is succ(b) whereb nat. Taking these rules to be exhaustive, it follows that

(21)

1.2 Inference Rules 5 anatiffais a natural number written in unary.

Similarly, the following rules constitute an inductive definition of the judgementatree:

emptytree (1.3a)

a₁tree a2 tree

node(a₁;a₂)tree (1.3b) These rules specify thatatreeholds if eitheraisempty, oraisnode(a₁;a₂), where a₁ treeanda₂ tree. Taking these to be exhaustive, these rules state thatais a binary tree, which is to say it is either empty, or a node consisting of two children, each of which is also a binary tree.

The judgementa=b natdefining equality ofa natandb natis inductively defined by the following rules:

zero=zeronat (1.4a)

a=bnat

succ(a)=succ(b)nat (1.4b) In each of the preceding examples we have made use of a notational convention for specifying an infinite family of rules by a finite number of patterns, or rule schemes. For example, Rule (1.2b) is a rule scheme that determines one rule, called aninstanceof the rule scheme, for each choice of object a in the rule. We will rely on context to determine whether a rule is stated for aspecificobject, a, or is instead intended as a rule scheme specifying a rule for each choice of objects in the rule. (In Chapter 3 we will remove this ambiguity by introducing parameterization of rules by objects.)

A collection of rules is considered to define thestrongestjudgement that isclosed under, orrespects, those rules. To be closed under the rules simply means that the rules are sufficientto show the validity of a judgement: J holdsif there is a way to obtain it using the given rules. To be thestrongest judgement closed under the rules means that the rules are also necessary:

J holdsonly if there is a way to obtain it by applying the rules. The suffi- ciency of the rules means that we may show that J holds byderivingit by composing rules. Their necessity means that we may reason about it using rule induction.

(22)

6 1.3 Derivations

1.3 Derivations

To show that an inductively defined judgement holds, it is enough to ex- hibit aderivationof it. A derivation of a judgement is a finite composition of rules, starting with axioms and ending with that judgement. It may be thought of as a tree in which each node is a rule whose children are derivations of its premises. We sometimes say that a derivation ofJisevidencefor the validity of an inductively defined judgementJ.

We usually depict derivations as trees with the conclusion at the bot- tom, and with the children of a node corresponding to a rule appearing above it as evidence for the premises of that rule. Thus, if

J1 . . . J_k J

is an inference rule and∇₁, . . . ,∇_kare derivations of its premises, then

∇₁ . . . ∇_k

J (1.5)

is a derivation of its conclusion. In particular, ifk=0, then the node has no children.

For example, this is a derivation ofsucc(succ(succ(zero)))nat:

zeronat succ(zero)nat succ(succ(zero))nat succ(succ(succ(zero)))nat .

(1.6)

Similarly, here is a derivation ofnode(node(empty;empty);empty)tree:

emptytree emptytree

node(empty;empty)tree emptytree node(node(empty;empty);empty)tree .

(1.7)

To show that an inductively defined judgement is derivable we need only find a derivation for it. There are two main methods for finding derivations, calledforward chaining, orbottom-up construction, andbackward chaining, ortop-down construction. Forward chaining starts with the axioms and works forward towards the desired conclusion, whereas backward

(23)

1.4 Rule Induction 7 chaining starts with the desired conclusion and works backwards towards the axioms.

More precisely, forward chaining search maintains a set of derivable judgements, and continually extends this set by adding to it the conclusion of any rule all of whose premises are in that set. Initially, the set is empty;

the process terminates when the desired judgement occurs in the set. As- suming that all rules are considered at every stage, forward chaining will eventually find a derivation of any derivable judgement, but it is impos- sible (in general) to decide algorithmically when to stop extending the set and conclude that the desired judgement is not derivable. We may go on and on adding more judgements to the derivable set without ever achiev- ing the intended goal. It is a matter of understanding the global properties of the rules to determine that a given judgement is not derivable.

Forward chaining is undirected in the sense that it does not take account of the end goal when deciding how to proceed at each step. In contrast, backward chaining is goal-directed. Backward chaining search maintains a queue of current goals, judgements whose derivations are to be sought. Initially, this set consists solely of the judgement we wish to derive. At each stage, we remove a judgement from the queue, and consider all rules whose conclusion is that judgement. For each such rule, we add the premises of that rule to the back of the queue, and continue. If there is more than one such rule, this process must be repeated, with the same starting queue, for each candidate rule. The process terminates whenever the queue is empty, all goals having been achieved; any pending consideration of candidate rules along the way may be discarded. As with forward chaining, backward chaining will eventually find a derivation of any derivable judgement, but there is, in general, no algorithmic method for determining in general whether the current goal is derivable. If it is not, we may futilely add more and more judgements to the goal set, never reaching a point at which all goals have been satisfied.

1.4 Rule Induction

Since an inductive definition specifies the strongestjudgement closed under a collection of rules, we may reason about them byrule induction. The principle of rule induction states that to show that a propertyP holds of a judgement J whenever J is derivable, it is enough to show thatP _isclosed under, orrespects, the rules defining J. WritingP(J)to mean that the prop-

(24)

8 1.4 Rule Induction

ertyPholds of the judgement J, we say thatPrespects the rule J₁ . . . J_k

J

ifP(J)holds wheneverP(J₁), . . . ,P(J_k). The assumptionsP(J₁), . . . ,P(J_k) are called theinductive hypotheses, andP(J)is called theinductive conclusion, of the inference.

In practice the premises and conclusion of the rule involve objects that are universally quantified in the inductive step corresponding to that rule.

Thus to show that a propertyP is closed under a rule of the form a₁J₁ . . . a_k J_k

aJ ,

we must show that for every a, a₁, . . . , a_k, if P(a₁J₁), . . . , P(a_k J_k), then P(aJ).

The principle of rule induction is simply the expression of the definition of an inductively defined judgement form as thestrongestjudgement form closed under the rules comprising the definition. This means that the judgement form is both (a) closed under those rules, and (b) sufficient for any other property also closed under those rules. The former property means that a derivation is evidence for the validity of a judgement; the latter means that we may reason about an inductively defined judgement form by rule induction.

IfP(J) is closed under a set of rules defining a judgement form, then so is the conjunction ofPwith the judgement itself. This means that when showingP to be closed under a rule, we may inductively assume not only thatP(J_i)holds for each of the premises J_i, but also that J_i itself holds as well. We shall generally take advantage of this without explicit mentioning that we are doing so.

When specialized to Rules (1.2), the principle of rule induction states that to showP(anat)wheneveranat, it is enough to show:

1. P(zeronat).

2. for everya, ifP(a nat), thenP(succ(a)nat).

This is just the familiar principle ofmathematical inductionarising as a special case of rule induction. The first condition is called thebasis of the induction, and the second is called theinductive step.

Similarly, rule induction for Rules (1.3) states that to show P(atree) wheneveratree, it is enough to show

(25)

1.4 Rule Induction 9

1. P(emptytree).

2. for everya₁anda₂, ifP(a₁ tree)_andP(a₂tree)_{, then}P(node(a₁;a₂)tree)_. This is called the principle oftree induction, and is once again an instance of rule induction.

As a simple example of a proof by rule induction, let us prove that natural number equality as defined by Rules (1.4) is reflexive:

Lemma 1.1. If anat, then a=anat.

Proof. By rule induction on Rules (1.2):

Rule(1.2a) Applying Rule (1.4a) we obtainzero=zeronat.

Rule(1.2b) Assume thata =a nat. It follows thatsucc(a)=succ(a)nat by an application of Rule (1.4b).

As another example of the use of rule induction, we may show that the predecessor of a natural number is also a natural number. While this may seem self-evident, the point of the example is to show how to derive this from first principles.

Lemma 1.2. Ifsucc(a)nat, then anat.

Proof. It is instructive to re-state the lemma in a form more suitable for inductive proof: ifbnatandbissucc(a)for somea, thenanat. We proceed by rule induction on Rules (1.2).

Rule(1.2a) Vacuously true, sincezerois not of the formsucc(−).

Rule(1.2b) We have thatbissucc(b⁰), and we may assume both that the lemma holds forb⁰and thatb⁰ nat. The result follows directly, since if succ(b⁰)=succ(a)for somea, thenaisb⁰.

Similarly, let us show that the successor operation is injective.

Lemma 1.3. Ifsucc(a₁)=succ(a₂)nat, then a₁ =a₂nat.

(26)

10 1.5 Iterated and Simultaneous Inductive Definitions Proof. It is instructive to re-state the lemma in a form more directly amenable to proof by rule induction. We are to show that ifb₁=b₂ natthen if b₁ is succ(a₁)andb₂ issucc(a₂), then a₁= a₂ nat. We proceed by rule induction on Rules (1.4):

Rule(1.4a) Vacuously true, sincezerois not of the formsucc(−_).

Rule(1.4b) Assuming the result forb₁ =b₂nat, and hence that the premise b₁ =b₂ natholds as well, we are to show that ifsucc(b₁)issucc(a₁) andsucc(b₂)issucc(a₂), thena₁= a₂nat. Under these assumptions we have b₁ is a₁ and b₂ isa₂, and so a₁ =a₂ nat is just the premise of the rule. (We make no use of the inductive hypothesis to complete this step of the proof.)

Both proofs rely on some natural assumptions about the universe of objects; see Section1.8on page14for further discussion.

1.5 Iterated and Simultaneous Inductive Definitions

Inductive definitions are often iterated, meaning that one inductive definition builds on top of another. In an iterated inductive definition the premises of a rule

J₁ . . . J_k J

may be instances of either a previously defined judgement form, or the judgement form being defined. For example, the following rules, define the judgementaliststating thatais a list of natural numbers.

nillist (1.8a)

anat blist

cons(a;b)list (1.8b)

The first premise of Rule (1.8b) is an instance of the judgement form anat, which was defined previously, whereas the premiseblistis an instance of the judgement form being defined by these rules.

Frequently two or more judgements are defined at once by a simultaneous inductive definition. A simultaneous inductive definition consists of a

(27)

1.5 Iterated and Simultaneous Inductive Definitions 11 set of rules for deriving instances of several different judgement forms, any of which may appear as the premise of any rule. Since the rules defining each judgement form may involve any of the others, none of the judgement forms may be taken to be defined prior to the others. Instead one must un- derstand that all of the judgement forms are being defined at once by the entire collection of rules. The judgement forms defined by these rules are, as before, the strongest judgement forms that are closed under the rules.

Therefore the principle of proof by rule induction continues to apply, albeit in a form that allows us to prove a property of each of the defined judgement forms simultaneously.

For example, consider the following rules, which constitute a simultaneous inductive definition of the judgements a even, stating that a is an even natural number, andaodd, stating thatais an odd natural number:

zeroeven (1.9a)

aodd

succ(a)even (1.9b)

aeven

succ(a)odd (1.9c)

The principle of rule induction for these rules states that to show simultaneously thatP(aeven)wheneveraevenandP(aodd)wheneveraodd, it is enough to show the following:

1. P(zeroeven);

2. ifP(aodd), thenP(succ(a)even); 3. ifP(aeven), thenP(succ(a)odd).

As a simple example, we may use simultaneous rule induction to prove that (1) ifa even, thena nat, and (2) ifa odd, then a nat. That is, we define the property P by (1)P(aeven)iff a nat, and (2) P(aodd)iff a nat. The principle of rule induction for Rules (1.9) states that it is sufficient to show the following facts:

1. zeronat, which is derivable by Rule (1.2a).

2. Ifanat, thensucc(a)nat, which is derivable by Rule (1.2b).

3. Ifanat, thensucc(a)nat, which is also derivable by Rule (1.2b).

(28)

12 1.6 Defining Functions by Rules

1.6 Defining Functions by Rules

A common use of inductive definitions is to define a function by giving an inductive definition of itsgraphrelating inputs to outputs, and then showing that the relation uniquely determines the outputs for given inputs. For example, we may define the addition function on natural numbers as the relationsum(a;b;c), with the intended meaning thatcis the sum ofaandb, as follows:

bnat

sum(zero;b;b) ^(1.10a) sum(a;b;c)

sum(succ(a);b;succ(c)) ^(1.10b) The rules define a ternary (three-place) relation,sum(a;b;c), among natural numbersa, b, andc. We may show thatcis determined bya andbin this relation.

Theorem 1.4. For every a natand b nat, there exists a unique c nat such that sum(a;b;c).

Proof. The proof decomposes into two parts:

1. (Existence) Ifanatandbnat, then there existscnatsuch thatsum(a;b;c)_. 2. (Uniqueness) Ifa nat,bnat,cnat,c⁰ nat,sum(a;b;c), andsum(a;b;c⁰),

thenc=c⁰ nat.

For existence, letP(anat)be the proposition if b natthen there exists c nat such thatsum(a;b;c). We prove that ifanatthenP(anat)by rule induction on Rules (1.2). We have two cases to consider:

Rule(1.2a) We are to show P(zeronat)_{. Assuming} b natand takingcto beb, we obtainsum(zero;b;c)by Rule (1.10a).

Rule(1.2b) AssumingP(anat), we are to showP(succ(a)nat). That is, we assume that ifb natthen there existscsuch thatsum(a;b;c), and are to show that ifb⁰ nat, then there existsc⁰such thatsum(succ(a);b⁰;c⁰)_. To this end, suppose thatb⁰ nat. Then by induction there existscsuch thatsum(a;b⁰;c). Takingc⁰ =succ(c), and applying Rule (1.10b), we obtainsum(succ(a);b⁰;c⁰), as required.

For uniqueness, we prove thatifsum(a;b;c₁), then ifsum(a;b;c₂), then c₁= c₂ nat by rule induction based on Rules (1.10).

(29)

1.7 Modes 13 Rule(1.10a) We have a = zero and c₁ = b. By an inner induction on the same rules, we may show that ifsum(_zero;b;c₂)_{, then}c₂isb. By Lemma1.1on page9we obtainb=bnat.

Rule(1.10b) We have thata=succ(a⁰)andc₁ =succ(c⁰₁), wheresum(a⁰;b;c⁰₁). By an inner induction on the same rules, we may show that ifsum(a;b;c2), then c₂ =succ(c⁰₂) nat where sum(a⁰;b;c⁰₂). By the outer inductive hypothesisc⁰₁ =c⁰₂natand soc₁ =c₂nat.

1.7 Modes

The statement that one or more arguments of a judgement is (perhaps uniquely) determined by its other arguments is called a mode specification for that judgement. For example, we have shown that every two natural numbers have a sum according to Rules (1.10). This fact may be restated as a mode specification by saying that the judgement sum(_a;_b;_c) _has_mode (∀,∀,∃). The notation arises from the form of the proposition it expresses: for all a nat and for all b nat, there exists c nat such thatsum(a;b;c). If we wish to further specify that cisuniquelydetermined by a andb, we would say that the judgement sum(a;b;c) has mode (∀,∀,∃!), corresponding to the propositionfor all a natand for all b nat, there exists a unique c natsuch that sum(a;b;c). If we wish only to specify that the sum is unique, if it exists, then we would say that the addition judgement has mode(∀,∀,∃^≤¹), corresponding to the propositionfor all anatand for all bnatthere exists at most one cnatsuch thatsum(a;b;c)_.

As these examples illustrate, a given judgement may satisfy several different mode specifications. In general the universally quantified arguments are to be thought of as the inputsof the judgement, and the existentially quantified arguments are to be thought of as itsoutputs. We usually try to arrange things so that the outputs come after the inputs, but it is not es- sential that we do so. For example, addition also has the mode(∀,∃^≤¹,∀), stating that the sum and the first addend uniquely determine the second addend, if there is any such addend at all. Put in other terms, this says that addition of natural numbers has a (partial) inverse, namely subtraction.

We could equally well show that addition has mode (∃^≤¹,∀,∀), which is just another way of stating that addition of natural numbers has a partial inverse.

(30)

14 1.8 Foundations Often there is an intended, or principal, mode of a given judgement, which we often foreshadow by our choice of notation. For example, when giving an inductive definition of a function, we often use equations to in- dicate the intended input and output relationships. For example, we may re-state the inductive definition of addition (given by Rules (1.10)) using equations:

anat

a+zero=anat (1.11a)

a+b=cnat

a+succ(b)=succ(c)nat (1.11b) When using this notation we tacitly incur the obligation to prove that the mode of the judgement is such that the object on the right-hand side of the equations is determined as a function of those on the left. Having done so, we abuse notation, writinga+bfor the uniquecsuch thata+b= cnat.

1.8 Foundations

An inductively judgement form, such asa nat, may be seen as isolating a class of objects,a, satisfying criteria specified by a collection of rules. While intuitively clear, this description is vague in that it does not specify what sorts of things may appear as the subjects of a judgement. Just what isa?

And what, exactly, are the objectszeroandsucc(a)used in the definition of the judgementanat? More generally, what sorts of objects are permissible in an inductive definition?

One answer to these questions is to fix in advance a particular set,U, to serve as theuniverse of discourseover which all judgements are defined. The universe must be rich enough to contain all objects of interest, and must be specified clearly enough to avoid concerns about its existence. Standard practice is to defineUto be a particular set that can be shown to exist using the standard axioms of set theory, and to specify how the various objects of interest are constructed as elements of this set.

But what should we demand of U to serve as a suitable universe of discourse? At the very least it should includelabeled finitary trees, which are trees of finite height each of whose nodes has finitely many children and is labeled with an operatordrawn from some infinite set. An object such assucc(succ(zero)) is a finitary tree with nodes labeledzerohaving no children and nodes labeledsucchaving one child. Similarly, a finite tuple (a₁, . . . ,a_n) may be thought of as a tree whose node is labeled by an n- tuple operator. Finitary trees will suffice for our work, but it is common

(31)

1.9 Exercises 15 to consider alsoregular trees, which are finitary trees in which a child of a node may also be an ancestor of it, andinfinitary trees, which admit nodes with infinitely many children,.

The standard way to show that the universe,U, exists (that is, is prop- erly defined) is to construct it explicitly from the axioms of set theory. This requires that we fix the representation of trees as particular sets, using well- known, but notoriously unenlightening, methods.¹ Instead we shall simply take it as given that this can be done, and takeU to be a suitably rich universe including at least the finitary trees. In particular we assume that U comes equipped with operations that allow us to construct finitary trees as elements ofU, and to deconstruct such elements ofU into an operator and finitely many children.

The advantage of working within set theory is that it settles any wor- ries about the existence of the universe, U. However, it is important to keep in mind that accepting the axioms of set theory is far more dubious, foundationally speaking, than just accepting the existence of finitary trees without recourse to encoding them as sets. Moreover, there is a significant disadvantage to working with sets, namely that abstract sets have no in- trinsic computational content, and hence are of no use to implementation.

Yet it is intuitively clear that finitary trees can be readily implemented on a computer by means that have nothing to do with their set-theoretic encod- ings. Thus we are better off just takingU as our starting point, from both a foundational and computational perspective.

1.9 Exercises

1. Give an inductive definition of the judgementmax(a;b;c)_{, where}anat, bnat, andcnat, with the meaning thatcis the larger ofaandb. Prove that this judgement has the mode(∀,∀,∃!).

2. Consider the following rules, which define the height of a binary tree as the judgementhgt(a;b).

hgt(_empty;zero) ^(1.12a) hgt(a₁;b₁) hgt(a₂;b₂) max(b₁;b₂;b)

hgt(node(a₁;a2);succ(b)) ^(1.12b)

1Perhaps you have seen the definition of the natural number 0 as the empty set,∅, and the numbern+1 as the setn∪ {n}, or the definition of the ordered pairha,bias the set {a,{a,b} }. Similar coding tricks can be used to represent any finitary tree.

(32)

16 1.9 Exercises Prove by tree induction that the judgement hgthas the mode(∀,∃), with inputs being binary trees and outputs being natural numbers.

3. Give an inductive definition of the judgement “∇is a derivation ofJ”

for an inductively defined judgement Jof your choice.

4. Give an inductive definition of the forward-chaining and backward- chaining search strategies.

(33)

Chapter 2

Hypothetical Judgements

Acategoricaljudgement is an unconditional assertion about some object of the universe. The inductively defined judgements given in Chapter 1are all categorical. A hypothetical judgement expresses an entailment between one or more hypothesesand a conclusion. We will consider two notions of entailment, called derivabilityand admissibility. Derivability expresses the stronger of the two forms of entailment, namely that the conclusion may be deduced directly from the hypotheses by composing rules. Admissibility expresses the weaker form, that the conclusion is derivable from the rules whenever the hypotheses are also derivable. Both forms of entailment en- joy the samestructuralproperties that characterize conditional reasoning.

One consequence of these properties is that derivability is stronger than admissibility (but the converse fails, in general). We then generalize the concept of an inductive definition to admit rules that have not only categorical, but also hypothetical, judgements as premises. Using these we may enrich the rules with new axioms that are available for use within a specified premise of a rule.

2.1 Derivability

For a given set, R, of rules, we define thederivability judgement, written J₁, . . . ,J_k `_R K, where eachJ_i andKare categorical, to mean that we may deriveKfrom theexpansionR[J₁, . . . ,J_k]of the rulesRwith the additional axioms

J₁ . . .

J_k .

(34)

18 2.1 Derivability That is, we treat thehypotheses, orantecedents, of the judgement, J₁, . . . ,J_n astemporary axioms, and derive theconclusion, orconsequent, by composing rules in R. That is, evidence for a hypothetical judgement consists of a derivation of the conclusion from the hypotheses using the rules inR.

We use capital Greek letters, frequentlyΓor∆, to stand for a finite collection of basic judgements, and writeR[_Γ] for the expansion of R with an axiom corresponding to each judgement inΓ. The judgementΓ `_R K means thatK is derivable from rules R[_Γ]. We sometimes write `_R _Γ to mean that `_R J for each judgement J in Γ. The derivability judgement J₁, . . . ,J_n`_R Jis sometimes expressed by saying that the rule

J₁ . . . J_n

J (2.1)

isderivablefrom the rulesR.

For example, consider the derivability judgement

anat`_(1.2)succ(succ(a))nat (2.2)

relative to Rules (1.2). This judgement is valid foranychoice of objecta, as evidenced by the derivation

anat succ(a)nat

succ(succ(a))nat , (2.3)

which composes Rules (1.2), starting witha natas an axiom, and ending with succ(succ(a)) nat. Equivalently, the validity of (2.2) may also be expressed by stating that the rule

anat

succ(succ(a))nat (2.4)

is derivable from Rules (1.2).

It follows directly from the definition of derivability that it is stable under extension with new rules.

Theorem 2.1(Uniformity). IfΓ`_R J, thenΓ`_R∪R0 J.

Proof. Any derivation ofJfromR[_Γ]is also a derivation from(R ∪ R⁰)[_Γ], since the presence of additional rules does not influence the validity of the derivation.

(35)

2.1 Derivability 19 Derivability enjoys a number ofstructural propertiesthat follow from its definition, independently of the rules,R, in question.

Reflexivity Every judgement is a consequence of itself: Γ,J `_R J. Each hypothesis justifies itself as conclusion.

Weakening If Γ `_R J, then Γ,K `_R J. Entailment is not influenced by unexercised options.

Exchange IfΓ1,J₁,J2,Γ2 `_R J, thenΓ1,J2,J₁,Γ2 `_R J. The relative ordering of the axioms is immaterial.

Contraction IfΓ,J,J `_R K, thenΓ,J `_R K. We may use a hypothesis as many times as we like in a derivation.

Transitivity IfΓ,K `_R J and Γ `_R K, thenΓ `_R J. If we replace an axiom by a derivation of it, the result is a derivation of its consequent without that hypothesis.

These properties may be summarized by saying that the derivability hypothetical judgement isstructural.

Theorem 2.2. For any rule set, R, the derivability judgementΓ `_R J is structural.

Proof. Reflexivity follows directly from the meaning of derivability. Weak- ening follows directly from uniformity. Exchange and contraction follow from the treatment of the rules,R, as a finite set, for which order does not matter and replication is immaterial. Transitivity is proved by rule induction on the first premise.

In view of the structural properties of exchange and contraction, we regard the hypotheses,Γ, of a derivability judgement as a finite set of assumptions, so that the order and multiplicity of hypotheses does not matter. In particular, when writingΓ as the unionΓ1Γ2 of two sets of hypotheses, a hypothesis may occur inbothΓ1andΓ2. This is obvious whenΓ1andΓ2are given, but when decomposing a givenΓinto two parts, it is well to remem- ber that the same hypothesis may occur in both parts of the decomposition.

(36)

20 2.2 Admissibility

2.2 Admissibility

Admissibility, writtenΓ |=_R J, is a weaker form of hypothetical judgement stating that`_R _Γ_implies`_R J. That is, the conclusion J is derivable from rules R whenever the assumptions Γ are all derivable from rules R. In particular if any of the hypotheses arenotderivable relative toR, then the judgement is vacuously true. The admissibility judgement J₁, . . . ,J_n |=_R J is sometimes expressed by stating that the rule,

J₁ . . . Jn

J ,

(2.5) isadmissiblerelative to the rules inR.

For example, the admissibility judgement

succ(a)nat|=_(1.2) anat (2.6) is valid, because any derivation ofsucc(a)natfrom Rules (1.2) must contain a sub-derivation ofa natfrom the same rules, which justifies the conclusion. The validity of (2.6) may equivalently be expressed by stating that the rule

succ(a)nat

anat (2.7)

is admissible for Rules (1.2).

In contrast to derivability the admissibility judgement isnotstable under extension to the rules. For example, if we enrich Rules (1.2) with the axiom

succ(junk)nat (2.8)

(wherejunk is some object for whichjunk nat is not derivable), then the admissibility (2.6) is invalid. This is because Rule (2.8) has no premises, and there is no composition of rules derivingjunk nat. Admissibility is as sensitive to which rules are absentfrom an inductive definition as it is to which rules arepresentin it.

The structural properties of derivability given by Theorem2.2 on the preceding page ensure that derivability is stronger than admissibility.

Theorem 2.3. IfΓ`_R J, thenΓ|=_R J.

Proof. Repeated application of the transitivity of derivability shows that if Γ`_R Jand`_R_{Γ, then}`_R J.

(37)

2.2 Admissibility 21 To see that the converse fails, observe that there is no composition of rules such that

succ(junk)nat`_(1.2)junknat, yet the admissibility judgement

succ(junk)nat|=_(1.2)junknat

holds vacuously.

Evidence for admissibility may be thought of as a mathematical function transforming derivations∇₁, . . . ,∇_nof the hypotheses into a derivation ∇ of the consequent. Therefore, the admissibility judgement enjoys the same structural properties as derivability, and hence is a form of hypothetical judgement:

Reflexivity IfJis derivable from the original rules, thenJis derivable from the original rules: J |=_R J.

Weakening If J is derivable from the original rules assuming that each of the judgements inΓare derivable from these rules, thenJmust also be derivable assuming thatΓand alsoKare derivable from the original rules: ifΓ|=_R J, thenΓ,K|=_R J.

Exchange The order of assumptions in an iterated implication does not matter.

Contraction Assuming the same thing twice is the same as assuming it once.

Transitivity IfΓ,K|=_R JandΓ|=_RK, thenΓ|=_R J. If the assumptionKis used, then we may instead appeal to the assumed derivability ofK.

Theorem 2.4. The admissibility judgementΓ|=_R J is structural.

Proof. Follows immediately from the definition of admissibility as stating that if the hypotheses are derivable relative toR, then so is the conclusion.

Just as with derivability, we may, in view of the properties of exchange and contraction, regard the hypotheses,Γ, of an admissibility judgement as a finite set, for which order and multiplicity does not matter.

(38)

22 2.3 Hypothetical Inductive Definitions

2.3 Hypothetical Inductive Definitions

It is useful to enrich the concept of an inductive definition to permit rules with derivability judgements as premises and conclusions. Doing so per- mits us to introducelocal hypothesesthat apply only in the derivation of a particular premise, and also allows us to constrain inferences based on the global hypothesesin effect at the point where the rule is applied.

Ahypothetical inductive definition consists of a collection ofhypothetical rulesof the form

Γ Γ1` J₁ . . . Γ Γn` Jn

Γ` J . (2.9)

The hypothesesΓ are theglobal hypothesesof the rule, and the hypotheses Γi are thelocal hypothesesof theith premise of the rule. Informally, this rule states thatJ is a derivable consequence ofΓwhenever eachJ_iis a derivable consequence ofΓ, augmented with the additional hypothesesΓi. Thus, one way to show that J is derivable fromΓ is to show, in turn, that each J_i is derivable from Γ Γi. The derivation of each premise involves a “context switch” in which we extend the global hypotheses with the local hypotheses of that premise, establishing a new set of global hypotheses for use within that derivation.

Often a hypothetical rule is given for each choice of global context, without restriction. In that case the rule is said to be pure, because it applies irrespective of the context in which it is used. A pure rule, being stated uniformly for all global contexts, may be given inimplicitform, as follows:

Γ1` J₁ . . . Γn` J_n

J . (2.10)

This formulation omits explicit mention of the global context in order to focus attention on the local aspects of the inference.

Sometimes it is necessary to restrict the global context of an inference, so that it applies only if a specifiedside conditionis satisfied. Such rules are said to beimpure. Impure rules generally have the form

Γ Γ1 ` J₁ . . . Γ Γn ` J_n Ψ

Γ` J , (2.11)

where the condition, Ψ, limits the applicability of this rule to situations in which it is true. For example, Ψ may restrict the global context of the inference to be empty, so that no instances involving global hypotheses are permissible.

(39)

2.4 Exercises 23 A hypothetical inductive definition is to be regarded as an ordinary inductive definition of a formal derivability judgement Γ ` J consisting of a finite set of basic judgements, Γ, and a basic judgement, J. A collection of hypothetical rules, R, defines thestrongestformal derivability judgement closed under rules R, which, by a slight abuse of notation, we write as Γ`_R J.

Since Γ `_R J is the strongest judgement closed under R, the principle ofhypothetical rule inductionis valid for reasoning about it. Specifically, to show that P(_Γ ` J)whenever Γ `_R J, it is enough to show, for each rule (2.9) inR,

ifP(_{Γ Γ}₁` J₁)and . . . andP(_{Γ Γ}_n ` J_n), thenP(_Γ` J).

This is just a restatement of the principle of rule induction given in Chap- ter1, specialized to the formal derivability judgementΓ` J.

In many cases we wish to ensure that the formal derivability relation defined by a collection of hypothetical rules is structural. This amounts to showing that the followingstructural rulesbe admissible:

Γ,J ` J (2.12a)

Γ` J

Γ,K` J (2.12b)

Γ` K Γ,K` J

Γ` J (2.12c)

In the common case that the rules of a hypothetical inductive definition are pure, the structural rules (2.12b) and (2.12c) may be easily shown admissible by rule induction. However, it is typically necessary to include Rule (2.12a) explicitly, perhaps in a restricted form, to ensure reflexivity.

2.4 Exercises

1. Prove that if all rules in a hypothetical inductive definition are pure, then the structural rules of weakening (Rule (2.12b)) and transitivity (Rule (2.12c)) are admissible.

2. DefineΓ⁰ `_Γto mean thatΓ⁰ ` J_i for eachJ_i inΓ. Show thatΓ ` J iff wheneverΓ⁰ `Γ, it follows thatΓ⁰ ` J.Hint: from left to right, appeal to transitivity of entailment; from right to left, consider the case of Γ⁰ =_Γ.

(40)

24 2.4 Exercises 3. Show that it is dangerous to permit admissibility judgements in the premise of a rule.Hint: show that using such rules one may “define”

an inconsistent judgement form J for which we have a J iff it isnot the case thata J.

(41)

Chapter 3

Parametric Judgements

Basic judgements express properties of objects of the universe of discourse.

Hypothetical judgements express entailments between judgements, or reasoning under hypotheses.Parametricjudgements express entailments among properties of objects involvingparameters, abstract symbols serving as atomic objects in an expanded universe.

Parameters have a variety of uses: as atomic symbols with no properties other than their identity, and as variables given meaning by substitution, the replacement of a parameter by an object. We shall make frequent use of parametric judgements throughout this book. Parametric inductive definitions, which generalize hypothetical inductive definitions to permit intro- duction of parameters in an inference, are of particular importance in our work.

3.1 Parameters and Objects

We assume given an infinite set ofparameters, which we will consider to be abstract atomic objects that are distinct from all other objects and that can be distinguished from one another (that is, we can tell whether any two given parameters are the same or different).¹It follows that if we are given an object possibly containing a parameter, x, we can rename x to another parameter,x⁰, within that object.

To account for parameters we consider the family U[X]of expansions of the universe of discourse with parameters drawn from the finite setX.

1Parameters are sometimes calledsymbols, atoms, ornamesto emphasize their atomic, featureless character.

(42)

26 3.2 Rule Schemes (The expansion U[_∅] may be identified with the universe, U, of finitary trees discussed in Chapter 1.) The elements of U[X] are finitary trees in which the parameters,X, may occur as leaves. We assume that parameters are distinct from operators so that there can be no confusion between a parameter and an operator that has no children.

Expansion of the universe is monotone in that ifX ⊆ Y_{, then}U[X] ⊆ U[Y], for a tree possibly involving parameters fromX is surely a tree possibly involving parameters fromY. A bijectionπ :X ↔ X⁰between parameter sets induces a renamingπ^† : U[X] ↔ U[X⁰]that, intuitively, replaces each occurrence ofx ∈ X byπ(x) ∈ X⁰ in any element ofU[X], yielding an element ofU[X⁰].

3.2 Rule Schemes

The concept of an inductive definition extends naturally to any fixed expansion of the universe by parameters, X. A collection of rules defined over the expansionU[X]determines the strongest judgement over that expansion closed under these rules. Extending the notation of Chapter2, we write Γ `^X_R J to mean that J is derivable from R[_Γ] over the expansion U[X].

It is often useful to consider rules that are defined over anarbitraryex- pansion of the universe by parameters. Recall Rule (1.2b) from Chapter1:

anat

succ(a)nat (3.1)

As discussed in Chapter1, this is actually arule schemethat stands for an infinite family of rules, called itsinstances, one for each choice of elementa of the universe,U. We extend the concept of rule scheme so that it applies to any expansion of the universe by parameters, so that for each choice of X, we obtain a family of instances of the rule scheme, one for each element aof the expansionU[X].

We will generally gloss over the distinction between a rule and a rule scheme, so that for example Rules (1.2) may be considered over any expansion of the universe by parameters without explicit mention. A collection of such rules defines the strongest judgement over a given expansion closed under all instances of the rule schemes over this expansion. Consequently, we may reason by rule induction as described in Chapter 1over any expansion of the universe by simply reading the rules as applying to objects in that expansion.

(43)

3.3 Parametric Derivability 27

3.3 Parametric Derivability

It will be useful to consider a generalizatiion of the derivability judgement that specifies the parameters, as well as the hypotheses, of a judgement. To a first approximation, theparametric derivabilityjudgement

X |_Γ`_R J (3.2)

means simply thatΓ `^X_R J. That is, the judgement J is derivable from hypotheses Γ over the expansionU[X]. For example, the parametric judgement

{x} |xnat`_(1.2)succ(succ(x))nat (3.3) is valid with respect to Rules (1.2), because the judgementsucc(succ(x))nat is derivable from the assumption x nat in the expansion of the universe with parameterx.

This is the rough-and-ready interpretation of the parametric judgement.

However, the full meaning is slightly stronger than that. In addition to the condition just specified, we also demand that the judgement hold for all renamings of the parameters X, so that the validity of the judgement cannot depend on the exact choice of parameters. To ensure this we define the meaning of the parametric judgement (3.2) to be given by the following condition:

∀π:X ↔ X⁰ π^†Γ`^X_π†⁰Rπ^†J.

Evidence for the judgement (3.2) consists of aparametric derivation,∇_X0, of the judgementπ^†Jfrom rulesπ^†R[π^†Γ]for some bijectionπ:X ↔ X⁰.

For example, judgement (3.3) is valid with respect to Rules (1.2) since, for everyx⁰, the judgement

succ(succ(x⁰))nat

is derivable from Rules (1.2) expanded with the axiomx⁰ nat. Evidence for this consists of the parametric derivation,∇_x⁰,

x⁰ nat succ(x⁰)nat succ(succ(x⁰))nat

(3.4)

composed of Rules (1.2) and the axiomx⁰nat.

Parametric derivability enjoys two structural properties in addition to those enjoyed by the derivability judgement itself:

Practical Foundations for Programming Languages