Third-order functionals on partial combinatory algebras

DOI10.1016/J.APAL.2022.103205MaRDI QIDQ2105095zbMATH OpenOpenAlexFDO

Authors Jetze Zoethout

Publication date 8 December 2022

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2103.09000

zbMATH Keywords

higher-order computabilitypartial combinatory algebrarealizability

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Higher-type and set recursion theory (03D65) Categorical logic, topoi (03G30) Categories of machines, automata (18B20) Topoi (18B25) Other nonclassical models of computation (68Q09)

Abstract: Computability relative to a partial function $f$ on the natural numbers can be formalized using the notion of an oracle for this function $f$. This can be generalized to arbitrary partial combinatory algebras, yielding a notion of `adjoining a partial function to a partial combinatory algebra $A$'. A similar construction is known for second-order functionals, but the third-order case is more difficult. In this paper, we prove several results for this third-order case. Given a third-order functional $Phi$ on a partial combinatory algebra $A$, we show how to construct a partial combinatory algebra $A[Phi]$ where $Phi$ is `computable', and which has a `lax' factorization property. Moreover, we show that, on the level of first-order functions, the effect of making a third-order functional computable can be described as adding an oracle for a first-order function.

Review text

This paper is concerned with computability on higher-order functions in the context of partial combinatory algebras (PCAs). The paper [\textit{J. van Oosten}, Notre Dame J. Formal Logic 47, No. 3, 311--318 (2006; Zbl 1113.03014)] offered a notion of oracle computability for general PCAs, while the paper [\textit{E. Faber} and \textit{J. van Oosten}, Computability 5, No. 2, 127--146 (2016; Zbl 1437.03136)] generalized this to second-order functional. This paper is now concerned with the third-order case. It was shown in [\textit{J. van Oosten}, Notre Dame J. Formal Logic 52, No. 4, 431--448 (2011; Zbl 1248.03026)] that, for each PCA \(A\), there is another PCA \(\mathcal{B}A\) whose elements are partial functions on \(A\). The main strategy in this paper is to view higher-order functional on \(A\) as lower-order ones on \(\mathcal{B}A\). The synopsis of the paper goes as follows: \begin{itemize} \item[\S 2] introduces partial combinatory algebras and the realizability toposes \textsf{RT}. In this paper, PCAs are always relative and ordered. \item[\S 3] introduces the relevant morphisms between PCAs, yielding a preorder-enriched bicategory of PCAs. \item[\S 4] revisits the paper [\textit{J. van Oosten}, Notre Dame J. Formal Logic 47, No. 3, 311--318 (2006; Zbl 1113.03014)], showing how to freely adjoin a partial function \(f:A\rightarrow A\) to get a new PCA \(A[f]\). \item[\S 5] introduces the PCA \(\mathcal{B}A\) of partial functions as in [\textit{J. van Oosten}, Notre Dame J. Formal Logic 52, No. 4, 431--448 (2011; Zbl 1248.03026)]. One of the central views of this paper is that \(\mathcal{B}A\) is best as a relative, ordered PCA, even if \(A\) itself is an ordinary PCA. It is shown how, at the level of realizability toposes, \(A[f]\) may be reconstructed using the construction \(\mathcal{B}-\), slicing, and image toposes, depending heavily on the fact that there is a geometric surjection \[ \mathsf{RT}(\mathcal{B}A)\rightarrow\mathsf{RT}(A) \] \item[\S 6] treats the second-order case, where the construction in [\textit{E. Faber} and \textit{J. van Oosten}, Computability 5, No. 2, 127--146 (2016; Zbl 1437.03136)] is reinterpreted as a construction actually taking place in \(\mathcal{B}A\). The author gives an example demonstrating that the elements of \(\mathcal{B}A\) enjoy a kind of double life in the sense that they are surely elements of \(\mathcal{B}A\), while, for each \(\alpha\in\mathcal{B}A\), there are other elements from \(\mathcal{B}A\) computing \(\alpha\) in a specific sense. \item[\S 7] is concerned with the third-order case. \end{itemize}

Recommendations

• Effective operations of type 2 in PCAs
• Partial combinatory algebras of functions
• On (co)products of partial combinatory algebras, with an application to pushouts of realizability toposes
• Internal partial combinatory algebras and their slices
• Ordered partial combinatory algebras

Cites work

• A general form of relative recursion
• Effective operations of type 2 in PCAs
• Geometric morphisms of realizability toposes
• Higher-order computability
• scientific article; zbMATH DE number 1405588 (Why is no real title available?)
• Internal partial combinatory algebras and their slices
• More on Geometric Morphisms between Realizability Toposes
• Ordered partial combinatory algebras
• Partial combinatory algebras of functions
• Realizability. An introduction to its categorical side

Cited in

(7)

• The cardinality of functionally complete algebras on a three element set
• Functional Pearls
• Ordinal analysis of partial combinatory algebras
• The Ohm-Rush content function III: Completion, globalization, and power-content algebras
• More on Geometric Morphisms between Realizability Toposes
• Effective operations of type 2 in PCAs
• A general form of relative recursion

This page was built for publication: Third-order functionals on partial combinatory algebras

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2105095)