========================================================================= Mathematical foundations -- domain theory and least fixed point semantics ========================================================================= Outline ------- A. Motivating example -- factorial B. Graph of a function C. Partially ordered sets D. Continuous functions E. Domains ------------------------------------------------------------------- Notation: backslash (\) is a lambda, ([=) is approximates, and (|_|) is least upper bound, _|_ is bottom. ------------------------------------------------------------------- Domain theory -- data structures approprate for semantics Data space -- values that programs can manipulate D = Nat + Tr + [D->D] But |D| < |D->D|, so we need to interpret [D->D] as some subset of D->D. Put a partial ordering on value space D. Ordering relations on elements of domains -- recursive data domains (e.g., D) -- recursive function definitions and fix A. Motivating Example --------------------- Consider fact(x) = if x=0 then 1 else x*fact(x-1) fi fact: Integers->Integers_|_ We can treat this as a functional equation, and look for solutions for fact(x), and there are multiple solutions. fact_|_(x) = { x! x >= 0 { _|_ x < 0 factV(x) = { x! x >= 0 { V/(((-1)^|x|)*(|x|-1)!) x < 0 for any V in Integers. To solve for 'fact', 1. Abstract on 'fact': fact = (\f.\x.if x=0 then 1 else x*f(x-1) ) fact Let F = \f.\x.if x=0 then 1 else x*f(x-1) 2. Notion of a partial function -- only terminates on certain inputs O = \x._|_ represents a program that never terminates regardless of the input, or a graph with no values. 3. Use F and O to define more functions, successive approximations to 'fact' f0 = O first approximation (not a very good one) f1 = F(f0) = F(O) = \x.if x=0 then 1 else x*O(x-1) fi = \x.if x=0 then 1 else _|_ fi f1 has the graph {(0,1)} f2 = F(f1) = \x.if x=0 then 1 else x*(if (x-1)=0 then 1 else _|_) = \x.if x-0 then 1 else if x=1 then 1 else _|_ f2 has the graph {(0,1),(1,1)} fi = F^i(O) is x! for 0<=xinfinity, this becomes fact_|_, which matches our intuition that the function we defined should not terminate for x<0. B. Graph of a function ---------------------- The graph of a function f is { (domain, range) | f(domain) = range }. For a function Omega = \x. undefined the graph(Omega) = null set. Finite subfunctions of factorial can be realized by the functional F where F = \f.\x. if x = 0 then 1 else x * f(x - 1) fi Then F(Omega) = \x. if x = 0 then 1 else undefined with graph(F(Omega)) = {(0, 1)} Taking the limit graph(fact) = lim graph(F^i(Omega)) as i -> infinity = Union graph(F(Omega)) for all i >= 0 The semantic interpretation of factorial can be extended to values less than zero, For example: factv = \x. { if x >= 0 then x! else v / ((-1)^|x| (|x| - 1)!)} where v is a number. This interpretation produces a class of definitions for fact and selecting the intersection of all the factv definitions produces a unique definition for fact. F^i(Omega) corresponds to a functions that performs i unrollings. F^i(Omega) = if x = 0 then 1 else if x = 1 then 1 else if x = 2 then 2! ... else if x = i-1 then ... else undefined C. Partially ordered sets ------------------------- If value = Nat + Bool + proc proc = stat -> stat@ where stat@ is stat extended with unbound state = Id -> (value union unbound) In a functional language D = Nat + Bool + (D -> D) ------------------------------------------------------------------------------ Note: There are more reals than integers. Proof: Assume that there is a map from the integers(1...) to the reals (0<= r < 1) r:int -> reals and that a map d from reals X integers -> digits giving a decimal representation so that d(r(i),j) is the jth digit of the ith real number. Then the real number r' = Sum( 10^-i * mod(d(r(i),i)+1,10) from 1 to infinity is a not in the map r because it differs from all of the other real numbers in at least one digit. Contradiction. ------------------------------------------------------------------------------ The map D -> D has cardinality greater than D if |D| >= 2. Proof: Suppose m maps D to D -> D such that for all f in D -> D there exists a d such that m(d) = f. Let f* = {(d, d') where d' != m(d)(d)} This is possible because |D| >= 2. Let d* satisy the supposition with m(d*) = f*. Then if f*(d*) = d*' the definition of f* implies that d*' != m(d*)(d*) but m(d*)(d*) = f*(d*) -- Contradiction. ------------------------------------------------------------------------------ D. Continuous Functions ----------------------- (A subset of the functions from D to D such that the diagonalization argument doesn't work.) An approximation of ordering of sets can be defined by set inclusion: X [= (approximates) Y if and only if Y contains X or X = Y. Definition. A relation [= : D X D -> Bool is a partial ordering on D if and only if: 1) for all a in D, a [= a (reflexivity) 2) for all a, b in D, a [= b, b [= a then a = b (antisymmetry) 3) for all a, b, c in D, a [= b, b [= c implies a [= c (transitivity) Definition. If f and g are functions then f [= g if and only if for all x, y such that x [= y then f(x) [= g(y). Least upper bounds (join operation) Definition. Given poset (D, [=), for all a, b in D "a |_| b" is the element in D (if it exists) such that: 1) a [= (a |_| b) and b [= (a |_| b). 2) for all elements d in D, a [= d and b [= d imply (a |_| b) [= d. Definition. If X is a subset of D partially ordered by [=, |_|X denotes the element (if it exists) such that: 1) for all x in X, x [= |_|X. 2) for all d in D, if for all x in X, x [= d, then |_|X [= d. The natural numbers Nat can be ordered by <= and |_|Nat [= infinity which is not an element of Nat but can be used to augment Nat. Definition. A chain is a sequence of elements x(0), x(1), ... such that for all i x(i-1) [= x(i). The limit of a chain C is |_|C. Definition. A complete partial order (cpo) D is a partial order in which every chain has a limit in D. Definition. If x [= y for all y in D then x is the least element of D. Definition. A partially ordered set is a pointed cpo if and only if it is a cpo and has a least element. E. Domains ---------- To impose a partial order on the primitive domains(Bool, Nat), we can have the discrete partial ordering a [= b if and only if a = b. Compound domains can be constructed using lifting, +, X, and ->. Lifting: Given a poset (D, [=) then its lifting D* is the set {D U {undefined}, [=* } where d [=* d' if and only if d = undefined or d, d' are elements of D and d [= d'. Cross Product (X): Given posets (A, [=A), (B, [=B) then the product (A X B, [=X) is the set {(a,b) | a is an element of A and b is an element of B} partially ordered by (a,b) [=X (a',b') if and only if a [=A a' and b [=B b'. Sum (+): Given posets (A, [=A), (B, [=B) then their disjoint union A+B is the set { (0,a) | a is an element of A and (0,b) | is an element of B} with partial order d [=+ d' if and only if (d = (0,a), d' = (0,a') and a [=A a') or (d = (1,b), d' = (1,b') and b [=B b'). Review: Approximations of function Fact 1st Approximation Graph(Omega) = {} 2nd Approximation Graph F(Omega) = { (0,1) } 3rd Approximation Graph F(F(Omega)) = { (0,1), (1,1) } . . inf Graph U = { (i, i!) } i=0 Graph is set of completed elements. An element is added to Graph for each new i Approximation relation between functions: f [= g = for all x f(x) [= g(x) Example: (a) ( lambda n.1 ) x = 1 (b) ( lambda n.n mod 2 = 0 --> 1 | bottom ) (i.e., returns 1 or bottom) ____________________ | ______________| | | | | | V 0 1 2 3 0 1 2 3 \ | | / \ | | / \ \/ / \ \/ / bottom bottom Therefore, (b) [= (a) X - cross product + - sum [ --> ] - function - watch for cardinality problems Monotonicity = order preserving f: D-->D x approx. y y \ f(y) / \ / \ / f(x) & f(y) map to \ y f(x) / comparable points ----> \ \ / / | \ x / | \ / | \ / Domain D | \ / | \ / V for all x,y such that x approx. y --> f(x) approx f(y) Example: factorial function fact: Nat-->Nat maps natural number to its factorial, another natural number The functional F: (Nat --> Nat) --> (Nat --> Nat) maps function to a function If F is monotonic we can form a chain omega [= F(omega) [= F(F(omega)) by monotonicity. Repeated application of function F can be shown as: F(F(F...(o)) @ infinity map to itself . o=omega \ . / \ | / \ F(F(F(F(o)))) / \ \ / \ F(F(F(o))) / \ | / \F(F(o)) / \ \ / \ F(o)/ \ | / \|/ o - - - - least element of domain This is a complete partial ordering (cpo) if function f [= g then for all x,y such that x [= y --> f(x) approx f(y) The (Nat -> Nat+bottom) is a cpo. The Least Upper Bound (|_|) of F above exists and is the F @ infinity shown above. The function maps to itself. ------------------------------------------------------------------------ If A and B are cpo's then A X B is a cpo If (a,b) s.t. a is an element of A, b is an element of B then: (a,b) [= (c,d) iff (a [= c) & (b [= d) If a is |_| of A, and b is |_| of B then (c,d) resides 'above' (a,b) in the domain of AXB. ------------------------------------------------------------------------ If F is monotonic then chains get mapped to chains. f: A-->B is continuous iff for any chain X f(|_|(X)) = |_|({f(x) | x is an element of X }) On finite domains, Monotonicity implies Continuity ------------------------------------------------------------------------ An example of a monotonic function that is not continuous: Let (D, <=) be the natural numbers ordered by arithmetic order, augmented with w as the greatest element: D = {0, 1, 2, . . ., w} 0 [= 1 [= 2 [= . . . [= w The domain of pairs D x D is defined as usual. Consider the function f: (D x D) -> (D x D) defined as follow: / if a = w or b = w f() = { \ otherwise Case analysis shows that f is monotonic. Now consider the chain C = { | k member Nat }: <0, 1> [= <1, 1> [= <2, 1> [= . . . Note that C does not contain the element , although the least upper bound of C (or |_| C, for short) is . For f to be continuous, we need to have f(|_| C) = |_| { f(c) | c member C }. However, we have: (1) f(|_| C) = f() = (2) |_| { f(c) | c member C } = |_| { c | c member C } = Thus, f is monotonic but not continuous. (f is order-preserving but not limit-preserving.) ----------------------------------------------------------------------- Proposition: Every continous function is monotonic. Let x [= y. y = |_| {x,y} Then f(y) = f(|_| {x,y} ) = |_| { f(x), f(y) } =] f(x) i.e., f(x) [= f(y) ------------------------------------------------------------------------ Booleans (Boolean ) _|_ T F bottom maps to T \ / F maps to T | T maps to itself bottom A picture of the domain [Boolean --> Boolean ]: _|_ _|_ {(t,t)(t,f)(bottom,t)} {(t,f)(f,f)(bottom,f)} | | | | {(t,t)(t,f)} {(t,t)(f,t)} {(t,f)(f,f)} {(f,t)(f,f)} \ | | / \ | | / { (t,t) } { (t,f) } { (f,t) } { (f,f) } \ \ / / \_________\_ _/_________/ \/ {} Each point in the above picture is the graph of a function in the domain [Boolean --> Boolean ]. _|_ _|_ (In each such function, all pairs of the form (a,bottom) have been omitted.) ------------------------------------------------------------------------ Continuous functions have fixed points Given F [D --> D] and an element of D, d d is a fixed point of F iff F(d)=d d is the least fixed point of F if for all elements e of D such that F(e) = e, d [= e. Theorem: If D is a pointed cpo then the least fixed point of a continuous function F: [D --> D] a.) exists inf. i b.) and has the value |_| F (bottom) i=0 inf. i Defn: fix F = |_| F (bottom) i=0 Proof of a.): Show that fix F is a fixed point of F (i.e. show that F(fix F) = fix F). inf. i inf. i F( |_| F (bottom)) = |_| F(F (bottom)) i=0 i=0 inf. i+1 inf. i+1 |_| F (bottom) = (|_| F (bottom)) join bottom = fix F i=0 i=0 Proof of b.): Show that fix F is the least fixed point of F. Recall definition of |_| X (join of set X) a.) for all x that is an element of X: x [= |_| X b.) if for all x that is an element of X, x [= d then |_| X [= d Let e, be an element of D and a fixed point bottom [= e (by definition of bottom) F(bottom) [= F(e) (by monotonicity of F) = e (because e is a fixed point of F) F(F(bottom)) [= F(e) = e . . i F (bottom) approx F(e) = e, forall i inf. i thus: fix F = |_| F (bottom) [= e i=0 and hence fix F is the least fixed point of F. ------------------------------------------------------------------------ Example: Fact = lambda x. if x=0 --> 1 | x*f(x-1) F = lambda f. lambda x. if x=0 --> 1 | x*f(x-1) (F is a functional) i Fact can be approximated using F (omega) F(omega) = (lambda f. lambda x. if x=0 --> 1 | x*f(x-1)) omega = lambda x. if x=0 --> 1 | x*omega(x-1) = lambda x. if x=0 --> 1 | bottom F(F(omega)) = (lambda f. lambda x. if x=0 --> 1 | x*f(x-1)) F(omega) = (lambda x. if x=0 --> 1 | x*F(omega)(x-1)) = (lambda x. if x=0 --> 1 | x*F(omega)(x-1)) F(omega)(x-1) = (lambda x. if x=0 --> 1 | bottom)(x-1) = (if (x-1)=0 --> 1 | bottom) F(F(omega)) = (lambda x. if x=0 --> 1 | x*(if (x-1)=0 --> 1 | bottom)) With each application of F we get a "more defined" function. ------------------------------------------------------------------------ How do we know that this is a continuous function? Functions that are strict return no information if they "encounter" bottom. For example: for a function that returns a triple. <1,2,bottom> [= <1,2,5> Monotonicity - < > triples lower down in the partial order will be more likely to contain bottom - results should preserve order. If..then..else is strict in the conditional slot. Read Schmidt for more info...