Interpreting higher computations as types with totality (Q1337495): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Set OpenAlex properties. |
||
(4 intermediate revisions by 3 users not shown) | |||
Property / author | |||
Property / author: Lill Kristiansen / rank | |||
Property / author | |||
Property / author: Dag Normann / rank | |||
Property / reviewed by | |||
Property / reviewed by: Simone Martini / rank | |||
Property / author | |||
Property / author: Lill Kristiansen / rank | |||
Normal rank | |||
Property / author | |||
Property / author: Dag Normann / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Simone Martini / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Total sets and objects in domain theory / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Π12-logic, Part 1: Dilators / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: The system \({\mathcal F}\) of variable types, fifteen years later / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Recursive Functionals and Quantifiers of Finite Types I / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Total objects in inductively defined types / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4694213 / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1007/bf01270624 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1965724811 / rank | |||
Normal rank |
Latest revision as of 10:05, 30 July 2024
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