Recursive function

Stream: new members

[Patrick Stevens]

I want to encode the following chain - you can probably ignore everything up til the final definition computes whose structure is quite clear. Basically, I say state A "computes to" state B if either A = B, or there is C such that A ~ C and C computes to B (for some fixed known notion of ~).

How can I specify this type? Lean lacks the usual phrasing of recursive functions that I would normally reach for in a programming language, so the following doesn't compile. Am I going to have to parameterise my type on the length of the chain and then define it by induction?

import data.pfun
import computability.turing_machine
import data.zmod.basic
import data.option.basic

structure modular_machine :=
  (M : nat)
  (mBig : 1 < M)
  (steps : (fin M) -> (fin M) -> option (prod (fin (M ^ 2)) turing.dir))

def reduces
  (m : modular_machine)
  (fromState : nat × nat) -- α , β , u m + a, v m + b
  (toState : nat × nat) -- α1 , β1 ,
  :=
  ∃ c < m.M,
  -- α1 = u m^2 + c , β1 = v
  -- α1 = u , β1 = v m^2 + c
  (toState.fst = (fromState.fst / m.M) * m.M * m.M + c ∧ toState.snd = fromState.snd / m.M)
  ∨
  (toState.fst = fromState.fst / m.M ∧ toState.snd = (fromState.snd / m.M) * m.M * m.M + c)

def computes
  (m : modular_machine)
  (fromState : nat × nat)
  (toState : nat × nat)
  :=
  fromState = toState ∨ (∃ c, (reduces m fromState c ∧ computes m c toState)

[Patrick Stevens]

(by the way, this is in aid of supplying an alternative Turing-complete form of computation which is fundamental to the proof I know of the unsolvability of the word problem in groups, see https://www.patrickstevens.co.uk/misc/ModularMachines/EmbedMMIntoTuringMachine.pdf if interested)

[Reid Barton]

The usual way to construct this is as an inductive proposition. In fact it already exists as https://leanprover-community.github.io/mathlib_docs/logic/relation.html#relation.refl_trans_gen

[Reid Barton]

(and I see that computability.turing_machine uses it, for example)

[Reid Barton]

Your "definition" is not really a definition at all as it stands--if we treat it as an equation, then the constant "true" relation also satisfies it. You need to say that computes is the smallest relation with this property, and that's what an inductive proposition is.

[Patrick Stevens]

Thanks - did you just know what you were looking for, or did you find this by some method?

[Mario Carneiro]

In this case you are describing a well known construction - the reflexive/transitive closure of a relation, so there is probably a mathlib definition about it, although the name refl_trans_gen is not the easiest to guess

[Mario Carneiro]

Assuming you don't find it in the library (or even if you do and find the API uncomfortable), you can also write it directly. As Reid says the minimality property (and non-well founded recursive structure) should lead you to an inductive definition, which looks like this:

inductive computes (m : modular_machine) : nat × nat → nat × nat → Prop
| refl {c} : computes c c
| trans {c₁ c₂ c₃} : reduces c₁ c₂ → computes c₂ c₃ → computes c₁ c₃

[Mario Carneiro]

Another way you could find your way to refl_trans_gen is by looking at your dependencies. turing_machine uses it all over the place, but it is wrapped up in another collection of definitions, reaches, reaches₁ and reaches₀ , which are suitable for deterministic state machines with a step function of type A -> option A

[Patrick Stevens]

Thanks!

[Mario Carneiro]

@Patrick Stevens Here's how you would write this model using the general framework in computability.turing_machine:

namespace modular_machine

section
parameters (M : nat) (mBig : 1 < M)

def machine := fin M -> fin M -> option (fin (M ^ 2) × turing.dir)

def cfg := ℕ × ℕ

def top (x : ℕ) : fin M := ⟨x % M, nat.mod_lt _ (nat.lt_of_succ_lt mBig)⟩

def step (m : machine) : cfg → option cfg
| (A, B) := (m (top A) (top B)).map $ λ ⟨xy, d⟩,
  match d with
  | turing.dir.left := ((A - A % M) * M + xy, B / M)
  | turing.dir.right := (A / M, (B - B % M) * M + xy)
  end

def computes (m : machine) := turing.reaches (step m)
end

end modular_machine

[Patrick Stevens]

Thanks a lot!