Turing Machines in Metamath

[andrew sauer]

Has there been any work done in Metamath so far in defining a model of computation such as a Turing machine? If not I'd love to try to get that started!

[Paul Chapman]

Andrew,

I had a go, although I found the Minsky Register Machine a better fit to formal mathematics and
set.mm. Ran out of steam in the end, though.

Cheers, Paul

[Thomas Brendan Leahy]

I'm actually working on an algorithm for plug-and-chug formula evaluation based on Paul's template (that is, the one running from algr0 to its realization in eucalg).  It seems to me that template could pretty much be used for any purpose a TM would be used for, though, with something like this:

seq 0 ( ( ( t e. ( ( A ^m ZZ ) X. E ) , h e. ZZ |-> [_ ( ( ( 1st ` t ) ` h ) T ( 2nd ` t ) ) / s ]_ <. ( ( ( 1st ` t ) \ ( { h } X. _V ) ) u. ( <. h , ( 1st ` ( 1st ` s ) ) >. ) ) , ( 2nd ` ( 1st ` s ) ) , ( h + ( 2nd ` s ) ) >. ) o. 1st ) , ( NN0 X. { <. ( ZZ X. { B } ) , S , 0 >. } ) )

(It's more legible than what I have in the other window, at least.)

[Mario Carneiro]

This might not be that useful, but I'm actually working on Turing machines in lean right now:

https://github.com/leanprover/mathlib/blob/master/computability/turing_machine.lean#L344

My advice, after a significant bit of formalization, is to avoid Turing machines completely if you can (I'm doing it mostly for completeness). Partial recursive functions are much easier to work with mathematically and you can recover most of what you want from Turing machines without all the coding stuff.

Mario

On Sat, Jul 21, 2018 at 12:51 AM, Thomas Brendan Leahy <tbrend...@gmail.com> wrote:

I'm a little creeped out, since I was actually working on an algorithm for plug-and-chug algebra based on Paul's template (running from algr0 to its realization in eucalg), but came here to make an unrelated comment regarding the definition of area and found this.  It seems to me that template could pretty much be used for any purpose a TM would be used for, though, with something like this:

seq 0 ( ( ( t e. ( ( A ^m ZZ ) X. E ) , h e. ZZ |-> [_ ( ( ( 1st ` t ) ` h ) T ( 2nd ` t ) ) / s ]_ <. ( ( ( 1st ` t ) \ ( { h } X. _V ) ) u. ( <. h , ( 1st ` ( 1st ` s ) ) >. ) ) , ( 2nd ` ( 1st ` s ) ) , ( h + ( 2nd ` s ) ) >. ) o. 1st ) , ( NN0 X. { <. ( ZZ X. { B } ) , S , 0 >. } ) )

(It's more legible than what I have in the other window, at least.)

On Friday, July 20, 2018 at 2:07:31 AM UTC-4, andrew sauer wrote:

Has there been any work done in Metamath so far in defining a model of computation such as a Turing machine? If not I'd love to try to get that started!

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Thomas Brendan Leahy]

I have to think, though, that as time goes on, we're going to want a lot of TM-related results.  (Cook's theorem, Fagin's theorem, Savitch's theorem, Immerman's theorem, Karp's problems, IP = PSPACE, etc.)  Partial recursive functions will work for the halting problem or the unsolvability of Diophantine equations, but what about time and space?

On Saturday, July 21, 2018 at 1:04:37 AM UTC-4, Mario Carneiro wrote:

This might not be that useful, but I'm actually working on Turing machines in lean right now:

https://github.com/leanprover/mathlib/blob/master/computability/turing_machine.lean#L344

