Computability by Turing machines

Stream: new members

[Pim Spelier]

Hi, me and @Daan van Gent are trying to define problems in computability sense, and hence we want to use the Turing machine code in mathlib. But the current definition of the second kind of Turing machine in mathlib seems to be too powerful: because \sigma (the type of states) can be infinite, and you can choose any function f: \sigma \to \Gamma k (the alphabet) to be the "output" of the Turing machine. Taking $\sigma = \N$ for example, this function f does not need to be computable, but with the Turing machine as implemented, I think it can be computed. It seems like an easy fix: just demand that \sigma is finite (as is usually done in the definition of Turing machines). Should that be done, or am I missing something?

(Note the same problem holds for Turing machines of the zeroth kind as defined in mathlib; there, the type of states is called \Lambda, and can still be infinite.)

[Alex J. Best]

@Mario Carneiro had some discussion of this at https://github.com/formalabstracts/formalabstracts/issues/52 recently.

[Pim Spelier]

Ah, that makes sense! I think that means we will be defining our own computable demanding that the state set is finite.

[Mario Carneiro]

@Pim Spelier The Turing machine file doesn't define "computable" (IIRC), only a Turing machine with fixed types for input alphabet and so on. This allows you to use them as required for your application. If you want to define TM-computable, you would probably say something like "f : N -> N is computable if there exists a finite alphabet S and a finite set of states G such that machine G S evaluates to f n given input n (after encoding and decoding nat to list S somehow"

[Mario Carneiro]

