Email Gateway (Aug 18 2022 at 14:06): Email Gateway (Aug 18 2022 at 14:06):From: Wang Zirui <zirui@nus.edu.sg>
Hi,
I'd like to formalize the definition of Turing machine. If possible,
I'd like to do it without relying on ZFC. That is, I don't use sets,
integers and so on.
Yes, in the definition of Turing machine we see sets, such as the set
of states, but I think the use of set is convenient but not necessary.
(Am I wrong?) So if you agree with me and think it's possible to go
without sets, could you please outline how to define Turing machine?
If you think this is impossible, can you give a proof?
Thanks.
Regards,
Zirui Wang
Email Gateway (Aug 18 2022 at 14:06):From: Alexander Krauss <krauss@in.tum.de>
Deac Zirui,
I'd like to formalize the definition of Turing machine. If possible,
I'd like to do it without relying on ZFC. That is, I don't use sets,
integers and so on.
There should be no problems with doing it in HOL. Note that HOL also has
a notion of a set, although it is not quite the same as in ZFC.
[...] So if you agree with me and think it's possible to go
without sets, could you please outline how to define Turing machine?
You may want to look at Tobias Nipkow's formalization of finite
automata, which you can find in the AFP:
http://afp.sourceforge.net/entries/Functional-Automata.shtml
It's not Turing Machines, but it may give you an idea...
Alex
Email Gateway (Aug 18 2022 at 14:06):From: Alexander Krauss <krauss@in.tum.de>
Dear Zirui,
The point of not relying on ZFC is because it's a strong theory. I
don't want the definition of Turing machine to be based on a strong
theory. I want it to be based on a theory that is as weak as possible.
So it's best if it's based on nothing.
Well, HOL is what people are typically using, and if you are new to
Isabelle and are trying to use anything else, you are going to have a
hard time, because other logics are much less developed in terms of tool
support.
Unfortunately HOL is at least as strong as ZFC because it has the idea
of a set.
HOL's notion of a set is much weaker, as sets are just identified with
predicates over the respective type.
My teacher Jain suggests that it might be possible to define
Turing machine based on Peano Arithmetic, which is weaker than ZFC.
And I'm going to try that.
You can certainly try, and I think there should not be fundamental
problems, but you will certainly suffer from the lack of tool support in
your custom-made logic, as opposed to using something well-established.
If these foundational issues of taking the weakest logic possible are
really the core of your interest, then you can try and go for Peano
Arithmetic, but if your main interest is formalizing Turing Machines
after all, then using anything but HOL is like cutting your left leg off
before climbing a mountain.
I don't understand the AFP formalization of automata as I read it.
Does the author use the idea of sets, functions or numbers? If yes, he
probably base the definition of automata on HOL or ZFC. But I want to
base it on a weaker theory. Does the author do that?
The formalization is based on HOL. If you have big trouble reading the
formalization, this is probably an indication that you should learn some
Isabelle basics first, e.g. by working through the Tutorial
(http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf)
Alex
Email Gateway (Aug 18 2022 at 14:07):From: Wang Zirui <zirui@nus.edu.sg>
Hi Alex,
The point of not relying on ZFC is because it's a strong theory. I
don't want the definition of Turing machine to be based on a strong
theory. I want it to be based on a theory that is as weak as possible.
So it's best if it's based on nothing.
Unfortunately HOL is at least as strong as ZFC because it has the idea
of a set. My teacher Jain suggests that it might be possible to define
Turing machine based on Peano Arithmetic, which is weaker than ZFC.
And I'm going to try that.
I don't understand the AFP formalization of automata as I read it.
Does the author use the idea of sets, functions or numbers? If yes, he
probably base the definition of automata on HOL or ZFC. But I want to
base it on a weaker theory. Does the author do that?
Your suggestion of automata is certainly good as it has the same
problem as Turing machines, but it's simpler.
Regards,
Zirui
Email Gateway (Aug 18 2022 at 14:07):From: Richard Waldinger <waldinger@AI.SRI.COM>
didn't turing's original paper do a formalization? in some sort of
number theory, i forget which logic.
Email Gateway (Aug 18 2022 at 14:07):From: Konrad Slind <slind@cs.utah.edu>
Hi,
Yes, you can define Turing machines in a very
simple base theory. For example, you can use lists
instead of sets because everything in a TM description
has to be finite. So at least the preliminary theory
of TMs can be done without higher order things like
sets and functions. But going even a little bit into the
theory, you will need to define computable functions etc.
On the face of it, even the undecidability of the Halting
Problem seems to need sets to state (i.e. the set of all
halting TMs is undecidable).
I did some work on formalizing TMs in HOL-4 and the
following definitions of the machines should be
completely straightforward to turn into Isabelle/HOL syntax.
Of course there is more to define, like machine configurations,
executions, languages, etc. but I will omit those.
Also, doesn't the AFP include some computability theory
already?
Cheers,
Konrad.
(*----------------------------------------------------------------------
-----*)
(* Turing machines, tape infinite in one
direction. *)
(*----------------------------------------------------------------------
-----*)
Hol_datatype dir = L | R;
(*----------------------------------------------------------------------
-----*)
(* Raw datatype of TMs. The only slightly odd thing may be that the
blank is *)
(* explicitly included. Also, it turns out to facilitate the
definition of *)
(* executions if the initial value of the current cell is set to a
value. *)
(* Because having a "left-edge" marker simplifies many TM algorithms,
we set *)
(* aside a particular "star" value for this
purpose. *)
(*----------------------------------------------------------------------
-----*)
Hol_datatype
TM = <| states : 'state -> bool ;
inputsymbs : 'alpha -> bool ;
tapesymbs : 'alpha -> bool ;
init : 'state ;
trans : 'state -> 'alpha -> 'state # 'alpha # dir;
accept : 'state ;
reject : 'state ;
blank : 'alpha ;
star : 'alpha |>;
(*----------------------------------------------------------------------
-----*)
(* Predicate singling out the real Turing machines. Is in principle
an *)
(* executable thing, but we don't currently handle (bounded)
quantifiers. *)
(*----------------------------------------------------------------------
-----*)
val isTM_def =
Define
isTM (M : ('alpha,'state)TM) =
FINITE M.states /\
FINITE M.inputsymbs /\
FINITE M.tapesymbs /\
M.blank IN M.tapesymbs /\
~(M.blank IN M.inputsymbs) /\
M.star IN M.inputsymbs /\
M.inputsymbs SUBSET M.tapesymbs /\
M.accept IN M.states /\
M.reject IN M.states /\
~(M.accept = M.reject) /\
M.init IN M.states /\
!a p q b d.
a IN M.tapesymbs /\ p IN M.states /\ (M.trans p a = (q,b,d))
==> q IN M.states /\ b IN M.tapesymbs;
Cheers,
Konrad.
Email Gateway (Aug 18 2022 at 14:08):From: Konrad Slind <konrad.slind@gmail.com>
Hi Zirui,
TMs can be represented by bitstrings (or numbers).
No sets. A TM evaluator can be written that takes
in a bitstring, decodes it into a TM and an input,
and simulates the execution of the TM on the input.
That evaluator can itself be written out as a bitstring
representing a TM. Any decent undergrad theory
textbook will go into this in some amount of detail.
So there is a certain portion of computability theory
that is basic programming and can be formalized in
a simple logic that doesn't formalize set theory.
On the other hand, much of computability is about
infinite sets (not lists), some of which can be
implemented by TMs and some which can't. Again,
any undergrad theory text (or wikipedia) has
plenty of detail.
Cheers,
Konrad.
Email Gateway (Aug 18 2022 at 14:08):From: Lawrence Paulson <lp15@cam.ac.uk>
You need to be much more specific about your research objectives and
about what you mean by set theory. Zermelo set theory is rather weak
(more or less equivalent to higher-order logic). ZF set theory is
considerably stronger, but there are set theories much stronger than
ZF. Then there is a question of the axiom of choice. Just to say "I
want to have nothing to do with the axioms of set theory" is not a
basis for a scientific discussion. People do choose to work in weak
formal systems, typically in order to investigate the power of those
systems.
Lawrence C Paulson
Professor of Computational Logic
Computer Laboratory, University of Cambridge
15 JJ Thomson Avenue, Cambridge CB3 0FD, England
Tel: +44(0)1223 334623 Fax: +44(0)1223 334678
Email Gateway (Aug 18 2022 at 14:08):From: Tjark Weber <webertj@in.tum.de>
Turing machines are finite objects. They can be encoded as numbers (via
some Gödel numbering, cf.
http://en.wikipedia.org/wiki/G%C3%B6del_number).
So depending on what you want to prove exactly, and provided that you
don't want to speak about (infinite) sets of Turing machines, you may
indeed be able to avoid set theory entirely, and merely work in (some
fragment of) a theory of arithmetic (cf.
http://www.math.ucsd.edu/~sbuss/ResearchWeb/handbookII/,
http://en.wikipedia.org/wiki/Robinson_arithmetic,
http://en.wikipedia.org/wiki/Peano_arithmetic). Since your teacher
suggested this in the first place, why not ask him to explain the
details?
Note that finite lists (of numbers) can be encoded as numbers (again,
via some Gödel numbering), so they are not "as high level as sets".
Also note that Alex was perfectly right when he wrote:
| If these foundational issues of taking the weakest logic possible are
| really the core of your interest, then you can try and go for Peano
| Arithmetic, but if your main interest is formalizing Turing Machines
| after all, then using anything but HOL is like cutting your left leg
| off before climbing a mountain.
If you really want to restrict yourself to Peano arithmetic, I suspect
that a formalization on paper (not using Isabelle) would already be
enough of a challenge for a small student project.
Regards,
Tjark
Email Gateway (Aug 18 2022 at 14:08):From: Wang Zirui <zirui@nus.edu.sg>
Lawrence wrote:
You need to be much more specific about your research objectives and
about what you mean by set theory. Zermelo set theory is rather weak
(more or less equivalent to higher-order logic). ZF set theory is
considerably stronger, but there are set theories much stronger than
ZF. Then there is a question of the axiom of choice. Just to say "I
want to have nothing to do with the axioms of set theory" is not a
basis for a scientific discussion. People do choose to work in weak
formal systems, typically in order to investigate the power of those
systems.
Based on ZFC you can define and derive much of mathematics, so I
imagine that it's easy to define Turing machine from ZFC. The problem
with this is that it's harder to do proofs in a strong theory.
Therefore I want to define Turing machine in a weaker theory (with
fewer axioms). Basically it would good to have the theory as weak as
possible (because it facilitates proofs). But when the theory gets
weaker, it also becomes less expressive. So I want the theory to be
just strong enough to define Turing machines. I think that would be
the ideal theory, because it can express the definition of Turing
machine and it is weak enough to do certain proofs.
Zirui Wang
Email Gateway (Aug 18 2022 at 14:08):From: Wang Zirui <zirui@nus.edu.sg>
I read a bit about proof theory. So if I want to prove from premises
P_1, ..., P_k one can derive conclusion C and I used the induction
principle (IND) in the proof, I'm actually showing that P_1, ..., P_k,
IND entail C instead of just P_1, ..., P_k entail C. And usually for a
problem whether Q_1, ..., Q_j entail D, we are actually showing Q_1,
..., Q_j, ZFC entail D.
Email Gateway (Aug 18 2022 at 14:08):From: Lawrence Paulson <lp15@cam.ac.uk>
You are quite right to be concerned about difficulty of proofs, but
there are many factors involved in this difficulty, and some weak
theories are much more difficult to use than stronger theories. If you
want to accomplish your project with the minimum of effort, you should
undoubtedly choose Isabelle/HOL. Not only is the logic easy-to-use;
the implementation provides lots of automation.
Larry Paulson
Email Gateway (Aug 18 2022 at 14:08):From: Wang Zirui <zirui@nus.edu.sg>
OK, maybe it's a bad choice to start with formalizing Turing machine,
which is a definition not a theorem. How about formalizing Cook's
theorem, the Probabilistically Checkable Proof (PCP) theorem and the
natural proof theorem? Yes, I'm very interested in formalizing
theorems in computational complexity theory. Has anyone done this?
Zirui Wang
Email Gateway (Aug 18 2022 at 14:08):From: Jens Doll <jd@cococo.de>
Churchs' thesis says, that all computability can be expressed by Turing
machines. So you probably cannot bypass sets when defining a such a
formalism. Mathematically spoken do groups, rings, (closed) fields rely
on sets in their definition. Also alphabets are sets. What do you have
on mind?
Jens
jd.vcf
Email Gateway (Aug 18 2022 at 14:11):From: Tjark Weber <webertj@in.tum.de>
There is no need to talk about the "set of all halting TMs" to state
undecidability of the halting problem. Simply put, undecidability of
the halting problem asserts that there is no Turing machine that decides
whether an arbitrary Turing machine halts. Stating this requires
quantification over all Turing machines, but no set comprehension. (Of
course, you chose a deliberately careful wording in the first place, so
I guess this was obvious to you.)
Maybe someone else can point out the precise theory required to prove
undecidability of the halting problem?
Regards,
Tjark
Email Gateway (Aug 18 2022 at 14:15):From: Wang Zirui <zirui@nus.edu.sg>
But think about lambda calculus. It is computationally as powerful as
Turing machine. Following your line of reasoning, it should also rely
on set in its definition. But I think it's simple enough to avoid the
use of set.
Zirui
Email Gateway (Aug 18 2022 at 14:15):From: Wang Zirui <zirui@nus.edu.sg>
I'm sorry, but I'd like to repeat again that I'm not talking about
programming tricks. So lists are as high level as sets, because you
can implement sets by lists. Actually I don't mean sets in particular
but rather set theory. I want to avoid the use of sets because I
want to have nothing to do with the axioms of set theory. So lists
probably also rely on the axioms of set theory, unless you can define
it without the axioms of set theory. So let repeat my question: Can we
define Turing machine without relying on the axioms of set theory? I
think part of the misconception is because I'm posting this topic
under Isabelle. Actually my question has nothing to do with Isabelle
or HOL; I just imagined that people here might be good at formalizing
concepts and proofs using rudimentary logic theory. Sorry for the
misunderstanding.
Zirui
Last updated: Nov 21 2024 at 12:39 UTC