[PLT logo] Lecture 6 Supplement, Comp 311

Domains Supporting Recursive Definitions

Slogan: Computation is successive approximation

Let us explore what properties domains (sets of data values) and functions on those domains must have to support recursive defintions. In the detour in Lecture 6, we informally showed how to construct the fixed-point of a function mapping sets to sets. In this lecture, we study this issue more rigorously in a general setting. Why does this question matter? It shows the boundaries of what can be expressed computationally. Much of mathematics lies outside the reach of computation.

We begin by reviewing a standard defintion from discrete mathematics.

A partial order is a set D together with a relation <= (which we will read as "approximates") on D (a subset of D x D) with the following three properties:

  • (reflexivity) For all d in D: d <= d.
  • (anti-symmetry) For all d1, d2 in D: d1 <= d2 and d2 <= d1 implies d1 = d2.
  • (transitivity) For all d1, d2, d3 in D: d1 <= d2 and d2 <= d3 implies d1 <= d3.

    • Some examples include:

  • 2^N (the set of all subsets of the natural numbers N) under the subset ordering.
  • the set of finite alphabetic strings under the prefix ordering.
  • the natural numbers 0, 1, ... under the usual <= ordering.
    •

    A partial order does not have enough structure to support the general solution of fixed point equations. We need to add the following restriction. A chain C in a partial order (D,<=) is a (possibly empty) denumerable sequence c1, c2, ..., cn, ... such that 

    c1 <= c2 <=  ... <= cn <= ...
    An upper bound for a chain C in (D,<=) is an element d in D such that ci <= d for all ci in C. A partial order (D,<=) is complete iff every chain C has a least upper bound. (An upper bound c* for C is least if c* approximates every upper bound for C.) We typically abbreviate the term complete partial order as cpo. Note that chain can be empty, implying that every cpo has a least element. We call this least element "bottom" and typically denote it bot. As we will see, bot corresponds to divergence.

    Of the three examples of partial orders given above, only the first one is complete. In the partial order of finite alphabetic strings, a chain of the form 

    "a" <= "aa" <= "aaa" <= ...
    has no upper bound, much less a least upper bound. Similarly, in the partial order (N,<=), the chain 
    0 <= 1 <= 2 <= ...
    has no upper bound. In essence, these spaces are missing the "limit" points of chains of approximations.

    Common CPO's in Programming Languages

    The domain of data values supported by a programming language forms a cpo. Assume that we prohibit functions as arguments and return values in LC. Then the only kinds of semantic objects in the language are numbers and unary functions mapping numbers to numbers. We can view this domain as a cpo as follows:
  • The numbers form a "flat" cpo where all distinct numbers m, n are incomparable, i.e., m <= n implies m = n. To satisfy the completeness property, we must add an extra element bot such that bot <= n for every integer n. The element bot represents a non-terminating computation.
  • The partial functions mapping integers to integers
    • are ordered as follows: F <= G iff F is a subset of G (when both F and G are interpreted as sets of ordered pairs).     The everywhere undefined function (empty set) obviously approximates all other functions. Numbers and functions are incomparable. The special element bot approximates all functions as well as all numbers. Why? An attempt to define a function can diverge, which is different from defining the everywhere divergent function. (The latter produces a closure which can be identified using the {\tt function?} primitive.)

    Consider the function definition written in Scheme: 

    (define fact 
  (lambda (n)
    (if (zero? n)
        1 
        (* n (fact (sub1 n))))))
    We can construct a functional corresonding to this function that maps an estimate for the meaning of fact into a better estimate: 
    (define FACT 
  (lambda (fact)
    (lambda (n) 
      (if (zero? n)
          1 
          (* n (fact (sub1 n))))))

    Given the empty function, FACT constructs the partial function {(0,1)} (that diverges everywhere except for returning 1 when the input is 0). All computable functions including FACT are monotonic: if x <= y then FACT(x) approximates FACT(y). Given this property and the property that FACT is continuous (all computable functions are continuous), we can deduce (by repeatedly appealing to the monotonicity of FACT): 

    empty <= FACT(empty) <= ... FACT(...FACT(emtpy)) <= ...
    The preceding sequence is clearly a chain. Hence, it must have a least upper bound which we write fix(FACT) because it is least fixed fixed-point of the functional FACT. This function the meaning of fact determined by the recursive definition above. In general, every computable function mapping a cpo D to D has a least fixed-point. Hence, we can interpret any recursive definition as the least fixed-point of the corresponding function.

    The Full Domain of LC

    We made the simplifying assumption that functions are never passed as arguments or returned as values in describing the domain of LC above. What happens if we relax these restrictions? Let D denote (stand for) the domain of LC. It must satisfy the following equation 
    D = Zbot + (D -> D)
    where Zbot is the integers augmented by bot, + means the standard union operation except bottom elements are coalesced, and (D -> D) means the set of all strict continuous functions mapping D into D. (An function f mapping the cpos D1, D2, ... Dn into the cpo D0 is strict iff f(d1,d2,...,dn) = bot if any di = bot.)

    This equation can be interpreted as a recursive definition of the domain D. We can solve this equation by constructing a functional on domains and taking its least fixed-point. But a lot of technical machinery must be developed. First we have to show that the set of domains forms a cpo. Then we have show that the + and -> operations (functions) on domains are continuous. This deeper inquiry into the semantics of LC is the subject matter of Comp 511.

    cork@cs.rice.edu/ (adapted from shriram@cs.rice.edu)