Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Abstracting the undecidability of the Halting Problem

Suraaj K S (Aug 09 2024 at 18:50):

Note: This is the same question as here: https://math.stackexchange.com/questions/4956536/abstracting-the-undecidability-of-the-halting-problem

The question asks something about abstraction, which is the bread and butter of CT, and I thought it'd be a good fit for here.

I'm reposting the original question below:

Let us work in some constructive metalogic (where we have at least the following: Natural numbers, Booleans, Lists, Disjoint Union, and Sets).

To reason about Turing machines, we could (probably) define the following (metalogical) functions and sets:

TMData : Set == Seq(Bool)
// TMData is the set of all finite boolean sequences

TMEval(alg: TMData, input: TMData) : TMData + "null"
// TMEval is the 'big step operational semantics' of Turing machines.
// It 'executes' `alg` with `input`, and returns "null" on divergence or the answer.

Now, we can prove the following metalogical theorem:

SolvesHalting(halt_solver: TMData) ==
               ∀inp_alg: TMData, TMEval(halt_solver, inp_alg) = (TMEval(inp_alg,[]) = "null" ? [0] : [1])
// SolvesHalting is a metalogical predicate which says whether `halt_solver` can solve the halting problem.

THEOREM HaltingUnsolvable == ∀ alg: TMData : ¬ SolvesHalting(alg)
// It is possible to prove this theorem in our metalogic. We would have to unfold the definitions of TMEval and TMData.

Now, I could define a "new" programming language / notion of computation. For instance, we could define:

* PythonData, PythonEval //PythonData is all python programs, which are ASTs
* GodelData, GodelEval //GodelData is just Nat. These are the traditional partial recursive functions
* TaggedTMData, TaggedTMEval //This is simply 'a copy' of TMData, where each finite boolean sequence has a tag '*', which makes the set different from TMData.

Now, I think that we could prove a version of the Halting problem undecidability for each of these (and more), which are different statements in the metalogic. My question is whether there is a way we can abstract the essence of this problem? The idea is to 'not repeat ourselves' with the proof, and have a single proof.

Maybe we can define something like a HaltUndecidable to be a set (the data - eg. TMData, TaggedTMData, etc.) and an evaluation function subject to various conditions which are required for the halting problem?
* Then <TMData, TMEval>, <PythonData, PythonEval>, etc. are instances of HaltUndeciable, and we don't have to prove anything else..
* I'm curious whether one of the well-formedness conditions requires the set to be countably infinite? Could it be possible to prove a version of the halting problem where the set is uncountably infinite?
Another approach might be to define the notion of a simulation between our different notions of computation, and prove a theorem that says that one version of the Halting problem "lifts" to another version if there is a simulation. Is this the way one typically goes about this?
Does anything change significantly when our metalogic is classical, instead of constructive?

Ryan Wisnesky (Aug 09 2024 at 20:36):

perhaps you are noticing "oracles and relativization"? https://faculty.cc.gatech.edu/~ladha/S24/4510/L21.pdf

Suraaj K S (Aug 09 2024 at 22:13):

@Ryan Wisnesky , on a cursory glance, it does not look like I am? The link you shared seems to talk about complexity, etc., which was not my concern...

Ryan Wisnesky (Aug 09 2024 at 22:18):

Here is the connection in mind: in complexity theory you assume problems are decidable with a black box called an oracle, and do complexity theory 'relative to an oracle', and as such you actually get an entirely family of results out (called relativized results). Each of your "new" programming languages struck me as having a 'black box' - not an oracle, but similar idea, imo

Morgan Rogers (he/him) (Aug 12 2024 at 09:32):

I have answered there without using CT. As far as CT is concerned, the halting problem is often considered a special case of Lawvere's fixed point theorem.