Autogenerating recursive calls

Stream: general

[Wojciech Nawrocki]

Hello! Something I would really like for working with types that have many constructors is some kind of code generator for structural recursion in which I only want to touch some subsets of the constructors. For example, consider a simple type of formulas:

inductive formula
| var: string → formula
| plus: formula → formula → formula
| mult: formula → formula → formula

for which I need to write a rename-variables function that changes all 'x's to 'y's:

def rename (x: string) (y: string): formula → formula
| (var nm) := if nm = x then (var y) else (var nm)
| (plus f₁ f₂) := plus (rename f₁) (rename f₂)
| (mult f₁ f₂) := mult (rename f₁) (rename f₂)

Most of this function is trivial and simply calls itself recursively on occurrences of the same type within constructors. Writing such functions is boring and most of the code is boilerplate. Instead, I would like a way to simply say:

@[recurse]
def rename (x: string) (y: string): formula → formula
| (var nm) := if nm = x then (var y) else (var x)

or something similarly short and have Lean autogenerate the rest. Does anyone know if something like or close to it is possible? Has it been done in another language?
(This seems like the kind of thing some variation on lenses could work for but I'm not quite sure.)

[Simon Hudon]

I think I would break down the problem into generating a replace function which looks like:

def replace (f: formula → option formula): formula → formula
| x :=
  match f x with
  | some y := y
  | none :=
    match x with
    | var v := var v
    | plus x y := plus (replace x) (replace y)
    | mult x y := mult (replace x) (replace y)
    end
  end

(not sure if that compiles) and then define your recursive function (by hand or automatically) as:

def rename (x: string) (y: string) : formula → option formula
| (var nm) := some $ if nm = x then (var y) else (var x)
| _ := none

def rename'  (x: string) (y: string) : formula → formula :=
replace (rename x y)

[Simon Hudon]

The code for replace can be generated using the induction tactic.

[Tim Daly]

Actually, no. All the hash function is doing is checking that the proof object is unchanged. Lean could concatenate a version number to the proof it gives to Axiom (for the GCD, for example). When Axiom returns the GCD computation, Lean has to decide to trust the result. So Axiom provides the proof that Lean initially provided for GCD (which Axiom stored a long time ago) and the hash code. Lean can then concatenate the version number of the proof checker to the proof source code, compute the hash and compare it to the prior hash. If either the version number is wrong or the proof text has changed then the hash won't match.

A hash mismatch due to a version number change on Lean's proof checker means that Lean needs to fully check the provided proof. If the version number hasn't changed then the proof text must have changed and Lean needs to fully check the provided proof. But if the hash matches then nothing has changed and there is evidence that the GCD proof previously passed Lean's proof checker so it doesn't need to be re-checked, saving a lot of work.

The hash has nothing to do with the actual method of proof.

The problem to solve is to scale proof checking and trusted computation to larger computations. A Groebner basis can have many steps using other algorithms and each proof of each sub-algorithm needs to be provided to Lean to be checked. A hash checker would make this a very low cost but very trustable operation.

[Tim Daly]

The cryptographic idea that directly applies is called HMAC.key-hashed message authentication codes.

[Wojciech Nawrocki]

Thanks Simon! replace doesn't compile but a version where the structural recursion is top-level does:

def replace₂ (f: formula → option formula): formula → formula
| z@(var v) := match f z with
  | some y := y
  | none := z
  end
| z@(plus x y) := match f z with
  | some y := y
  | none := plus (replace₂ x) (replace₂ y)
  end
| z@(mult x y) := match f z with
  | some y := y
  | none := mult (replace₂ x) (replace₂ y)
  end

It works for the simple case, however I should have been more specific in that I also want to consider functions which may include arbitrary processing of recursive results, e.g.

@[recurse]
def rename (x: string) (y: string): formula → formula
| (var nm) := if nm = x then (var y) else (var nm)
| (plus f₁ f₂) := mult (rename f₁) (rename f₂)

which I'm not sure generalize into a single higher-order function since then one cannot call replace from rename. This is the reason why I asked about code generation. I guess that's what tactics do and induction is a good shout for going some way towards shorter definitions.

[Simon Hudon]

Let's try this again, then.

def rewrite (f: formula → formula): formula → formula
| e@(var _) := f e
| (plus e e') := f (plus (rewrite e) (rewrite e'))
| (mult e e') := f (mult (rewrite e) (rewrite e'))

