Topic: exception handling by unique value
Topic: type algebras, typed lambda calculus, and typecomplete 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 wellbehaved functions, and many subdomains. 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 subdomains 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; bottompreserving, 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 welldefined [»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 typecomplete languages (28 items)
Topic: type retract (12 items)
Topic: universal data type (18 items)
