Constructive and Synthetic Reducibility Degrees: Post's Problem for Many-one and Truth-table Reducibility in Coq - Archive ouverte HAL Access content directly
Conference Papers Year :

Constructive and Synthetic Reducibility Degrees: Post's Problem for Many-one and Truth-table Reducibility in Coq

(1, 2) , (2)
1
2

Abstract

We present a constructive analysis and machine-checked theory of one-one, many-one, and truth-table reductions based on synthetic computability theory in the Calculus of Inductive Constructions, the type theory underlying the proof assistant Coq. We give elegant, synthetic, and machine-checked proofs of Post's landmark results that a simple predicate exists, is enumerable, undecidable, but many-one incomplete (Post's problem for many-one reducibility), and a hypersimple predicate exists, is enumerable, undecidable, but truth-table incomplete (Post's problem for truth-table reducibility). In synthetic computability, one assumes axioms allowing to carry out computability theory with all definitions and proofs purely in terms of functions of the type theory with no mention of a model of computation. Proofs can focus on the essence of the argument, without having to sacrifice formality. Synthetic computability also clears the lense for constructivisation. Our constructively careful definition of simple and hypersimple predicates allows us to not assume classical axioms, not even Markov's principle, still yielding the expected strong results.
Fichier principal
Vignette du fichier
forster_jahn_synthetic_reducibility_csl23.pdf (674.96 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03901942 , version 1 (15-12-2022)

Identifiers

Cite

Yannick Forster, Felix Jahn. Constructive and Synthetic Reducibility Degrees: Post's Problem for Many-one and Truth-table Reducibility in Coq. CSL 2023 - 31st EACSL Annual Conference on Computer Science Logic, Feb 2023, Warsaw, Poland. ⟨10.4230/LIPIcs.CSL.2023.16⟩. ⟨hal-03901942⟩
0 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More