Understanding Turing.eval

Stream: lean4

[Stuart Geipel]

I am digging into Turing machines and started with a simple Collatz function:

def collatzStep (n : Nat) : Option Nat :=
  let next := if n % 2 = 0 then n / 2 else n * 3 + 1
  if n > 1 then Option.some next
  else Option.none

Then I can make a machine with Turing.eval which uses partial functions to expect a proof it halts:

def collatz := Turing.eval collatzStep
lemma eleven_halts : (collatz 11).Dom := sorry

But unfortunately that's where I've gotten stuck. How do I prove for example that collatz 11 halts, or collatz (2^n)? Proving the Dom requires understanding PFun.fix which I'm struggling with. Unfolding the definitions creates an enormous proof goal.

[Mario Carneiro]

you probably want to use dom_of_mem_fix and then fix_fwd to advance the machine and fix_stop to terminate

[Stuart Geipel]

This is great, thank you!

[Martin Dvořák]

I am really confused by what this means. Do we have a crosspiler that automatically generates a Turing machine for such a complicated function?!

[Mario Carneiro]

there is no TM here. This is just using PFun.fix with a specific step function

[Martin Dvořák]

Doesn't Turing.eval refer to a Turing machine?

[Stuart Geipel]

Turing.eval doesn't actually interact with the Turing machine types, it just takes a function f : α -> Option α and recurses f using PFun.fix - it handles creating the Sum type for you and makes sure it returns the second to last state (the state it halted on).
So I am using it to iterate the Collatz function (which might not halt for all we know) but there's no tape or anything.