CS611 Lecture 6 Inductively Defined Sets and Functions 12 September 2001Scribe: Stephen Chong and Prakash Linga Lecturer: Andrew MyersMotivationWe have been using inference rules to define evaluation. For example,a0,σ⇓n0a1,σ⇓n1a0+ a1,σ⇓n(n0+ n1= n)However, when we do proof trees we use rule instances:2,σ⇓2 x, σ⇓22+x, σ⇓4Note that we don’t bother writing the side condition for rule instances: 2 + 2 = 4. The side condition isonly used to decide that this is a valid rule instance.We have been interested in finding the set A of all valid evaluations. An evaluation maps a commandand a state onto a new state, so A ⊆ Com × Σ × Σ. More generally, consider defining an arbitary set Ausing inference rules.TheRuleOperatorSuppose we have a rule instance of the formx1x2... xnxThis rule instance means that if the elements x1,x2,...,xnare all in A then x is also in A.Needless to say, if we have an axiom of the formxthen x ∈ A, as there are no premises to satisfy.For a given set of axioms and inference rules, we define the rule operator R : P(Com × Σ × Σ) →P(Com × Σ × Σ) as follows:R(S)=xx1x2... xnxis a rule instance and x1,...,xn∈ S The operator R “encapsulates” everything we know about the axioms and inference rules.Properties of the Rule OperatorThe rule operator R satisfies the following properties -• R(AB) ⊇ R(A)R(B)• R(AB) ⊆ R(A)R(B)• A ⊆ B ⇒ R(A) ⊆ R(B) (Operator R is monotonic)R(∅) gives all instances of the axioms. R2(∅) gives all evaluations that can be deduced in one step, i.e.that have a proof tree of depth 1.1What properties do we need for A?• Consistent — every element in A should be derivable from a rule, i.e. A ⊆ R(A)• Closed — there are no new elements to derive, i.e. A ⊇ R(A)These properties imply A = R (A). A is therefore a fixed point of R.Definition: For some function f : D → D and some x ∈ D,iff (x)=x then x is said to be a fixed pointof f .One function could have multiple fixed points, and indeed our rule operator R does in general havemultiple fixed points.Defining AFor inductively defined sets, we want A to contain all and only the evaluations with finite proof trees, i.e.we would likeA = R(∅) ∪ R2(∅) ∪ ...=n∈ωRn(∅)Claim: A =n∈ωRn(∅)isafixedpointofR.Proof:(1) A ⊇ R(A)Let x ∈ R(A). We need to show that x ∈ A.For this we will first show that ∀nRn(∅) ⊆ Rn+1(∅)For n = 0 this trivially holds for ∅⊆R(∅ ).Now assume the inductive hypothesis,Rn(∅) ⊆ Rn+1(∅)Using the monotonicity property of R we haveRn+1(∅) ⊆ Rn+2(∅)Hence, by induction, ∀nRn(∅) ⊆ Rn+1(∅).Now, x ∈ R(A),sothereissomeruleinstancex1x2... xnxwith x1,x2,...,xn∈ A.Since all the premises x1,x2,...,xn∈ A have finite proof trees, there must be some finite m such thatx1,x2,...,xn∈ Rm(∅), which implies x ∈ Rm+1(∅) ⊆ A. (Note: if there were an infinite number of premisesin the rule instance, then we would not be able to find a finite m. However, as all our inference rules have afinite number of premises, we are safe!)So, x ∈ R(A) ⇒ x ∈ A and thus A ⊇ R(A).(2) A ⊆ R(A)Let x ∈ A. x has a finite proof tree, so there exists some finite m such that x ∈ Rm(∅). So x1,x2,...,xn∈Rm−1(∅). Therefore x ∈ R(Rm−1(∅)).Since Rm−1(∅) ⊆ A, from monotonicity, R(Rm−1(∅)) ⊆ R(A). Therefore x ∈ R(A).So A ⊆ R(A).From (1) and (2) it follows that A = R(A)andsoA is a fixed point.Claim: A is the least closed set of R.Proof: Suppose B is closed under R,thatisB ⊇ R(B). We need to show that A ⊆ B.2∅⊆BSo R(∅) ⊆ R (B)R2(∅) ⊆ R2(B)......Rn(∅) ⊆ Rn(B)⇒ A =n∈ωRn(∅) ⊆n∈ωRn(B)=BSo A is the least closed set of R.Since all fixed points of R must be closed, A is also the least fixed point of R:∀B ⊆ Com × Σ × Σ,R(B)=B ⇒ A ⊆ BDefinition: fix :(D → D) → D is the least fixed point operator. It takes some relationship defined onD → D, and returns the least fixed point that the relationship implies. This is relative to some ordering onD: in this case, ⊆.We have just shown that fix(R)=A.FunctionsA function f : A → B can be regarded as a set{a0,b0, a0,b0,...}≡{a0→ b0,a1→ b1,...} ai∈ A, bi∈ BThis set is known as the extension of f .Whenf is regarded in this way f ⊆ A × B.Alternatively, we could write f ∈ A → B ⊆P(A × B)whereP(X)isthepowersetofX —thesetofall possible subsets of X. Note that we can also write BAfor A → B.By convention A → B means total functions from A to B,andABmeans partial functions from Ato B. In general we will only be dealing with total functions.Total functions must have certain properties:1. No a shows up more than once in the extension of f .Thatis,iff(a)=b1and f(a)=b2then b1= b2.2. Every a shows up at least once in the extension of f .We can write functions like inference rules provided the following conditions are met:1. Every a is covered by exactly 1 rule.2. There is a well-founded relation on A that the rules respect.For example, consider the successor function s : N → N:s(a)=2ifa =1s(n)+1 ifa = n +1Each natural number is covered by exactly one rule for s : 1 is covered by the first rule, and all numbersgreater than 1 are covered by the second. Since s(a)isdefinedintermsofs(n), we need some well–foundedordering ≺ on the natural numbers such that n ≺ a to ensure no infinite descending chains occur. Thenatural ordering on natural numbers satisifes this.The axiom and inference rule for s are:s(a)=2(where a =1)3s(n)=ys(a)=x(where a = n+1, x=y+1)An instance of the inference rule iss(37) = 38s(38) =