5 Search Results for "Larchey-Wendling, Dominique"

Document
DOI: 10.4230/LIPIcs.CSL.2024.29
The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions

Authors: Yannick Forster, Dominik Kirst, and Niklas Mück

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
The Kleene-Post theorem and Post’s theorem are two central and historically important results in the development of oracle computability theory, clarifying the structure of Turing reducibility degrees. They state, respectively, that there are incomparable Turing degrees and that the arithmetical hierarchy is connected to the relativised form of the halting problem defined via Turing jumps. We study these two results in the calculus of inductive constructions (CIC), the constructive type theory underlying the Coq proof assistant. CIC constitutes an ideal foundation for the formalisation of computability theory for two reasons: First, like in other constructive foundations, computable functions can be treated via axioms as a purely synthetic notion rather than being defined in terms of a concrete analytic model of computation such as Turing machines. Furthermore and uniquely, CIC allows consistently assuming classical logic via the law of excluded middle or weaker variants on top of axioms for synthetic computability, enabling both fully classical developments and taking the perspective of constructive reverse mathematics on computability theory. In the present paper, we give a fully constructive construction of two Turing-incomparable degrees à la Kleene-Post and observe that the classical content of Post’s theorem seems to be related to the arithmetical hierarchy of the law of excluded middle due to Akama et. al. Technically, we base our investigation on a previously studied notion of synthetic oracle computability and contribute the first consistency proof of a suitable enumeration axiom. All results discussed in the paper are mechanised and contributed to the Coq library of synthetic computability.
Cite as

