Towards a Formal Theory of Computability
Simon Huber, Basil A. Karádais, Helmut Schwichtenberg · 2010
We sketch a constructive formal theory TCF + of computable functionals which allows to reason not only about the functionals themselves but also about their finite approximations. Types are built from base types by the formation of function types, ρ → σ. The intended semantical domains for the base types are non-flat free algebras, given by their constructors, where the latter are injective and have disjoint ranges; both properties do not hold in the flat case. In this setting we give an informal proof (based on Berger [2]) of Kreisel’s density theorem [7], and an adaption of Plotkin’s definability theorem [10, 11]. We then show that both proofs can be formalized in TCF +. The naive model of a finitely typed theory like TCF + is the full set theoretic hierarchy of functionals of finite types. However, this immediately leads to higher cardinalities, and does not lend itself well for a constructive theory of computability. A more appropriate semantics for typed languages has its roots in work of Kreisel [7] (which used formal neighborhoods) and Kleene [6]. This line of research was developed in a mathematically more