Zulip Chat Archive

Stream: general

Topic: forcing structural recursion


view this post on Zulip Simon Hudon (Feb 27 2018 at 23:18):

I have a mutually inductive type of tree (which is not a type family) and I'm trying to define a recursive function on it but the termination checker seems to default to well founded recursion while it should be clear that structural recursion works. Is there a way to nudge Lean in the right direction?

view this post on Zulip Simon Hudon (Feb 27 2018 at 23:20):

In case that helps, here's my type definition and my function:

mutual inductive proxy_v, proxy_leaf_v (var : Type (max u v+1)) (α : Type u)
with proxy_v : Type (max u v+1)
  | ret {} : α  proxy_v
  | action {} :  β, m β  (β  proxy_leaf_v)  proxy_v
  | yield {}  : y'  (y  proxy_leaf_v)   proxy_v
  | await {} :  x   (x'  proxy_leaf_v)  proxy_v
  | think {} : proxy_leaf_v  proxy_v
with proxy_leaf_v : Type (max u v+1)
  | hole {} : var  proxy_leaf_v
  | more {} : proxy_v  proxy_leaf_v

@[reducible]
def proxy  : Type (max u v+1) :=
proxy_v (proxy_intl α) α

@[reducible]
def proxy_leaf  : Type (max u v+1) :=
proxy_leaf_v (proxy_intl α) α
mutual def to_intl_aux, to_intl
with to_intl_aux : proxy_leaf x x' y y' m α  proxy_intl x x' y y' m α
 | (hole x) := x
 | (more x) := to_intl x
with to_intl : proxy x x' y y' m α  proxy_intl x x' y y' m α
 | (ret i) := cofix.mk (proxy_node.ret i) empty.rec'
 | (action β cmd f) := cofix.mk (proxy_node.action cmd) (λ i, to_intl_aux (f i))
 | (yield o f) := cofix.mk (proxy_node.yield o) (λ i, to_intl_aux (f i))
 | (await o f) := cofix.mk (proxy_node.await o) (λ i, to_intl_aux (f i))
 | (think cmd) := cofix.mk (proxy_node.think) (λ _, to_intl_aux cmd)

view this post on Zulip Sebastian Ullrich (Feb 27 2018 at 23:29):

The equations compiler does not support mutual structural recursion https://github.com/leanprover/lean/blob/8a93d2770e5e4c349d761ded334f8fb7119e7082/src/library/equations_compiler/compiler.cpp#L52

view this post on Zulip Simon Hudon (Feb 27 2018 at 23:32):

Arrg! tears hair out

view this post on Zulip Simon Hudon (Feb 27 2018 at 23:33):

I have a feeling that recursion based on sizeof will be difficult because of that components of type something -> proxy_v

view this post on Zulip Simon Hudon (Feb 27 2018 at 23:33):

Any advice?

view this post on Zulip Sebastian Ullrich (Feb 27 2018 at 23:35):

I don't think I've really used mutual recursion so far

view this post on Zulip Simon Hudon (Feb 27 2018 at 23:42):

Ok here's my next attempt: I'm inlining the function to_intl_aux

def to_intl : proxy x x' y y' m α  proxy_intl x x' y y' m α
 | (ret i) := cofix.mk (proxy_node.ret i) empty.rec'
 | (action β cmd f) := cofix.mk (proxy_node.action cmd) (λ i,
   match (f i) with
    | (hole x) := x
    | (more x) := to_intl x
   end )
 | (yield o f) := cofix.mk (proxy_node.yield o) (λ i,
   match (f i) with
    | (hole x) := x
    | (more x) := to_intl x
   end )
 | (await o f) := cofix.mk (proxy_node.await o) (λ i,
   match (f i) with
    | (hole x) := x
    | (more x) := to_intl x
   end )
 | (think cmd) := cofix.mk (proxy_node.think) (λ _,
   match cmd with
    | (hole x) := x
    | (more x) := to_intl x
   end )

Again, it's falling back on well founded recursion and trying to prove that, in many cases sizeof x < 1

view this post on Zulip Simon Hudon (Feb 27 2018 at 23:45):

Is there any theoretical limitation that prevents the use of structural recursion in mutually recursive functions?

view this post on Zulip Simon Hudon (Feb 27 2018 at 23:57):

Good news everyone! I made it work by hardcoding the details of the mutually inductive type

view this post on Zulip Simon Hudon (Feb 28 2018 at 00:14):

Is there any plan to make io universe polymorphic?

view this post on Zulip Sebastian Ullrich (Feb 28 2018 at 09:50):

Is there any theoretical limitation that prevents the use of structural recursion in mutually recursive functions?

I don't think so

view this post on Zulip Sebastian Ullrich (Feb 28 2018 at 09:52):

Is there any plan to make io universe polymorphic?

No plans, but I don't see why not

view this post on Zulip Simon Hudon (Mar 01 2018 at 20:08):

With regards to structural recursion, would it be any better if instead of having a proxy_leaf_v branch, I would just use ? Would that block my structural recursion then too?

view this post on Zulip Sebastian Ullrich (Mar 01 2018 at 22:09):

Ah, that should probably work...?

view this post on Zulip Simon Hudon (Mar 01 2018 at 22:10):

Maybe that's better than coding my own mutually inductive type then. I'll give it a try

view this post on Zulip Sebastian Ullrich (Apr 25 2018 at 12:54):

@Simon Hudon Did you ever make progress on this issue? Should mutual inductives in Lean 3 simply be avoided?

view this post on Zulip Simon Hudon (Apr 25 2018 at 13:09):

I ended up encoding my mutually inductive type by hand using an inductive family. I think that was the only way to do it.

view this post on Zulip Simon Hudon (Apr 25 2018 at 13:12):

It's been a few months since I touched that project but I'm wondering if the situation would improved if has_well_founded had two type parameter. When you're using polymorphic recursion, i.e. your function foo has type foo : Π {α : Type*}, my_type α and that your recursive call is on my_type β, I wonder if that would make well founded recursion work nonetheless

view this post on Zulip Sebastian Ullrich (Apr 25 2018 at 13:50):

Good to know, thanks. I'm not sure I understand your has_well_founded idea. Do you not have a (monomorphic) measure on your type?

view this post on Zulip Simon Hudon (Apr 25 2018 at 14:01):

Yes, the one based on has_sizeof should do.

view this post on Zulip Simon Hudon (Apr 25 2018 at 14:05):

What I mean is that has_well_founded.r x y might be the appropriate proof obligation in situations where x : my_type α and y : my_type β but that's not well typed. That where the only solution is structural recursion

view this post on Zulip Sebastian Ullrich (Apr 25 2018 at 15:39):

I think the current equation compiler may actually be... acceptable... if we had tactics that could deal with these usually very simple inequations. We don't currently, do we? :)

view this post on Zulip Simon Hudon (Apr 25 2018 at 18:51):

Are you suggesting that it could be fixed using a using_well_founded clause?

view this post on Zulip Sebastian Ullrich (Apr 25 2018 at 22:34):

Yes. The first issue is that the default wf tactic pair uses the sum of the measures of all arguments, which makes the inequations harder, or possibly even contradictory. So the first step may be a rel_tac tactic that uses the measure of only a single argument (probably the first one that is discriminated), which should generate inequations of the form x < ... + x + ... + 1. It should not be too hard to write a dec_tac to solve those. With that we should get a wf tactic pair that proves all mutual structural recursions over a single argument.

view this post on Zulip Simon Hudon (Apr 25 2018 at 22:38):

Nice! Do you think there might be a way to integrate it to the default well founded recursion tactic?

view this post on Zulip Sebastian Ullrich (Apr 25 2018 at 22:45):

Well, I hope that in the next version of Lean there will simply be native support for mutual structural recursion


Last updated: May 11 2021 at 00:31 UTC