Oracle Computability Theory

Stream: mathlib4

[Edwin Park]

I have formalised the Kleene-Post theorem in computability theory, along with a large amount of mechanical foundations for it in https://github.com/hyeoniuwu/CiL. (The capstone KP54 proof is found in https://github.com/hyeoniuwu/CiL/blob/main/Computability/Constructions/KP54.lean). (There are also other basic degree theoretic theorems and proofs included.)

I have not yet refactored the codebase yet, so it's largely uncommented/poorly organised/is very slow, but I'm wondering if this is something people would be interested evnetually being merged into mathlib?

One thing of note is that I "redo" a lot of the primitive recursive constructions in a different format from the current way in Mathlib, which helps in later constructions for the KP54 proof.

[Snir Broshi]

Have you considered #CSLib?

[Tanner Duve]

This is firmly within mathematics IMO, and isn't very related to the kind of cs theory that would go into cslib. the main difficulty would be finding reviewers for this kind of content, but that wouldn't be any easier at cslib.

I think this would be great to have in mathlib personally

[Thomas C.]

Interesting project!

Just out of curiosity, why did you have to modify the way primitive recursion is defined in Mathlib?

[Edwin Park]

It's not a huge modification, but it makes proving certain theorems much more convenient.

The way I build primitive recursive functions in this project is by building an explicit code, asserting that it is built only from primitive recursive constructors, then proving that it has a specified behavior on evaluation; for example, that it implements the addition function. This is opposed to just giving a theorem that addition is primitive recursive, where the "code" is kinda fuzzily written in the proof itself, making it hard to extract when needed.

A practical example where my approach is needed is when proving (primitive) recursiveness of functions from codes to codes.

For example, consider the foldl operator (as an operator from functions to functions), and suppose we have shown

$$\begin{align} \text{Property 1. }f\in\text{PRIMREC}\Rightarrow\text{foldl}(f)\in\text{PRIMREC}. \end{align}$$

Oftentimes however, one also has to prove that the operator itself is a primitive recursive function, from codes to codes. (Property 1 only states that the output of the operator is primitive recursive, if the input is.) That is,

$$\begin{align} \text{Property 2. }\exists g\in\text{PRIMREC},\ \text{eval}\ g(c)=\text{foldl}(\text{eval}\ c). \end{align}$$

Our approach allows easily proving the second property from the first, while this can't really be done directly with the way it's done in Mathlib.

