Zulip Chat Archive

Stream: general

Topic: Autogenerating recursive calls


view this post on Zulip Wojciech Nawrocki (Jan 10 2020 at 01:24):

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

view this post on Zulip Simon Hudon (Jan 10 2020 at 01:34):

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)

view this post on Zulip Simon Hudon (Jan 10 2020 at 01:35):

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

view this post on Zulip Tim Daly (Jan 10 2020 at 04:50):

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.

view this post on Zulip Tim Daly (Jan 10 2020 at 05:00):

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

view this post on Zulip Wojciech Nawrocki (Jan 10 2020 at 11:30):

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.

view this post on Zulip Simon Hudon (Jan 10 2020 at 12:55):

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?

view this post on Zulip Chris B (Jan 10 2020 at 13:01):

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?

view this post on Zulip Simon Hudon (Jan 10 2020 at 13:14):

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.

view this post on Zulip Wojciech Nawrocki (Jan 10 2020 at 13:33):

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!

view this post on Zulip Simon Hudon (Jan 10 2020 at 14:19):

No worries

view this post on Zulip Simon Hudon (Jan 10 2020 at 14:19):

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)

view this post on Zulip Simon Hudon (Jan 10 2020 at 14:19):

(it compiles)

view this post on Zulip Simon Hudon (Jan 10 2020 at 14:20):

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

view this post on Zulip Simon Hudon (Jan 10 2020 at 14:20):

You can also opt for a different well-founded relation

view this post on Zulip Wojciech Nawrocki (Jan 10 2020 at 15:05):

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?

view this post on Zulip Simon Hudon (Jan 10 2020 at 19:06):

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.

view this post on Zulip Wojciech Nawrocki (Jan 10 2020 at 23:43):

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.

view this post on Zulip Simon Hudon (Jan 10 2020 at 23:49):

We could get formula_struct generated ourselves


Last updated: May 10 2021 at 00:31 UTC