Effective operations of type 2 in PCAs

DOI10.3233/COM-150048zbMATH Open1437.03136arXiv1408.4984OpenAlexW2121004126MaRDI QIDQ5740205FDOQ5740205

Authors: Eric Faber, Jaap van Oosten 

Publication date: 25 July 2016

Published in: Computability (Search for Journal in Brave)

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.

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

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

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)

Cites Work

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

Cited In (5)

• 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
• Internal partial combinatory algebras and their slices

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)