Interpreting higher computations as types with totality
type: Item
instance of: scholarly article
title: Interpreting higher computations as types with totality
zbMATH Open document ID: 0830.03019
DOI: 10.1007/BF01270624
published in: Archive for Mathematical Logic
publication date: 1994-11-06T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03D65
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 68Q05
zbMATH DE Number: 682649
zbMATH Keywords: recursive functionals
zbMATH Keywords: qualitative domains
zbMATH Keywords: totality domains
zbMATH Keywords: mollification
author: Lill Kristiansen
author: Dag Normann
reviewed by: Simone Martini
MaRDI profile type: Publication
cites work: Total sets and objects in domain theory
cites work: Π12-logic, Part 1: Dilators
cites work: The system \({\mathcal F}\) of variable types, fifteen years later
cites work: Recursive Functionals and Quantifiers of Finite Types I
cites work: Total objects in inductively defined types
cites work: Q4694213
full work available at URL: https://doi.org/10.1007/bf01270624
OpenAlex ID: W1965724811
Recommended article: Q3750112
Recommended article: Computational higher-dimensional type theory
Recommended article: An intuitionistic theory of types with assumptions of high-arity variables
Recommended article: Semantics of higher inductive types
Recommended article: Q4247306
Recommended article: Q4348037
Recommended article: Computability in higher types, P\(\omega\) and the completeness of type assignment
Recommended article: Denotational semantics for intuitionistic type theory using a hierarchy of domains with totality
Recommended article: Interpreting descriptions in intensional type theory
Recommended article: Expressing computational complexity in constructive type theory
description: scientific article; zbMATH DE number 682649