My advice, after a significant bit of formalization, is to avoid Turing machines completely if you can (I'm doing it mostly for completeness). Partial recursive functions are much easier to work with mathematically and you can recover most of what you want from Turing machines without all the coding stuff.

Mario

On Sat, Jul 21, 2018 at 12:51 AM, Thomas Brendan Leahy <tbrend...@gmail.com> wrote:

I'm a little creeped out, since I was actually working on an algorithm for plug-and-chug algebra based on Paul's template (running from algr0 to its realization in eucalg), but came here to make an unrelated comment regarding the definition of area and found this.  It seems to me that template could pretty much be used for any purpose a TM would be used for, though, with something like this:

seq 0 ( ( ( t e. ( ( A ^m ZZ ) X. E ) , h e. ZZ |-> [_ ( ( ( 1st ` t ) ` h ) T ( 2nd ` t ) ) / s ]_ <. ( ( ( 1st ` t ) \ ( { h } X. _V ) ) u. ( <. h , ( 1st ` ( 1st ` s ) ) >. ) ) , ( 2nd ` ( 1st ` s ) ) , ( h + ( 2nd ` s ) ) >. ) o. 1st ) , ( NN0 X. { <. ( ZZ X. { B } ) , S , 0 >. } ) )

(It's more legible than what I have in the other window, at least.)

On Friday, July 20, 2018 at 2:07:31 AM UTC-4, andrew sauer wrote:

Has there been any work done in Metamath so far in defining a model of computation such as a Turing machine? If not I'd love to try to get that started!

--
You received this message because you are subscribed to the Google Groups "Metamath" group.

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

[Mario Carneiro]

These results are all in complexity theory. Of course one of the major findings of computability theory and later complexity theory is that the exact model of computation is almost completely irrelevant except very low in the polynomial hierarchy, and in these areas (i.e. NC) Turing machines are actually not a good idea because they are too slow. It is largely a historical artifact that caused Turing machines to become the de facto standard model of computation, they rank pretty poorly compared to others on almost every front. If you want to define P and NP, you can do so using partial recursive functions as well; you just use a restriction of primitive recursion based on the 2^|x| function (I think it's called the smash function, I forget the details).

On Sat, Jul 21, 2018 at 1:40 AM, Thomas Brendan Leahy <tbrend...@gmail.com> wrote:

I have to think, though, that as time goes on, we're going to want a lot of TM-related results.  (Cook's theorem, Fagin's theorem, Savitch's theorem, Immerman's theorem, Karp's problems, IP = PSPACE, etc.)

On Saturday, July 21, 2018 at 1:04:37 AM UTC-4, Mario Carneiro wrote:

This might not be that useful, but I'm actually working on Turing machines in lean right now:

https://github.com/leanprover/mathlib/blob/master/computability/turing_machine.lean#L344

My advice, after a significant bit of formalization, is to avoid Turing machines completely if you can (I'm doing it mostly for completeness). Partial recursive functions are much easier to work with mathematically and you can recover most of what you want from Turing machines without all the coding stuff.

Mario

On Sat, Jul 21, 2018 at 12:51 AM, Thomas Brendan Leahy <tbrend...@gmail.com> wrote:

I'm a little creeped out, since I was actually working on an algorithm for plug-and-chug algebra based on Paul's template (running from algr0 to its realization in eucalg), but came here to make an unrelated comment regarding the definition of area and found this.  It seems to me that template could pretty much be used for any purpose a TM would be used for, though, with something like this:

seq 0 ( ( ( t e. ( ( A ^m ZZ ) X. E ) , h e. ZZ |-> [_ ( ( ( 1st ` t ) ` h ) T ( 2nd ` t ) ) / s ]_ <. ( ( ( 1st ` t ) \ ( { h } X. _V ) ) u. ( <. h , ( 1st ` ( 1st ` s ) ) >. ) ) , ( 2nd ` ( 1st ` s ) ) , ( h + ( 2nd ` s ) ) >. ) o. 1st ) , ( NN0 X. { <. ( ZZ X. { B } ) , S , 0 >. } ) )

(It's more legible than what I have in the other window, at least.)

On Friday, July 20, 2018 at 2:07:31 AM UTC-4, andrew sauer wrote:

Has there been any work done in Metamath so far in defining a model of computation such as a Turing machine? If not I'd love to try to get that started!

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.

[andrew sauer]

You guys are probably right that Turing Machines aren't the most efficient way to create a Turing equivalent model of computation (partial recursive functions sound very promising). My main motivation for this is demonstrating the uncomputability of the Halting Problem, which could in the even longer term lead to a proof of Godel's first Incompleteness Theorem.

On Friday, July 20, 2018 at 10:04:37 PM UTC-7, Mario Carneiro wrote:

This might not be that useful, but I'm actually working on Turing machines in lean right now:

https://github.com/leanprover/mathlib/blob/master/computability/turing_machine.lean#L344

My advice, after a significant bit of formalization, is to avoid Turing machines completely if you can (I'm doing it mostly for completeness). Partial recursive functions are much easier to work with mathematically and you can recover most of what you want from Turing machines without all the coding stuff.

Mario

On Sat, Jul 21, 2018 at 12:51 AM, Thomas Brendan Leahy <tbrend...@gmail.com> wrote:

I'm a little creeped out, since I was actually working on an algorithm for plug-and-chug algebra based on Paul's template (running from algr0 to its realization in eucalg), but came here to make an unrelated comment regarding the definition of area and found this.  It seems to me that template could pretty much be used for any purpose a TM would be used for, though, with something like this:

seq 0 ( ( ( t e. ( ( A ^m ZZ ) X. E ) , h e. ZZ |-> [_ ( ( ( 1st ` t ) ` h ) T ( 2nd ` t ) ) / s ]_ <. ( ( ( 1st ` t ) \ ( { h } X. _V ) ) u. ( <. h , ( 1st ` ( 1st ` s ) ) >. ) ) , ( 2nd ` ( 1st ` s ) ) , ( h + ( 2nd ` s ) ) >. ) o. 1st ) , ( NN0 X. { <. ( ZZ X. { B } ) , S , 0 >. } ) )

(It's more legible than what I have in the other window, at least.)

On Friday, July 20, 2018 at 2:07:31 AM UTC-4, andrew sauer wrote:

Has there been any work done in Metamath so far in defining a model of computation such as a Turing machine? If not I'd love to try to get that started!

--
You received this message because you are subscribed to the Google Groups "Metamath" group.

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

[Thomas Brendan Leahy]

While it is a basic result of complexity theory that most computation models are equivalent to a point (and I don't know how the heck you'd define NC by anything but circuits, except via Barrington's theorem, which seems like cheating), I don't know that primitive recursion will quite fit.  I agree with Paul that register machines might be a better fit than TMs - they usually are, although I do think Cook's and Fagin's theorems would go more smoothly with TMs - but either seems a better fit than working with primitive recursion directly.

[Mario Carneiro]

On Sat, Jul 21, 2018 at 2:51 AM, andrew sauer <mrper...@gmail.com> wrote:

You guys are probably right that Turing Machines aren't the most efficient way to create a Turing equivalent model of computation (partial recursive functions sound very promising). My main motivation for this is demonstrating the uncomputability of the Halting Problem, which could in the even longer term lead to a proof of Godel's first Incompleteness Theorem.

I've already done that much in lean, with no reference to Turing machines. I defined the partial recursive functions as a subset PartRec C_ ( NN0 ^pm NN0 ), then I defined a coding system for partial recursive functions (i.e. a surjective function from NN0 to PartRec) and proved that the evaluation map ( n, m |-> ((code`n)`m) ) is partial recursive. This function is a universal partial recursive function, and you can easily use the fixed point theorem to prove the halting problem (i.e. that the set of codes of partial recursive functions that terminate on input 0 is not enumerated by any partial recursive function).

On Sat, Jul 21, 2018 at 2:53 AM, Thomas Brendan Leahy <tbrend...@gmail.com> wrote:

While it is a basic result of complexity theory that most computation models are equivalent to a point (and I don't know how the heck you'd define NC by anything but circuits, except via Barrington's theorem, which seems like cheating), I don't know about using just primitive recursive functions.  I agree with Paul that register machines might be a better fit than TMs - they usually are, although I do think Cook's and Fagin's theorems would go more smoothly with TMs - but either seems a better fit than working with primitive recursion directly.

The idea isn't to use primitive recursion directly. It is to define a set of coding systems for everything in sight, and use primitive recursion to prove that all the normal functions are primitive recursive. At that point everything becomes easy and you don't have to look back at the construction.

Lean's "typeclass inference" is a very nice way to express the set of coding systems in a canonical way (essentially you build a compositional framework for coding different kinds of sets), but it wouldn't be too hard to just reference the projections and unpairing functions and such directly when needed. That's always the tedious part with this stuff. In metamath we have a tendency of stating results like ( NN X. NN ) ~~ NN which abstract away the concrete isomorphism, but when doing codings it is important that the coding is fixed, so you can prove it is computable and different theorems use the same coding function.

 

On Saturday, July 21, 2018 at 1:54:18 AM UTC-4, Mario Carneiro wrote:

These results are all in complexity theory. Of course one of the major findings of computability theory and later complexity theory is that the exact model of computation is almost completely irrelevant except very low in the polynomial hierarchy, and in these areas (i.e. NC) Turing machines are actually not a good idea because they are too slow. It is largely a historical artifact that caused Turing machines to become the de facto standard model of computation, they rank pretty poorly compared to others on almost every front. If you want to define P and NP, you can do so using partial recursive functions as well; you just use a restriction of primitive recursion based on the 2^|x| function (I think it's called the smash function, I forget the details).