constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
The notion of Scott-complete categories is a category theoretic generalization of the notion of Scott domains from domain theory, and as such it provides categorical semantics for the un-typed lambda calculus and related programming languages.
A Scott domain is a directed-complete partial order (dcpo) that is
algebraic, in that every element is a directed join of compact elements, and there is a bottom element;
consistently complete, i.e., every nonempty subset with an upper bound has a least upper bound.
The suitable notion of morphisms between Scott domains is that of directed-join-preserving monotone functions. These are the same as continuous functions with respect to the Scott topology.
Scott domains forms a cartesian closed category that supports the solution of recursive domain equations.
Scott domains admit a simple description in terms of “information systems”, which can help to calculate Scott domains and to cement the computation / information-based intuitions.
A category is Scott-complete if it is
Scott-complete categories and directed colimit-preserving functors form a category .
This category is cartesian closed and supports the solution of recursive domain equations.
Last revised on May 4, 2023 at 09:02:42. See the history of this page for a list of all contributions to it.