Effective operations of type 2 in PCAs

DOI10.3233/COM-150048MaRDI QIDQ5740205zbMATH OpenOpenAlexFDO

Authors Eric Faber, Jaap van Oosten

Publication date 25 July 2016

Published in Computability (Search for Journal in Brave)

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

zbMATH Keywords

realizabilitycomputability theorypartial combinatory algebraTuring degreerealizability toposcomputable functionaleffective operation

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Higher-type and set recursion theory (03D65) Abstract and axiomatic computability and recursion theory (03D75)

Abstract: We exhibit a way of "forcing a functional to be an effective operation" for arbitrary partial combinatory algebras (pcas). This gives a method of defining new pcas from old ones for some fixed functional, where the new partial functions can be viewed as computable relative to that functional. It is shown that this generalizes a notion of computation relative to a functional as defined by Kleene for the natural numbers. The construction can be used to study subtoposes of the Effective Topos. We will do this for a particular functional that forces every arithmetical set to be decidable. In this paper we also prove the convenient result that the two definitions of a pca that are common in the literature are essentially the same.

Recommendations

• On (co)products of partial combinatory algebras, with an application to pushouts of realizability toposes
• Third-order functionals on partial combinatory algebras
• Internal partial combinatory algebras and their slices
• A general form of relative recursion
• Partial combinatory algebras of functions

Cites work

• A general form of relative recursion
• Geometric morphisms of realizability toposes
• More on Geometric Morphisms between Realizability Toposes
• Ordered partial combinatory algebras
• Realizability with a local operator of A. M. Pitts
• Recursive Functionals and Quantifiers of Finite Types I
• Relative computability in the effective topos

Cited in

(5)

• Internal partial combinatory algebras and their slices
• A general form of relative recursion
• Third-order functionals on partial combinatory algebras
• Realizability interpretation of PA by iterated limiting PCA
• Characterizing partitioned assemblies and realizability toposes

This page was built for publication: Effective operations of type 2 in PCAs

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