Map Index Random Help Topics

Topic: lattice theory of types

topics > computer science > data > Group: data type

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

Summary

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

 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

 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

 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

 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

 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

 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

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

Related Topics

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