Stream: general

Topic: forcing structural recursion

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?

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)


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

Simon Hudon (Feb 27 2018 at 23:32):

Arrg! tears hair out

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

Sebastian Ullrich (Feb 27 2018 at 23:35):

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

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

Simon Hudon (Feb 27 2018 at 23:45):

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

Simon Hudon (Feb 27 2018 at 23:57):

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

Simon Hudon (Feb 28 2018 at 00:14):

Is there any plan to make io universe polymorphic?

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

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

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?

Sebastian Ullrich (Mar 01 2018 at 22:09):

Ah, that should probably work...?

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

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?

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.

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

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?

Simon Hudon (Apr 25 2018 at 14:01):

Yes, the one based on has_sizeof should do.

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

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? :)

Simon Hudon (Apr 25 2018 at 18:51):

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

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.

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?

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