(For reference, see the foldl theorem in mathlib: https://github.com/leanprover-community/mathlib4/blob/1839d10be81233f804dab4e1d43fc1027219d3fa/Mathlib/Computability/Primrec/List.lean#L53.)

The actual construction of foldl is in the proof, not explicitly defined outside. The problem is that the second property relies on the details of that construction. So to prove the second property, one effectively has to repeat the construction in the first property, and furthermore demonstrate the primitive recursiveness of the process.

This is trivial in our approach, because those construction procedures are explicitly defined, as codes. Once one has property 1, one can get property 2 "for free".

[Thomas C.]

Thanks for the explanation!

Wouldn't such a change require rewriting most proofs using e.g. Primrec?

Maybe @Mario Carneiro would have something to say about it since he wrote the initial formalization of computability in Lean? (see https://arxiv.org/abs/1810.08380)

[Mario Carneiro]

This principle is already applied for the most part in the primrec library; the reason why those early examples are done directly is because Code has not been defined yet

[Edwin Park]

Thomas C. said:

Wouldn't such a change require rewriting most proofs using e.g. Primrec?

Yes, but rewriting existing theorems is most of the time trivial.

[Edwin Park]

@Mario Carneiro

By the principle being applied in the library, did you mean there are examples of property 2 being proven trivially from property 1 (or the converse)? If so, could you point me to an example?

[Mario Carneiro]

I think most of the code functions are proved unapplied

[Mario Carneiro]

part of the issue might be that the definition of Code is one of the last things in the library since the original goal was to prove the smn theorem and undecidability of the halting problem

[Edwin Park]

I have a few comments to make.

Firstly, the definition of TuringDegree in mathlib currently is incorrect.

It defines the "oracles" as partial functions - this is not equivalent to having set oracles. Instead, the oracle functions should be total. (See https://link.springer.com/chapter/10.1007/BFb0086114.)

Also, I would like to merge some of my work into Mathlib. One "weird" thing however is that the first few files in my formalisation are simply relativisations of existing Mathlib code (Oracle.lean and Encoding.lean), so there'd be some code duplication - is this fine?

[Aaron Liu]

docs#TuringDegree

[Edwin Park]

Rather, maybe I should've said the problem is with TuringReducible; Turing reducibility is a relation on oracles (i.e. total functions) not partial functions

[Aaron Liu]

does it restrict to the correct relation if you only feed it total functions?

[Edwin Park]

I believe so. But that doesn't change the fact that the current definition of "TuringDegree" is not what a Turing degree actually is.

[James E Hanson]

The current definition is actually the enumeration degrees, right?

[James E Hanson]

Oh, I should have looked at your link.

[Edwin Park]

I believe page 61 of my link shows that they are different

[James E Hanson]

Right, I'm seeing that now.

[James E Hanson]

In any case, this will be pretty easy to fix, right?

[Edwin Park]

I've already fixed it in https://github.com/hyeoniuwu/CiL/blob/ee2e1648d8b34f8c2a849de9cb0e5fb8d1ee5429/Computability/Oracle.lean#L145

[Aaron Liu]

I think docs#RecursiveIn should definitely take a set of partial functions

[James E Hanson]

Is this notion still called 'T-reducibility'? My gut tells me that name probably wouldn't have caught on.

[Edwin Park]

I'm not aware of any work on 'T-reducibility' after that paper, I'd love to know too though

[Edwin Park]

Aaron Liu said:

I think docs#RecursiveIn should definitely take a set of partial functions

Why? Oracles are supposed to give you answers in finite time, so it doesn't make sense for them to be partial

[James E Hanson]

Edwin Park said:

Why? Oracles are supposed to give you answers in finite time, so it doesn't make sense for them to be partial

Computability relative to a Turing ideal is something that shows up kind of often, so there's a case for the more general definition there.

[James E Hanson]

Specifically allowing a set of oracles rather than just a single oracle.

[Edwin Park]

I see. But in that case wouldn't it still be a set of total functions, not partial functions

[James E Hanson]

Right.

[James E Hanson]

It's not clear to me what the 'right' base level of generality is for this.

[James E Hanson]

Most degree structures naturally embed into the Muchnik degrees, for instance, but that might not be a good definition to work from.

[James E Hanson]

(Although that said I don't know for a fact that the T-degrees do.)

[Eric Wieser]

I think @Tanner Duve has some open PRs in this area

[Tanner Duve]

I think the concerns above are correct. But the definition of TuringReducible we currently have is a strict generalization of the typical definition. We can perhaps change the current TuringReducible to something like PartialReducible and then we can recover the typical reducibility definition as something like

def TuringReducible (f g : ℕ → ℕ) :=
 PartialReducible (fun x => Part.some (f x)) (fun x => Part.some (g x))

RecursiveIn I think is fine as-is as a general definition. A total function is just a partial function which is total. Making these edits in a PR would make more sense to me than replacing the existing API with something less general. I think this is more an issue of misnaming than definitions being incorrect.

[Tanner Duve]

The question of what to do with Encoding is a good one. I have an encoding for the general "set of partial oracles" RecursiveIn definition which is similar to the one @Edwin Park has for the single total oracle definition. But there would be code duplication if we just added an encoding. One idea is to redefine Partrec as "recursive in the empty set" which @Mario Carneiro mentioned at some point before, but this would incur a large refactor I think.

[Mario Carneiro]

IMO we shouldn't change the definitions here, this is like the question of whether to use VectorSpace or Module over a field. It's better to take the trivial generalization since it is available, since getting the equivalent notion is much harder without it (not even sure it is possible). If you want to talk about total functions, that's the responsibility of whatever derived notion writes a quantification over those functions

[Palalansoukî]

Computable functions that take partial oracles are natural notion when considering higher-order recursion theory (e.g. partial computable functional), so I think the idea of computable functions that take partial oracles isn't so nonsensical. Defining TuringReducible from PartialReducible feels reasonable.

[Edwin Park]

Fair.