Then you should be able to write rename so that, together with rewrite it will form rename_all. What do you think?

[Chris B]

I think this is also one of the big selling points of recursion schemes (ala Haskell) if you're interested, but I haven't actually studied them enough to know if you could implement them in Lean. @Simon Hudon Do you know if anything like Haskell's Fix can be done with Lean?

[Simon Hudon]

I also love recursion schemes. Fix is hard to encode directly but there are ways to get close. The simplest approach would be to define it as:

inductive fix (F : Type -> Type) : Type 1
| intro (a : Type) : F a -> (a -> fix) -> fix

It's not quite perfect though. For one thing, fix lies in a different universe than F so F fix is not type correct. More type trickery can still help here.

In another direction, @Mario Carneiro, @Jeremy Avigad and I wrote a paper last year defining quotients of polynomial functors and using them to construct broader classes of inductive and coinductive data types in Lean. Fix is a direct result of that theory QPF.

[Wojciech Nawrocki]

Then you should be able to write rename so that, together with rewrite it will form rename_all. What do you think?

Indeed that should work, but it will not if I modify the function a bit:

def weird_rename (x: string) (y: string): formula → formula
| (var nm) := if nm = x then (var y) else (var nm)
| (plus f₁ f₂) := mult f₁ (weird_rename f₂)

To express this, rewrite would have to pass both rewritten and not-rewritten results, which can be done but I think it would have to make the resulting rewrite' very specific. On first glance recursion schemes do seem to be solving a similar problem, thanks for the link!

[Simon Hudon]

No worries

[Simon Hudon]

Consider the following, I think it helps with your weird case:

open formula

inductive formula_struct : formula → formula → Prop
| plus₁ (f₁ f₂) : formula_struct f₁ (plus f₁ f₂)
| plus₂ (f₁ f₂) : formula_struct f₂ (plus f₁ f₂)
| mult₁ (f₁ f₂) : formula_struct f₁ (mult f₁ f₂)
| mult₂ (f₁ f₂) : formula_struct f₂ (mult f₁ f₂)

def weird_rename (x: string) (y: string): Π f : formula, (Π f', formula_struct f' f → formula) → option formula
| (var nm) rec := some $ if nm = x then (var y) else (var nm)
| (plus f₁ f₂) rec := some $ mult f₁ (rec f₂ $ by constructor)
| (mult _ _) _ := none

lemma well_founded_struct : well_founded formula_struct := sorry

variable step : Π f : formula, (Π f', formula_struct f' f → formula) → option formula

notation `♯` := by constructor

def rewrite : formula → formula :=
well_founded.fix well_founded_struct $
λ x,
match x with
| e@(var v) := λ rec,
               match step e rec with
               | some e' := e'
               | none := e
               end
| e@(plus x y) := λ rec,
               match step e rec with
               | some e' := e'
               | none := plus (rec x ♯) (rec y ♯)
               end
| e@(mult x y) := λ rec,
               match step e rec with
               | some e' := e'
               | none := mult (rec x ♯) (rec y ♯)
               end
end

def weird_rename_all (x: string) (y: string): formula → formula :=
rewrite (weird_rename x y)

[Simon Hudon]

(it compiles)

[Simon Hudon]

But the proof of well-foundedness of the structural ordering is left as an exercise

[Simon Hudon]

You can also opt for a different well-founded relation

[Wojciech Nawrocki]

Thanks Simon, this is quite an interesting solution! By the way, is the generation of a formula_struct roughly similar to what the equation compiler does?

[Simon Hudon]

By the way, is the generation of a formula_struct roughly similar to what the equation compiler does?

No. When declaring formula, an axiom is added to the system:

#check @formula.rec
-- formula.rec :
--   Π {C : formula → Sort u_1},
--     (Π (a : string), C (formula.var a)) →
--     (Π (a a_1 : formula), C a → C a_1 → C (formula.plus a a_1)) →
--     (Π (a a_1 : formula), C a → C a_1 → C (formula.mult a a_1)) →
--      Π (n : formula), C n

This is called a recursor. It is expressive enough to encode structural recursion and induction.

[Wojciech Nawrocki]

Right, weird_rename is indeed expressible via formula.rec. I was wondering more whether the equation compiler is capable of generating well-foundedness relations similar to formula_struct in the wf_rec module when structural recursion fails, as is the case for rewrite but to think of it now that seems to be asking for way too much.

[Simon Hudon]

We could get formula_struct generated ourselves