There is a definition of "computable" in partrec that I recommend you use as "the" definition of computable in the abstract, and it does require that the TM that computes it has finitely many states and is on a finite alphabet. (Well not really because it's not defined using TMs at all, but it is equivalent to such.)

[Mario Carneiro]

There are also some words on this in the module comment for computability.turing_machine

[Mario Carneiro]

In particular, docs#turing.TM0.supports formalizes exactly how a TM is supposed to be finite without actually requiring that the types involved are finite. This is very useful for writing concrete TMs since it is nice to be able to use an inductive type for the space of states, and then just ensure that only a finite part of it is accessible from the initial state.

[Pim Spelier]

Thanks! I think we do want to work with Turing machines though, to define computability, because we also want to work with it in practice (right now for example, we're working on showing that sat is decidable). Then definining computability only for functions of type \N \to \N seems restricted, and we'd rather work in higher generality. I agree, we will then have to demand that the alphabets and states are finite in some way.

[Pim Spelier]

I did see the definition of the multiple supports functions, and that does seem a natural way to demand finiteness. Right now, in TM2, this is only done for the type of function labels \Lambda; would it make sense to make a similar definition for the type of states $\sigma$?

[Mario Carneiro]

If you want to show SAT is decidable, you can probably do so using the partrec API. Don't use TMs unless you like pain or are specifically interested in TMs

[Mario Carneiro]

The partrec API defines computability over general types FYI, that was just a sketch

[Mario Carneiro]

Pim Spelier said:

I did see the definition of the multiple supports functions, and that does seem a natural way to demand finiteness. Right now, in TM2, this is only done for the type of function labels \Lambda; would it make sense to make a similar definition for the type of states $\sigma$?

If only finitely many states is accessible, this implies that only finitely many elements of the alphabet can be written. You will still have to ask that the input be encoded on the tape using finitely many symbols, but Sigma can be infinite (with the cofinitely many symbols being auxiliaries that never appear on the tape)

[Mario Carneiro]

Oops, misread, you are talking about the local state variable $\sigma$. Yes this has to be finite too, and you can enforce this with a fintype sigma. It is possible to do a more refined thing but I haven't found as much use for sigma being "essentially finite" like the other types

[Mario Carneiro]

My plan has been to prove the equivalence of computable (as defined in partrec) with the existence of a TM that computes the function, and that theorem will of course have all the necessary finiteness assumptions. Since I'm not using TMs for the definition of computable, it's not so important if the definition allows infinite states and so on.

[Pim Spelier]

We did think about using the partrec functions instead of Turing machines, but we saw two problems: first of all, if I understand correctly, although partrec is defined for any primcodable types, it still is fundamentally a statement about a function \N \to \N being primitive recursive. For SAT, you'd then need an encoding from propositional_formula to \N, and work with such an encoded propositional formula. Our main concern was that such an encoding feels ugly, and difficult to work with (if there is an easy way to do this, I'd love to know where I can read about it). While in theory doable, for us it seemed nicer to think of a function list \Gamma \to list \Gamma' being computable; then you'd need to encode a propositional_formula to a list \Gamma for some alphabet \Gamma. Taking for example a postfix notation, this kind of encoding seems to reflect the original structure a lot better than an encoding propositional_formal \to \N could.

[Pim Spelier]

Second of all, we want to be able to define the classes P, NP and NPC, and for that you need the runtime of an algorithm. For Turing machines, this seems like an easy addition to the code that is already there; for partrec functions, we didn't know how we would do that.

[Mario Carneiro]

Ultimately, yes every type you want to talk about has to be encoded as a nat. But besides the abstract computability of this encoding, not much is required about it (and more to the point using TM's doesn't save you any trouble here). You can encode to another primcodable type if you prefer, such as list Sigma where Sigma is primcodable (for example if Sigma is finite then this is easy), and so that should put it on the same footing as what you get with TMs

[Mario Carneiro]

It would be nice if such an encoding is generated automatically for inductive types, but the required derive handler hasn't been written yet. So you have to cobble it from sums and products right now

[Mario Carneiro]

As for defining P and NP, it's true that TMs have a more natural description of what runtime means. It is possible to define polytime computable primrec functions; you need to restrict the growth rate of functions inside the prec constructor IIRC

[Mario Carneiro]

@Pim Spelier Here's a general interface for encoding inductive types:

import computability.primrec

inductive W (α : Type*) (β : α → Type*)
| mk (a) : (β a → W) → W

class listable (α : Type*) :=
[dec_eq [] : decidable_eq α]
(elems [] : list α)
(complete : ∀ x, x ∈ elems)

instance listable.to_fintype {α} [listable α] : fintype α :=
by haveI := listable.dec_eq α; exact
⟨(listable.elems α).to_finset, λ x, by simp [listable.complete x]⟩

instance (α : Type*) (β : α → Type*)
  [primcodable α] [∀ a, listable (β a)] : primcodable (W α β) :=
sorry

[Mario Carneiro]

If you have some inductive type of propositional formulas, you can define a bijection to W of the appropriate types and get an encoding that way

[Daan van Gent]

I have trouble parsing this, but that might have to do with me not understanding what W is supposed to be. If I understand correctly you say that every inductive type should be primcodable, but that it hasn't been proved yet? We have a inductive type for propositional formulas:

@[derive inhabited]
inductive propositional_formula (α : Type*)
| atom (a:α) : propositional_formula
| conj (a b: propositional_formula) : propositional_formula
| disj (a b: propositional_formula) : propositional_formula
| neg (a:propositional_formula) : propositional_formula

We already managed to prove that it is encodable, which is enough when working with Turing machines. Proving primcodability shouldn't be very much harder.

How is propositional_formula in bijection with W for some choice of parameters?

[Reid Barton]

the first parameter of W is a type with α + 3 values, say ATOM α | CONJ | DISJ | NEG, and the second parameter of W takes these four constructors to, respectively, the empty type, the type with 2 values, the type with 2 values, the type with 1 value

[Daan van Gent]

I see. If we say s is the type with values ATOM \alpha | CONJ | DISJ | NEG , then this W has a 'natural' map to list(s) via postfix notation, since s is trivially primcodable so is list(s) (supposing alpha is primcodable). At least, this is how I see it with how I proved propositional_formula is primcodable in the back of my mind. This bijection of W with propositional_formula seems very canonical. Is there a way to automate that, or is that just way too much technicalities with inductive types?

[Mario Carneiro]

It is definitely automatable, but I haven't bothered to write the derive handler for it

[Mario Carneiro]

It is reminiscent of Haskell's deriving Generic

[Mario Carneiro]

The encodings I was thinking of use the encodings for lists and pairs. That is, you encode conj (atom x) (neg (atom y)) as
(CONJ, [(ATOM x, []), (NEG, [(ATOM y, [])])]) where (x, y) denotes the pair encoding function and [x,..] is the list encoding function

[Mario Carneiro]

Up until now there hasn't really been a demand for deriving primcodable, and the only real usage of such a thing in mathlib would be src#nat.partrec.code.encode_code (which you should totally use as a blueprint for your propositional_formula implementation)

[Daan van Gent]

But what is the type of (CONJ, [(ATOM x, []), (NEG, [(ATOM y, [])])])? it seems like a recursive type instead of some composition of products and lists.

[Daan van Gent]

Oh nevermind, I think I understand. I should read it as a way to evaluate it as a natural number using the encodings for lists and products.

[Pim Spelier]

@Mario Carneiro Thanks for all the help!
On the subject of definining computability through partrec functions or through turing_machines: another objection we came up with for using partrec instead of turing_machine, is that in defining of computable through partial recursive functions, one seems to forget about the actual computation: i.e., once you've proven it's computable, you don't care about the algorithm. This is fine when you only want to talk about stuff being computable, but seems like a problem when you also want to talk about the algorithms, e.g. when defining P and NP. Do you agree, or am I missing something?

[Mario Carneiro]

That's correct, and in fact that's the whole point

[Mario Carneiro]

computable f means f is abstractly computable. It does not make any guarantees about the complexity of the algorithm, nor does it provide an algorithm

[Mario Carneiro]

for example, it should be the case that the function that computes 1 if the riemann hypothesis is true and 0 otherwise, is computable

[Mario Carneiro]

because it is either the function return 0 or return 1, both of which are computable

[Mario Carneiro]

I would say that P and NP are the same way, in the sense that they should not be "effective" but rather mere existence claims

[Mario Carneiro]

In particular cases, you can often say something more precise than that a particular problem is in P, but for the basic definition I wouldn't want any more than that, so that you can do nonconstructive proofs

[Pim Spelier]

Isn't that also the case with computability by Turing machines? It is computable by either the algorithm that outputs 0, or the algorithm that outputs 1. So this problem would still be in P, as either way it has a constant time algorithm, right?

[Mario Carneiro]

Right, I imagine the TM-based definition would be something like def ptime (f : A -> B) := \ex G S [fintype G] (M : machine G S) (p : polynomial nat), \all x, eval_in_at_most M x (p.eval (size x)) = f x

[Mario Carneiro]

(I made up several things in that so don't expect it to type check)

[Mario Carneiro]

but because it uses \ex, there is no actual turing machine that is "data" in the predicate

[Pim Spelier]

Exactly, that's the same kind of definition that we're working towards! But I do get your problem, there's no way to go from \ex (a : \alpha), ... to \alpha without using choice.

[Mario Carneiro]

Daan van Gent said:

But what is the type of (CONJ, [(ATOM x, []), (NEG, [(ATOM y, [])])])? it seems like a recursive type instead of some composition of products and lists.

I omitted the encodes that keep shoving everything back into nat. With the encodes, it looks like
e (CONJ, [e (ATOM x, []), e (NEG, [e (ATOM y, [])])]) where e is encode : prop_A x list nat -> nat

[Pim Spelier]

Do you think there is a similarly easy definition of ptime using the partrec framework? Or would one need to define a similar inductive type ptime_computable_partrec, with a different way of constructing it? It seems rather difficult to pin down when a function is ptime_computable_partrec without directly referring to some sort of runtime.

[Mario Carneiro]

Well there is evaln, which seems to give a kind of step indexing to partrec evaluation, but I don't think it is correct for ptime, because it uses encoding to nat - many functions are going to be off by an exponential or so even with the optimal coding. The way I have heard for doing P properly using primitive recursion is to use "bounded recursion on notation", basically treating nat as list bool through a canonical bijection and defining simple recursive functions there. Cobham seems to be the progenitor of the idea, but there are several internet writeups, for example https://www.cs.toronto.edu/~sacook/homepage/survey_Dec26.2016.pdf

[Mario Carneiro]

By the way, while reading that paper I saw an idea that had never occurred to me: they call it $m$-adic notation, which is basically the same as $m$-ary positional notation for natural numbers except that digits come from $\{1,\dots,m\}$ instead of $\{0,\dots,m-1\}$. Amazingly, this simple change makes the notation a bijection between digit strings and nonnegative integers. Now I wish that lean had bit1 and bit2 instead of bit0 and bit1

[Kenny Lau]

yeah but now you can't have extra 0's

[Kenny Lau]

00003754 is no longer the same as 3754 because the former is not defined

[Mario Carneiro]

That's the point

[Mario Carneiro]

that's a failure of bijectivity

[Mario Carneiro]

those multiple representations are a formal headache

[Pim Spelier]

Thanks for the link, I'll take a look at it! I do think we'll stick with Turing machines for now, although I suppose the ultimate result would be to define polynomial time for both, and prove the definitions are equal :).

[Mario Carneiro]

I agree that polytime for TMs is more obviously correct