WellFoundedness and functions

Stream: new members

[Thomas Vigouroux]

Hey there
I am trying to learn a little about WellFounded and the likes, in the context of an proof I am trying about Turing Machines.

Here is the context: Given a TM, I want to build the (possibly empty) list of states it goes through before writing the first non-zero symbol.

I would like to do so using a WellFounded relation, do you have any ideas ?

[Quang Dao]

Can you post your current definition of Turing machines?

[Thomas Vigouroux]

Here it is:

abbrev Label (l: ℕ) := Fin (l + 1)
abbrev Symbol (s: ℕ) := Fin (s + 1)

inductive Stmt (l s: ℕ)
| halt
| next: Symbol s → Turing.Dir → Label l → Stmt l s
deriving DecidableEq

def Machine (l s: ℕ):= Label l → Symbol s → Stmt l s

structure Config (l s: ℕ) [Inhabited $ Symbol s] where
  state: Label l
  tape: Turing.Tape (Symbol s)

def Machine.step (M: Machine l s) (orig: Config l s): Option (Config l s) := match M orig.state orig.tape.head with
| .halt => none
| .next sym dir state => some { state, tape := orig.tape.write sym |>.move dir}

[Thomas Vigouroux]

I ended up being able to show what I wanted.

For the record, this is an attempt at formalizing the results of Busy Beaver in lean (it has been done in Coq already).

Here is the project link: https://git.sr.ht/~vigoux/busybeaver