14 2.2 Inference Rules 2.2 Inference Rules An inductive definition of a judgment form consists of a collection of rules of the form h…k (2.1) in which I and /1,...,Ik are all judgments of the form being defined.The judgments above the horizontal line are called the premises of the rule,and the judgment below the line is called its conclusion.If a rule has no premises(that is,when k is zero),the rule is called an axiom;otherwise it is called a proper rule. An inference rule can be read as stating that the premises are sufficient for the conclusion:to show J,it is enough to show J1,...,Ik.When k is zero,a rule states that its conclusion holds unconditionally.Bear in mind that there may be,in general,many rules with the same conclusion, each specifying sufficient conditions for the conclusion.Consequently,if the conclusion of a rule holds,then it is not necessary that the premises hold,for it might have been derived by another rule. For example,the following rules form an inductive definition of the judgment form-nat: (2.2a) zero nat a nat succ(a)nat (2.2b) These rules specify that a nat holds whenever either a is zero,or a is succ(b)where b nat for some b.Taking these rules to be exhaustive,it follows that a nat iff a is a natural number. Similarly,the following rules constitute an inductive definition of the judgment form-tree: (2.3a) empty tree a tree a2 tree node(a1;a2)tree (2.3b) These rules specify that a tree holds if either a is empty,or a is node(a1;a2),where a1 tree and a2 tree.Taking these to be exhaustive,these rules state that a is a binary tree,which is to say it is either empty,or a node consisting of two children,each of which is also a binary tree. The judgment form a is b expressing the equality of two abts a and b such that a nat and b nat is inductively defined by the following rules: (2.4a) zero is zero aisb succ(a)is succ(b) (2.4b)
PREVIEW 14 2.2 Inference Rules 2.2 Inference Rules An inductive definition of a judgment form consists of a collection of rules of the form J1 . . . Jk J (2.1) in which J and J1, . . . , Jk are all judgments of the form being defined. The judgments above the horizontal line are called the premises of the rule, and the judgment below the line is called its conclusion. If a rule has no premises (that is, when k is zero), the rule is called an axiom; otherwise it is called a proper rule. An inference rule can be read as stating that the premises are sufficient for the conclusion: to show J, it is enough to show J1, . . . , Jk . When k is zero, a rule states that its conclusion holds unconditionally. Bear in mind that there may be, in general, many rules with the same conclusion, each specifying sufficient conditions for the conclusion. Consequently, if the conclusion of a rule holds, then it is not necessary that the premises hold, for it might have been derived by another rule. For example, the following rules form an inductive definition of the judgment form − nat: zero nat (2.2a) a nat succ( a ) nat (2.2b) These rules specify that a nat holds whenever either a is zero, or a is succ( b ) where b nat for some b. Taking these rules to be exhaustive, it follows that a nat iff a is a natural number. Similarly, the following rules constitute an inductive definition of the judgment form − tree: empty tree (2.3a) a1 tree a2 tree node( a1 ; a2 ) tree (2.3b) These rules specify that a tree holds if either a is empty, or a is node( a1 ; a2 ), where a1 tree and a2 tree. Taking these to be exhaustive, these rules state that a is a binary tree, which is to say it is either empty, or a node consisting of two children, each of which is also a binary tree. The judgment form a is b expressing the equality of two abts a and b such that a nat and b nat is inductively defined by the following rules: zero is zero (2.4a) a is b succ( a ) is succ( b ) (2.4b)
2.3 Derivations 15 In each of the preceding examples we have made use of a notational convention for specifying an infinite family of rules by a finite number of patterns,or rule schemes.For example,rule(2.2b) is a rule scheme that determines one rule,called an instance of the rule scheme,for each choice of object a in the rule.We will rely on context to determine whether a rule is stated for a specific object a or is instead intended as a rule scheme specifying a rule for each choice of objects in the rule. A collection of rules is considered to define the strongest judgment form that is closed under,or respects,those rules.To be closed under the rules simply means that the rules are sufficient to show the validity of a judgment:I holds if there is a way to obtain it using the given rules.To be the strongest judgment form closed under the rules means that the rules are also necessary:I holds only if there is a way to obtain it by applying the rules.The sufficiency of the rules means that we may show that I holds by deriving it by composing rules.Their necessity means that we may reason about it using rule induction. 2.3 Derivations To show that an inductively defined judgment holds,it is enough to exhibit a derivation of it.A derivation of a judgment is a finite composition of rules,starting with axioms and ending with that judgment.It can be thought of as a tree in which each node is a rule whose children are derivations of its premises.We sometimes say that a derivation of J is evidence for the validity of an inductively defined judgment J. We usually depict derivations as trees with the conclusion at the bottom,and with the children of a node corresponding to a rule appearing above it as evidence for the premises of that rule. Thus,if k is an inference rule and 71,...,Vr are derivations of its premises,then 71.7k is a derivation of its conclusion.In particular,if k=0,then the node has no children. For example,this is a derivation of succ(succ(succ(zero)))nat: zero nat succ(zero)nat (2.5) succ(succ(zero))nat succ(succ(succ(zero)))nat
PREVIEW 2.3 Derivations 15 In each of the preceding examples we have made use of a notational convention for specifying an infinite family of rules by a finite number of patterns, or rule schemes. For example, rule (2.2b) is a rule scheme that determines one rule, called an instance of the rule scheme, for each choice of object a in the rule. We will rely on context to determine whether a rule is stated for a specific object a or is instead intended as a rule scheme specifying a rule for each choice of objects in the rule. A collection of rules is considered to define the strongest judgment form that is closed under, or respects, those rules. To be closed under the rules simply means that the rules are sufficient to show the validity of a judgment: J holds if there is a way to obtain it using the given rules. To be the strongest judgment form closed under the rules means that the rules are also necessary: J holds only if there is a way to obtain it by applying the rules. The sufficiency of the rules means that we may show that J holds by deriving it by composing rules. Their necessity means that we may reason about it using rule induction. 2.3 Derivations To show that an inductively defined judgment holds, it is enough to exhibit a derivation of it. A derivation of a judgment is a finite composition of rules, starting with axioms and ending with that judgment. It can be thought of as a tree in which each node is a rule whose children are derivations of its premises. We sometimes say that a derivation of J is evidence for the validity of an inductively defined judgment J. We usually depict derivations as trees with the conclusion at the bottom, and with the children of a node corresponding to a rule appearing above it as evidence for the premises of that rule. Thus, if J1 . . . Jk J is an inference rule and ` 1 , . . . , ` k are derivations of its premises, then ` 1 . . . ` k J is a derivation of its conclusion. In particular, if k = 0, then the node has no children. For example, this is a derivation of succ( succ( succ( zero ) ) ) nat: zero nat succ( zero ) nat succ( succ( zero ) ) nat succ( succ( succ( zero ) ) ) nat . (2.5)
16 2.4 Rule Induction Similarly,here is a derivation of node(node(empty;empty);empty)tree: empty tree empty tree (2.6) node(empty;empty)tree empty tree node(node(empty;empty);empty )tree To show that an inductively defined judgment is derivable we need only find a derivation for it.There are two main methods for finding derivations,called forward chaining,or bottom- up construction,and backward chaining,or top-down construction.Forward chaining starts with the axioms and works forward towards the desired conclusion,whereas backward chaining starts with the desired conclusion and works backwards towards the axioms. More precisely,forward chaining search maintains a set of derivable judgments,and continu- ally extends this set by adding to it the conclusion of any rule all of whose premises are in that set.Initially,the set is empty;the process terminates when the desired judgment occurs in the set.Assuming that all rules are considered at every stage,forward chaining will eventually find a derivation of any derivable judgment,but it is impossible(in general)to decide algorithmically when to stop extending the set and conclude that the desired judgment is not derivable.We may go on and on adding more judgments to the derivable set without ever achieving the intended goal.It is a matter of understanding the global properties of the rules to determine that a given judgment is not derivable. Forward chaining is undirected in the sense that it does not take account of the end goal when deciding how to proceed at each step.In contrast,backward chaining is goal-directed.Back- ward chaining search maintains a queue of current goals,judgments whose derivations are to be sought.Initially,this set consists solely of the judgment we wish to derive.At each stage,we remove a judgment from the queue,and consider all rules whose conclusion is that judgment. For each such rule,we add the premises of that rule to the back of the queue,and continue.If there is more than one such rule,this process must be repeated,with the same starting queue,for each candidate rule.The process terminates whenever the queue is empty,all goals having been achieved;any pending consideration of candidate rules along the way can be discarded.As with forward chaining,backward chaining will eventually find a derivation of any derivable judgment, but there is,in general,no algorithmic method for determining in general whether the current goal is derivable.If it is not,we may futilely add more and more judgments to the goal set,never reaching a point at which all goals have been satisfied. 2.4 Rule Induction Because an inductive definition specifies the strongest judgment form closed under a collection of rules,we may reason about them by rule induction.The principle of rule induction states that to show that a property a p holds whenever a J is derivable,it is enough to show that P is closed under,or respects,the rules defining the judgment form J.More precisely,the property P respects the rule a J...ak J aJ
PREVIEW 16 2.4 Rule Induction Similarly, here is a derivation of node( node( empty ; empty ) ; empty ) tree: empty tree empty tree node( empty ; empty ) tree empty tree node( node( empty ; empty ) ; empty ) tree . (2.6) To show that an inductively defined judgment is derivable we need only find a derivation for it. There are two main methods for finding derivations, called forward chaining, or bottomup construction, and backward chaining, or top-down construction. Forward chaining starts with the axioms and works forward towards the desired conclusion, whereas backward chaining starts with the desired conclusion and works backwards towards the axioms. More precisely, forward chaining search maintains a set of derivable judgments, and continually extends this set by adding to it the conclusion of any rule all of whose premises are in that set. Initially, the set is empty; the process terminates when the desired judgment occurs in the set. Assuming that all rules are considered at every stage, forward chaining will eventually find a derivation of any derivable judgment, but it is impossible (in general) to decide algorithmically when to stop extending the set and conclude that the desired judgment is not derivable. We may go on and on adding more judgments to the derivable set without ever achieving the intended goal. It is a matter of understanding the global properties of the rules to determine that a given judgment is not derivable. Forward chaining is undirected in the sense that it does not take account of the end goal when deciding how to proceed at each step. In contrast, backward chaining is goal-directed. Backward chaining search maintains a queue of current goals, judgments whose derivations are to be sought. Initially, this set consists solely of the judgment we wish to derive. At each stage, we remove a judgment from the queue, and consider all rules whose conclusion is that judgment. For each such rule, we add the premises of that rule to the back of the queue, and continue. If there is more than one such rule, this process must be repeated, with the same starting queue, for each candidate rule. The process terminates whenever the queue is empty, all goals having been achieved; any pending consideration of candidate rules along the way can be discarded. As with forward chaining, backward chaining will eventually find a derivation of any derivable judgment, but there is, in general, no algorithmic method for determining in general whether the current goal is derivable. If it is not, we may futilely add more and more judgments to the goal set, never reaching a point at which all goals have been satisfied. 2.4 Rule Induction Because an inductive definition specifies the strongest judgment form closed under a collection of rules, we may reason about them by rule induction. The principle of rule induction states that to show that a property a P holds whenever a J is derivable, it is enough to show that P is closed under, or respects, the rules defining the judgment form J. More precisely, the property P respects the rule a1 J . . . ak J a J
2.4 Rule Induction 17 if P(a)holds whenever P(a),...,P(ak)do.The assumptions P(a),...,P(ak)are called the inductive hypotheses,and P(a)is called the inductive conclusion of the inference. The principle of rule induction is simply the expression of the definition of an inductively defined judgment form as the strongest judgment form closed under the rules comprising the def- inition.Thus,the judgment form defined by a set of rules is both(a)closed under those rules, and(b)sufficient for any other property also closed under those rules.The former means that a derivation is evidence for the validity of a judgment;the latter means that we may reason about an inductively defined judgment form by rule induction. When specialized to rules(2.2),the principle of rule induction states that to show P(a)when- ever a nat,it is enough to show: 1.P(zero) 2.for every a,if P(a),then P(succ(a)). The sufficiency of these conditions is the familiar principle of mathematical induction. Similarly,rule induction for rules(2.3)states that to show P(a)whenever a tree,it is enough to show 1.P(empty) 2.for every a and a2,if P(a),and if P(a2),then P(node(a1;a2)) The sufficiency of these conditions is called the principle of tree induction. We may also show by rule induction that the predecessor of a natural number is also a natural number.Although this may seem self-evident,the point of the example is to show how to derive this from first principles. Lemma 2.1.If succ(a)nat,then a nat Proof.Define P(a)to mean that if a succ(b),then b nat.It suffices to show that P is closed under rules(2.2). Rule(2.2a)Vacuous,because zero is not of the form succ(-) Rule(2.2b)The premise of the rule ensures that b nat when a succ(b). 口 Using rule induction we may show that equality,as defined by rules(2.4)is reflexive. Lemma 2.2.If a nat,then a is a. Proof.By rule induction on rules(2.2): Rule(2.2a)Applying rule(2.4a)we obtain zero is zero. Rule (2.2b)Assume that a is a.It follows that succ(a)is succ(a)by an application of rule (2.4b)
PREVIEW 2.4 Rule Induction 17 if P(a) holds whenever P(a1), . . . ,P(ak ) do. The assumptions P(a1), . . . ,P(ak ) are called the inductive hypotheses, and P(a) is called the inductive conclusion of the inference. The principle of rule induction is simply the expression of the definition of an inductively defined judgment form as the strongest judgment form closed under the rules comprising the definition. Thus, the judgment form defined by a set of rules is both (a) closed under those rules, and (b) sufficient for any other property also closed under those rules. The former means that a derivation is evidence for the validity of a judgment; the latter means that we may reason about an inductively defined judgment form by rule induction. When specialized to rules (2.2), the principle of rule induction states that to show P(a) whenever a nat, it is enough to show: 1. P(zero). 2. for every a, if P(a), then P(succ( a )). The sufficiency of these conditions is the familiar principle of mathematical induction. Similarly, rule induction for rules (2.3) states that to show P(a) whenever a tree, it is enough to show 1. P(empty). 2. for every a1 and a2, if P(a1), and if P(a2), then P(node( a1 ; a2 )). The sufficiency of these conditions is called the principle of tree induction. We may also show by rule induction that the predecessor of a natural number is also a natural number. Although this may seem self-evident, the point of the example is to show how to derive this from first principles. Lemma 2.1. If succ( a ) nat, then a nat. Proof. Define P(a) to mean that if a = succ( b ), then b nat. It suffices to show that P is closed under rules (2.2). Rule (2.2a) Vacuous, because zero is not of the form succ( − ). Rule (2.2b) The premise of the rule ensures that b nat when a = succ( b ). Using rule induction we may show that equality, as defined by rules (2.4) is reflexive. Lemma 2.2. If a nat, then a is a. Proof. By rule induction on rules (2.2): Rule (2.2a) Applying rule (2.4a) we obtain zero is zero. Rule (2.2b) Assume that a is a. It follows that succ( a ) is succ( a ) by an application of rule (2.4b)
18 2.5 Iterated and Simultaneous Inductive Definitions Similarly,we may show that the successor operation is injective. Lemma 2.3.If succ(a)is succ(a2),then a is a2. Proof.Similar to the proof of Lemma 2.1. 2.5 Iterated and Simultaneous Inductive Definitions Inductive definitions are often iterated,meaning that one inductive definition builds on top of another.In an iterated inductive definition the premises of a rule may be instances of either a previously defined judgment form,or the judgment form being de- fined.For example,the following rules define the judgment form-list,which states that a is a list of natural numbers: (2.7a) nil list anat blist cons(a;b)list (2.7b) The first premise of rule(2.7b)is an instance of the judgment form a nat,which was defined previously,whereas the premise b list is an instance of the judgment form being defined by these rules. Frequently two or more judgments are defined at once by a simultaneous inductive definition. A simultaneous inductive definition consists of a set of rules for deriving instances of several different judgment forms,any of which may appear as the premise of any rule.Because the rules defining each judgment form may involve any of the others,none of the judgment forms can be taken to be defined prior to the others.Instead we must understand that all of the judgment forms are being defined at once by the entire collection of rules.The judgment forms defined by these rules are,as before,the strongest judgment forms that are closed under the rules.Therefore the principle of proof by rule induction continues to apply,albeit in a form that requires us to prove a property of each of the defined judgment forms simultaneously. For example,consider the following rules,which constitute a simultaneous inductive defini- tion of the judgments a even,stating that a is an even natural number,and a odd,stating that a is an odd natural number: 2.8a) zero even b odd succ(b)even (2.8b) a even succ(a)odd (2.8c)
PREVIEW 18 2.5 Iterated and Simultaneous Inductive Definitions Similarly, we may show that the successor operation is injective. Lemma 2.3. If succ( a1 ) is succ( a2 ), then a1 is a2. Proof. Similar to the proof of Lemma 2.1. 2.5 Iterated and Simultaneous Inductive Definitions Inductive definitions are often iterated, meaning that one inductive definition builds on top of another. In an iterated inductive definition the premises of a rule J1 . . . Jk J may be instances of either a previously defined judgment form, or the judgment form being defined. For example, the following rules define the judgment form − list, which states that a is a list of natural numbers: nil list (2.7a) a nat b list cons( a ; b ) list (2.7b) The first premise of rule (2.7b) is an instance of the judgment form a nat, which was defined previously, whereas the premise b list is an instance of the judgment form being defined by these rules. Frequently two or more judgments are defined at once by a simultaneous inductive definition. A simultaneous inductive definition consists of a set of rules for deriving instances of several different judgment forms, any of which may appear as the premise of any rule. Because the rules defining each judgment form may involve any of the others, none of the judgment forms can be taken to be defined prior to the others. Instead we must understand that all of the judgment forms are being defined at once by the entire collection of rules. The judgment forms defined by these rules are, as before, the strongest judgment forms that are closed under the rules. Therefore the principle of proof by rule induction continues to apply, albeit in a form that requires us to prove a property of each of the defined judgment forms simultaneously. For example, consider the following rules, which constitute a simultaneous inductive definition of the judgments a even, stating that a is an even natural number, and a odd, stating that a is an odd natural number: zero even (2.8a) b odd succ( b ) even (2.8b) a even succ( a ) odd (2.8c)