turing machine proof

Stream: new members

[Harold Cooper]

Hi all! I'm learning Lean, and playing around with computability.turing_machine

I made the simplest possible machine M1 which just immediately halts (i.e. returns none).

It was easy for me to prove the theorem M1_halts_immediately that it halts after a single call to step, but I'd also like to prove the theorem M1_halts that the higher-level eval also halts, since I want to play with more complicated machines next.

Anyway here's my code:

import computability.turing_machine

inductive Λ -- states
| initial : Λ
| a : Λ
| b : Λ
instance Λ.inhabited : inhabited Λ := ⟨Λ.initial⟩

inductive Γ -- symbols
| zero : Γ
| one : Γ
instance Γ.inhabited : inhabited Γ := ⟨Γ.zero⟩

-- initial state and empty tape:
def initial_cfg : turing.TM0.cfg Γ Λ := turing.TM0.init []

-- machine that halts immediately:
def M1 : turing.TM0.machine Γ Λ
| _ _ := none

theorem M1_halts_immediately : turing.TM0.step M1 initial_cfg = none :=
rfl

theorem M1_halts : turing.TM0.eval M1 [] ≠ part.none :=
begin
  sorry
end

How can I replace the sorry at the end? I have no idea what tactics are relevant here.

And am I even trying to prove the correct statement? I also considered ∃ x, turing.TM0.eval M1 [] = part.some x

[Harold Cooper]

(docs#turing.TM0.eval is implemented on top of docs#turing.eval which uses docs#pfun.fix and I have no idea what tactics can run/reduce pfun.fix to get to a part.some result)

[Mario Carneiro]

The main theorem for proving things about pfun.fix is docs#pfun.mem_fix_iff

[Mario Carneiro]

at least for "positive" statements, i.e. "this program halts and returns x". For negative statements you need docs#pfun.fix_induction

[Harold Cooper]

okay thanks, I'll try that!

[Mario Carneiro]

Here's one way to state and prove the theorem:

theorem M1_halts : (turing.TM0.eval M1 []).dom :=
begin
  rw [turing.TM0.eval, part.map_dom, part.dom_iff_mem],
  existsi _,
  rw [turing.mem_eval],
  refine ⟨relation.refl_trans_gen.refl, _⟩,
  refl,
end

[Harold Cooper]

oh awesome, I think this will teach me a lot.

so is the theorem(…).dom saying that the partial function has a non-empty domain, and thus halts?

[Mario Carneiro]

part A is actually a "partial value", kind of like a partial function but over just one point. So if p : part A then p.dom is a proposition that says whether the value exists, and p.get : p.dom -> A is either the empty function or a function on a singleton returning a single value of type A

[Mario Carneiro]

So turing.TM0.eval M1 [] is "the value that results from executing M1 on [], if it exists", and (turing.TM0.eval M1 []).dom is asserting that the value exists, i.e. the machine halts

[Mario Carneiro]

A partial function A ->. B is defined as A -> part B

[Harold Cooper]

ah okay got it, that makes sense

[YJ]

Hello all! I am new to Lean and am currently following the tutorials from the theorem proving in lean 3, are there any published solutions with the questions?

[Kevin Buzzard]

You're in the wrong thread (hint: start a new one) but the answer to your question is that as far as I know there aren't; however if you're stuck on something you could ask in a new thread in #new members

[Harold Cooper]

I did a bit more with this recently, including proving that a simple looping machine doesn't halt which was more fun than proving that things do halt :p

However, I was only able to do that using an alternative formulation of halting, which I'm pretty sure is equivalent to what we used earlier in this thread, but now I would like to prove that it is!

Specifically, the two definitions of halting which I want to prove are equivalent are:

def halts (M : turing.TM0.machine Γ Λ) : Prop :=
∃ n, multistep M n [] = none

def halts''' (M : turing.TM0.machine Γ Λ) : Prop :=
∃ x, turing.TM0.eval M [] = part.some x

(multistep M n just steps the machine n times—I'll include the full code below.)

[Harold Cooper]

In the following code, I started an attempt at the proof halts_iff''', where the sorry statements are. Based on @Mario Carneiro's tips above, I'm guessing I need to do something with docs#pfun.mem_fix_iff or docs#pfun.fix_induction ?

import computability.turing_machine

inductive Λ -- states
| A : Λ
| B : Λ
| C : Λ
instance Λ.inhabited : inhabited Λ := ⟨Λ.A⟩

inductive Γ -- symbols
| zero : Γ
| one : Γ
instance Γ.inhabited : inhabited Γ := ⟨Γ.zero⟩

-- initial state and empty tape:
def cfg₀ : turing.TM0.cfg Γ Λ := turing.TM0.init []

-- chainable step function:
def step' (M : turing.TM0.machine Γ Λ) (x : option (turing.TM0.cfg Γ Λ)) :
  option (turing.TM0.cfg Γ Λ) :=
x.bind (turing.TM0.step M)

def multistep (M : turing.TM0.machine Γ Λ) :
  ℕ → option (turing.TM0.cfg Γ Λ) → option (turing.TM0.cfg Γ Λ) :=
nat.repeat (λ _, step' M)

theorem multistep_none_add {cfg M n m} (hn : multistep M n cfg = none) :
  multistep M (n + m) cfg = none :=
begin
  induction m with m hm,
  { exact hn, },
  { rw [multistep, nat.add_succ, nat.repeat, ← multistep, hm],
    refl, },
end

theorem multistep_none_ge {cfg M n} {m ≥ n} (hn : multistep M n cfg = none) :
  multistep M m cfg = none :=
begin
  rw ← nat.add_sub_of_le H,
  exact multistep_none_add hn,
end


-- equivalent definitions of halting:

def halts (M : turing.TM0.machine Γ Λ) : Prop :=
∃ n, multistep M n cfg₀ = none

def halts' (M : turing.TM0.machine Γ Λ) : Prop :=
(turing.TM0.eval M []).dom

def halts'' (M : turing.TM0.machine Γ Λ) : Prop :=
turing.TM0.eval M [] ≠ part.none

def halts''' (M : turing.TM0.machine Γ Λ) : Prop :=
∃ x, turing.TM0.eval M [] = part.some x

theorem halts'_iff'' {M} : halts' M ↔ halts'' M :=
begin
  rw [halts'', ne.def, part.eq_none_iff', ← halts'],
  exact not_not.symm,
end

theorem halts''_iff''' {M} : halts'' M ↔ halts''' M :=
part.ne_none_iff

theorem halts_iff''' {M} : halts M ↔ halts''' M :=
begin
  rw [halts, halts'''],
  split; intro h,
  { cases h with n h,
    induction n with n hn,
    { sorry, },
    { sorry, },
  },
  { cases h with x h,
    sorry, },
end


-- machine that halts immediately:
def M₁ : turing.TM0.machine Γ Λ
| _ _ := none

theorem M₁_halts_immediately : turing.TM0.step M₁ cfg₀ = none :=
rfl

theorem M₁_halts : halts M₁ :=
⟨1, rfl⟩

theorem M₁_halts' : halts' M₁ :=
begin
  rw [halts', turing.TM0.eval, part.map_dom, part.dom_iff_mem],
  existsi _,
  rw turing.mem_eval,
  split,
  { exact relation.refl_trans_gen.refl, },
  { refl, },
end

theorem M₁_halts'' : halts'' M₁ :=
halts'_iff''.mp M₁_halts'

theorem M₁_halts''' : halts''' M₁ :=
halts''_iff'''.mp M₁_halts''


-- machine that goes A → B → halt:
def M₂ : turing.TM0.machine Γ Λ
| Λ.A symbol := some ⟨Λ.B, turing.TM0.stmt.write symbol⟩
| _ _ := none

theorem M₂_halts : halts M₂ :=
⟨2, rfl⟩

theorem M₂_halts' : halts' M₂ :=
begin
  rw [halts', turing.TM0.eval, part.map_dom, part.dom_iff_mem],
  existsi turing.TM0.cfg.mk Λ.B (turing.tape.mk₁ []),
  rw turing.mem_eval,
  split,
  { sorry, },
  { refl, },
end


-- machine that loops A → B → A → B → ⋯:
def M₃ : turing.TM0.machine Γ Λ
| Λ.A symbol := some ⟨Λ.B, turing.TM0.stmt.write symbol⟩
| Λ.B symbol := some ⟨Λ.A, turing.TM0.stmt.write symbol⟩
| _ _ := none

lemma M₃_AB_only {n} : ∃ tape,
  multistep M₃ n cfg₀ = some ⟨Λ.A, tape⟩ ∨ multistep M₃ n cfg₀ = some ⟨Λ.B, tape⟩ :=
begin
  induction n with n hn,
  { existsi _,
    left,
    refl, },
  { cases hn with tape_n hn,
    cases hn; existsi _,
    {
      right,
      rw [multistep, nat.repeat, ← multistep, hn, step', option.bind, turing.TM0.step],
      simp,
      existsi _,
      existsi _,
      split; refl, },
    {
      left,
      rw [multistep, nat.repeat, ← multistep, hn, step', option.bind, turing.TM0.step],
      simp,
      existsi _,
      existsi _,
      split; refl, },
  },
end

theorem M₃_not_halts : ¬ halts M₃ :=
begin
  intro h,
  cases h with n hn,
  cases M₃_AB_only with tape h_tape,
  cases h_tape; {
    rw h_tape at hn,
    exact option.no_confusion hn,
  },
end

(There's also an unfinished proof M₂_halts' of a machine halting in two steps, just because I felt like I should be able to figure it out after proving M₁_halts' that a machine halts in one step, but I couldn't… am curious to learn what I'm missing)

[Harold Cooper]

Sorry this is a bit long, any tips appreciated!

[Harold Cooper]

Here's a much more concise version of what I'm trying to prove in case anyone has some tips:

import computability.turing_machine

inductive Λ -- states
| A : Λ
| B : Λ
| C : Λ
instance Λ.inhabited : inhabited Λ := ⟨Λ.A⟩

inductive Γ -- symbols
| zero : Γ
| one : Γ
instance Γ.inhabited : inhabited Γ := ⟨Γ.zero⟩

-- initial state and empty tape:
def cfg₀ : turing.TM0.cfg Γ Λ := turing.TM0.init []

-- chainable step function (since both its input and output have the same option type):
def step' (M : turing.TM0.machine Γ Λ) (x : option (turing.TM0.cfg Γ Λ)) :
  option (turing.TM0.cfg Γ Λ) :=
x.bind (turing.TM0.step M)

-- step a given number of times:
def multistep (M : turing.TM0.machine Γ Λ) :
  ℕ → option (turing.TM0.cfg Γ Λ) → option (turing.TM0.cfg Γ Λ) :=
nat.repeat (λ _, step' M)


-- I'm trying to prove this:
example {M} : (∃ n, multistep M n cfg₀ = none) ↔ (∃ x, turing.TM0.eval M [] = part.some x) :=
begin
  sorry
end


-- or this if it's easier, since I've already proven (turing.TM0.eval M []).dom ↔ (∃ x, turing.TM0.eval M [] = part.some x)
example {M} : (∃ n, multistep M n cfg₀ = none) ↔ (turing.TM0.eval M []).dom :=
begin
  sorry
end

Thanks!

[Mario Carneiro]

Sorry, I forgot to respond to this one. I made some minor tweaks but it's essentially the same theorem:

def multistep (M : turing.TM0.machine Γ Λ) :
  ℕ → option (turing.TM0.cfg Γ Λ) → option (turing.TM0.cfg Γ Λ) :=
nat.iterate (step' M)

example {M} : (∃ n, multistep M n (some cfg₀) = none) ↔ (turing.TM0.eval M []).dom :=
begin
  simp [turing.TM0.eval, cfg₀, multistep],
  split,
  { rintro ⟨n, e⟩,
    generalize_hyp : turing.TM0.init [] = k at e ⊢,
    induction n with n IH generalizing k, {cases e},
    rw [nat.iterate, step', option.bind] at e,
    cases e' : turing.TM0.step M k; rw e' at e,
    { exact part.dom_iff_mem.2 ⟨_, turing.mem_eval.2 ⟨relation.refl_trans_gen.refl, e'⟩⟩ },
    { rw turing.reaches_eval (relation.refl_trans_gen.single e'),
      exact IH _ e } },
  { intro h,
    obtain ⟨a, h⟩ := part.dom_iff_mem.1 h,
    refine turing.eval_induction h (λ k h IH, _),
    cases e : turing.TM0.step M k,
    { exact ⟨1, e⟩ },
    { obtain ⟨n, hn⟩ := IH _ _ e,
      { exact ⟨n+1, by simp [nat.iterate, step', e, hn]⟩ },
      { rwa ← turing.reaches_eval (relation.refl_trans_gen.single e) } } }
end

[Harold Cooper]

Oh awesome, thanks as always @Mario Carneiro!

I'll step through this and likely learn quite a few things

[Harold Cooper]

oh and good call on nat.iterate, I didn't know about that