Status of Ciaffaglione's "Towards Turing computability via coinduction"

[ruplet]

Hey,

I want to ask someone who knows more than me about the status of formalizing undecidability proofs: from what I understand, in this repo we focus on constructing reductions between the different decidability problems, taking the undecidability of a couple of them as axioms. But in 2014, Alberto Ciaffaglione (https://doi.org/10.1016/j.scico.2016.02.004) managed to formalize the undecidabiliy of the halting problem using coinductive types in Coq. Would integrating that proof with the work done in this repo not be a big milestone for us?

[DmxLarchey]

Dear Pawel,

This issue of seeding is not really that critical, although, depending on your base model of computation, it can become complicated. Certainly going the Turing machine way may be adventurous. Those who tried often end up saying: "I did it once ... but never again." (I am quoting an observation made by @yforster here). The L-way, ie via call-by-value lambda calculus is much easier. But you are welcome to try yourself just to get a glimpse on how hard it is to write and certify programs in the Turing model of computation.

Notice that we do not assume any axiom in the library, hence we do not assume that some problems are "undecidable" axiomatically. The definition we give, "the existence of a reduction from TM-halting", makes TM-halting undecidable by definition.

But the real issue, and this is a feature of the library rather than a defect, is with the computability of reductions, which we do not have to establish because you can only write computable functions in axiom free Coq. That is why we do not add axioms, because this may break this essential property that made our library relatively successful in a short period of time.

Now you could claim that we do not have a mechanized proof of that property of computability of Coq terms, and you'd be correct. But recall that pen&paper proofs almost never show that reductions are computable (by a Turing machine) either. For a very good reason. It is almost infeasible for a human to review such proofs in all the details.

The way out, hopefully in a near future, is a Coq extraction plugin that produces eg an untyped lambda term with its correctness proof, from any "simply typed" Coq term, but which works even when the term is built using inner higher-order dependent typed terms. The paper https://dl.acm.org/doi/10.1145/3656379 is a step in that direction. Notice that we do not need a generic correctness proof but simply something that works for all the reductions that pop up in the library, hence a tactic would be sufficient.

I personally consider this endeavour to be very important but also best to keep it orthogonal to the goals of the library of undecidability proofs. So that we can keep writing reductions in the high-level language of Coq w/o having to establish that they are computable by implementing them as low-level Turing machines.

Best regards,

Dominique

[mrhaandi]

I fully agree with @DmxLarchey. From our perspective (taking axiom free Coq as the underlying model of computation for reductions) it is silly to always construct and talk about Turing machines.
@eerio note that we also can show statements regarding non-computability directly: https://github.com/uds-psl/coq-library-undecidability/blob/coq-8.20/theories/L/Computability/Rice.v
This is cleaner than the proof presented in https://dl.acm.org/doi/10.1145/3656379 https://doi.org/10.1016/j.scico.2016.02.004 which uses axioms (existence of function gamma in section 9). I would argue that Rice.v is a strict improvement compared to the approach in the mentioned paper.
We could use metacoq to systematically apply the approach from Rice.v to the whole library (this is not complicated).
However, this would be computationally intensive, somewhat hinder development of new results, and provide no new insights.

[DmxLarchey]

This is cleaner than the proof presented in https://dl.acm.org/doi/10.1145/3656379 which uses axioms (existence of function gamma in section 9).

Hi @mrhaandi I have the impression you are quoting the wrong reference which IMHO should be https://doi.org/10.1016/j.scico.2016.02.004 instead.

[mrhaandi]

This is cleaner than the proof presented in https://dl.acm.org/doi/10.1145/3656379 which uses axioms (existence of function gamma in section 9).

Hi @mrhaandi I have the impressed your are quoting the wrong reference which IMHO should be https://doi.org/10.1016/j.scico.2016.02.004 instead.

You are correct, I copy-pasted the wrong link.