Yannick Forster, Dominik Kirst, and Niklas Mück. The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{forster_et_al:LIPIcs.CSL.2024.29,
  author =	{Forster, Yannick and Kirst, Dominik and M\"{u}ck, Niklas},
  title =	{{The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.29},
  URN =		{urn:nbn:de:0030-drops-196728},
  doi =		{10.4230/LIPIcs.CSL.2024.29},
  annote =	{Keywords: Constructive mathematics, Computability theory, Logical foundations, Constructive type theory, Interactive theorem proving, Coq proof assistant}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.21
Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq

Authors: Dominique Larchey-Wendling and Jean-François Monin

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
Basing on an original Coq implementation of unbounded linear search for partially decidable predicates, we study the computational contents of μ-recursive functions via their syntactic representation, and a correct by construction Coq interpreter for this abstract syntax. When this interpreter is extracted, we claim the resulting OCaml code to be the natural combination of the implementation of the μ-recursive schemes of composition, primitive recursion and unbounded minimization of partial (i.e., possibly non-terminating) functions. At the level of the fully specified Coq terms, this implies the representation of higher-order functions of which some of the arguments are themselves partial functions. We handle this issue using some techniques coming from the Braga method. Hence we get a faithful embedding of μ-recursive algorithms into Coq preserving not only their extensional meaning but also their intended computational behavior. We put a strong focus on the quality of the Coq artifact which is both self contained and with a line of code count of less than 1k in total.
Cite as

Dominique Larchey-Wendling and Jean-François Monin. Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{larcheywendling_et_al:LIPIcs.ITP.2023.21,
  author =	{Larchey-Wendling, Dominique and Monin, Jean-Fran\c{c}ois},
  title =	{{Proof Pearl: Faithful Computation and Extraction of \mu-Recursive Algorithms in Coq}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{21:1--21:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.21},
  URN =		{urn:nbn:de:0030-drops-183963},
  doi =		{10.4230/LIPIcs.ITP.2023.21},
  annote =	{Keywords: Unbounded linear search, \mu-recursive functions, computational contents, Coq, extraction, OCaml}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.18
Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq

Authors: Dominique Larchey-Wendling

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
We present an alternate undecidability proof for entailment in (intuitionistic) multiplicative sub-exponential linear logic (MSELL). We contribute the result and its mechanised proof to the Coq library of synthetic undecidability. The result crucially relies on the undecidability of the halting problem for two counters Minsky machines, which we also hand out to the library. As a seed of undecidability, we start from FRACTRAN halting which we (many-one) reduce to Minsky machines termination by implementing Euclidean division using two counters only. We then give an alternate presentation of those two counters machines as sequent rules, where computation is performed by proof-search, and halting reduced to provability. We use this system called non-deterministic two counters Minsky machines to describe and compare both the legacy reduction to linear logic, and the more recent reduction to MSELL. In contrast with that former MSELL undecidability proof, our correctness argument for the reduction uses trivial phase semantics in place of a focused calculus.
Cite as

Dominique Larchey-Wendling. Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{larcheywendling:LIPIcs.FSCD.2021.18,
  author =	{Larchey-Wendling, Dominique},
  title =	{{Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{18:1--18:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.18},
  URN =		{urn:nbn:de:0030-drops-142568},
  doi =		{10.4230/LIPIcs.FSCD.2021.18},
  annote =	{Keywords: Undecidability, computability theory, many-one reduction, Minsky machines, Fractran, sub-exponential linear logic, Coq}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.21
Church’s Thesis and Related Axioms in Coq’s Type Theory

Authors: Yannick Forster

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
"Church’s thesis" (CT) as an axiom in constructive logic states that every total function of type ℕ → ℕ is computable, i.e. definable in a model of computation. CT is inconsistent both in classical mathematics and in Brouwer’s intuitionism since it contradicts weak Kőnig’s lemma and the fan theorem, respectively. Recently, CT was proved consistent for (univalent) constructive type theory. Since neither weak Kőnig’s lemma nor the fan theorem is a consequence of just logical axioms or just choice-like axioms assumed in constructive logic, it seems likely that CT is inconsistent only with a combination of classical logic and choice axioms. We study consequences of CT and its relation to several classes of axioms in Coq’s type theory, a constructive type theory with a universe of propositions which proves neither classical logical axioms nor strong choice axioms. We thereby provide a partial answer to the question as to which axioms may preserve computational intuitions inherent to type theory, and which certainly do not. The paper can also be read as a broad survey of axioms in type theory, with all results mechanised in the Coq proof assistant.
Cite as

Yannick Forster. Church’s Thesis and Related Axioms in Coq’s Type Theory. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 21:1-21:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{forster:LIPIcs.CSL.2021.21,
  author =	{Forster, Yannick},
  title =	{{Church’s Thesis and Related Axioms in Coq’s Type Theory}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{21:1--21:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.21},
  URN =		{urn:nbn:de:0030-drops-134552},
  doi =		{10.4230/LIPIcs.CSL.2021.21},
  annote =	{Keywords: Church’s thesis, constructive type theory, constructive reverse mathematics, synthetic computability theory, Coq}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.27
Hilbert’s Tenth Problem in Coq

Authors: Dominique Larchey-Wendling and Yannick Forster

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq’s constructive type theory. To do so, we give the first full mechanisation of the Davis-Putnam-Robinson-Matiyasevich theorem, stating that every recursively enumerable problem - in our case by a Minsky machine - is Diophantine. We obtain an elegant and comprehensible proof by using a synthetic approach to computability and by introducing Conway’s FRACTRAN language as intermediate layer.
Cite as

Dominique Larchey-Wendling and Yannick Forster. Hilbert’s Tenth Problem in Coq. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 27:1-27:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{larcheywendling_et_al:LIPIcs.FSCD.2019.27,
  author =	{Larchey-Wendling, Dominique and Forster, Yannick},
  title =	{{Hilbert’s Tenth Problem in Coq}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{27:1--27:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.27},
  URN =		{urn:nbn:de:0030-drops-105342},
  doi =		{10.4230/LIPIcs.FSCD.2019.27},
  annote =	{Keywords: Hilbert’s tenth problem, Diophantine equations, undecidability, computability theory, reduction, Minsky machines, Fractran, Coq, type theory}
}
  • Refine by Author
  • 3 Forster, Yannick
  • 3 Larchey-Wendling, Dominique
  • 1 Kirst, Dominik
  • 1 Monin, Jean-François
  • 1 Mück, Niklas

  • Refine by Classification
  • 5 Theory of computation → Type theory
  • 3 Theory of computation → Models of computation
  • 2 Theory of computation → Constructive mathematics
  • 1 Software and its engineering → Formal methods
  • 1 Software and its engineering → Functional languages
  • Show More...

  • Refine by Keyword
  • 4 Coq
  • 2 Fractran
  • 2 Minsky machines
  • 2 computability theory
  • 1 Church’s thesis
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 2 2021
  • 1 2019
  • 1 2023
  • 1 2024

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact