RePred

Stream: mathlib4

[Martin Dvořák]

We have docs4#RePred that characterizes recursively enumerable sets using partial recursive functions.
Do we have a characterization of recursively enumerable sets using Turing machines as well?

[Martin Dvořák]

We have Turing machines that compute stuff in the sense that the machine changes symbols on the tape (or stacks).
Do we also have the notion of a Turing machine that can accept or reject the input?

[James Gallicchio]

I don’t think so. Encoding data to TM tape is a bit more complicated than encoding to Nat, and I’m not even sure we have a notion of this encoding.

[James Gallicchio]

I was working for a while on a register machine formalization that could be used as an intermediary to transport results with PRFs to results with TMs. So I would be interested in helping build a notion of TM tape encodings and computability

[James Gallicchio]

Oh, we do have tm encodings: https://leanprover-community.github.io/mathlib_docs/computability/encoding.html

[James Gallicchio]

Is there a reason you want to characterize RE sets in terms of TMs? I think PRFs are almost always nicer to work with, no?

[Martin Dvořák]

I think it will be easier to connect Grammars to Turing machines than to connect Grammars to PRFs.
https://github.com/madvorak/chomsky

[Martin Dvořák]

Ultimately, I believe we will want to have all three versions of computability theory (TMs, PRFs, grammars) and possibly more.

[James Gallicchio]

Totally. When I get home I’ll push my RM stuff to a repository in case anyone wants to pick it up again.

[Martin Dvořák]

Martin Dvořák said:

Do we also have the notion of a Turing machine that can accept or reject the input?

We don't have this, do we?

[Martin Dvořák]

Please, prove me wrong; it seems that docs#Language is connected to neither PRFs nor TMs.

[Mario Carneiro]

Martin Dvořák said:

Martin Dvořák said:

Do we also have the notion of a Turing machine that can accept or reject the input?

We don't have this, do we?

well you can just leave a 0 or 1 on the tape, or depending on the situation you can also use halting/non-halting to signal acceptance

[James Gallicchio]

Maybe it's worth adding definitions for deciders & semideciders

[James Gallicchio]

where a decider always halts and we interpret 0/1 as reject/accept

[Martin Dvořák]

We should definitely add semideciders. I hope the API will be in terms of a docs#Language recognized by a Turing machine.

[James Gallicchio]

I'm not thrilled by the idea of fixing it to TMs when they are so much harder to work with formally... but having TM-specific definitions of "turing machine decider" and "TM semidecider" seems reasonable

[Martin Dvořák]

James Gallicchio said:

I'm not thrilled by the idea of fixing it to TMs

Fixing what?

I would like docs#Language to be the central notion about which we speak in computability theory (and later also in complexity theory). Turing machines would be just one of the ways to characterize languages.

[James Gallicchio]

Sorry, I meant fixing (the definition of deciding/semideciding a language) to TMs

[James Gallicchio]

Or I guess I mean it should be in the turing machine namespace if it is specialized to TMs

[James Gallicchio]

It seems reasonable though to specialize the notion of deciding/semideciding a language to each computational model, since they each have differences in terms of input encoding/output decoding

[James Gallicchio]

and then eventually we will have constructions for turning a TM decider on L to a PRF decider on L

[Martin Dvořák]

It sounds like we have conflated two decisions (both of which are important):
(1) What is the object we want to characterize?
(2) What is the computational model we want to use for the characterization?

Possibilities for (1) include:
(a) α → Prop where α is docs#Primcodable
(b) List α → Prop where α is docs#Fintype
‣ perhaps expressed as Language α
(c) ℕ → Prop
‣ perhaps expressed as Set ℕ

Possibilities for (2) include:
(a) Partial recursive functions
(b) Turing machine variants
(c) RAM-like programs

We will eventually have several versions of (1) and (2).
However, we should decide what is the version we want to see in top-level theorems.
The existence of docs#RePred suggests (1a) and (2a).
There are not many theorems about docs#RePred currently, so we can still change direction if we want to.

In question (1), I have a strong preference towards (1b).
In question (2), I don't have any significant preference.

Please, let's talk about both (1) and (2) without conflating the issues.

[James Gallicchio]

Thank you for splitting out the issues. I'm not convinced Language A is the right choice for anything other than TM as the computational model, right?

Do we have to select a version for "top-level theorems?" Do we want to generalize across computational models yet?

[Martin Dvořák]

James Gallicchio said:

I'm not convinced Language A is the right choice for anything other than TM as the computational model, right?

I think that Language α is perfect for TMs, RAMs, and grammars alike!

[James Gallicchio]

But for PRFs you have to encode Nat as List Bool or something

[Martin Dvořák]

Yes. Each version comes with a price.

However, there is an important advantage of Language over other (1). In addition to the above, you can use Language to characterize models of computation that are not Turing complete, including those that are too weak to perform necessary encoding. If we define "recursively enumerable" in terms of Language over finite alphabet, we can make meaningful theorems like "every regular language is recursively enumerable" (in fact, there would be several intermediate inclusions).

[James Gallicchio]

It definitely makes that one definition nicer. But I'm wondering if there's a generalization of computational models that would let us use any of these definitions to characterize RE sets.

Like, say you have an arbitrary computational model over some state type σ, and you have a set s : S -> Prop where S is computably encodable in σ (computable encoding can be generalized). Then s is RE in terms of this model iff there exists a program that decides s.

And then maybe we pick one model as the "base" computational model and expect these computational models to be proven equivalent to that base.

That way we can characterize Languages as RE, or subsets of Nat, or whatever else we want to characterize, without having to go through a single specific definition.

I don't think we have fleshed out the computational models enough at this point to make such a generalization, but I think it would be reasonable to make a RE definition in terms of Language and TM, without presenting it as "the" definition of recursive enumerability in mathlib.

[Martin Dvořák]

I don't think we need to make it an exercise on abstract programming. Note that the relationship between various (1) is independent of which (2) you use.

Let me illustrate my idea on a small example with some pseudocode. For simplicity, consider now only (1b) and (1c) with (2a) and (2b).

We make two model-independent conversion functions for (1):
SetN_of_Lang : Language Bool → Set ℕ
Lang_of_SetN : Set ℕ → Language Bool
We establish they are inverse of each other.

We define these two notions manually:
TmReLang : Language Bool → Prop using Turing machines
PrfReSetN : Set ℕ → Prop using Partial recursive functions

We get these two notions for free:
TmReSetN : Set ℕ → Prop := TmReLang ∘ Lang_of_SetN
PrfReLang : Language Bool → Prop := PrfReSetN ∘ SetN_of_Lang

Now a hard work comes:
∀ L, TmReLang L ↔ PrfReLang L

Then we trivially prove:
∀ S, PrfReSetN S ↔ TmReSetN S

[Martin Dvořák]

The advantage becomes important when broadening our library. In order to have N versions of (1) and M versions of (2), we have to manually:

• write N conversion functions
• write M definitions of RE
• prove M implications about a computational model simulating a different computational model

Having done that, we can easily have:

• all M*N definitions of RE
• all (M choose 2) theorems about equivalence of computational models (à la Church-Turing thesis)

[Martin Dvořák]

PS: We don't have to flood Mathlib with all M*N definitions of RE. We can settle for those M definitions, like:
TmReLang : Language Bool → Prop using Turing machines
PrfReSetN : Set ℕ → Prop using Partial recursive functions

Then the theorems will be like:
∀ L, PrfReSetN (SetN_of_Lang L) ↔ TmReLang L

[James Gallicchio]

I agree completely. It seems like an apt place to have a typeclass to manage the conversions to whatever base computational model we choose. For now I'd support adding TmReLang without necessarily worrying about all the conversions.

[Martin Dvořák]

Unfortunately, I don't understand typeclasses enough. Nevertheless, adding TmReLang is the logical step to do now.

[Mario Carneiro]

I think that as elsewhere in mathlib we should be using one definition and N equivalences, not N definitions and N^2 equivalences

[Martin Dvořák]

Would you agree with the one definition to be in terms of Language Bool using PRFs?

[James Gallicchio]

I really think it's easiest for it to be Set Nat with PRFs...

[James Gallicchio]

but I haven't tried it, so am conjecturing

[James Gallicchio]

just that the Set Nat definition would be a single line in today-mathlib

[Martin Dvořák]

Martin Dvořák said:

It sounds like we have conflated two decisions (both of which are important):
(1) What is the object we want to characterize?
(2) What is the computational model we want to use for the characterization?

Possibilities for (1) include:
(a) α → Prop where α is docs#Primcodable
(b) List α → Prop where α is docs#Fintype
‣ perhaps expressed as Language α
(c) ℕ → Prop
‣ perhaps expressed as Set ℕ

Possibilities for (2) include:
(a) Partial recursive functions
(b) Turing machine variants
(c) RAM-like programs

