Interpreting higher computations as types with totality (Q1337495): Difference between revisions

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.