Lecture 10 Fixed Points ad Infinitum M C Escher Moebius Ants CS655 Programming Languages University of Virginia Computer Science David Evans http www cs virginia edu evans Goal Understand the Least Fixed Point Theorem If D is a pointed complete partial order then a continuous function f D D has a least fixed point fixD f defined by D 20 Feb 2000 fn D n 0 University of Virginia CS 655 2 Last Time A domain is a structured set of values A function domain is constructed from two primitive domains D1 D2 by associating an element of D2 with each element of D1 A fixed point of a function f D1 D2 is an element d D such that f 20 Feb 2000 University of Virginia CS 655 d d 3 Last Time cont Any recursive definition can be encoded with a non recursive generating function by abstracting out the thing that is defined A fixed point of a generating function is a solution of its associated recursive definition 20 Feb 2000 University of Virginia CS 655 4 Last Time cont D is a partial order if is reflexive a transitive a anti symmetric a b and b c imply a c a b and b a imply a b D is a pointed partial order if it has a bottom element u D such that u d for all elements d D 20 Feb 2000 University of Virginia CS 655 5 Ordered Product Domains If D D and E E is are POs D x E D x E is a partial order ordered by d1 e1 if d1 20 Feb 2000 D DxE d2 e2 d2 and e1 E e2 University of Virginia CS 655 6 Ordered Product Example What is Nat x Nat 1 73 3 3 0 2 2 0 0 1 1 0 0 0 20 Feb 2000 University of Virginia CS 655 Hasse diagram 7 Ordered Function Domains If D D and E E is are POs D E D E is a partial order ordered by f D E f1 D E f2 if for all d D f1 d 20 Feb 2000 E f2 d University of Virginia CS 655 8 Ordered Function Example Bool false true false true true false What is Bool Bool false true true true false false true true false true true false false false true false 20 Feb 2000 University of Virginia CS 655 9 T Shirt Exercise What is the order of the domain Bool x Bool Bool includes xor and or implies 20 Feb 2000 University of Virginia CS 655 10 The Domain Nat 0 1 2 3 4 Nat 20 Feb 2000 University of Virginia CS 655 11 Ordered Function Bottom What is the bottom of Nat Nat 0 1 2 x If a function map has no entry for x it maps x to 20 Feb 2000 University of Virginia CS 655 12 Least Upper Bounds The least upper bound of a subset X of a domain D is the weakest element of X that is at least as strong as every other element of X l X D X if for every x X x l and for every m X such that x m x X l m 20 Feb 2000 University of Virginia CS 655 13 Least Upper Bounds in Nat Nat Nat 0 1 0 2 4 6 any element of 0 2 4 6 Nat 3 17 3 or 17 2 3 4 Nat 20 Feb 2000 University of Virginia CS 655 14 Complete Partial Orders A partial order D is complete if every chain in D has a least upper bound in D Any upward chain through a Hasse diagram converges to a limit All finite partial orders are complete Most sensible partial orders including Nat are complete see Gifford s notes for some incomplete POs 20 Feb 2000 University of Virginia CS 655 15 Monotonic Functions f D E is monotonic if d1 implies f d1 E D d2 f d2 Is not over Bool Bool monotonic Is x x 2 over Nat Nat monotonic What functions are monotonic over Nat Nat 20 Feb 2000 University of Virginia CS 655 16 Continuous Functions f D E is continuous if for all chains C in D f applied to the least element of the chain over D is the least element of f c for c C over E Continuity is like monotonicity but it works for limits of infinite chains also If the CPO is finite monotonicity implies continuity Continuity always implies monotonicity 20 Feb 2000 University of Virginia CS 655 17 Monotonic Continuous Functions in Domain Nat 0 1 2 3 4 Nat What is a monotonic function in Nat What is a continuous function in Nat 20 Feb 2000 University of Virginia CS 655 18 Least Fixed Point Theorem If D is a pointed complete partial order then a continuous function f D D has a least fixed point fixD f defined by fn D n 0 The least upper bound of applying f any number of times starting with D D 20 Feb 2000 University of Virginia CS 655 19 InSanity Check g Nat Nat Nat Nat f n if n 0 then 1 else n f n 1 What is fixNat Nat g 20 Feb 2000 University of Virginia CS 655 20 Sanity Check g Nat Nat Nat Nat f n if n 0 then 1 else n f n 1 What is fixNat Nat g 20 Feb 2000 University of Virginia CS 655 21 What is the bottom of Nat Nat x x Nat 20 Feb 2000 University of Virginia CS 655 22 What is g x x Nat g f n if n 0 then 1 else n f n 1 g x x Nat 0 1 x x 0 and x Nat 20 Feb 2000 University of Virginia CS 655 23 What is g g x x Nat g f n if n 0 then 1 else n f n 1 g 0 1 x x 0 and x Nat 0 1 1 1 x x 1 and x Nat 20 Feb 2000 University of Virginia CS 655 24 What is LUB gn x x Nat g f n if n 0 then 1 else n f n 1 g 0 1 x x 0 and x Nat 0 1 1 1 2 2 3 6 x x x Nat 20 Feb 2000 University of Virginia CS 655 25 Getting to the of things Think of bottom as the element with the least information or the worst possible approximation To find the least fixed point in a function domain start with the bottom of the function domain and iterate 20 Feb 2000 University of Virginia CS 655 26 Fixed Point Theorem Do all calculus terms have a fixed point Smullyan Is there a Sage bird 20 Feb 2000 University of Virginia CS 655 27 Finding the Sage Bird F X such that FX X Proof Let W x F xx and X WW X WW x F xx W F WW FX 20 Feb 2000 University of Virginia …