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)
|
