Zulip Chat Archive

Stream: new members

Topic: Recursive function


view this post on Zulip Patrick Stevens (May 07 2020 at 17:49):

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)

view this post on Zulip Patrick Stevens (May 07 2020 at 17:53):

(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)

view this post on Zulip Reid Barton (May 07 2020 at 17:58):

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

view this post on Zulip Reid Barton (May 07 2020 at 17:58):

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

view this post on Zulip Reid Barton (May 07 2020 at 18:00):

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.

view this post on Zulip Patrick Stevens (May 07 2020 at 18:07):

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

view this post on Zulip Mario Carneiro (May 07 2020 at 18:11):

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

view this post on Zulip Mario Carneiro (May 07 2020 at 18:15):

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₃

view this post on Zulip Mario Carneiro (May 07 2020 at 18:18):

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

view this post on Zulip Patrick Stevens (May 07 2020 at 18:19):

Thanks!

view this post on Zulip Mario Carneiro (May 07 2020 at 18:40):

@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

view this post on Zulip Patrick Stevens (May 07 2020 at 19:37):

Thanks a lot!


Last updated: May 14 2021 at 00:42 UTC