PowerPoint PresentationGoal: Understand the Least Fixed Point TheoremLast TimeLast Time, cont.Slide 5Ordered Product DomainsOrdered Product ExampleOrdered Function DomainsOrdered Function ExampleT-Shirt ExerciseThe Domain NatOrdered Function BottomLeast Upper BoundsLeast Upper Bounds in NatComplete Partial OrdersMonotonic FunctionsContinuous FunctionsMonotonic/Continuous Functions in Domain NatLeast Fixed Point TheoremSanity CheckSlide 21What is the bottom of Nat  Nat?What is (g { <x, > | x  Nat })?What is (g (g { <x, > | x  Nat }))?What is LUB (gn { <x, > | x  Nat }))?Getting to the  of thingsFixed Point TheoremFinding the Sage BirdWhy of Y?Still Uncomfortable?Remember the problem reducing YChurch-Rosser TheoremChargeDavid Evanshttp://www.cs.virginia.edu/~evansCS655: Programming LanguagesUniversity of VirginiaComputer ScienceLecture 10: Fixed Points ad InfinitumM.C. Escher, Moebius Ants20 Feb 2000 University of Virginia CS 655 2Goal: Understand theLeast Fixed Point TheoremIf D is a pointed complete partial order, then a continuous function f: D  D has a least fixed point (fixD f) defined byD { (fn D ) | n  0 }20 Feb 2000 University of Virginia CS 655 3Last 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 d = d.20 Feb 2000 University of Virginia CS 655 4Last 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 5Last Time, cont.•(D, ) is a partial order if is:–reflexive: –transitive: –anti-symmetric: •(D, ) is a pointed partial order if it has a bottom element u  D such that u d for all elements d  D.a b and b a imply a = ba aa b and b c imply a c20 Feb 2000 University of Virginia CS 655 6Ordered Product DomainsIf <D, D > and <E, E > is are POs, <D x E , D x E > is a partial order, ordered by:<d1, e1> D x E <d2, e2> if d1 D d2 and e1 E e220 Feb 2000 University of Virginia CS 655 7Ordered Product Example•What is << Nat,  > x < Nat,  >>?<0, 0><0, 1><1, 0><0, 2><2, 0><1, 73><3, 3>(Hasse diagram)20 Feb 2000 University of Virginia CS 655 8Ordered Function DomainsIf <D, D > and <E, E > is are POs, <D  E , D  E > is a partial order, ordered by: f  D  Ef1 D  E f2 if for all d  D,(f1 d) E (f2 d)20 Feb 2000 University of Virginia CS 655 9Ordered Function Example< Bool,  > = { false, true } false  true true  falseWhat is << Bool,  >  < Bool,  >>?<{false, false}, {true, false}><{false, false}, {true, true}><{false, true}, {true, false}><{false, true}, {true, true}>20 Feb 2000 University of Virginia CS 655 10T-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 11The Domain Nat Nat 0123 4...20 Feb 2000 University of Virginia CS 655 12Ordered 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 13Least 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 Xif for every x  X, x l and for every m  X such that x m x  X, l m20 Feb 2000 University of Virginia CS 655 14Least Upper Bounds in Nat Nat 0123 4...Nat{ 0, 2, 4, 6, ... } =Nat{Nat, 3, 17} = any element of { 0, 2, 4, 6, ... } 3 or 1720 Feb 2000 University of Virginia CS 655 15Complete 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 16Monotonic Functions•f  D  E is monotonic if d1 D d2 implies (f d1) E (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 17Continuous 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 monotonicity20 Feb 2000 University of Virginia CS 655 18Monotonic/Continuous Functions in Domain Nat Nat 0123 4...What is a monotonic function in Nat?What is a continuous function in Nat?20 Feb 2000 University of Virginia CS 655 19Least 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 byD { (fn D ) | n  0 } The least upper bound of applying f any number of times, starting with D.20 Feb 2000 University of Virginia CS 655 20Sanity Checkg: (Nat  Nat)  (Nat  Nat) =  f. n. if (n = 0) then 1 else (n * ( f (n - 1)))What is (fixNat  Nat g)?In20 Feb 2000 University of Virginia CS 655 21Sanity Checkg: (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 22What is the bottom of Nat  Nat? { <x, > | x  Nat }20 Feb 2000 University of Virginia CS 655 23What 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 24What 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,