Consider the expressions 𝟢,𝗌𝗎𝖼(𝟢),𝗌𝗎𝖼(𝗌𝗎𝖼(𝟢)),… A formal claim about one of these expressions is a judgment. A judgment form is a pattern for such claims: the one-place form −𝗇𝖺𝗍 reads “is a numeral.” Filling its place with an expression 𝑎 gives the judgment 𝑎𝗇𝖺𝗍.
𝟢𝗇𝖺𝗍
Nat-Z
𝑎𝗇𝖺𝗍
𝗌𝗎𝖼(𝑎)𝗇𝖺𝗍
Nat-S
A displayed rule has zero or more judgments as premises above the horizontal bar and one judgment as its conclusion below; the small-capital text at the right names it. Thus Nat-Z has no premises and establishes 𝟢𝗇𝖺𝗍. Rule Nat-S establishes 𝗌𝗎𝖼(𝑎)𝗇𝖺𝗍 whenever its premise 𝑎𝗇𝖺𝗍 has been established.
A derivation is a finite tree of rule instances: its root is the conclusion of the final rule, and the immediate subtrees derive that rule’s premises. For example,
𝟢𝗇𝖺𝗍
Nat-Z
𝗌𝗎𝖼(𝟢)𝗇𝖺𝗍
Nat-S
has one leaf, the Nat-Z instance, and root 𝗌𝗎𝖼(𝟢)𝗇𝖺𝗍, the conclusion of the final Nat-S instance. The two displayed rules yield infinitely many numeral judgments. Which judgments have derivations? To prove a property of every numeral, may we inspect its derivation’s final rule, assume the property for each premise derivation, and prove it for the conclusion?
Fix a set O of syntactic objects, the formal expressions that may fill the argument places below. A judgment form of arity 𝑛≥1 is a relation symbol 𝐽 with 𝑛 argument places; a judgment, or instance of 𝐽, is a formal expression 𝐽(𝑎1,…,𝑎𝑛) with 𝑎1,…,𝑎𝑛∈O, called its subjects. We restrict attention to judgment forms with at least one subject. A judgment is still only a formal expression. The rules determine which judgments hold.
For the first examples the syntactic objects are the finite ordered trees freely generated by operators of fixed arity. Examples are 𝟢, 𝗌𝗎𝖼(−), and 𝗇𝗈𝖽𝖾(−;−). “Freely” means that different operators have disjoint images and that every operator is injective in its ordered arguments. Thus, for all syntactic objects 𝑎,𝑏, 𝟢≠𝗌𝗎𝖼(𝑎), and 𝗌𝗎𝖼(𝑎)=𝗌𝗎𝖼(𝑏) implies 𝑎=𝑏. A dash marks an argument place. Semicolons separate arguments of one formal operator; they carry no logical meaning and play the role commas often play in programming notation. For example, every tree built from 𝟢 and 𝗌𝗎𝖼(−) remains a syntactic object when 𝗇𝗈𝖽𝖾(−;−) is also allowed.
Judgment notation may place the relation symbol before, between, or after its subjects. Thus 𝑎𝗇𝖺𝗍 reads “𝑎 is a numeral” and 𝑎𝗂𝗌𝑏 reads “𝑎 is the same numeral as 𝑏.”
A rule over a collection of judgments is a pair of a finite list of judgments 𝐽1,…,𝐽𝑘 (its premises, 𝑘≥0) and a single judgment 𝐽 (its conclusion), displayed
𝐽1⋯𝐽𝑘
𝐽
A rule with no premises is an axiom; a rule setR is a set of rules over a common collection of judgments.
The symbol 𝑎 in Nat-S is a metavariable, a placeholder that ranges over syntactic objects. The displayed rule is a rule scheme: it denotes one rule for every replacement of 𝑎 by a syntactic object. Schemes may also have a side condition, a metalevel restriction such as 𝑎≠𝟢. A side condition restricts the instances of the scheme; it is not one of the judgments being defined. When a proof follows such a finite tree upward, each judgmental premise has a premise subtree to which the proof can be applied recursively. A side condition has no subtree; it is checked only for the chosen rule instance.
Let R be a rule set. A rule-closed set for R is a set 𝑆 of judgments such that for every rule of R with premises 𝐽1,…,𝐽𝑘 and conclusion 𝐽: if 𝐽1,…,𝐽𝑘∈𝑆, then 𝐽∈𝑆. The inductive definition generated by R is the least rule-closed set for R. We denote this set by 𝐼(R); its members are the judgments inductively defined by R.
The intersection of a family of sets contains exactly the objects that belong to every set in the family. Sets are ordered by inclusion, so a rule-closed set is least when it is contained in every other rule-closed set.
Proof. The set of all judgments is closed, so the family of closed sets is nonempty; and if the premises of a rule lie in an intersection of closed sets, its conclusion lies in each of them and hence in the intersection. The intersection of all closed sets is therefore closed, and it is contained in every closed set. ◻
For each nonnegative integer 𝑘, define 𝗌𝗎𝖼0(𝟢)=𝟢 and 𝗌𝗎𝖼𝑘+1(𝟢)=𝗌𝗎𝖼(𝗌𝗎𝖼𝑘(𝟢)). For the rule set R consisting of the two rules displayed at the beginning of the section, put 𝑁={𝗌𝗎𝖼𝑘(𝟢)𝗇𝖺𝗍∣𝑘isanonnegativeinteger}. The set 𝑁 is closed under Nat-Z and Nat-S, so minimality gives 𝐼(R)⊆𝑁. Conversely, Nat-Z followed by 𝑘 uses of Nat-S derives 𝗌𝗎𝖼𝑘(𝟢)𝗇𝖺𝗍, so 𝑁⊆𝐼(R). Thus 𝐼(R)=𝑁.
★☆☆ Find a rule set and two sets of judgments, each closed under it, whose union is not closed. Thus intersection, rather than union, is the operation used in proposition 1.5.
A nonterminal is a placeholder naming the class of expressions being generated. A production is one permitted replacement for that placeholder. In 𝑛::=𝟢∣𝗌𝗎𝖼(𝑛),𝑛 is the nonterminal, and the two productions replace it by 𝟢 or by 𝗌𝗎𝖼(𝑛). Starting from 𝑛, successive replacements can produce 𝑛,𝗌𝗎𝖼(𝑛),𝗌𝗎𝖼(𝗌𝗎𝖼(𝑛)),𝗌𝗎𝖼(𝗌𝗎𝖼(𝟢)). The last expression has no placeholder left. It is generated by the grammar, and its replacement history has the same shape as its derivation built from Nat-Z and Nat-S.
The tree grammar 𝑡::=𝖾𝗆𝗉∣𝗇𝗈𝖽𝖾(𝑡;𝑡) makes the defining restriction visible. After replacing 𝑡 by 𝗇𝗈𝖽𝖾(𝑡;𝑡), either remaining 𝑡 may be replaced by the same two productions; the expression in the other branch does not change the permitted choices. Formally, a context-free grammar consists of finite disjoint sets 𝑁 and Σ, an element 𝑆∈𝑁 called its start symbol, and a finite set of productions 𝐴::=𝑤,𝐴∈𝑁, where 𝑤 is a finite word whose symbols belong to 𝑁∪Σ. The elements of 𝑁 are the nonterminals. The elements of Σ are the terminal symbols that remain in a completed expression. The single nonterminal on the left is the context-free restriction: replacing 𝐴 depends on 𝐴, not on adjacent symbols. A generated word is obtained by starting with 𝑆 and replacing nonterminals until only terminal symbols remain. In the numeral grammar, 𝑁={𝑛}, the start symbol is 𝑛, and the terminal tokens are 𝟢, 𝗌𝗎𝖼, the left parenthesis, and the right parenthesis. Its two productions have right sides 𝟢 and 𝗌𝗎𝖼(𝑛); in the second right side, only 𝑛 is a nonterminal. Thus the generated words are the printed forms of exactly those expressions 𝑎 that have a derivation of 𝑎𝗇𝖺𝗍 from the rules of example 1.6. Their parse trees, which record the successive production choices, become the freely generated syntax trees used above after one relabelling: label the choice 𝑛::=𝟢 by a 𝟢 leaf, and label 𝑛::=𝗌𝗎𝖼(𝑛) by a 𝗌𝗎𝖼 node whose child records the remaining choice. The productions are compact notation for this inductive definition.
Inductive syntax also supports functions defined by recursive calls on smaller syntax trees. The next example isolates the data needed for such a definition. For a set 𝑋, the notation 𝑋𝑘 means the set of ordered 𝑘-tuples of elements of 𝑋. The more general clause below also permits a recursive call on a smaller tree that is not an immediate child. For 𝑋={0,1,2,…}, consider 𝐹(𝟢)=0,𝐹(𝗌𝗎𝖼(𝟢))=1,𝐹(𝗌𝗎𝖼(𝗌𝗎𝖼(𝑎)))=𝐹(𝑎)+2. For a clause at an input tree 𝑟, let 𝑚(𝑟) be its number of recursive calls, let 𝑏𝑖(𝑟) be the input tree of its 𝑖-th recursive call, and let 𝑔𝑟 combine the returned elements of 𝑋. At the third clause above, these data are 𝑚(𝗌𝗎𝖼(𝗌𝗎𝖼(𝑎)))=1,𝑏1(𝗌𝗎𝖼(𝗌𝗎𝖼(𝑎)))=𝑎,𝑔𝗌𝗎𝖼(𝗌𝗎𝖼(𝑎))(𝑛)=𝑛+2. The three disjoint input forms select exactly one clause for every numeral.
Let a syntactic class be the finite trees generated by a grammar. Fix a set 𝑋. For a syntax tree 𝑎, its constructor count|𝑎| is the number of constructor occurrences in 𝑎. For every 𝑘-ary grammar constructor 𝑐, fix an operation 𝑓𝑐:𝑋𝑘→𝑋. There is a unique function 𝐹 on the syntactic class satisfying 𝐹(𝑐(𝑎1,…,𝑎𝑘))=𝑓𝑐(𝐹(𝑎1),…,𝐹(𝑎𝑘)). More generally, suppose that for every syntax tree 𝑎 one natural number 𝑚(𝑎), trees 𝑏1(𝑎),…,𝑏𝑚(𝑎)(𝑎), and exactly one clause are specified, of the form 𝐹(𝑎)=𝑔𝑎(𝐹(𝑏1(𝑎)),…,𝐹(𝑏𝑚(𝑎)(𝑎))),𝑔𝑎:𝑋𝑚(𝑎)→𝑋, and that all recursive arguments satisfy |𝑏𝑖(𝑎)|<|𝑎|(1≤𝑖≤𝑚(𝑎)), Then the clauses determine a unique total function 𝐹. The requirements “exactly one” and 𝑔𝑎:𝑋𝑚(𝑎)→𝑋 are respectively the determinacy and totality conditions on the clauses. Decrease alone is insufficient: the two clauses 𝐹(𝟢)=0 and 𝐹(𝟢)=1 conflict, while omitting a clause for some tree leaves the function undefined there.
Thus 𝑓𝑐 combines the 𝑘 recursively computed child results. For a binary constructor 𝗇𝗈𝖽𝖾(𝑎1;𝑎2), its clause has the programming form 𝐹(𝗇𝗈𝖽𝖾(𝑎1;𝑎2))=𝑓𝗇𝗈𝖽𝖾(𝐹(𝑎1),𝐹(𝑎2)).
Proof of Proposition 1.10 — Structural recursion on syntax
Proof. Here the height of a syntax tree is one for a nullary constructor and one plus the maximum height of its children otherwise. For each 𝑛≥0, define 𝐹𝑛 on the trees of height at most 𝑛. The height-zero domain is empty. At stage 𝑛+1, the unique outer constructor of a tree determines its children, all of height at most 𝑛, so its displayed clause determines 𝐹𝑛+1. The construction leaves the values from earlier stages unchanged. Hence 𝐹(𝑎):=𝐹𝑛(𝑎), for any 𝑛 at least the height of 𝑎, is well defined and satisfies every clause. A second such function agrees at height zero and then at height 𝑛+1 by induction on 𝑛, which proves uniqueness. Height decreases for constructor children, but the general clause assumes only a decrease in constructor count. For that claim, use complete induction on constructor count: at count 𝑛, assume the claim for every count smaller than 𝑛. At a tree 𝑎, every 𝐹(𝑏𝑖(𝑎)) in its unique clause has already been defined, and the total operation 𝑔𝑎 determines one element of 𝑋. A second function satisfying the clauses agrees on every 𝑏𝑖 by the induction hypothesis and therefore agrees at 𝑎. This proves existence, totality, and uniqueness. ◻
For the numeral grammar, take 𝑋={0,1,2,…}, 𝑓𝟢=1, and 𝑓𝗌𝗎𝖼(𝑛)=1+𝑛. The resulting function is constructor count.
The numeral construction recurses on the immediate child of 𝗌𝗎𝖼(𝑎). In the general clause, a recursive argument 𝑏𝑖(𝑎) need only satisfy |𝑏𝑖(𝑎)|<|𝑎|; it need not be an immediate child of 𝑎.
A recursive construction with one total clause for each constructor and recursive calls only on constructor children therefore determines a unique total function by proposition 1.10.
★☆☆ Combinator expressions are generated by the grammar 𝑎::=𝗌∣𝗄∣𝖺𝗉(𝑎1;𝑎2). Display the corresponding rules for a judgment 𝑎𝖼𝗈𝗆𝖻 (remark 1.9), and give an inductive definition of a judgment 𝗅𝖾𝗇(𝑎;𝑛) relating each combinator 𝑎 to the numeral 𝑛 counting the occurrences of 𝗌 and 𝗄 in 𝑎. You may use the metalevel operation 𝑚⊕𝑛, defined recursively by 𝟢⊕𝑛=𝑛 and 𝗌𝗎𝖼(𝑚)⊕𝑛=𝗌𝗎𝖼(𝑚⊕𝑛), in the application rule. “Metalevel” means that ⊕ is an ordinary mathematical operation used while specifying rule instances; it is neither a new judgment nor an additional premise above the bar.
Let R be a rule set. Suppose a rule has premises 𝐽1,…,𝐽𝑘 and conclusion 𝐽. Given derivations D𝑖 of all the premises, place those derivations above an instance of the rule. The resulting finite tree is a derivation of 𝐽. When 𝑘=0, the rule is an axiom and the tree has a single inference. A judgment 𝐽 is derivable from R if some derivation D of 𝐽 exists (written D::𝐽 and read “D is a derivation of 𝐽”). We draw these trees with the root—the conclusion—at the bottom and the premises growing upward. The height of a derivation is ℎ(D):=1+max(ℎ(D1),…,ℎ(D𝑘)), the maximum of the empty list being 0.
Proof. Suppose first that D::𝐽. We use complete (also called strong) induction on ℎ(D). If the final rule has premises 𝐽1,…,𝐽𝑘, its immediate subtrees derive the 𝐽𝑖 and have smaller height. Hence 𝐽1,…,𝐽𝑘∈𝐼(R) by the induction hypothesis. Closure under the final rule gives 𝐽∈𝐼(R).
Conversely, let 𝐷 be the set of derivable judgments. If 𝐽1,…,𝐽𝑘∈𝐷 and R contains the rule 𝐽1,…,𝐽𝑘/𝐽, place the chosen premise derivations above that rule instance. The resulting tree derives 𝐽; thus 𝐷 is closed under R. Minimality gives 𝐼(R)⊆𝐷. ◻
Finiteness alone does not make derivations searchable: the labels and the rule-instance test must also be effective. An effective code for a set 𝑋 is a natural-number representation equipped with a total algorithm 𝖽𝖾𝖼𝗈𝖽𝖾𝑋:ℕ→𝑋∪{𝗂𝗇𝗏𝖺𝗅𝗂𝖽} such that every element of 𝑋 is decoded from some natural number. Thus the decoder halts on every number and either returns one represented object or reports that the number is not a valid code. The property is semidecidable when an algorithm returns yes exactly on the positive instances, terminates with that answer on every positive instance, and may run forever on a negative instance. Such an algorithm has both a soundness obligation—every returned positive answer is correct—and a positive-termination obligation. By contrast, a property is decidable when an algorithm halts on every input and returns yes exactly on the positive instances.
Proof of Proposition 1.14 — Enumeration of derivations
Proof. First construct codes for finite rule-instance trees. Write 𝗇𝗈𝖽𝖾ℓ(𝑇1,…,𝑇𝑘) for a tree whose root label has code ℓ and whose immediate subtrees are 𝑇1,…,𝑇𝑘, in that order. Define its code recursively by 𝖾𝗇𝖼(𝗇𝗈𝖽𝖾ℓ(𝑇1,…,𝑇𝑘)):=1⋯1⏟ℓones01⋯1⏟𝑘ones0𝖾𝗇𝖼(𝑇1)⋯𝖾𝗇𝖼(𝑇𝑘). A parser counts the ones before each of the first two zeroes, then recursively parses the recorded number of subtrees. It accepts a complete code only when no bits remain. For each length 𝑚, listing the 2𝑚 bit strings of length 𝑚 therefore enumerates every finite rule-instance tree.
Given a judgment code for 𝐽, enumerate those bit strings. Skip a string if the parser fails or the total decoder returns 𝗂𝗇𝗏𝖺𝗅𝗂𝖽 for a node label. If a label decodes to an instance with premises 𝐽1,…,𝐽𝑘 and conclusion 𝐽0, require the node to have exactly 𝑘 children and require their root conclusions to have the codes of 𝐽1,…,𝐽𝑘, in that order. Return yes only when the root conclusion has the same code as 𝐽.
Every parser and decoder call halts, so the check of each candidate tree halts. Every returned tree is a derivation of 𝐽, so the procedure is sound. If 𝐽 is derivable, its finite derivation has one of the enumerated bit-string codes; the procedure reaches that code and returns yes. Hence it terminates on every derivable judgment. ◻
Thus the search terminates with a positive answer on every derivable judgment and may continue forever on an underivable one.
★☆☆ Show that 𝗌𝗎𝖼(𝟢)𝗂𝗌𝟢 is not derivable from the rules of example 1.8, and that every derivation of 𝗌𝗎𝖼(𝑎)𝗂𝗌𝗌𝗎𝖼(𝑏) ends with an instance of Is-S; no induction is needed, only inspection of the final rule.
To prove that no malformed object has slipped into the least closed set, we reason according to the rule by which an object was built. This is rule induction: one proves one case for every rule that could conclude the judgment.
Let R be a rule set and let 𝑃 be a property of judgments. Suppose that 𝑃 is closed under R: for every rule instance with premises 𝐽1,…,𝐽𝑘 and conclusion 𝐽, if 𝑃(𝐽1),…,𝑃(𝐽𝑘) all hold, then 𝑃(𝐽) holds. Then 𝑃(𝐽) holds for every judgment 𝐽 derivable from R.
Proof. The set 𝑆={𝐽∣𝑃(𝐽)} is closed under R by hypothesis, so 𝐼(R)⊆𝑆 by minimality (definition 1.4), and every derivable judgment lies in 𝐼(R) by proposition 1.13. ◻
To “proceed by rule induction on D::𝐽” is to apply theorem 1.15 with one case per rule, the assumptions 𝑃(𝐽𝑖) being the induction hypotheses, the properties assumed for the premise derivations of that rule case. This principle concerns a property of the root judgment. A property that genuinely depends on the chosen finite derivation tree instead uses structural induction on that tree, equivalently complete induction on its height as in proposition 1.13. We call both arguments “induction on a derivation,” but state the strengthened property explicitly whenever the distinction matters. Specialized to example 1.6, rule induction is mathematical induction; to example 1.7, induction on binary trees. More generally, structural induction over a syntactic class is rule induction for the rules implicit in its grammar (remark 1.9); we use the two expressions interchangeably. Concretely, one proves one case for each grammar constructor and assumes the property for each immediate syntactic subexpression.
Let R be a rule set and 𝑃 a property of judgments. In each rule case, suppose both that every premise 𝐽𝑖 is derivable and that 𝑃(𝐽𝑖) holds. If these assumptions imply 𝑃(𝐽) for the conclusion, then 𝑃(𝐽) holds for every derivable judgment 𝐽.
Proof of Proposition 1.16 — Strengthened rule induction
Proof. Apply theorem 1.15 to the conjunction 𝑄(𝐽):𝐽isderivableand𝑃(𝐽). Thus 𝑄(𝐽) holds exactly when the two conjuncts in this definition hold. Suppose a rule has premises 𝐽𝑖, and assume 𝑄(𝐽𝑖) for each of them. From their first conjuncts, reapply the rule to derive its conclusion 𝐽. From the second conjuncts, use the assumed closure condition for 𝑃 to obtain 𝑃(𝐽). These are the two conjuncts of 𝑄(𝐽), so rule induction applies. ◻
Proof. Use rule induction with the property: if the subject is 𝗌𝗎𝖼(𝑏), then 𝑏𝗇𝖺𝗍 is derivable. The Nat-Z case is vacuous. In the Nat-S case, the required predecessor judgment is exactly the premise of the final rule. The strengthened rule-induction principle of proposition 1.16 makes that premise derivation available. This case does not use the induction hypothesis. ◻
Proof of Lemma 1.18 — Symmetry of numeral equality
Proof. Apply rule induction to a derivation of 𝑎𝗂𝗌𝑏. For Is-Z, the required conclusion is again 𝟢𝗂𝗌𝟢, obtained by Is-Z. For Is-S, the premise is 𝑎𝗂𝗌𝑏. The inductive hypothesis gives 𝑏𝗂𝗌𝑎, and Is-S gives 𝗌𝗎𝖼(𝑏)𝗂𝗌𝗌𝗎𝖼(𝑎). ◻
★★☆ Prove by rule induction that 𝑎𝗇𝖺𝗍 implies 𝑎𝗂𝗌𝑎. For transitivity, from derivations of 𝑎𝗂𝗌𝑏 and 𝑏𝗂𝗌𝑐, derive 𝑎𝗂𝗌𝑐 by induction on the first derivation and final-rule inspection on the second. Finally prove successor injectivity: from 𝗌𝗎𝖼(𝑎)𝗂𝗌𝗌𝗎𝖼(𝑏) derive 𝑎𝗂𝗌𝑏 by inspecting the final rule.
The list rules exhibit a one-way dependency: they may use the numeral relation as a premise while recursively defining the new list relation. In general, this is an iterated inductive definition: one inductive definition may use a previously completed one. Both old and recursively defined premises are judgmental premises. A side condition, by contrast, merely restricts which rule instances exist (remark 1.3).
The parity rules have a two-way dependency: an even derivation may contain an odd premise, and conversely. More generally, a simultaneous inductive definition uses one collection of rules to generate several judgment forms, and a rule may mention any of the forms in its premises. Their rule-induction principle treats all the forms together. Each premise—whether even or odd—provides the corresponding induction hypothesis.
Proof. Use rule induction with the property that 𝑎𝖾𝗏𝖾𝗇 or 𝑎𝗈𝖽𝖽 is derivable. Case Nat-Z: 𝟢𝖾𝗏𝖾𝗇 by Ev-Z. Case Nat-S: if 𝑎 is even, Od-S derives 𝗌𝗎𝖼(𝑎) as odd; if 𝑎 is odd, Ev-S derives 𝗌𝗎𝖼(𝑎) as even. ◻
Proof of Lemma 1.24 — Parity expressions are numerals
Proof. This is the first use of simultaneous rule induction. For both judgment forms use the property “the subject is a numeral.” There are three cases.
For Ev-Z, rule Nat-Z gives 𝟢𝗇𝖺𝗍. For Ev-S, the premise is 𝑏𝗈𝖽𝖽; its inductive hypothesis gives 𝑏𝗇𝖺𝗍, and Nat-S gives 𝗌𝗎𝖼(𝑏)𝗇𝖺𝗍. For Od-S, use the inductive hypothesis for the even premise and apply the same rule Nat-S. Thus the same induction proves the result for both the even and odd judgments. ◻
Proof. We use simultaneous rule induction. The two properties are 𝑃𝖾(𝑎):𝑎𝗈𝖽𝖽isnotderivable,𝑃𝗈(𝑎):𝑎𝖾𝗏𝖾𝗇isnotderivable. To prove that a judgment is not derivable, assume a derivation and inspect its final rule. A contradiction is obtained when that rule requires a premise excluded by the corresponding induction hypothesis. Here 𝑃𝖾(𝑎) is proved for each derivation of 𝑎𝖾𝗏𝖾𝗇, and 𝑃𝗈(𝑎) for each derivation of 𝑎𝗈𝖽𝖽. A rule case with premise 𝑏𝗈𝖽𝖽 assumes 𝑃𝗈(𝑏), and a rule case with premise 𝑎𝖾𝗏𝖾𝗇 assumes 𝑃𝖾(𝑎). These are the induction hypotheses. There are three rule cases.
For Ev-Z, no rule has conclusion 𝟢𝗈𝖽𝖽, so 𝑃𝖾(𝟢) holds. For Ev-S, the premise is 𝑏𝗈𝖽𝖽 and its inductive hypothesis says that 𝑏𝖾𝗏𝖾𝗇 is not derivable. If 𝗌𝗎𝖼(𝑏)𝗈𝖽𝖽 were derivable, its final rule would have to be Od-S, whose premise is exactly 𝑏𝖾𝗏𝖾𝗇, a contradiction. For Od-S, exchange the two judgment forms and exchange the rule names Ev-S and Od-S. Its premise is 𝑎𝖾𝗏𝖾𝗇, so the induction hypothesis excludes 𝑎𝗈𝖽𝖽; final-rule inspection of a supposed derivation of 𝗌𝗎𝖼(𝑎)𝖾𝗏𝖾𝗇 then selects Ev-S and produces exactly that excluded premise. ◻
The inversion step inspects every rule that could have produced a given conclusion and reads off the premises forced by its outer form; it is the final-rule inspection used in the proof.
★★☆ Prove by final-rule inspection that a derivation of 𝗌𝗎𝖼(𝑎)𝖾𝗏𝖾𝗇 contains a derivation of 𝑎𝗈𝖽𝖽, and a derivation of 𝗌𝗎𝖼(𝑎)𝗈𝖽𝖽 contains a derivation of 𝑎𝖾𝗏𝖾𝗇. Use these inversion facts to give a second proof of lemma 1.25. From either assumed parity derivation first obtain 𝑎𝗇𝖺𝗍 by lemma 1.24; then induct on that numeral derivation and use the inversion facts in the successor case.
Addition of numerals is the judgment 𝗌𝗎𝗆(𝑎;𝑏;𝑐), defined by
𝑏𝗇𝖺𝗍
𝗌𝗎𝗆(𝟢;𝑏;𝑏)
Sum-Z
𝗌𝗎𝗆(𝑎;𝑏;𝑐)
𝗌𝗎𝗆(𝗌𝗎𝖼(𝑎);𝑏;𝗌𝗎𝖼(𝑐))
Sum-S
The judgment 𝗌𝗎𝗆(𝑎;𝑏;𝑐) means that adding 𝑏 to 𝑎 produces 𝑐. The first argument controls the computation: Sum-Z returns 𝑏, and each use of Sum-S adds one successor to the result.
Proof of Lemma 1.27 — Subjects of addition are numerals
Proof. Induct on the sum derivation. A Sum-Z derivation has premise 𝑏𝗇𝖺𝗍 and conclusion 𝗌𝗎𝗆(𝟢;𝑏;𝑏); Nat-Z derives the first subject, and the premise derives both the second and third. A Sum-S derivation has premise 𝗌𝗎𝗆(𝑎;𝑏;𝑐). Its induction hypothesis derives 𝑎𝗇𝖺𝗍, 𝑏𝗇𝖺𝗍, and 𝑐𝗇𝖺𝗍; Nat-S derives the first and third subjects of the conclusion, while 𝑏𝗇𝖺𝗍 is unchanged. ◻
Proof. Use rule induction on the derivation of 𝑎𝗇𝖺𝗍, keeping the derivation of 𝑏𝗇𝖺𝗍 fixed.
For Nat-Z, take 𝑐=𝑏. The required sum is 𝗌𝗎𝗆(𝟢;𝑏;𝑏) by Sum-Z, and 𝑏𝗇𝖺𝗍 is the fixed premise.
For Nat-S, the premise is 𝑎𝗇𝖺𝗍. By the induction hypothesis there is a 𝑐 with 𝑐𝗇𝖺𝗍 and 𝗌𝗎𝗆(𝑎;𝑏;𝑐). Rules Nat-S and Sum-S give respectively 𝗌𝗎𝖼(𝑐)𝗇𝖺𝗍 and 𝗌𝗎𝗆(𝗌𝗎𝖼(𝑎);𝑏;𝗌𝗎𝖼(𝑐)). ◻
Proof. Induct on the first sum derivation and inspect the last rule of the second. If the first derivation ends in Sum-Z, then 𝑎=𝟢 and 𝑐=𝑏. Only Sum-Z can conclude a sum judgment with first argument 𝟢, so the second derivation also has 𝑐′=𝑏.
If the first derivation ends in Sum-S, write its premise as 𝗌𝗎𝗆(𝑎0;𝑏;𝑑); thus 𝑎=𝗌𝗎𝖼(𝑎0) and 𝑐=𝗌𝗎𝖼(𝑑). The second derivation must also end in Sum-S, with a premise 𝗌𝗎𝗆(𝑎0;𝑏;𝑑′) and 𝑐′=𝗌𝗎𝖼(𝑑′). The induction hypothesis gives 𝑑=𝑑′, hence 𝑐=𝑐′. ◻
By totality (proposition 1.28) and single-valuedness (lemma 1.29), each pair 𝑎,𝑏 of numerals has exactly one 𝑐 satisfying 𝗌𝗎𝗆(𝑎;𝑏;𝑐). Thus the relation defined by the two rules is a function on numeral pairs.
★☆☆ Exhibit a derivation of 𝗌𝗎𝗆(𝗌𝗎𝖼(𝗌𝗎𝖼(𝟢));𝗌𝗎𝖼(𝟢);𝗌𝗎𝖼(𝗌𝗎𝖼(𝗌𝗎𝖼(𝟢)))). Delete its final Sum-S. Which judgment remains at the root of the smaller derivation? Explain why this is the premise forced by inversion, not merely one possible way to construct the original tree.
A primitive rule is one of the rules chosen to define a judgment. It may have premises; it is an axiom only when it has none. Suppose a proposed rule is not primitive. We may be able to derive its conclusion while treating its premises as assumptions. Or it may only be the case that whenever all its premises are derivable without assumptions, so is its conclusion. The first property is derivability of a rule; the second is admissibility.
For a rule set R and a finite set Γ of judgments, hypothetical derivability is the relation Γ⊢R𝐽 that holds when 𝐽 is derivable after adjoining, for every 𝐾∈Γ, the zero-premise rule
𝐾
We abbreviate this enlarged rule set by R∪Γ; Γ=∅ adds no hypothesis leaves. Read Γ⊢R𝐽 as “the rules R derive 𝐽 when every judgment in Γ may be used as a hypothesis leaf.” Here Γ,𝐽 abbreviates the unordered finite set Γ∪{𝐽}.
Proof.1. The axiom 𝐽 derives itself. 2. A derivation over R∪Γ is one over R∪Γ∪{𝐾}. 3. Fix a derivation E of 𝐾 from Γ, and induct on the given derivation D of 𝐽 from Γ,𝐾. If the final node is the hypothesis axiom 𝐾, replace it by E. If it is a different hypothesis axiom from Γ, retain it. If it is a primitive rule of R, transform each immediate subderivation by the inductive hypothesis and reapply that rule. The resulting tree derives 𝐽 from Γ alone. ◻
★★☆ Generalize transitivity to simultaneous discharge of finitely many hypotheses: if Γ,𝐾1,…,𝐾𝑛⊢R𝐽 and each Γ⊢R𝐾𝑖, then Γ⊢R𝐽. Give both a proof by repeated use of weakening and proposition 1.31.3 and a single induction that replaces all 𝐾𝑖-axiom nodes at once. For the latter, induct on the derivation of 𝐽 with the property “after replacing every leaf labeled by some 𝐾𝑖 with its fixed derivation from Γ, the transformed tree derives the same root from Γ.”
Let R be a rule set and 𝑟 a candidate rule with premises 𝐽1,…,𝐽𝑘 and conclusion 𝐽. The rule 𝑟 is derivable with respect to R when 𝐽1,…,𝐽𝑘⊢R𝐽: a single derivation of 𝐽 over R from the premises taken as axioms. It is an admissible rule with respect to R when, whenever each of 𝐽1,…,𝐽𝑘 is derivable from R, so is 𝐽. A candidate rule scheme is derivable when every concrete instance is derivable, and admissible when every concrete instance is admissible.
Every rule derivable with respect to R is admissible with respect to R; moreover, a rule derivable with respect to R is derivable with respect to any R′⊇R (stability under extension).
Proof. Take the derivation of 𝐽 from the premise axioms. Replace every occurrence of a premise axiom 𝐽𝑖 by its given derivation without assumptions. Proposition 1.31.3 guarantees that the resulting tree derives 𝐽 without assumptions. For 𝑘=2, the two transitive steps are 𝐽1,𝐽2⊢R𝐽,𝐽2⊢R𝐽1⟹𝐽2⊢R𝐽,𝐽2⊢R𝐽,∅⊢R𝐽2⟹∅⊢R𝐽. The middle derivation is the closed proof of 𝐽1 weakened by 𝐽2. For general 𝑘, eliminate 𝐽1,…,𝐽𝑘 in that order; the 𝑖-th transitivity step uses the derivation already obtained from 𝐽𝑖,…,𝐽𝑘 and the closed proof of 𝐽𝑖, weakened by the remaining hypotheses.
Stability: every non-hypothesis node of the given derivation is an instance of a rule of R and therefore of R′; its hypothesis nodes are unchanged. The same tree is the required derivation over the larger rule set. ◻
Proof of Proposition 1.35 — Admissibility is conservative one-rule extension
Proof. Suppose first that 𝑟 is admissible. The right-to-left implication reuses the same derivation because every rule of R belongs to the extension. For the converse, induct on an R∪{𝑟}-derivation. If its final rule lies in R, transform every premise by the induction hypotheses and reapply that rule. If its final rule is an instance of 𝑟, the induction hypotheses give closed R-derivations of all its premises; by admissibility, its conclusion has a closed R-derivation.
Conversely, assume the displayed equivalence. Fix a concrete instance of 𝑟 whose premises all have closed R-derivations. Reuse those derivations in the extension and apply the added rule once. Its conclusion is therefore derivable over R∪{𝑟}. The right-to-left implication in the displayed equivalence gives a closed R-derivation of that conclusion. This is admissibility of the chosen instance; the instance was arbitrary. ◻
★★☆ Reconstruct both directions of proposition 1.35 for a two-premise rule. In the forward direction, display the final-rule case for the added rule. In the reverse direction, display the one use of the added rule and the reflection step.
With respect to the parity rules of example 1.21, the inversion rule
𝗌𝗎𝖼(𝑎)𝖾𝗏𝖾𝗇
𝑎𝗈𝖽𝖽
Ev-Inv
is admissible—any derivation of 𝗌𝗎𝖼(𝑎)𝖾𝗏𝖾𝗇 ends with Ev-S and so contains a derivation of 𝑎𝗈𝖽𝖽 —but the scheme is not derivable. It suffices to inspect the instance 𝑎=𝟢. From the sole hypothesis 𝗌𝗎𝖼(𝟢)𝖾𝗏𝖾𝗇 one cannot derive 𝟢𝗈𝖽𝖽: neither parity rule concludes 𝟢𝗈𝖽𝖽, so no possible final rule exists. Extend the rule set with the axiom 𝗌𝗎𝖼(𝟢)𝖾𝗏𝖾𝗇: now Ev-Inv is inadmissible, since 𝗌𝗎𝖼(𝟢)𝖾𝗏𝖾𝗇 became derivable while 𝟢𝗈𝖽𝖽 did not. Admissibility is as sensitive to the absent rules as to the present ones; this sensitivity is exactly what proofs by rule induction exploit.
★★☆ Verify the admissibility argument instance by instance, including the fact that a derivation of 𝗌𝗎𝖼(𝑎)𝖾𝗏𝖾𝗇 can only end in Ev-S. Then draw the one-node derivation created by adjoining 𝗌𝗎𝖼(𝟢)𝖾𝗏𝖾𝗇 and explain why the same concrete instance 𝑎=𝟢 destroys admissibility.
The judgment 𝗌𝗎𝗆(𝑎;𝑏;𝑐) computes a result only after its first two subjects have already been recognized as numerals. A program is less orderly: it may contain additions inside additions, and it must specify which unfinished part is evaluated first. We therefore turn the numerals into a small programming language before introducing functions.
Arithmetic expressions are finite trees 𝑒::=𝟢∣𝗌𝗎𝖼(𝑒)∣𝖺𝖽𝖽(𝑒;𝑒). The judgment 𝑒𝗇𝗎𝗆 is generated by
𝟢𝗇𝗎𝗆
Num-Z
𝑛𝗇𝗎𝗆
𝗌𝗎𝖼(𝑛)𝗇𝗎𝗆
Num-S
A numeral is therefore an expression containing no 𝖺𝖽𝖽. A value is an expression designated as a completed result. In this first language the values are exactly the numerals.
Proof of Lemma 1.37 — The two numeral judgments coincide
Proof. Rule induction in either direction re-applies the final rule with the other name. ◻
The two names mark different roles: 𝗇𝖺𝗍 is used by the addition relation, while 𝗇𝗎𝗆 marks values of the arithmetic language. By lemma 1.37, either judgment may be converted to the other when needed.
The judgment 𝑒⟼𝖠𝑒′, read “𝑒 takes one small step to 𝑒′,” is generated by
𝑒⟼𝖠𝑒′
𝗌𝗎𝖼(𝑒)⟼𝖠𝗌𝗎𝖼(𝑒′)
A-Suc
𝑒1⟼𝖠𝑒′1
𝖺𝖽𝖽(𝑒1;𝑒2)⟼𝖠𝖺𝖽𝖽(𝑒′1;𝑒2)
A-Add-L
𝑛1𝗇𝗎𝗆𝑒2⟼𝖠𝑒′2
𝖺𝖽𝖽(𝑛1;𝑒2)⟼𝖠𝖺𝖽𝖽(𝑛1;𝑒′2)
A-Add-R
𝑛2𝗇𝗎𝗆
𝖺𝖽𝖽(𝟢;𝑛2)⟼𝖠𝑛2
A-Add-Z
𝑛1𝗇𝗎𝗆𝑛2𝗇𝗎𝗆
𝖺𝖽𝖽(𝗌𝗎𝖼(𝑛1);𝑛2)⟼𝖠𝗌𝗎𝖼(𝖺𝖽𝖽(𝑛1;𝑛2))
A-Add-S
The first three rules are congruence rules: they allow a step inside a selected subexpression. This use of “congruence” means compatibility of evaluation with a term constructor. The first argument is evaluated before the second. The last two rules perform the addition only after both arguments are numerals.
For example, the first step of 𝖺𝖽𝖽(𝗌𝗎𝖼(𝖺𝖽𝖽(𝟢;𝗌𝗎𝖼(𝟢)));𝟢) is forced by two congruence rules. Read the innermost bar first: the inner addition contracts, that step is lifted through 𝗌𝗎𝖼, and the result is then lifted through the outer addition.
𝟢𝗇𝗎𝗆
Num-Z
𝗌𝗎𝖼(𝟢)𝗇𝗎𝗆
Num-S
𝖺𝖽𝖽(𝟢;𝗌𝗎𝖼(𝟢))⟼𝖠𝗌𝗎𝖼(𝟢)
A-Add-Z
𝗌𝗎𝖼(𝖺𝖽𝖽(𝟢;𝗌𝗎𝖼(𝟢)))⟼𝖠𝗌𝗎𝖼(𝗌𝗎𝖼(𝟢))
A-Suc
𝖺𝖽𝖽(𝗌𝗎𝖼(𝖺𝖽𝖽(𝟢;𝗌𝗎𝖼(𝟢)));𝟢)⟼𝖠𝖺𝖽𝖽(𝗌𝗎𝖼(𝗌𝗎𝖼(𝟢));𝟢)
A-Add-L
The remaining computation is 𝖺𝖽𝖽(𝗌𝗎𝖼(𝗌𝗎𝖼(𝟢));𝟢)𝐴−𝐴𝑑𝑑−𝑆⟼𝖠𝗌𝗎𝖼(𝖺𝖽𝖽(𝗌𝗎𝖼(𝟢);𝟢))𝐴−𝑆𝑢𝑐/𝐴−𝐴𝑑𝑑−𝑆⟼𝖠𝗌𝗎𝖼(𝗌𝗎𝖼(𝖺𝖽𝖽(𝟢;𝟢)))𝐴−𝑆𝑢𝑐2/𝐴−𝐴𝑑𝑑−𝑍⟼𝖠𝗌𝗎𝖼(𝗌𝗎𝖼(𝟢)).
Proof. Use rule induction on 𝑛𝗇𝗎𝗆. No rule concludes a step whose source is 𝟢. If the source is 𝗌𝗎𝖼(𝑛), the only possible final rule is A-Suc, and its premise would be a step from 𝑛, excluded by the induction hypothesis. ◻
Proof. Induct on the first step derivation. The strengthened induction property for a derivation D:𝑒⟼𝖠𝑒1 is 𝑃(D):foreveryderivationE:𝑒⟼𝖠𝑒2,onehas𝑒1=𝑒2. Thus the induction hypothesis can be applied to any competing step from the same immediate subexpression, not merely to a previously chosen one.
For A-Suc, the second derivation can only end in A-Suc. If its argument reduct is 𝑒′2, the induction hypothesis gives 𝑒′1=𝑒′2. Applying the constructor 𝗌𝗎𝖼(−) to both sides gives 𝗌𝗎𝖼(𝑒′1)=𝗌𝗎𝖼(𝑒′2).
For A-Add-L, a competing A-Add-R, A-Add-Z, or A-Add-S derivation would contain a premise saying that the first argument is a numeral. That contradicts lemma 1.39, because the first derivation contains a step from it. Thus the second rule is again A-Add-L. The induction hypothesis gives equality of the two first-argument reducts, hence equality of the two 𝖺𝖽𝖽 targets.
For A-Add-R, both sources have the form 𝖺𝖽𝖽(𝑛1;𝑒2) with 𝑛1𝗇𝗎𝗆. A competing A-Add-L would step from 𝑛1, contrary to lemma 1.39. A competing A-Add-Z or A-Add-S would require 𝑒2𝗇𝗎𝗆, contrary to the step premise of A-Add-R. Thus both derivations end in A-Add-R; the induction hypothesis equates their second-argument reducts, and congruence equates their targets.
For A-Add-Z, the outer form of the first argument excludes A-Add-S; the numeral premises and lemma 1.39 exclude both congruence rules. Only A-Add-Z remains, with the same target. For A-Add-S, the successor-headed first argument excludes A-Add-Z. Its two numeral premises and lemma 1.39 exclude both congruence rules. Both derivations therefore end in A-Add-S, whose target is the same expression 𝗌𝗎𝖼(𝖺𝖽𝖽(𝑛1;𝑛2)). Matching the common source against both A-Add-S conclusions and using injectivity of the free constructors forces the same 𝑛1 and 𝑛2 in the two rule instances. These cases exhaust the rules. ◻
Proof. Induct on the first many-step derivation. For M-Refl, use the second derivation. For M-Step, retain its first one-step premise, compose its many-step tail with the second derivation by the induction hypothesis, and reapply M-Step. ◻
Proof of Lemma 1.44 — Big-step results are numerals
Proof. Induct on the big-step derivation. The AB-Z and AB-S cases use Num-Z and Num-S. In the AB-Add case, lemma 1.27 gives 𝑛3𝗇𝖺𝗍; induction on that derivation, replacing Nat-Z/Nat-S by Num-Z/Num-S, gives 𝑛3𝗇𝗎𝗆. ◻
Proof. Induct on the many-step derivation. The M-Refl case is M-Refl. In the M-Step case, use respectively A-Suc, A-Add-L, or A-Add-R on the first step, apply the induction hypothesis to the tail, and join them with M-Step. ◻
Proof. Use rule induction on the sum derivation. For Sum-Z, the rule premise is 𝑏𝗇𝖺𝗍, so lemma 1.37 gives 𝑏𝗇𝗎𝗆, the premise of A-Add-Z. That rule gives the sole step, and M-Refl closes its target. For Sum-S, write the premise as 𝗌𝗎𝗆(𝑎;𝑏;𝑐). The induction hypothesis gives 𝖺𝖽𝖽(𝑎;𝑏)⟼∗𝖠𝑐, and the conclusion to prove is 𝖺𝖽𝖽(𝗌𝗎𝖼(𝑎);𝑏)⟼∗𝖠𝗌𝗎𝖼(𝑐). By lemma 1.27, lemma 1.37, 𝑎,𝑏𝗇𝗎𝗆. Hence 𝖺𝖽𝖽(𝗌𝗎𝖼(𝑎);𝑏)𝐴−𝐴𝑑𝑑−𝑆⟼𝖠𝗌𝗎𝖼(𝖺𝖽𝖽(𝑎;𝑏))𝐼𝐻+𝑙𝑒𝑚𝑚𝑎1.46⟼∗𝖠𝗌𝗎𝖼(𝑐). ◻
Proof of Theorem 1.48 — Big step implies small steps
Proof. Use rule induction on the big-step derivation. The AB-Z case is M-Refl. The AB-S case follows from the induction hypothesis and the first clause of lemma 1.46.
For AB-Add, lemma 1.44 applied to the first premise gives 𝑛1𝗇𝗎𝗆, as required by the second congruence. The induction hypotheses and the two addition congruences now give 𝖺𝖽𝖽(𝑒1;𝑒2)𝐼𝐻1+𝑙𝑒𝑚𝑚𝑎1.46⟼∗𝖠𝖺𝖽𝖽(𝑛1;𝑒2)𝐼𝐻2+𝑙𝑒𝑚𝑚𝑎1.46⟼∗𝖠𝖺𝖽𝖽(𝑛1;𝑛2)𝑙𝑒𝑚𝑚𝑎1.47⟼∗𝖠𝑛3. ◻
Proof of Proposition 1.49 — Arithmetic always advances or is a numeral
Proof. Use structural induction on 𝑒. Zero is a numeral. For 𝗌𝗎𝖼(𝑒), the induction hypothesis either gives 𝑒𝗇𝗎𝗆, whence Num-S applies, or a step lifted by A-Suc.
Let 𝑒=𝖺𝖽𝖽(𝑒1;𝑒2). If 𝑒1 steps, use A-Add-L. Otherwise the induction hypothesis shows that 𝑒1 is a numeral. If 𝑒2 steps, use A-Add-R; otherwise the induction hypothesis shows that 𝑒2 is a numeral. Final-rule inspection of the first numeral derivation says that it is either 𝟢 or 𝗌𝗎𝖼(𝑛); use A-Add-Z or A-Add-S, respectively. ◻
Fix a countably infinite supply of variables. Raw terms are the formal trees generated by 𝑒::=𝑥∣𝜆𝑥.𝑒∣𝑒𝑒∣𝗍𝗍∣𝖿𝖿∣𝗂𝖿(𝑒;𝑒;𝑒)∣𝟢∣𝗌𝗎𝖼(𝑒)∣𝖺𝖽𝖽(𝑒;𝑒). Variables, abstractions, and applications form the untyped lambda calculus (ULC). Here untyped means that no type judgment restricts which generated trees count as terms: for example, 𝗍𝗍𝖿𝖿 is a raw term even though a Boolean occurs in function position. We extend the ULC grammar with Boolean and arithmetic terms. Application is written by juxtaposition: 𝑒1𝑒2 means “apply 𝑒1 to 𝑒2,” and it associates to the left. The abstraction 𝜆𝑥.𝑒 is read “the anonymous function sending 𝑥 to 𝑒”; it binds 𝑥 in its body. For application, FV(𝑒1𝑒2)=FV(𝑒1)∪FV(𝑒2); the other nonbinding constructors recurse in each argument. The binding clauses are FV(𝑥)={𝑥},FV(𝜆𝑥.𝑏)=FV(𝑏)∖{𝑥}. The constants 𝗍𝗍 and 𝖿𝖿 are the two Boolean values, and 𝗂𝖿(𝑒;𝑒1;𝑒2) selects a branch according to its first argument. Call a term a closed term when its free-variable set is empty. This use of “closed” is distinct from a set of judgments being closed under a rule set. Write Names(𝑒) for all free and bound names in 𝑒. Write BN(𝑒) for its binder labels, defined by BN(𝑥)=∅, BN(𝜆𝑥.𝑏)={𝑥}∪BN(𝑏), and union over the arguments of every nonbinding constructor. Finally, |𝑒| is its number of constructor nodes.
Evaluation must replace a free variable in a function body by an argument. Literal replacement is unsafe: it may turn a free variable in the argument into a bound one. The failure occurs already in one abstraction. Define the raw operation [𝑎/𝑥]naive to replace each free 𝑥 by 𝑎 while recursing under every differently named binder. Its abstraction clause gives (𝜆𝑦.𝑥)[𝑦/𝑥]naive=𝜆𝑦.𝑥[𝑦/𝑥]naive=𝜆𝑦.𝑦. The formerly free inserted 𝑦 has become bound. Capture-avoiding substitution must therefore rename a conflicting binder before inserting the argument.
The following binding-edge diagram records the same failure. Solid edges are syntax-tree edges. A dashed edge runs from a binder to the occurrences it binds, and the boxed node is the free occurrence inserted for 𝑥. Literal replacement moves that node below the binder and thereby creates the dashed edge.
Diagram
The represented equation is (𝜆𝑦.𝑥)[𝑦/𝑥]naive=𝜆𝑦.𝑦; the dashed edge is absent before substitution and present afterward.
If 𝑧∉Names(𝑒), the fresh renaming𝑒⟨𝑧/𝑥⟩ replaces the free occurrences of 𝑥 by 𝑧. Read ⟨𝑧/𝑥⟩ as “rename 𝑥 to fresh 𝑧.” Square brackets [𝑎/𝑥] instead mean insertion of the possibly compound term 𝑎 for 𝑥. The variable and abstraction clauses are 𝑥⟨𝑧/𝑥⟩=𝑧,𝑦⟨𝑧/𝑥⟩=𝑦(𝑦≠𝑥),(𝜆𝑥.𝑏)⟨𝑧/𝑥⟩=𝜆𝑥.𝑏,(𝜆𝑦.𝑏)⟨𝑧/𝑥⟩=𝜆𝑦.𝑏⟨𝑧/𝑥⟩(𝑦≠𝑥). Every other constructor recursively renames each argument.
Let 𝑒 be a raw term and let 𝑥,𝑧 be variables with 𝑧∉Names(𝑒). Then items 1–3 hold for this 𝑒,𝑥,𝑧. Items 4 and 5 hold under the additional hypotheses printed in those items; these hypotheses include every freshness premise required by definition 1.51.
Proof. For items 1–3, prove simultaneously, by structural induction on 𝑒, the three claims for every source 𝑥 and every target 𝑧 outside Names(𝑒). A variable has the two subcases 𝑒=𝑥 and 𝑒≠𝑥. Constants are fixed. For application, conditional, successor, and addition, apply the corresponding induction hypotheses to each immediate argument and then use, respectively, addition of constructor counts and union of free-variable sets.
Let 𝑒=𝜆𝑢.𝑏. If 𝑢=𝑥, fresh renaming stops: size is unchanged, the free-variable formula deletes 𝑥=𝑢 on both sides, and the absent-source premise 𝑥∉FV(𝜆𝑥.𝑏) makes item 3 the defining identity. If 𝑢≠𝑥, then 𝑧∉Names(𝜆𝑢.𝑏) gives 𝑧≠𝑢 and 𝑧∉Names(𝑏). The renaming passes under 𝑢. The three induction hypotheses for 𝑏 give the body size, free-variable, and absent-source equations; reattaching 𝑢 preserves size, and deleting 𝑢 from both free-variable sets gives the required abstraction equations.
For items 4 and 5, use separate structural inductions on 𝑒. Variables, constants, and nonbinding constructors follow from the defining clauses and the induction hypotheses on their immediate arguments.
Here is the composition calculation, including its binder side conditions. If 𝑢=𝑥, the first renaming stops and the second changes nothing because 𝑦∉Names(𝜆𝑥.𝑏); the right-hand renaming also stops. The case 𝑢=𝑦 is excluded by that same freshness condition. Otherwise both renamings pass under 𝑢, and the induction hypothesis on 𝑏 gives 𝜆𝑢.𝑏⟨𝑦/𝑥⟩⟨𝑧/𝑦⟩=𝜆𝑢.𝑏⟨𝑧/𝑥⟩. The case 𝑢=𝑧 is excluded by freshness of the second target. For commutation, the binder is either one of the two source names, in which case that renaming stops and the other passes under the binder, or neither source, in which case both pass under it and the induction hypothesis on 𝑏 applies. Pairwise distinctness and freshness of 𝑧,𝑤 exclude the two target-name cases. These cases exhaust the abstraction clauses. ◻
★☆☆ Let 𝑥,𝑦,𝑧,𝑤 be pairwise distinct, with 𝑤 absent from the displayed terms. Compute (𝜆𝑦.𝑥(𝑦𝑧))⟨𝑤/𝑥⟩and(𝜆𝑥.𝑥𝑦)⟨𝑤/𝑥⟩. For each result, verify the free-variable equation in lemma 1.52 and identify the abstraction clause used.
The tempting two-name clause 𝜆𝑥.𝑏=𝛼?𝜆𝑦.𝑐⟺𝑐=𝑏⟨𝑦/𝑥⟩ is not capture-safe: it would identify 𝜆𝑥.𝑦 with 𝜆𝑦.𝑦. Renaming both binders to a third name fresh for both raw terms avoids that failure.
Alpha-equivalence𝑒=𝛼𝑒′ identifies raw terms that differ only in bound-variable names; it is defined by complete induction on |𝑒|+|𝑒′|. Variables satisfy 𝑥=𝛼𝑦 exactly when 𝑥=𝑦. Two nonbinding operator applications are alpha-equivalent when they have the same operator and their corresponding arguments are alpha-equivalent. Two abstractions satisfy 𝜆𝑥.𝑏=𝛼𝜆𝑦.𝑐 when there is a variable 𝑧, occurring nowhere in either raw term, such that 𝑏⟨𝑧/𝑥⟩=𝛼𝑐⟨𝑧/𝑦⟩. Expressions with different outer constructors are not alpha-equivalent. The common fresh opening makes the two bodies directly comparable while ignoring the spelling of their binders. The recursion is well founded: every compared argument is smaller than its parent, and |𝑏⟨𝑧/𝑥⟩|=|𝑏| by the size clause of lemma 1.52.
The common-opening clause compares two abstractions by sending both binder labels to one fresh name. In the diagram, solid arrows are fresh-renaming operations, and the horizontal double line is the smaller alpha-equivalence comparison that defines the comparison above it.
Diagram
The diagram represents the defining equation 𝜆𝑥.𝑏=𝛼𝜆𝑦.𝑐⟺∃𝑧∉(Names(𝜆𝑥.𝑏)∪Names(𝜆𝑦.𝑐)).𝑏⟨𝑧/𝑥⟩=𝛼𝑐⟨𝑧/𝑦⟩. Its induction measure decreases because |𝑏|+|𝑐|<|𝜆𝑥.𝑏|+|𝜆𝑦.𝑐|. The diagram records this bookkeeping; it does not replace the compatibility proof below.
Thus 𝜆𝑥.𝜆𝑦.𝑥=𝛼𝜆𝑢.𝜆𝑣.𝑢,𝜆𝑥.𝜆𝑦.𝑥⧸=𝛼𝜆𝑢.𝜆𝑣.𝑣. Renaming the outer binders of the first pair to a name 𝑤 fresh for all four binders gives 𝜆𝑦.𝑤 and 𝜆𝑣.𝑤. These terms are alpha-equivalent after opening their inner binders once more.
Proof of Lemma 1.54 — Alpha compatibility and common openings
Proof. For item 1, induct over the defining comparison. For every nonbinding constructor, apply the induction hypothesis to each argument. In the abstraction case, the two opened bodies have the same constructor count by the induction hypothesis and the size clause of lemma 1.52, so the original bodies do also. For free variables, apply the free-variable clause of lemma 1.52 to the common fresh opening and delete the opening name on both sides. The outer constructor is fixed by every defining clause.
For items 2 and 3, the obstruction is a mutual dependency: changing the fresh name in a common opening uses compatibility of renaming, while compatibility under an abstraction uses independence of the common opening. Define two quantified claims. The claim 𝐶0(𝑁) is item 3 for every alpha-equivalent pair of abstractions whose constructor counts sum to 𝑁, for every common opening name fresh for the two complete abstractions. The claim 𝐶1(𝑁) is item 2 for every alpha-equivalent pair whose constructor counts sum to 𝑁, for every source name 𝑥 and every target 𝑧 fresh for the two complete terms. Prove all 𝐶𝑞(𝑁) by complete induction on (𝑁,𝑞)∈ℕ×{0,1}, ordered lexicographically. For 𝑁′<𝑁, the relevant comparisons are (𝑁′,0)<(𝑁,0)becausethefirstcoordinatedecreases,(𝑁′,1)<(𝑁,0)becausethefirstcoordinatedecreases,(𝑁,0)<(𝑁,1)because0<1atfixed𝑁. This order is well founded. Indeed, if a descending sequence lowered the first coordinate infinitely often, it would give an infinite strictly decreasing sequence of natural numbers. Otherwise there is an index after which that coordinate is constant; beyond that index, the second coordinate can decrease from 1 to 0 only once. At the case (𝑁,𝑞), the induction hypothesis contains every 𝐶𝑞′(𝑁′) with (𝑁′,𝑞′)<(𝑁,𝑞). The proof of 𝐶0(𝑁) invokes 𝐶1(𝑁′) only for opened bodies with 𝑁′<𝑁. The abstraction case of 𝐶1(𝑁) first invokes 𝐶0(𝑁), then invokes 𝐶1(𝑁′) for smaller bodies. Thus the induction order records the dependency chain 𝐶1(𝑁′)(𝑁′<𝑁)⟹𝐶0(𝑁)⟹𝐶1(𝑁). These are the only cross-invocations.
Common opening: 𝐶0(𝑁). For item 3, the definition gives a fresh witness 𝑤 with 𝑏⟨𝑤/𝑥⟩=𝛼𝑐⟨𝑤/𝑦⟩. If 𝑤=𝑧, this is already the required conclusion. Otherwise apply the renaming-compatibility induction hypothesis to the smaller bodies with ⟨𝑧/𝑤⟩. The names 𝑥,𝑤,𝑧 are then distinct, and 𝑧 is fresh for both opened bodies, because it occurs in neither original raw term and differs from 𝑤. The composition clause of lemma 1.52 changes the two resulting terms to 𝑏⟨𝑧/𝑥⟩ and 𝑐⟨𝑧/𝑦⟩. Thus the common opening is independent of the witness used in the definition.
Renaming compatibility: 𝐶1(𝑁). For item 2, variables are direct, and each nonbinding constructor follows by applying the induction hypothesis to its arguments. Suppose the compared terms are 𝜆𝑢.𝑏 and 𝜆𝑣.𝑐. Choose 𝑟 fresh for both bodies and their binders, and distinct from 𝑥,𝑧. If 𝑥=𝑧, freshness says that 𝑥 is absent from both complete terms. Hence the absent-source equation gives 𝑒⟨𝑧/𝑥⟩=𝑒and𝑒′⟨𝑧/𝑥⟩=𝑒′, so the desired alpha-equivalence is the hypothesis. Assume henceforth that 𝑥≠𝑧. The common-opening claim gives 𝑏⟨𝑟/𝑢⟩=𝛼𝑐⟨𝑟/𝑣⟩. Apply the renaming-compatibility induction hypothesis to these smaller bodies with ⟨𝑧/𝑥⟩. The following table names the equation used on each side in the four binder cases: 𝑢=𝑥𝑣=𝑥bothabstractionrenamingsstop𝑢=𝑥𝑣≠𝑥absentsourceontheleft;commutationontheright𝑢≠𝑥𝑣=𝑥commutationontheleft;absentsourceontheright𝑢≠𝑥𝑣≠𝑥commutationonbothsides. If neither 𝑢 nor 𝑣 equals 𝑥, the commutation clause of lemma 1.52 commutes the opening and the free renaming: 𝑏⟨𝑟/𝑢⟩⟨𝑧/𝑥⟩=𝑏⟨𝑧/𝑥⟩⟨𝑟/𝑢⟩. The same equation holds for 𝑐 with 𝑢,𝑏 replaced by 𝑣,𝑐, so the abstraction clause with witness 𝑟 proves this case.
If 𝑢=𝑣=𝑥, both abstraction renamings stop, so the original alpha-equivalence is the conclusion. In the mixed case 𝑢=𝑥 and 𝑣≠𝑥, the left abstraction renaming stops. On opened bodies, 𝑥∉FV(𝑏⟨𝑟/𝑥⟩) by the free-variable clause of lemma 1.52; hence its later ⟨𝑧/𝑥⟩ is the identity, while commutation gives 𝑐⟨𝑟/𝑣⟩⟨𝑧/𝑥⟩=𝑐⟨𝑧/𝑥⟩⟨𝑟/𝑣⟩. Thus 𝑟 witnesses alpha-equivalence of the renamed abstractions. The other mixed case 𝑢≠𝑥 and 𝑣=𝑥 uses the same two equations on the opposite bodies: commutation on 𝑏 and the absent-source equation on 𝑐⟨𝑟/𝑥⟩. These four binder cases exhaust item 2. ◻
★☆☆ Let 𝑒=𝜆𝑥.𝜆𝑦.𝑥 and 𝑒′=𝜆𝑢.𝜆𝑣.𝑢. Choose 𝑤 outside Names(𝑒)∪Names(𝑒′), compute the two outer openings, then choose 𝑟∉Names(𝜆𝑦.𝑤)∪Names(𝜆𝑣.𝑤) and compute the inner openings. Use the variable and abstraction clauses of definition 1.53 to derive 𝑒=𝛼𝑒′. Explain why choosing 𝑤=𝑦 would not meet the common opening hypothesis.
For all raw terms 𝑒,𝑒′,𝑒″, alpha-equivalence is reflexive (𝑒=𝛼𝑒), symmetric (𝑒=𝛼𝑒′⇒𝑒′=𝛼𝑒), and transitive (𝑒=𝛼𝑒′∧𝑒′=𝛼𝑒″⇒𝑒=𝛼𝑒″). These three properties make it an equivalence relation. It preserves constructor count, outer constructor, and free variables. It is a congruence: replacing any immediate argument of a term constructor by an alpha-equivalent term preserves alpha-equivalence of the whole term.
Proof of Proposition 1.55 — Alpha-equivalence is an equivalence relation
Proof. Reflexivity is induction on syntax; symmetry is induction on the given alpha-equivalence comparison. For reflexivity of an abstraction 𝜆𝑥.𝑏, choose 𝑧∉Names(𝜆𝑥.𝑏) and open both copies with 𝑧. The induction hypothesis gives 𝑏=𝛼𝑏, and lemma 1.54(2) transports it to 𝑏⟨𝑧/𝑥⟩=𝛼𝑏⟨𝑧/𝑥⟩, as required by the abstraction clause. Symmetry uses the same witness in the opposite order.
For transitivity, use complete induction on the common constructor count, which exists by lemma 1.54(1). In the abstraction case suppose 𝜆𝑥.𝑏=𝛼𝜆𝑦.𝑐 and 𝜆𝑦.𝑐=𝛼𝜆𝑢.𝑑. Choose one name 𝑤 fresh for all three raw terms. Lemma 1.54(3) gives 𝑏⟨𝑤/𝑥⟩=𝛼𝑐⟨𝑤/𝑦⟩,𝑐⟨𝑤/𝑦⟩=𝛼𝑑⟨𝑤/𝑢⟩. The complete-induction hypothesis applies to these smaller bodies; their transitivity and the abstraction clause yield 𝜆𝑥.𝑏=𝛼𝜆𝑢.𝑑. For a nonbinding constructor, apply the induction hypothesis to every argument. Every defining clause preserves the outer constructor. Those same clauses prove congruence for nonbinding constructors; the common-opening abstraction clause and lemma 1.54(2) prove it for abstraction. ◻
The avoid set must grow between siblings. For example, clean the left child of (𝜆𝑥.𝑥)(𝜆𝑦.𝑦) against a finite set 𝑋, obtaining 𝜆𝑝.𝑝 with 𝑝∉𝑋. Clean the right child against 𝑋∪{𝑝}, obtaining 𝜆𝑞.𝑞. Then 𝑞∉𝑋∪{𝑝}, so the rebuilt application has two distinct binder labels, both outside 𝑋. Cleaning both children independently against 𝑋 would not force 𝑝≠𝑞.
Proof of Lemma 1.56 — Fresh representatives and common opening
Proof. Strengthen the first clause before applying complete induction on |𝑒|: for every finite avoid set 𝑋, construct 𝑒𝑋 with all three stated properties. The induction hypothesis is available for every smaller raw term and every finite avoid set.
For a nonbinding constructor with immediate subterms 𝑒1,…,𝑒𝑘, process the children from left to right. Set 𝑋0=𝑋. After constructing (𝑒𝑖)𝑋𝑖−1, set 𝑋𝑖=𝑋𝑖−1∪BN((𝑒𝑖)𝑋𝑖−1). The induction hypothesis says that the 𝑖-th child’s binder labels avoid 𝑋𝑖−1. Hence they avoid 𝑋 and every earlier child’s binder labels. Rebuilding the constructor preserves alpha-equivalence by congruence and makes all sibling binder-label sets pairwise disjoint.
For an abstraction 𝑒=𝜆𝑥.𝑏, choose 𝑧∉𝑋∪Names(𝑏)∪{𝑥} and set 𝑏𝑧=𝑏⟨𝑧/𝑥⟩. Since |𝑏𝑧|=|𝑏|<|𝜆𝑥.𝑏|, apply the strengthened induction hypothesis to 𝑏𝑧 with avoid set 𝑋∪{𝑧}. It gives a raw term 𝑐 with 𝑏𝑧=𝛼𝑐, distinct binder labels, and BN(𝑐)∩(𝑋∪{𝑧})=∅. Choose 𝑟∉Names(𝑏)∪Names(𝑏⟨𝑧/𝑥⟩)∪Names(𝑐)∪{𝑥,𝑧}. Compatibility of 𝑏𝑧=𝛼𝑐 with ⟨𝑟/𝑧⟩ and fresh-renaming composition give 𝑏⟨𝑟/𝑥⟩=𝛼𝑐⟨𝑟/𝑧⟩. The abstraction clause therefore relates 𝜆𝑥.𝑏 to 𝜆𝑧.𝑐. The outer label 𝑧 avoids 𝑋, the inner labels avoid 𝑋∪{𝑧}, and the induction hypothesis already makes the inner labels pairwise distinct. Thus all labels in 𝜆𝑧.𝑐 are distinct and avoid 𝑋, completing the strengthened induction.
The alpha-equivalence class of a raw term 𝑒, written [𝑒], is the set of all raw terms alpha-equivalent to 𝑒. A quotient term is one such class. Henceforth terms are quotient terms, and each written raw expression denotes one representative of its class. By lemma 1.56, before a calculation we may choose a representative whose bound names avoid any specified finite collection of names. In particular, given raw terms 𝑎1,…,𝑎𝑘 and variables 𝑥1,…,𝑥𝑚, we may require all binders to avoid the finite set Names(𝑎1)∪⋯∪Names(𝑎𝑘)∪{𝑥1,…,𝑥𝑚}. Ordinary equality = compares these quotient terms; 𝑟=𝛼𝑠 continues to compare the explicitly named raw representatives 𝑟 and 𝑠.
Let 𝐸 be a quotient term, let 𝑥,𝑧 be variables, and suppose 𝑧∉FV(𝐸). Here FV(𝐸) is the common free-variable set of the representatives of 𝐸, whose equality follows from lemma 1.54(1). Choose a raw representative 𝑟∈𝐸 with 𝑧∉Names(𝑟), and define 𝐸⟨𝑧/𝑥⟩:=[𝑟⟨𝑧/𝑥⟩]. Such a representative exists: lemma 1.56 moves all bound names away from 𝑧, while lemma 1.54(1) gives FV(𝑟)=FV(𝐸). If 𝑟,𝑠∈𝐸 are two representatives with 𝑧 fresh for both, then lemma 1.54(2) gives 𝑟⟨𝑧/𝑥⟩=𝛼𝑠⟨𝑧/𝑥⟩. Hence the displayed alpha-class is independent of the representative.
Capture-avoiding substitution inserts a term without turning its free variables into bound occurrences. By lemma 1.56, choose a representative of 𝑒 whose bound names are pairwise distinct and avoid FV(𝑎)∪{𝑥}. On this representative define 𝑒[𝑎/𝑥] structurally: 𝑥[𝑎/𝑥]=𝑎,𝑦[𝑎/𝑥]=𝑦(𝑦≠𝑥),(𝜆𝑦.𝑏)[𝑎/𝑥]=𝜆𝑦.𝑏[𝑎/𝑥],(𝑒1𝑒2)[𝑎/𝑥]=𝑒1[𝑎/𝑥]𝑒2[𝑎/𝑥]. The abstraction equation assumes 𝑦≠𝑥; the chosen representative also has 𝑦∉FV(𝑎). There is no separate shadowing equation on the chosen representative: a source binder named 𝑥 has already been alpha-renamed away from 𝑥, and the abstraction equation returns an alpha-equivalent copy of that binder and body. For a conditional, successor, or addition, substitute recursively in each immediate subterm. Substitution fixes the three constants 𝗍𝗍, 𝖿𝖿, and 𝟢. The resulting alpha-equivalence class is 𝑒[𝑎/𝑥].
This representative choice repairs the failed literal calculation at the start of the section. Capture avoidance first chooses 𝑧∉{𝑥,𝑦}: (𝜆𝑦.𝑥)[𝑦/𝑥]=(𝜆𝑧.𝑥)[𝑦/𝑥]=𝜆𝑧.𝑦. The first equality is equality of alpha-classes; on the two displayed raw representatives, the corresponding structural substitution outputs are alpha-equivalent.
The substitution-composition equation below says that performing the 𝑥-substitution before the 𝑦-substitution requires updating the inserted term 𝑎 by that later substitution. For distinct 𝑥,𝑦,𝑧, (𝑥𝑦)[𝑧/𝑥][𝗍𝗍/𝑦]=𝑧𝗍𝗍=(𝑥𝑦)[𝗍𝗍/𝑦][𝑧[𝗍𝗍/𝑦]/𝑥]. The condition 𝑥≠𝑦 keeps the two replacement sites distinct, and 𝑥∉FV(𝑐) prevents the right-hand 𝑥-substitution from rewriting inside the term 𝑐 inserted by the first step.
The abstraction case of representative independence needs one interchange equation. It is proved on raw representatives before substitution is passed to alpha-equivalence classes.
Let 𝑏 and 𝑎 be raw representatives, and let 𝑥,𝑢,𝑧 be pairwise distinct. Suppose every binder of 𝑏 avoids {𝑥,𝑢}∪FV(𝑎), suppose 𝑢∉FV(𝑎), and suppose 𝑧∉Names(𝑏)∪Names(𝑎). Then 𝑏⟨𝑧/𝑢⟩[𝑎/𝑥]=𝛼𝑏[𝑎/𝑥]⟨𝑧/𝑢⟩.
Proof of Lemma 1.59 — Fresh opening commutes with substitution
Proof. Use structural induction on 𝑏. For the variable 𝑢, both sides are 𝑧. For the variable 𝑥, the left side is 𝑎; the right side is 𝑎⟨𝑧/𝑢⟩=𝑎 by the absent-source equation and 𝑢∉FV(𝑎). Every other variable and every constant is fixed. Each nonbinding constructor follows by applying the induction hypothesis to its immediate subterms.
For an abstraction 𝜆𝑟.𝑐, the representative choice gives 𝑟∉{𝑥,𝑢,𝑧}∪FV(𝑎). Opening and substitution therefore both pass under 𝑟. The induction hypothesis gives 𝑐⟨𝑧/𝑢⟩[𝑎/𝑥]=𝛼𝑐[𝑎/𝑥]⟨𝑧/𝑢⟩, and abstraction congruence reattaches 𝜆𝑟. ◻
The alpha-class in definition 1.58 is independent of the chosen representative of 𝑒 whose binders are pairwise distinct and avoid FV(𝑎)∪{𝑥}, and of the representative of 𝑎. Moreover:
if 𝑥∉FV(𝑒), then 𝑒[𝑎/𝑥]=𝑒;
if 𝑥∈FV(𝑒), then FV(𝑒[𝑎/𝑥])=(FV(𝑒)∖{𝑥})∪FV(𝑎);
if 𝑟 is a raw representative of 𝑒 and 𝑧∉Names(𝑟), then substitution by 𝑧 agrees with fresh renaming of that representative: 𝑒[𝑧/𝑥]=[𝑟⟨𝑧/𝑥⟩];
if 𝑥≠𝑦 and 𝑥∉FV(𝑐), then 𝑒[𝑎/𝑥][𝑐/𝑦]=𝑒[𝑐/𝑦][𝑎[𝑐/𝑦]/𝑥].
Proof of Proposition 1.60 — Substitution is well defined
Proof.Independence of the source representative. For independence of the representative of 𝑒, use complete induction on the common constructor count of alpha-equivalent representatives; its equality follows from proposition 1.55. Hold the representative of 𝑎 fixed. Variables and constants are direct, and nonbinding constructors use congruence after the induction hypotheses. For abstractions 𝜆𝑢.𝑏=𝛼𝜆𝑣.𝑐, choose the clean representatives with pairwise distinct bound names. Their outer binders satisfy 𝑢,𝑣∉FV(𝑎)∪{𝑥}, and no binder inside 𝑏 equals 𝑢, while no binder inside 𝑐 equals 𝑣. Choose 𝑧∉Names(𝜆𝑢.𝑏)∪Names(𝜆𝑣.𝑐)∪Names(𝑎)∪{𝑥}. The common-opening lemma gives 𝑏⟨𝑧/𝑢⟩=𝛼𝑐⟨𝑧/𝑣⟩. The induction hypothesis on these smaller bodies gives 𝑏⟨𝑧/𝑢⟩[𝑎/𝑥]=𝛼𝑐⟨𝑧/𝑣⟩[𝑎/𝑥]. Apply lemma 1.59 on both sides to obtain 𝑏[𝑎/𝑥]⟨𝑧/𝑢⟩=𝛼𝑐[𝑎/𝑥]⟨𝑧/𝑣⟩. The displayed choice makes 𝑧 fresh for both substituted abstractions, so this equation is exactly the abstraction clause proving 𝜆𝑢.𝑏[𝑎/𝑥]=𝛼𝜆𝑣.𝑐[𝑎/𝑥].
Independence of the inserted representative. Let 𝑎=𝛼𝑎′ and choose one representative of 𝑒 whose binders avoid FV(𝑎)∪{𝑥}; alpha-equivalence gives FV(𝑎)=FV(𝑎′). Structural induction on this representative proves 𝑒[𝑎/𝑥]=𝛼𝑒[𝑎′/𝑥]. The variable 𝑥 case is the hypothesis 𝑎=𝛼𝑎′; other variables and constants are fixed; nonbinding constructors use congruence; and a clean abstraction reattaches its binder after the induction hypothesis for its body.
The absent-source and free-variable laws. Claims 1 and 2 are structural inductions on a representative whose bound names avoid the finite sets named in definition 1.58. For the free-variable equation, the variable case uses 𝑥∈FV(𝑒), and every nonbinding constructor follows by taking unions. In each abstraction case the binder has already been chosen away from the names under discussion, so the induction hypothesis applies to the body; deleting the same binder on both sides gives the free-variable equation, and reattaching it gives the absent-source equation.
Substitution by a fresh variable. For claim 3, begin with the arbitrary representative 𝑟 named in the statement. Choose 𝑟0=𝛼𝑟 whose binders avoid {𝑥,𝑧}. Since 𝑧∉Names(𝑟), lemma 1.54(1) gives FV(𝑟0)=FV(𝑟), so 𝑧∉FV(𝑟0). The binder choice therefore gives 𝑧∉Names(𝑟0). Alpha compatibility yields [𝑟⟨𝑧/𝑥⟩]=[𝑟0⟨𝑧/𝑥⟩]. Structural induction on 𝑟0 now proves [𝑟0][𝑧/𝑥]=[𝑟0⟨𝑧/𝑥⟩]. The variable 𝑥 is the defining fresh-renaming equation. Other variables and constants are fixed, and nonbinding constructors use the induction hypotheses. At 𝜆𝑢.𝑏, the choice of 𝑟0 gives 𝑢≠𝑥,𝑧, so substitution and fresh renaming both pass under 𝑢; reattaching 𝑢 proves the abstraction case. Source-representative independence then replaces [𝑟0] by 𝑒=[𝑟], proving claim 3 even when 𝑟 itself has a binder named 𝑥.
Substitution composition. For the substitution-composition equation, strengthen the induction statement by choosing every binder in 𝑒 outside {𝑥,𝑦}∪FV(𝑎)∪FV(𝑐). Variables give the two sides directly; the case 𝑒=𝑦 uses 𝑥∉FV(𝑐). Apply the induction hypothesis to every argument of a nonbinding constructor. For 𝑒=𝜆𝑧.𝑏, the choice of 𝑧 makes every abstraction equation applicable on both sides. The induction hypothesis gives 𝑏[𝑎/𝑥][𝑐/𝑦]=𝛼𝑏[𝑐/𝑦][𝑎[𝑐/𝑦]/𝑥], and abstraction congruence completes the binder-sensitive case. ◻
Let 𝑏 and 𝑣 be raw representatives, put 𝐵=[𝑏] and 𝑉=[𝑣], let 𝑥 and 𝑧 be distinct variables, and suppose 𝑧∉Names(𝑏). Then [𝑏⟨𝑧/𝑥⟩][𝑉/𝑧]=𝐵[𝑉/𝑥] in the quotient of raw terms by alpha-equivalence.
Proof. Choose 𝑏0=𝛼𝑏 whose binders avoid {𝑥,𝑧}∪FV(𝑣). Because 𝑧∉Names(𝑏), the name 𝑧 occurs neither free nor bound in 𝑏0. Alpha compatibility gives 𝑏⟨𝑧/𝑥⟩=𝛼𝑏0⟨𝑧/𝑥⟩, while [𝑏]=[𝑏0]. Well-definedness of substitution gives [𝑏⟨𝑧/𝑥⟩][𝑉/𝑧]=[𝑏0⟨𝑧/𝑥⟩][𝑉/𝑧],[𝑏][𝑉/𝑥]=[𝑏0][𝑉/𝑥].
It remains to prove the equation for 𝑏0; use structural induction on 𝑏0. At the variable 𝑥, both sides are 𝑉. For any other variable 𝑢, the case assumption gives 𝑢≠𝑥, and freshness gives 𝑢≠𝑧, so both sides are [𝑢]. Both substitutions fix every constant. For a nonbinding constructor, apply the induction hypothesis to every immediate subterm and reattach the constructor.
For 𝑏0=𝜆𝑢.𝑐, the representative choice gives 𝑢∉{𝑥,𝑧}∪FV(𝑣). Fresh renaming and both substitutions pass under 𝑢. The induction hypothesis equates the quotient classes of the two bodies, and abstraction congruence reattaches 𝜆𝑢.−. The two displayed well-definedness equalities then replace 𝑏0 by 𝑏, which proves the stated equation. ◻
★★☆ Let 𝑥,𝑦,𝑧 be distinct. Compute (𝜆𝑦.𝑥(𝑦𝑧))[(𝑦𝑥)/𝑥] from a representative with fresh bound names, and list the free variables of the result. Then verify equation 1.1 on 𝑒=𝜆𝑧.𝑥𝑦 with 𝑎=𝑦 and 𝑐=𝗍𝗍.
The extended syntax contains two kinds of value: data already computed and an abstraction waiting for an argument. Evaluation is call by value. Thus an application first evaluates its function, then its argument, and only then performs substitution. The collection of rules specifying how terms execute is their operational semantics, also called their dynamics.
For raw representatives, the predicates 𝖱𝖺𝗐𝖵𝖺𝗅(𝑣) and 𝖱𝖺𝗐𝖭𝗎𝗆(𝑛) are generated by
𝖱𝖺𝗐𝖵𝖺𝗅(𝜆𝑥.𝑏)
V-Lam
𝖱𝖺𝗐𝖵𝖺𝗅(𝗍𝗍)
V-True
𝖱𝖺𝗐𝖵𝖺𝗅(𝖿𝖿)
V-False
𝖱𝖺𝗐𝖭𝗎𝗆(𝑛)
𝖱𝖺𝗐𝖵𝖺𝗅(𝑛)
V-Num
𝖱𝖺𝗐𝖭𝗎𝗆(𝟢)
Num-Z
𝖱𝖺𝗐𝖭𝗎𝗆(𝑛)
𝖱𝖺𝗐𝖭𝗎𝗆(𝗌𝗎𝖼(𝑛))
Num-S
The last two rules define exactly the numeral expressions introduced in definition 1.36; the separate judgment records when an arithmetic value is numeric. The separate numeric judgment prevents 𝗌𝗎𝖼(𝜆𝑥.𝑥) and 𝖺𝖽𝖽(𝟢;𝜆𝑥.𝑥) from being mistaken for values.
The one-step judgment 𝑒⟼𝑒′, read “takes one step,” combines call-by-value function and boolean reduction with the arithmetic rules. It is generated on raw representatives by the following rules. For this definition only, 𝑒⟼𝑒′ is read between raw representatives. In E-Beta, the term displayed as 𝑏[𝑣/𝑥] ranges over the raw representatives of the alpha-class produced by definition 1.58. That substitution cleans binders internally; the displayed source binder has no additional freshness side condition.
Proof of Proposition 1.66 — Raw judgments respect alpha-equivalence
Proof. For item 1, induct on the raw-numeral derivation. Lemma 1.54(1) says that alpha-equivalent terms have the same outer constructor. The zero case therefore remains zero. In the successor case, inversion gives 𝑟=𝗌𝗎𝖼(𝑟0), 𝑠=𝗌𝗎𝖼(𝑠0), and 𝑟0=𝛼𝑠0; apply the induction hypothesis and reapply Num-S. Symmetry of alpha-equivalence gives the reverse implication. Item 2 is the corresponding induction on the raw-value derivation. Lambda and Boolean constructors are preserved; the numeric case uses item 1 and reapplies V-Num. Symmetry again gives the reverse implication.
For item 3, induct on the raw-step derivation and invert 𝑟=𝛼𝑠 using the same-outer-constructor clause of definition 1.53. In each congruence case—E-App-L, E-App-R, E-If, E-Suc, E-Add-L, and E-Add-R—inversion relates the corresponding arguments by alpha-equivalence. Apply the induction hypothesis to the argument that steps, use item 1 or item 2 for the numeral or value side premise, and reapply the same rule. Congruence of alpha-equivalence relates the two targets.
For E-If-T, E-If-F, E-Add-Z, and E-Add-S, inversion preserves the Boolean or arithmetic head constructor and relates each branch or numeral component by alpha-equivalence. Items 1–2 preserve the side premises. Reapply the same root rule; the selected branch or constructed arithmetic target is alpha-equivalent to the original target by those component equalities and alpha congruence.
For E-Beta, inversion gives (𝜆𝑥.𝑏)𝑣=𝛼(𝜆𝑦.𝑐)𝑣′,𝜆𝑥.𝑏=𝛼𝜆𝑦.𝑐,𝑣=𝛼𝑣′. Item 2 transfers the value premise. Choose a name 𝑧 outside the names of all four displayed raw subterms. The common-opening clause gives 𝑏⟨𝑧/𝑥⟩=𝛼𝑐⟨𝑧/𝑦⟩. Together with 𝑣=𝛼𝑣′, well-definedness of substitution gives [𝑏⟨𝑧/𝑥⟩][[𝑣]/𝑧]=[𝑐⟨𝑧/𝑦⟩][[𝑣′]/𝑧]. Apply lemma 1.63 first to 𝑏,𝑣,𝑥,𝑧 and then to 𝑐,𝑣′,𝑦,𝑧. These two instances give the outer equalities in [𝑏][[𝑣]/𝑥]𝑠𝑦𝑚𝑚𝑒𝑡𝑟𝑦𝑜𝑓𝑙𝑒𝑚𝑚𝑎1.63=[𝑏⟨𝑧/𝑥⟩][[𝑣]/𝑧](1.2)=[𝑐⟨𝑧/𝑦⟩][[𝑣′]/𝑧]𝑙𝑒𝑚𝑚𝑎1.63=[𝑐][[𝑣′]/𝑦]. Choose the raw target of the right-hand E-Beta instance as 𝑞′. Equality of the first and last terms in the annotated chain is exactly 𝑞=𝛼𝑞′. The six congruence families and five root families exhaust the raw-step rules. ◻
For quotient terms 𝑣=[𝑟], 𝑛=[𝑠], 𝑒=[𝑝], and 𝑒′=[𝑞], define 𝑣𝗏𝖺𝗅⟺𝖱𝖺𝗐𝖵𝖺𝗅(𝑟),𝑛𝗇𝗎𝗆⟺𝖱𝖺𝗐𝖭𝗎𝗆(𝑠),𝑒⟼𝑒′⟺𝑝⟼𝑞byarawruleinstanceforsome𝑝∈𝑒,𝑞∈𝑒′.Proposition 1.66 proves that these definitions do not depend on representatives. The induced quotient derivations retain the rule names V-Lam–Num-S and E-App-L–E-Add-S. The result of a root step is its contractum.
The judgment 𝑒⟼∗𝑒′ records zero or more full call-by-value steps from 𝑒 to 𝑒′. It is the reflexive-transitive closure of ⟼: reflexivity permits zero steps, and transitivity joins finite chains. It is generated by the following two rules.
Proof of Lemma 1.64 — One-step inclusion and many-step transitivity
Proof. For the first claim, apply CBV-Step to the given step and CBV-Refl. For transitivity, induct on the first many-step derivation. The CBV-Refl case is the second derivation. In the CBV-Step case, retain its first one-step premise, compose its many-step tail with the second derivation by the induction hypothesis, and reapply CBV-Step. ◻
The subscript 𝖠 distinguishes the arithmetic-fragment relations ⟼𝖠 and ⟼∗𝖠 from the full-language relations ⟼ and ⟼∗; a star always means reflexive-transitive closure of the corresponding unstarred relation.
Proof of Lemma 1.65 — Arithmetic rules embed in the enlarged dynamics
Proof.A-Suc, A-Add-L, A-Add-R, A-Add-Z, and A-Add-S have the same premises and conclusions as E-Suc, E-Add-L, E-Add-R, E-Add-Z, and E-Add-S. Induct on the one-step derivation, then on the arithmetic M-Refl/M-Step many-step derivation. The many-step cases replace M-Refl by CBV-Refl and M-Step by CBV-Step; every one-step premise is transformed by the first part. ◻
Let 𝑡:=(𝜆𝑓.𝑓𝖿𝖿)(𝜆𝑥.𝗂𝖿(𝑥;𝖿𝖿;𝗍𝗍)). Its first step uses E-Beta with a value argument:
𝜆𝑥.𝗂𝖿(𝑥;𝖿𝖿;𝗍𝗍)𝗏𝖺𝗅
V-Lam
(𝜆𝑓.𝑓𝖿𝖿)(𝜆𝑥.𝗂𝖿(𝑥;𝖿𝖿;𝗍𝗍))⟼(𝜆𝑥.𝗂𝖿(𝑥;𝖿𝖿;𝗍𝗍))𝖿𝖿
E-Beta
The rest is forced: 𝑡𝐸−𝐵𝑒𝑡𝑎⟼(𝜆𝑥.𝗂𝖿(𝑥;𝖿𝖿;𝗍𝗍))𝖿𝖿𝐸−𝐵𝑒𝑡𝑎⟼𝗂𝖿(𝖿𝖿;𝖿𝖿;𝗍𝗍)𝐸−𝐼𝑓−𝐹⟼𝗍𝗍.
Proof. Rule induction on the value derivation reduces the numeric case to rule induction on 𝑛𝗇𝗎𝗆. No reduction rule has a lambda, boolean, or zero as its left-hand term. A successor numeral could step only by E-Suc, whose premise would step from its numeric predecessor, excluded by induction. ◻
The congruence rules locate the next computation by a stack of outer constructors. An evaluation context packages that stack as one object: it is a term-shaped expression with one hole, written [−], marking the place where the next step occurs. In the grammar below the metavariable 𝑣 ranges over all values and 𝑛 ranges over all numerals; their side conditions are 𝑣𝗏𝖺𝗅 and 𝑛𝗇𝗎𝗆. The grammar is 𝐸::=[−]∣𝐸𝑒∣𝑣𝐸∣𝗂𝖿(𝐸;𝑒1;𝑒2)∣𝗌𝗎𝖼(𝐸)∣𝖺𝖽𝖽(𝐸;𝑒)∣𝖺𝖽𝖽(𝑛;𝐸). Write 𝐸⟨𝑒⟩ for filling the unique hole, defined recursively by [−]⟨𝑒⟩=𝑒,𝐸𝑒2⟨𝑒⟩=𝐸⟨𝑒⟩𝑒2,𝑣𝐸⟨𝑒⟩=𝑣𝐸⟨𝑒⟩,𝗂𝖿(𝐸;𝑒1;𝑒2)⟨𝑒⟩=𝗂𝖿(𝐸⟨𝑒⟩;𝑒1;𝑒2),𝗌𝗎𝖼(𝐸)⟨𝑒⟩=𝗌𝗎𝖼(𝐸⟨𝑒⟩),𝖺𝖽𝖽(𝐸;𝑒2)⟨𝑒⟩=𝖺𝖽𝖽(𝐸⟨𝑒⟩;𝑒2),𝖺𝖽𝖽(𝑛;𝐸)⟨𝑒⟩=𝖺𝖽𝖽(𝑛;𝐸⟨𝑒⟩). The hole is a metasyntactic marker, not a term constructor; plugging produces a term. No evaluation-context frame binds a variable, so plugging respects alpha-equivalence of the inserted term. A redex is the source of a basic contraction. Write 𝑟⇝0𝑟′, read “𝑟 contracts to 𝑟′,” for one of (𝜆𝑥.𝑏)𝑣⇝0𝑏[𝑣/𝑥],𝗂𝖿(𝗍𝗍;𝑒1;𝑒2)⇝0𝑒1,𝗂𝖿(𝖿𝖿;𝑒1;𝑒2)⇝0𝑒2,𝖺𝖽𝖽(𝟢;𝑛)⇝0𝑛,𝖺𝖽𝖽(𝗌𝗎𝖼(𝑛1);𝑛2)⇝0𝗌𝗎𝖼(𝖺𝖽𝖽(𝑛1;𝑛2)), with the value and numeral premises displayed in definition 1.65. The relation ⇝0 records a root contraction, before any evaluation-context frame surrounds the redex.
The context decomposition below uses the arithmetic term from the first small-step calculation. Thin edges are syntax-tree edges, heavy edges mark the path selected by the evaluation context, and the dashed box encloses the basic redex.
Diagram
The heavy path consists of the frames 𝖺𝖽𝖽([−];𝟢) and 𝗌𝗎𝖼([−]). The represented equation is 𝖺𝖽𝖽(𝗌𝗎𝖼(𝖺𝖽𝖽(𝟢;𝗌𝗎𝖼(𝟢)));𝟢)=𝖺𝖽𝖽(𝗌𝗎𝖼([−]);𝟢)⟨𝖺𝖽𝖽(𝟢;𝗌𝗎𝖼(𝟢))⟩.
Proof. The trichotomy is structural induction on the closed term. Every immediate subterm visited below is closed because the complete term is closed; the induction never descends under an abstraction. Constants, abstractions, and numeral successors are values. For an application 𝑒1𝑒2, decompose 𝑒1. If it contains the unique redex 𝑟 in context 𝐸, then the application contains that redex in context 𝐸𝑒2. If 𝑒1 is stuck, so is the application. If 𝑒1 is a value, decompose 𝑒2 and use the frame 𝑒1𝐸 when it steps. When both are values, the application is a beta redex exactly when 𝑒1 is an abstraction; a boolean or numeral in function position is stuck.
For conditionals, successors, and additions, the corresponding context frames select the leftmost argument that can step. Once both addition arguments are numeric, the first is uniquely either 𝟢 or 𝗌𝗎𝖼(𝑛), selecting one root contraction. A final but nonnumeric argument of 𝗌𝗎𝖼 or 𝖺𝖽𝖽 makes the complete term stuck. A conditional with a final guard other than 𝗍𝗍 or 𝖿𝖿, such as 𝗂𝖿(𝜆𝑥.𝑥;𝑒1;𝑒2), is likewise stuck.
Uniqueness. Prove the strengthened property 𝑈(𝑒):𝑒=𝐸⟨𝑟⟩=𝐸′⟨𝑟′⟩⟹𝐸=𝐸′and𝑟=𝑟′ by structural induction on the common term 𝑒. There are seven possible outer context cases: 0[−]1𝐸0𝑒22𝑣1𝐸03𝗂𝖿(𝐸0;𝑒1;𝑒2)4𝗌𝗎𝖼(𝐸0)5𝖺𝖽𝖽(𝐸0;𝑒2)6𝖺𝖽𝖽(𝑛1;𝐸0). First separate case 0 from cases 1–6. Every earlier call-by-value position of a basic redex contains a value: these are the operator and argument of a beta redex, the guard of a conditional redex, and the required numeric arguments of an addition redex. If one of those values were instead 𝐸0⟨𝑟0⟩, induction on 𝐸0 would lift the basic contraction of 𝑟0 to a step of that value, contradicting lemma 1.66. Hence case 0 cannot compete with cases 1–6.
Now compare two nonempty cases. Cases 1 and 2 are separated by whether the operator is already a value: an operator of the form 𝐸0⟨𝑟0⟩ with nonempty 𝐸0 can step and hence is not a value. Cases 5 and 6 are separated by whether the left operand is already a numeral. Cases 3 and 4, and the application and addition families, have distinct outer constructors. Thus the two decompositions use the same outer frame. Remove that frame and apply the induction hypothesis 𝑈 to obtain the same inner context and basic redex. In case 0, both decompositions give 𝑟=𝑒=𝑟′ directly. Therefore 𝐸=𝐸′ and 𝑟=𝑟′ in all seven cases.
For the final assertion, induction on a step derivation extracts the context: each congruence rule adds its corresponding frame, and each computation rule uses the empty context. Conversely, induction on 𝐸 lifts the basic contraction by the corresponding congruence rule. The beta case uses proposition 1.60 to identify contracta obtained from different fresh representatives. ◻
Proof of Theorem 1.70 — Determinism of call-by-value reduction
Proof. By lemma 1.69, both steps expose the same context and the same basic redex. Each basic redex has one contractum: the two conditional heads are disjoint, the two addition heads are disjoint, and capture-avoiding substitution is a function on alpha-classes by proposition 1.60. Filling the common context gives 𝑒1=𝑒2. ◻
★★☆ Give the evaluation context and basic redex at each step of (𝜆𝑥.𝖺𝖽𝖽(𝑥;𝗌𝗎𝖼(𝟢)))(𝖺𝖽𝖽(𝟢;𝗌𝗎𝖼(𝟢))). Then replace the argument by 𝜆𝑦.𝑦. Show that its single beta step produces 𝖺𝖽𝖽(𝜆𝑦.𝑦;𝗌𝗎𝖼(𝟢)), which is in clause 3 of lemma 1.69.
The big-step judgment𝑒⇓𝑣 relates a term directly to its final value. It is generated by
𝑣𝗏𝖺𝗅
𝑣⇓𝑣
B-Val
𝑒1⇓𝜆𝑥.𝑏𝑒2⇓𝑣2𝑏[𝑣2/𝑥]⇓𝑣
𝑒1𝑒2⇓𝑣
B-App
𝑒⇓𝗍𝗍𝑒1⇓𝑣
𝗂𝖿(𝑒;𝑒1;𝑒2)⇓𝑣
B-If-T
𝑒⇓𝖿𝖿𝑒2⇓𝑣
𝗂𝖿(𝑒;𝑒1;𝑒2)⇓𝑣
B-If-F
𝑒⇓𝑛𝑛𝗇𝗎𝗆
𝗌𝗎𝖼(𝑒)⇓𝗌𝗎𝖼(𝑛)
B-Suc
𝑒1⇓𝑛1𝑒2⇓𝑛2𝗌𝗎𝗆(𝑛1;𝑛2;𝑛3)
𝖺𝖽𝖽(𝑒1;𝑒2)⇓𝑛3
B-Add
The numeral premise in B-Suc excludes a final nonnumeric value under 𝗌𝗎𝖼. The stuck term 𝗍𝗍𝖿𝖿 matches the source shape of B-App, but its required premise 𝗍𝗍⇓𝜆𝑥.𝑏 has no derivation: final-rule inspection of an evaluation whose source is 𝗍𝗍 leaves only B-Val, whose result is 𝗍𝗍. Matching a rule’s conclusion shape is therefore not enough to derive its premises. This full-language judgment is distinct from ⇓𝖠. For arithmetic expressions 𝑒 and numerals 𝑛, the exact comparison is 𝑒⇓𝖠𝑛 if and only if 𝑒⇓𝑛, as proved in lemma 1.73.
Proof of Lemma 1.72 — Full big-step results are values
Proof. Use rule induction on the big-step derivation. The B-Val premise is the required judgment. In B-App, use the induction hypothesis for the third evaluation premise. In B-If-T and B-If-F, use the induction hypothesis for the selected branch. In B-Suc, Num-S changes the premise 𝑛𝗇𝗎𝗆 to 𝗌𝗎𝖼(𝑛)𝗇𝗎𝗆, and V-Num gives the required value judgment. In B-Add, lemma 1.27, lemma 1.37 give 𝑛3𝗇𝗎𝗆 from the sum premise, and V-Num concludes 𝑛3𝗏𝖺𝗅. ◻
Proof of Lemma 1.73 — Agreement on arithmetic expressions
Proof. For the forward implication, use rule induction on the arithmetic big-step derivation. In AB-Z, derive 𝟢𝗏𝖺𝗅 by V-Num(Num-Z) and apply B-Val. In AB-S, the induction hypothesis gives the premise evaluation and lemma 1.44 gives its numeric result; apply B-Suc. In AB-Add, retain the sum premise, transform both evaluation premises by the induction hypotheses, and apply B-Add.
For the reverse implication, induct on the full big-step derivation while assuming its source has the arithmetic grammar. In B-Val, inversion of the value derivation excludes lambdas and booleans, so the source and result are the same numeral; apply lemma 1.45. Rules B-App, B-If-T, and B-If-F have nonarithmetic source constructors and therefore cannot be the final rule. In B-Suc, the source premise is again arithmetic; apply the induction hypothesis and then AB-S. In B-Add, both source premises are arithmetic. From the retained 𝗌𝗎𝗆(𝑛1;𝑛2;𝑛3) derivation, lemma 1.27 gives 𝑛1𝗇𝖺𝗍 and 𝑛2𝗇𝖺𝗍, and lemma 1.37 converts both judgments to 𝗇𝗎𝗆. The induction hypotheses therefore transform the two evaluation premises; retain the sum derivation and apply AB-Add. ◻
For the running term 𝑡, the complete big-step derivation is 𝑋𝜆𝑓.𝑓𝖿𝖿𝗏𝖺𝗅V−Lam𝜆𝑓.𝑓𝖿𝖿⇓𝜆𝑓.𝑓𝖿𝖿B−Val𝑋𝜆𝑥.𝗂𝖿(𝑥;𝖿𝖿;𝗍𝗍)𝗏𝖺𝗅V−Lam𝜆𝑥.𝗂𝖿(𝑥;𝖿𝖿;𝗍𝗍)⇓𝜆𝑥.𝗂𝖿(𝑥;𝖿𝖿;𝗍𝗍)B−Val𝑋𝜆𝑥.𝗂𝖿(𝑥;𝖿𝖿;𝗍𝗍)𝗏𝖺𝗅V−Lam𝜆𝑥.𝗂𝖿(𝑥;𝖿𝖿;𝗍𝗍)⇓𝜆𝑥.𝗂𝖿(𝑥;𝖿𝖿;𝗍𝗍)B−Val𝑋𝖿𝖿𝗏𝖺𝗅V−False𝖿𝖿⇓𝖿𝖿B−Val𝑋𝖿𝖿𝗏𝖺𝗅V−False𝖿𝖿⇓𝖿𝖿B−Val𝑋𝗍𝗍𝗏𝖺𝗅V−True𝗍𝗍⇓𝗍𝗍B−Val𝗂𝖿(𝖿𝖿;𝖿𝖿;𝗍𝗍)⇓𝗍𝗍B−If−F(𝜆𝑥.𝗂𝖿(𝑥;𝖿𝖿;𝗍𝗍))𝖿𝖿⇓𝗍𝗍B−App𝑡⇓𝗍𝗍B−App.
Proof. First induct on the many-step derivation for a one-frame context, lifting each first step by the frame’s congruence rule. Then induct on the grammar of 𝐸, applying the one-frame result at the outer frame and the context induction hypothesis inside it. ◻
Proof of Theorem 1.75 — Big step implies small steps
Proof. Use rule induction on the big-step derivation. The B-Val case is CBV-Refl. For B-App, V-Lam proves 𝜆𝑥.𝑏𝗏𝖺𝗅, so (𝜆𝑥.𝑏)[−] is an evaluation context. The first induction hypothesis lifts through [−]𝑒2, and the second lifts through (𝜆𝑥.𝑏)[−]. Moreover, lemma 1.72 applied to the second evaluation premise gives 𝑣2𝗏𝖺𝗅, the side premise for E-Beta. The three induction hypotheses therefore give 𝑒1𝑒2𝐼𝐻1+𝑙𝑒𝑚𝑚𝑎1.74⟼∗(𝜆𝑥.𝑏)𝑒2𝐼𝐻2+𝑙𝑒𝑚𝑚𝑎1.74⟼∗(𝜆𝑥.𝑏)𝑣2𝐸−𝐵𝑒𝑡𝑎⟼𝑏[𝑣2/𝑥]𝐼𝐻3⟼∗𝑣.Lemma 1.64 turns the one-step segment into a many-step derivation and composes the four annotated segments. If the big-step derivation ends in a true conditional, its test induction hypothesis gives 𝑒0⟼∗𝗍𝗍, contextual closure gives 𝗂𝖿(𝑒0;𝑒1;𝑒2)⟼∗𝗂𝖿(𝗍𝗍;𝑒1;𝑒2), E-If-T contracts to 𝑒1, and the selected-branch induction hypothesis reaches the result; the false case uses E-If-F and the hypothesis for 𝑒2. The successor hypothesis lifts through 𝗌𝗎𝖼 by lemma 1.74. In the addition case, the last big-step premise is 𝗌𝗎𝗆(𝑛1;𝑛2;𝑛3). By lemma 1.27, lemma 1.37, both 𝑛1𝗇𝗎𝗆 and 𝑛2𝗇𝗎𝗆; in particular, 𝖺𝖽𝖽(𝑛1;[−]) is an evaluation context. Hence 𝖺𝖽𝖽(𝑒1;𝑒2)IH1+𝑙𝑒𝑚𝑚𝑎1.74⟼∗𝖺𝖽𝖽(𝑛1;𝑒2)IH2+𝑙𝑒𝑚𝑚𝑎1.74⟼∗𝖺𝖽𝖽(𝑛1;𝑛2)𝑙𝑒𝑚𝑚𝑎1.47,𝑙𝑒𝑚𝑚𝑎1.65⟼∗𝑛3. ◻
Proof of Corollary 1.81 — Stuck terms do not evaluate
Proof. Suppose 𝑒⇓𝑣. By theorem 1.75, 𝑒⟼∗𝑣. Since a stuck term has no one-step reduct, final-rule inspection leaves only CBV-Refl; hence 𝑒=𝑣. But lemma 1.72 makes 𝑣 a value, contradicting the definition of a stuck term. ◻
Proof of Lemma 1.82 — A value evaluates only to itself
Proof. By theorem 1.75, the evaluation gives 𝑤⟼∗𝑣. Induct on this many-step derivation. The CBV-Refl case gives 𝑣=𝑤. The CBV-Step case would begin with a step from the value 𝑤, contradicting lemma 1.66. ◻
Proof of Lemma 1.83 — One-step expansion of big-step evaluation
Proof. Use rule induction on 𝑒⟼𝑒′. Six congruence cases share one reconstruction. Invert the target evaluation, replace the displayed premise by the induction hypothesis, and reapply the same big-step rule: stepruletarget’sfinalrulepremisereplaced𝐸−𝐴𝑝𝑝−𝐿𝐵−𝐴𝑝𝑝𝑒′1⇓𝜆𝑥.𝑏↦𝑒1⇓𝜆𝑥.𝑏𝐸−𝐴𝑝𝑝−𝑅𝐵−𝐴𝑝𝑝𝑒′2⇓𝑣2↦𝑒2⇓𝑣2𝐸−𝐼𝑓𝐵−𝐼𝑓−𝑇or𝐵−𝐼𝑓−𝐹𝑒′0⇓𝑞↦𝑒0⇓𝑞𝐸−𝑆𝑢𝑐𝐵−𝑆𝑢𝑐𝑒′⇓𝑛↦𝑒⇓𝑛𝐸−𝐴𝑑𝑑−𝐿𝐵−𝐴𝑑𝑑𝑒′1⇓𝑛1↦𝑒1⇓𝑛1𝐸−𝐴𝑑𝑑−𝑅𝐵−𝐴𝑑𝑑𝑒′2⇓𝑛2↦𝑒2⇓𝑛2. Here 𝑞 is 𝗍𝗍 or 𝖿𝖿, as selected by the final conditional rule. The only extra final-rule possibility occurs for E-Suc: the target evaluation may end in B-Val. Its inversion gives 𝑒′𝗇𝗎𝗆. Rules V-Num and B-Val give 𝑒′⇓𝑒′; the induction hypothesis and then B-Suc derive 𝗌𝗎𝖼(𝑒)⇓𝗌𝗎𝖼(𝑒′), the target of the assumed B-Val derivation.
For E-Beta, the assumed target evaluation is 𝑏[𝑣2/𝑥]⇓𝑣. Rule B-Val derives evaluations of 𝜆𝑥.𝑏 and of the premise value 𝑣2 to themselves; these two derivations and the assumed target evaluation form B-App. The E-If-T case combines 𝗍𝗍⇓𝗍𝗍, by B-Val, with the assumed evaluation of the selected branch and applies B-If-T. The E-If-F case uses V-False, B-Val, and B-If-F.
In E-Add-Z, the premise 𝑛2𝗇𝗎𝗆 makes 𝑛2 a value. Hence lemma 1.82 changes the assumed 𝑛2⇓𝑣 to 𝑣=𝑛2. Rules B-Val derive 𝟢⇓𝟢 and 𝑛2⇓𝑛2; by lemma 1.37, 𝑛2𝗇𝖺𝗍, so Sum-Z and B-Add derive 𝖺𝖽𝖽(𝟢;𝑛2)⇓𝑛2.
In E-Add-S, the target 𝗌𝗎𝖼(𝖺𝖽𝖽(𝑛1;𝑛2)) is not a value: inversion of a hypothetical numeral derivation would require 𝖺𝖽𝖽(𝑛1;𝑛2)𝗇𝗎𝗆, but no numeral rule concludes an addition. The assumed target evaluation therefore ends in B-Suc, with 𝖺𝖽𝖽(𝑛1;𝑛2)⇓𝑞,𝑞𝗇𝗎𝗆,𝑣=𝗌𝗎𝖼(𝑞). Inverting the first premise gives 𝑛1⇓𝑝1, 𝑛2⇓𝑝2, and 𝗌𝗎𝗆(𝑝1;𝑝2;𝑞). The two numeral premises of E-Add-S make 𝑛1,𝑛2 values, so lemma 1.82 gives 𝑝1=𝑛1 and 𝑝2=𝑛2. Rule Sum-S gives 𝗌𝗎𝗆(𝗌𝗎𝖼(𝑛1);𝑛2;𝗌𝗎𝖼(𝑞)). Together with the B-Val evaluations of 𝗌𝗎𝖼(𝑛1) and 𝑛2, rule B-Add derives the required source evaluation to 𝑣=𝗌𝗎𝖼(𝑞). ◻
Proof of Theorem 1.84 — Small steps to a value imply big-step evaluation
Proof. Induct on 𝑒⟼∗𝑣. In CBV-Refl, apply B-Val to the assumed value judgment. In CBV-Step, the induction hypothesis turns the many-step tail into 𝑒1⇓𝑣; apply lemma 1.83 to the first step. ◻
The E-Beta reduction step may rename a binder before substituting the argument. The chosen name must not affect the reduct. The first required fact is that fresh renaming commutes with substitution.
Proof of Lemma 1.76 — Fresh renaming commutes with substitution
Proof. The right-hand quotient renaming is defined: if 𝑦∉FV(𝑏), substitution fixes [𝑏]; otherwise the free-variable equation in proposition 1.60 excludes 𝑧 from the result. Choose 𝑏0=𝛼𝑏 whose bound names avoid {𝑥,𝑦,𝑧}∪Names(𝑣). Lemma 1.54(1) gives FV(𝑏0)=FV(𝑏), so the hypothesis on 𝑧 gives 𝑧∉Names(𝑏0). Replacing 𝑏 by 𝑏0 changes neither side, by definition 1.59, proposition 1.60. Use structural induction on 𝑏0. For a variable 𝑢, there are three cases. If 𝑢=𝑦, both sides are [𝑣]⟨𝑧/𝑥⟩=[𝑣⟨𝑧/𝑥⟩]. If 𝑢=𝑥, both sides are [𝑧] by pairwise distinctness of 𝑥,𝑦,𝑧. Every other variable is fixed. Constants are fixed, and each nonbinding constructor follows by applying the induction hypothesis to its arguments.
For an abstraction 𝜆𝑢.𝑐, our representative satisfies 𝑢∉{𝑥,𝑦,𝑧} and 𝑢∉Names(𝑣). Both operations therefore pass under the same binder. The induction hypothesis gives [𝑐⟨𝑧/𝑥⟩][[𝑣⟨𝑧/𝑥⟩]/𝑦]=[𝑐][[𝑣]/𝑦]⟨𝑧/𝑥⟩. Reattaching 𝜆𝑢 gives the required equality of alpha-classes. Independence of the chosen representative is proposition 1.60. ◻
Let 𝑒,𝑒′,𝑣,𝑛 be quotient terms. If 𝑧∉FV(𝑒)∪FV(𝑒′) and 𝑒⟼𝑒′, then 𝑒⟨𝑧/𝑥⟩⟼𝑒′⟨𝑧/𝑥⟩. If 𝑧∉FV(𝑣) and 𝑣𝗏𝖺𝗅, then 𝑣⟨𝑧/𝑥⟩𝗏𝖺𝗅. If 𝑧∉FV(𝑛) and 𝑛𝗇𝗎𝗆, then 𝑛⟨𝑧/𝑥⟩𝗇𝗎𝗆.
Proof of Lemma 1.77 — Renaming evaluation derivations
Proof. If 𝑥=𝑧, the freshness hypotheses imply that 𝑥 is absent from every chosen fresh representative. The absent-source equation reduces each conclusion to its original derivation. Assume henceforth that 𝑥≠𝑧.
First use rule induction on 𝑛𝗇𝗎𝗆 to prove 𝑛⟨𝑧/𝑥⟩=𝑛. Fresh renaming fixes 𝟢, and the Num-S induction hypothesis gives the equality beneath 𝗌𝗎𝖼. Thus the renamed term retains the original numeral derivation. Next use rule induction on 𝑣𝗏𝖺𝗅. The Boolean rules are fixed by renaming, and the V-Num case uses the numeral result just proved. In V-Lam, choose a raw representative 𝜆𝑦.𝑏 with all its bound names outside {𝑥,𝑧}, as permitted by lemma 1.56; its renaming is still an abstraction, so V-Lam applies.
Finally use rule induction on 𝑒⟼𝑒′. In E-App-L, E-If, E-Suc, and E-Add-L, apply the step induction hypothesis to the unique step premise and reapply the same rule. Rule E-App-R also uses the value-renaming result for its function premise. Rule E-Add-R uses the numeral-renaming result for its left premise. Renaming fixes the Boolean heads in E-If-T and E-If-F; it also fixes the numeral shapes in E-Add-Z and E-Add-S, whose numeral premises follow from the numeral-renaming result.
In E-Beta, choose a raw representative 𝑣0 of the argument whose bound names avoid {𝑥,𝑧}. Next represent the abstraction as 𝜆𝑦.𝑏 with every bound name outside {𝑥,𝑧}∪Names(𝑣0). Since 𝑧 is absent from the free variables of the source, these choices give 𝑧∉Names(𝑏)∪Names(𝑣0),𝑦∉Names(𝑣0). The value-renaming result proves [𝑣0]⟨𝑧/𝑥⟩𝗏𝖺𝗅. The renamed source contracts to [𝑏⟨𝑧/𝑥⟩][[𝑣0⟨𝑧/𝑥⟩]/𝑦]. By lemma 1.76, [𝑏⟨𝑧/𝑥⟩][[𝑣0⟨𝑧/𝑥⟩]/𝑦]=[𝑏][[𝑣0]/𝑦]⟨𝑧/𝑥⟩. Thus the target is the required renamed contractum. ◻
Proof of Lemma 1.78 — Substitution of evaluation derivations
Proof. First use rule induction on 𝑛𝗇𝗎𝗆 to prove 𝑛[𝑎/𝑥]=𝑛. Substitution fixes 𝟢, and the Num-S induction hypothesis gives the equality beneath 𝗌𝗎𝖼. Thus the substituted term retains the original numeral derivation. Next use rule induction on 𝑣𝗏𝖺𝗅. Substitution fixes both Boolean values, and the V-Num case uses the numeral result just proved. In V-Lam, choose a raw representative 𝜆𝑦.𝑏 with 𝑦∉{𝑥}∪FV(𝑎). Substitution produces 𝜆𝑦.𝑏[𝑎/𝑥], so V-Lam applies.
Now use rule induction on 𝑒⟼𝑒′. Rules E-App-L, E-If, E-Suc, and E-Add-L use the step induction hypothesis and reapply the same rule. Rule E-App-R also uses the value-substitution result; E-Add-R also uses the numeral-substitution result. Substitution fixes the Boolean heads of E-If-T and E-If-F and the numeral terms of E-Add-Z and E-Add-S; reapply those four root rules.
For one E-Beta instance, choose its abstraction representative 𝜆𝑦.𝑏 with 𝑦∉{𝑥}∪FV(𝑎). This choice changes neither the source alpha-class nor its contractum, by proposition 1.60. Substitution sends the source to (𝜆𝑦.𝑏[𝑎/𝑥])𝑣[𝑎/𝑥]. The value component of the preceding induction proves that 𝑣[𝑎/𝑥] is a value, so E-Beta applies with target 𝑏[𝑎/𝑥][𝑣[𝑎/𝑥]/𝑦]. Equation 1.1, used with the roles of 𝑥 and 𝑦 interchanged and with 𝑦∉FV(𝑎), gives 𝑏[𝑎/𝑥][𝑣[𝑎/𝑥]/𝑦]=𝑏[𝑣/𝑦][𝑎/𝑥], which is the substituted target of the original step. ◻
★★☆ Start with the E-Beta derivation of (𝜆𝑦.𝑥𝑦)𝗍𝗍⟼𝑥𝗍𝗍. Substitute 𝜆𝑧.𝑧 for 𝑥, give the new derivation, and reduce its target one further step. Repeat with the original binder also named 𝑧, first alpha-renaming that binder to a name outside {𝑥,𝑧}∪FV(𝜆𝑧.𝑧).
The term 𝗍𝗍𝖿𝖿 is closed and is not a value. Its function and argument cannot step, so neither application congruence rule applies; its function is not an abstraction, so it is not a beta redex. Hence it is stuck. The term 𝗌𝗎𝖼(𝜆𝑥.𝑥) is stuck for the same structural reason: the argument is final but not numeric.
Stuckness is not nondeterminism: theorem 1.70 says that every available next step is unique. It is not divergence either. Divergence is the existence of an infinite sequence of steps beginning at a term; that term continues to step, whereas 𝗍𝗍𝖿𝖿 has no first step. The evaluator discovers the defect only after the offending term is reached. The next problem is therefore static: construct a judgment that rejects such shape mismatches before the program is run, and prove that every accepted closed program is either a value or can take another step.
★☆☆ Let 𝜔:=𝜆𝑥.𝑥𝑥. Show that 𝜔𝜔⟼𝜔𝜔, so it diverges but is not stuck. Then prove that (𝜆𝑥.𝗍𝗍)(𝗍𝗍𝖿𝖿) is stuck under call by value even though substituting its unevaluated argument into the body would discard the defect.
★★☆ Reconstruct the proof of lemma 1.66 as a complete rule induction. For each final value rule, list the reduction rules whose left-hand term cannot match, and explain why raw structural induction is less precise in the numeric case.
★★☆ Delete E-Suc and show that the rule from 𝑒⟼𝑒′ to 𝗌𝗎𝖼(𝑒)⟼𝗌𝗎𝖼(𝑒′) is no longer admissible: give one derivable premise with an underivable conclusion. Restore E-Suc and give the one-case transformation proving admissibility.
★★★ Prove that if 𝑒⟼∗𝖠𝑛 and 𝑛𝗇𝗎𝗆, then 𝑒⇓𝖠𝑛. First prove, by induction on the one-step derivation, that 𝑒⟼𝖠𝑒′ and 𝑒′⇓𝖠𝑛 imply 𝑒⇓𝖠𝑛. Then prove, by induction on the many-step derivation, that 𝑒⟼∗𝖠𝑛 and 𝑛𝗇𝗎𝗆 imply 𝑒⇓𝖠𝑛. Treat every arithmetic step rule in the first induction.
★★★Practical project.ulc-evaluator Using the Kappa scaffold specified in the practical tutorial, spend four to six hours implementing the call-by-value one-step relation of definition 1.62. Implement free-name calculation, fresh-name selection, capture-avoiding substitution, one-step reduction, and fueled iteration. Maintain the invariant that a returned raw beta target 𝑞 for (𝜆𝑥.𝑏)𝑣 satisfies [𝑞]=[𝑏][[𝑣]/𝑥]. Distinguish values, closed stuck terms, open nonvalues with no step, and fuel exhaustion.
Test every rule family. Add a substitution mutant that omits freshening and test it on (𝜆0.𝜆1.0)(𝜆2.1): name 1 must remain free in the correct contractum but becomes bound in the mutant’s result. The remaining tests must reduce the term 𝑡 defined in equation 1.3 to 𝗍𝗍, classify 𝗍𝗍𝖿𝖿 as stuck, and exhaust ten units of fuel on 𝜔𝜔. Place each test source beside its selected rule and expected target. State why the corpus proves none of alpha compatibility, determinism, or divergence for all terms.
Diagram
Diagram
Diagram