English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We develop synthetic notions of oracle computability and Turing reducibilityin the Calculus of Inductive Constructions (CIC), the constructive type theoryunderlying the Coq proof assistant. As usual in synthetic approaches, we employa definition of oracle computations based on meta-level functions rather thanobject-level models of computation, relying on the fact that in constructivesystems such as CIC all definable functions are computable by construction.Such an approach lends itself well to machine-checked proofs, which we carryout in Coq.  There is a tension in finding a good synthetic rendering of the higher-ordernotion of oracle computability. On the one hand, it has to be informativeenough to prove central results, ensuring that all notions are faithfullycaptured. On the other hand, it has to be restricted enough to benefit fromaxioms for synthetic computability, which usually concern first-order objects.Drawing inspiration from a definition by Andrej Bauer based on continuousfunctions in the effective topos, we use a notion of sequential continuity tocharacterise valid oracle computations.  As main technical results, we show that Turing reducibility forms an uppersemilattice, transports decidability, and is strictly more expressive thantruth-table reducibility, and prove that whenever both a predicate $p$ and itscomplement are semi-decidable relative to an oracle $q$, then $p$Turing-reduces to $q$.

Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions