Logic in Computer Science An Introductory Course for Master Students Wang Ji jiwang@nudt.edu.cn Lecture One Preliminaries Logic in Computer Science { p.1/16 Theory of Equivalence Relations (A;R) (E1) For all x : xRx. (E2) For all x;y : If xRy then yRx. (E3) For all x;y;z : If xRy and yRz then xRz. Logic in Computer Science { p.2/16 Theory of Equivalence Relations (A;R) (E1) For all x : xRx. (E2) For all x;y : If xRy then yRx. (E3) For all x;y;z : If xRy and yRz then xRz. For all x and y, if there is a u such that xRu and yRu, then for all z, xRz if and only if yRz. Logic in Computer Science { p.2/16 A Primary Analysis The concept \Proposition" A formal language, formulas The concept \Follow from" Consequence relation The concept \Proof" A sequence of formulas, Axioms, Rules Logic in Computer Science { p.3/16 Induction Consider an initial set B U and a class F of functions containing just two members f and g, where f : U U ! U and g : U ! U Let B = fa;bg. How to de ne the set C which contains b;f(b;b);g(a);f(g(a);f(b;b)); Logic in Computer Science { p.4/16 Induction: from the top down A subset of S of U is closed under f and g i whenever elements x and y belong to S, then so do f(x;y) and g(x). S is inductive i B S and S is closed under f and g. Let C be the intersection of all the inductive subsets of U. Then C is inductive. Logic in Computer Science { p.5/16 Induction: from the bottom up Let C be the set of things which can be reached from B by applying f and g a nite number of times. De ne a constructive sequence to be a nite sequence < x 0 ; ;x n > of elements of U such that for each i n we have at least one of x i 2 B x i = f(x j ;x k ) for some j < i;k < i x i = g(x j ) for some j < i Then C is the set of all points x such that some construction sequence ends with x. Logic in Computer Science { p.6/16 C = C Let C = T fS : S is inductive g C = S n C n where C n is the set of points x such that some construction sequence of length n ends with x. We have C = C So, we call the set simply C and refer to it as the set generated from B by the functions in F. Logic in Computer Science { p.7/16 Induction Principle Assume that C is the set generated from B by the functions in F. If S is a subset of C which includes B and is closed under the functions of F, then S = C Logic in Computer Science { p.8/16 Recursion There is a set U, a subset B of U, and two functions f and g, where f : U U ! U and g : U ! U C is the set generated from B by f and g. The problem is how to de ne a function on C recur- sively. Logic in Computer Science { p.9/16 A Possible Solution 1. Rules for computing h(x) for x 2 B. 2. (a) Rules for computing h(f(x;y)), making use of h(x) and h(y). (b) Rules for computing h(g(x)), making use of h(x). Logic in Computer Science { p.10/16 A Possible Solution 1. Rules for computing h(x) for x 2 B. 2. (a) Rules for computing h(f(x;y)), making use of h(x) and h(y). (b) Rules for computing h(g(x)), making use of h(x). Is it enough? Logic in Computer Science { p.10/16 An Example Let U = R B = f0g f(x;y) = x y g(x) = x + 1 Then C is the set of natural numbers. Suppose we impose the following requirements on h: 1. h(0) = 0 2. (a) h(f(x;y)) = f( h(x); h(y)) (b) h(g(x)) = h(x) + 2 Logic in Computer Science { p.11/16 An Example Let U = R B = f0g f(x;y) = x y g(x) = x + 1 Then C is the set of natural numbers. Suppose we impose the following requirements on h: 1. h(0) = 0 2. (a) h(f(x;y)) = f( h(x); h(y)) (b) h(g(x)) = h(x) + 2 No such function h can exist. Why? Logic in Computer Science { p.11/16 Freely Generated Say that C is freely generated from B by f and g i in addition to the requirements for being generated we have 1. f c and g c are one to one, and 2. The range of f c , the range of g c , and the set B are pairwise disjoint. Here f c and g c are the restrictions of f and g to C. Logic in Computer Science { p.12/16 Recursion Theorem Assume that the subset C of U is freely generated from B by f and g. Further assume V is a set and F, G, and h functions such that h : B ! V and F : V V ! V and G : V ! V There there is a unique function h : C ! V such that 1. For x in B, h(x) = h(x) 2. For x, y in C, h(f(x;y)) = F( h(x); h(y)) and h(g(x)) = G( h(x)) Logic in Computer Science { p.13/16 Recursion Theorem: Proof Idea The idea is to let h be the union of many approximating functions. Logic in Computer Science { p.14/16 Recursion Theorem: Proof Sketch A function v is acceptable i the domain of v is a subset of C, the range a subset of V , and for any x and y in C: 1. If x 2 B and x 2 dom(v), then v(x) = h(x) 2. If f(x;y) 2 dom(v), then so do x and y, and v(f(x;y)) = F(v(x);v(y)). If g(x) 2 dom(v), then so do x, and v(g(x)) = G(v(x)). Let K be the collection of all acceptable functions, and let h be the union of K. Thus < x;y >2 h i v(x) = y for some v 2 K Logic in Computer Science { p.15/16 Recursion Theorem: Proof Sketch h meets the requirements. h is a function. h 2 K h is de ned throughout C h is unique. Logic in Computer Science { p.16/16