Interpreting higher computations as types with totality (Q1337495)

From MaRDI portal
Revision as of 09:05, 30 July 2024 by Openalex240730090724 (talk | contribs) (Set OpenAlex properties.)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
scientific article
Language Label Description Also known as
English
Interpreting higher computations as types with totality
scientific article

    Statements

    Interpreting higher computations as types with totality (English)
    0 references
    6 November 1994
    0 references
    The paper may be seen as a foundational study on the notion of totality, using Girard's qualitative domains as a tool. The starting observation is that in qualitative domains there is no ``intrinsic'' way to refer to total objects. Hence, the authors add more structure to qualitative domains, defining (partial) \(E\)-structures and totality domains, where a certain subset of total elements is selected (interestingly, these total elements are not in general the maximal elements of the domain). Each of these new classes of structures is proved closed under products \(\Pi (x\in X)Y_x\) indexed by stable parameterization. The principal object of study is now introduced by a monotone inductive definition: a hierarchy of totality domains and of names for them, where new structures are obtained via stable parameterization. The main theorem of the paper, proved by the so-called mollification method, is that the complexity of the hierarchy definition is equivalent to recursion in Kleene's \({}^3 E\) functional.
    0 references
    recursive functionals
    0 references
    qualitative domains
    0 references
    totality domains
    0 references
    mollification
    0 references
    0 references
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references