2.6 Defining Functions by Rules 19 The principle of rule induction for these rules states that to show simultaneously that P(a) whenever a even and (b)whenever b odd,it is enough to show the following: 1.P(zero); 2.if Q(b),then P(succ(b)); 3.if P(a),then (succ(a)). As an example,we may use simultaneous rule induction to prove that(1)if a even,then either a is zero or a is succ(b)with b odd,and(2)if a odd,then a is succ(b)with b even.We define P(a) to hold iff a is zero or a is succ(b)for some b with b odd,and define (b)to hold iff b is succ(a) for some a with a even.The desired result follows by rule induction,because we can prove the following facts: 1.P(zero),which holds because zero is zero. 2.If (b),then succ(b)is succ(b')for some b'with (b').Take b'to be b and apply the inductive assumption. 3.If P(a),then succ(a)is succ(a')for some a'with P(a').Take a'to be a and apply the inductive assumption. 2.6 Defining Functions by Rules A common use of inductive definitions is to define a function by giving an inductive definition of its graph relating 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 relation sum(a;b;c),with the intended meaning that c is the sum of a and b,as follows: bnat sum(zero;b;b) (2.9a) sum(a;b;c) (2.9b) sum(succ(a);b;succ(c)) The rules define a ternary (three-place)relation sum(a;b;c)among natural numbers a,b,and c. We may show that c is determined by a and b in this relation. Theorem 2.4.For every a nat and b nat,there exists a unique c nat such that sum(a;b;c). Proof.The proof decomposes into two parts: 1.(Existence)If a nat and b nat,then there exists c nat such that sum(a;b;c). 2.(Uniqueness)If sum(a;b;c),and sum(a;b;c),then cisc'. For existence,let P(a)be the proposition if b nat then there exists c nat such that sum(a;b;c).We prove that if a nat then P(a)by rule induction on rules(2.2).We have two cases to consider:
PREVIEW 2.6 Defining Functions by Rules 19 The principle of rule induction for these rules states that to show simultaneously that P(a) whenever a even and Q(b) whenever b odd, it is enough to show the following: 1. P(zero); 2. if Q(b), then P(succ( b )); 3. if P(a), then Q(succ( a )). As an example, we may use simultaneous rule induction to prove that (1) if a even, then either a is zero or a is succ( b ) with b odd, and (2) if a odd, then a is succ( b ) with b even. We define P(a) to hold iff a is zero or a is succ( b ) for some b with b odd, and define Q(b) to hold iff b is succ( a ) for some a with a even. The desired result follows by rule induction, because we can prove the following facts: 1. P(zero), which holds because zero is zero. 2. If Q(b), then succ( b ) is succ( b ′ ) for some b ′ with Q(b ′ ). Take b ′ to be b and apply the inductive assumption. 3. If P(a), then succ( a ) is succ( a ′ ) for some a ′ with P(a ′ ). Take a ′ to be a and apply the inductive assumption. 2.6 Defining Functions by Rules A common use of inductive definitions is to define a function by giving an inductive definition of its graph relating 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 relation sum(a ; b ; c), with the intended meaning that c is the sum of a and b, as follows: b nat sum(zero ; b ; b) (2.9a) sum(a ; b ; c) sum(succ( a ) ; b ; succ( c )) (2.9b) The rules define a ternary (three-place) relation sum(a ; b ; c) among natural numbers a, b, and c. We may show that c is determined by a and b in this relation. Theorem 2.4. For every a nat and b nat, there exists a unique c nat such that sum(a ; b ; c). Proof. The proof decomposes into two parts: 1. (Existence) If a nat and b nat, then there exists c nat such that sum(a ; b ; c). 2. (Uniqueness) If sum(a ; b ; c), and sum(a ; b ; c ′ ), then c is c ′ . For existence, let P(a) be the proposition if b nat then there exists c nat such that sum(a ; b ; c). We prove that if a nat then P(a) by rule induction on rules (2.2). We have two cases to consider:
20 2.7 Notes Rule(2.2a)We are to show P(zero).Assuming b nat and taking c to be b,we obtain sum(zero; b;c)by rule (2.9a). Rule(2.2b)Assuming P(a),we are to show P(succ(a)).That is,we assume that if b nat then there exists c such that sum(a;b;c),and are to show that if b'nat,then there exists c'such that sum(succ(a);b';c).To this end,suppose that b'nat.Then by induction there exists c such that sum(a;b';c).Takingc'to be succ(c),and applying rule(2.9b),we obtain sum(succ(a); b';c),as required. For uniqueness,we prove that if sum(a;b;c1),then if sum(a;b;c2),then ci is c2 by rule induction based on rules(2.9). Rule(2.9a)We have a is zero and c is b.By an inner induction on the same rules,we may show that if sum(zero;b;c2),then c2 is b.By Lemma 2.2 we obtain b is b. Rule (2.9b)We have that a is succ(a')and ci is succ(c),where sum(a';b;c).By an inner induction on the same rules,we may show that if sum(a;b;c2),then c2 is succ(c2)where sum(a';b;c2).By the outer inductive hypothesis c isc2 and so ci is c2. 口 2.7 Notes Aczel (1977)provides a thorough account of the theory of inductive definitions on which the present account is based.A significant difference is that we consider inductive definitions of judgments over abts as defined in Chapter 1,rather than with natural numbers.The emphasis on judgments is inspired by Martin-Lof's logic of judgments(Martin-Lof,1983,1987). Exercises 2.1.Give an inductive definition of the judgment max(m;n;p),where m nat,n nat,and p nat, with the meaning that p is the larger of m and n.Prove that every m and n are related to a unique p by this judgment. 2.2.Consider the following rules,which define the judgment hgt(t;n)stating that the binary tree t has height n. (2.10a) hgt(empty;zero) hgt(t1;n1)hgt(t2 n2)max(n1;n2;n) (2.10b) hgt(node(1 f2);succ(n)) Prove that the judgment hgt defines a function from trees to natural numbers
PREVIEW 20 2.7 Notes Rule (2.2a) We are to show P(zero). Assuming b nat and taking c to be b, we obtain sum(zero ; b ; c) by rule (2.9a). Rule (2.2b) Assuming P(a), we are to show P(succ( a )). That is, we assume that if b nat then there exists c such that sum(a ; b ; c), and are to show that if b ′ nat, then there exists c ′ such that sum(succ( a ) ; b ′ ; c ′ ). To this end, suppose that b ′ nat. Then by induction there exists c such that sum(a ; b ′ ; c). Taking c ′ to be succ( c ), and applying rule (2.9b), we obtain sum(succ( a ); b ′ ; c ′ ), as required. For uniqueness, we prove that if sum(a ; b ; c1), then if sum(a ; b ; c2), then c1 is c2 by rule induction based on rules (2.9). Rule (2.9a) We have a is zero and c1 is b. By an inner induction on the same rules, we may show that if sum(zero ; b ; c2), then c2 is b. By Lemma 2.2 we obtain b is b. Rule (2.9b) We have that a is succ( a ′ ) and c1 is succ( c ′ 1 ), where sum(a ′ ; b ; c ′ 1 ). By an inner induction on the same rules, we may show that if sum(a ; b ; c2), then c2 is succ( c ′ 2 ) where sum(a ′ ; b ; c ′ 2 ). By the outer inductive hypothesis c ′ 1 is c ′ 2 and so c1 is c2. 2.7 Notes Aczel (1977) provides a thorough account of the theory of inductive definitions on which the present account is based. A significant difference is that we consider inductive definitions of judgments over abts as defined in Chapter 1, rather than with natural numbers. The emphasis on judgments is inspired by Martin-Lof’s logic of judgments ( ¨ Martin-Lof¨ , 1983, 1987). Exercises 2.1. Give an inductive definition of the judgment max(m ; n ; p), where m nat, n nat, and p nat, with the meaning that p is the larger of m and n. Prove that every m and n are related to a unique p by this judgment. 2.2. Consider the following rules, which define the judgment hgt(t ; n) stating that the binary tree t has height n. hgt(empty ; zero) (2.10a) hgt(t1 ; n1) hgt(t2 ; n2) max(n1 ; n2 ; n) hgt(node(t1 ; t2 ) ; succ( n )) (2.10b) Prove that the judgment hgt defines a function from trees to natural numbers
2.7 Notes 21 2.3.Given an inductive definition of ordered variadic trees whose nodes have a finite,but variable, number of children with a specified left-to-right ordering among them.Your solution should consist of a simultaneous definition of two judgments,t tree,stating that t is a variadic tree, and f forest,stating that f is a "forest"(finite sequence)of variadic trees. 2.4.Give an inductive definition of the height of a variadic tree of the kind defined in Exercise 2.3. Your definition should make use of an auxiliary judgment defining the height of a forest of variadic trees,and will be defined simultaneously with the height of a variadic tree.Show that the two judgments so defined each define a function 2.5.Give an inductive definition of the binary natural numbers,which are either zero,twice a binary number,or one more than twice a binary number.The size of such a representation is logarithmic,rather than linear,in the natural number it represents. 2.6.Give an inductive definition of addition of binary natural numbers as defined in Exercise 2.5 Hint:Proceed by analyzing both arguments to the addition,and make use of an auxiliary function to compute the successor of a binary number.Hint:Alternatively,define both the sum and the sum-plus-one of two binary numbers mutually recursively. PREY
PREVIEW 2.7 Notes 21 2.3. Given an inductive definition of ordered variadic trees whose nodes have a finite, but variable, number of children with a specified left-to-right ordering among them. Your solution should consist of a simultaneous definition of two judgments, t tree, stating that t is a variadic tree, and f forest, stating that f is a “forest” (finite sequence) of variadic trees. 2.4. Give an inductive definition of the height of a variadic tree of the kind defined in Exercise 2.3. Your definition should make use of an auxiliary judgment defining the height of a forest of variadic trees, and will be defined simultaneously with the height of a variadic tree. Show that the two judgments so defined each define a function. 2.5. Give an inductive definition of the binary natural numbers, which are either zero, twice a binary number, or one more than twice a binary number. The size of such a representation is logarithmic, rather than linear, in the natural number it represents. 2.6. Give an inductive definition of addition of binary natural numbers as defined in Exercise 2.5. Hint: Proceed by analyzing both arguments to the addition, and make use of an auxiliary function to compute the successor of a binary number. Hint: Alternatively, define both the sum and the sum-plus-one of two binary numbers mutually recursively
22 2.7 Notes PREVIEW
PREVIEW 22 2.7 Notes
Chapter 3 Hypothetical and General Judgments A hypothetical judgment expresses an entailment between one or more hypotheses and a conclusion. We will consider two notions of entailment,called derivability and admissibility.Both express a form of entailment,but they differ in that derivability is stable under extension with new rules, admissibility is not.A general judgment expresses the universality,or genericity,of a judgment. There are two forms of general judgment,the generic and the parametric.The generic judgment expresses generality with respect to all substitution instances for variables in a judgment.The parametric judgment expresses generality with respect to renamings of symbols. 3.1 Hypothetical Judgments The hypothetical judgment codifies the rules for expressing the validity of a conclusion conditional on the validity of one or more hypotheses.There are two forms of hypothetical judgment that differ according to the sense in which the conclusion is conditional on the hypotheses.One is stable under extension with more rules,and the other is not. 3.1.1 Derivability For a given set R of rules,we define the derivability judgment,written h,...,IkHR K,where each Ji and K are basic judgments,to mean that we may derive K from the expansion RU[h,...,Ik}of the rules R with the axioms h We treat the hypotheses,or antecedents,of the judgment,h,....Ik as "temporary axioms",and de- rive the conclusion,or consequent,by composing rules in R.Thus,evidence for a hypothetical judgment consists of a derivation of the conclusion from the hypotheses using the rules in R. We use capital Greek letters,usually I or A,to stand for a finite set of basic judgments,and write RUr for the expansion of R with an axiom corresponding to each judgment in I.The
PREVIEW Chapter 3 Hypothetical and General Judgments A hypothetical judgment expresses an entailment between one or more hypotheses and a conclusion. We will consider two notions of entailment, called derivability and admissibility. Both express a form of entailment, but they differ in that derivability is stable under extension with new rules, admissibility is not. A general judgment expresses the universality, or genericity, of a judgment. There are two forms of general judgment, the generic and the parametric. The generic judgment expresses generality with respect to all substitution instances for variables in a judgment. The parametric judgment expresses generality with respect to renamings of symbols. 3.1 Hypothetical Judgments The hypothetical judgment codifies the rules for expressing the validity of a conclusion conditional on the validity of one or more hypotheses. There are two forms of hypothetical judgment that differ according to the sense in which the conclusion is conditional on the hypotheses. One is stable under extension with more rules, and the other is not. 3.1.1 Derivability For a given set R of rules, we define the derivability judgment, written J1, . . . , Jk ⊢R K, where each Ji and K are basic judgments, to mean that we may derive K from the expansion R ∪ { J1, . . . , Jk } of the rules R with the axioms J1 . . . Jk . We treat the hypotheses, or antecedents, of the judgment, J1, . . . , Jk as “temporary axioms”, and derive the conclusion, or consequent, by composing rules in R. Thus, evidence for a hypothetical judgment consists of a derivation of the conclusion from the hypotheses using the rules in R. We use capital Greek letters, usually Γ or ∆, to stand for a finite set of basic judgments, and write R ∪ Γ for the expansion of R with an axiom corresponding to each judgment in Γ. The