We will eventually have several versions of (1) and (2).
However, we should decide what is the version we want to see in top-level theorems.
The existence of docs#RePred suggests (1a) and (2a).
There are not many theorems about docs#RePred currently, so we can still change direction if we want to.

In question (1), I have a strong preference towards (1b).
In question (2), I don't have any significant preference.

Please, let's talk about both (1) and (2) without conflating the issues.

We should return here. We want one definition. Which of them will be the one?

[James Gallicchio]

The reason I don't want to get into this yet is cuz we haven't proven the equivalence of TMs and PRFs yet, so if you're gonna be working in TMs there's no reason for you to introduce a definition in terms of PRFs.

[Martin Dvořák]

I'll just repeat that I have strong interest in being able to state theorems like "every regular language is recursively enumerable" smoothly (i.e., the theorem statement is as simple as possible (having conversion in a statement is usually not nice), even if it makes the proofs longer).

[James Gallicchio]

RE is a property of sets. Language A = Set (List A). So long as the elements are encodable to Nat (which List A is for any encodable A, which includes any FinType A). So with a very slight generalization of the Set Nat definition it would be a very smooth theorem statement.

[James Gallicchio]

(the generalization being to make it over Set A for any primcodable A)

[James Gallicchio]

so I guess 1(a)/2(a)

[Martin Dvořák]

It seems that you two (James and Mario) prefer to keep docs#RePred as the definition of RE. Then the theorem would be something like the following:

∀ p, (∃ M : TM, M.semidecides (Lang_of_Pred p)) ↔ RePred p

Is it what you want? For the sake of not introducing new definitions?

[James Gallicchio]

or just ∀ L, (∃ M : TM, M.semidecides L) ↔ RePred L since languages are already sets of primcodable objects.

[Martin Dvořák]

(possibly left-hand side Skolemized)

[James Gallicchio]

Now, I have no clue how we're going to prove that theorem any time soon :joy: so we'll have to live with a sorry for now

[James Gallicchio]

the forward direction is at least probably provable with sufficient effort right now

[Martin Dvořák]

If we don't see ourselves proving equivalence between two concepts anytime soon, shouldn't we rather write two definitions?

[Martin Dvořák]

James Gallicchio said:

For now I'd support adding TmReLang without necessarily worrying about all the conversions.

If @Mario Carneiro doesn't want to see two equivalent definitions in Mathlib, we should perhaps forget about TmReLang now and define TM.semidecides only.

[James Gallicchio]

Yeah, I think \exists M, M.semidecides L is already quite clean

[Martin Dvořák]

You mean for ∃ M, M.semidecides L to appear in a theorem, or in a definition?

[James Gallicchio]

The former. But that's up to you.

[Martin Dvořák]

If it is really up to me, I'd rather have a definition TmReLang wrapping it. However, I don't think @Mario Carneiro would approve.

[Mario Carneiro]

I think in most cases you can have more precise theorems that trivially imply the desired equivalences

[Martin Dvořák]

You mean, imply in our head (an interpretation of what it means)?

[Martin Dvořák]

Martin Dvořák said:

James Gallicchio said:

For now I'd support adding TmReLang without necessarily worrying about all the conversions.

define TM.semidecides

In textbooks, there is often a definition of a TM that can accept, reject, or go on forever. The language of the TM is the set of words for which it accepts.

I suppose we don't want it because it [having three behaviours] is harder for formalization. The desired definition TM.semidecides for Mathlib is that it either halts or goes on forever. The language of the TM is the set of words for which it halts. Do we all agree on this approach?

[Martin Dvořák]

On the other hand, the three-way definition of semideciders has a big advantage:

In this framework, a decider is (a special case of) a semidecider. You don't have to convert a decider to a semidecider by making it loop instead of rejecting a word.

[James Gallicchio]

Yep. I think you want a definition with three outcomes.

[James Gallicchio]

I think it's also probably nice to have both the "yes-or-halt" and "no-or-halt" options accessible, just because people use both pretty interchangeably

[Martin Dvořák]

What do you mean by "yes-or-halt" and "no-or-halt" please?

[James Gallicchio]

err, yes-or-doesn't-halt :joy: words are hard

[Martin Dvořák]

Should I implement TM.semidecides as follows?

When the machine halts (i.e., when step returns none), if the tape symbol under the head is default Γ then the word [what was written on the tape before the computation started] gets accepted (regardless of Cfg.q a.k.a. the state of the head). We will have a machine that can accept, reject, or go on forever.