Topic: lattice theory of types

topics > computer science > data > Group: data type

exception handling by unique value
type algebras, typed lambda calculus, and type-complete languages
type retract
universal data type


Dana Scott discovered a lattice representation for computation which includes its own continuous function space. The lattice domain includes all well-behaved functions, and many sub-domains. It corresponds to a universal type with many type interpretations.

Scott's lattice is built by a partial ordering of partially defined functions. The number of "undefined" values orders each function, with the undefined everywhere function being zero or bottom. Allowable functions are monotonic on this ordering. The partially ordered functions form a mathematical lattice structure, and all monotonic functions on complete lattices have a fixed point. These fixed points are the solutions to recursive functions and the retracts for type value spaces. (cbb 5/80)

Subtopic: universal domain up

Quote: Scott proved the existence of a universal domain that contains sub-domains including function spaces [»straC3_1973]
Quote: Scott found universal domains that contained their own function spaces [»demeA_1978]

Subtopic: what is a lattice up

Quote: a lattice is a partially ordered set in which every pair has a greatest lower bound and least upper bound; meet and join [»simmGF_1963]

Subtopic: partial ordering via approximation up

Quote: in lattice theory, allow elements of a data type which approximate other elements [»scotD_1970]
Quote: Scott enhances a domain with a partial ordering based on degree of approximation

Subtopic: bottom as base of type lattice up

Quote: define the lattice for integers as: bottom, the integers, top [»scotD_1970]
Quote: a functional program for matrix multiply yields .bottom. for inappropriate arguments; it is perfectly general [»backJ8_1978a]

Subtopic: partial functions, function spaces, and fixed point up

Quote: in lattice theory, the set of partial functions are ordered by approximateness [»scotD8_1971]
Quote: solving partial functions for recursion is finding a fixed point; complete lattices guarantee this fixed point [»scotD8_1971]
Quote: the function spaces found by Scott include all ordinary and reasonable functions [»straC3_1973]
Quote: Scott argued that a universal domain only needs continuous functions [»straC3_1973]
Quote: all functions in an FP system map objects into objects; bottom-preserving, f.bottom. = .bottom. [»backJ8_1978a]

Subtopic: types on universal set up

Quote: Scott's type theory defines types on a universal set while avoiding Russell's paradox
Quote: if types define subsets of a universal type, then their unions and intersections are well-defined [»reynJC9_1983]

Subtopic: are there incomparable types up

Quote: shouldn't there be types sufficiently different that they do not induce union or intersection types?

Related Topics up

Topic: exception handling by unique value (8 items)
Topic: type algebras, typed lambda calculus, and type-complete languages (28 items)
Topic: type retract (12 items)
Topic: universal data type
(18 items)

Updated barberCB 7/04
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.