Zulip Chat Archive

Stream: general

Topic: unexpected occurrence of recursive function


view this post on Zulip Keeley Hoek (Jun 12 2019 at 11:27):

The following snippet does not compile: unexpected occurrence of recursive function

def height :   
| 0 := 0
| (n + 1) := id height n

I am very disturbed!

view this post on Zulip Neil Strickland (Jun 12 2019 at 11:33):

Did you mean id height n (which is (id height) n, of course) or id (height n)? I am not surprised that the former fails.

view this post on Zulip Keeley Hoek (Jun 12 2019 at 11:36):

I mean't the former---why is it expected that it fails?

view this post on Zulip Reid Barton (Jun 12 2019 at 11:37):

It wouldn't be so great if you instead had id' height n where id' f n := f (n+1)

view this post on Zulip Reid Barton (Jun 12 2019 at 11:38):

So basically you're asking Lean to reduce the right hand side before attempting to determine whether it is syntactically a valid recursive call

view this post on Zulip Keeley Hoek (Jun 12 2019 at 11:39):

Sure, but normally when this happens we get could not prove recursive application is decreasing well-founded relation (or something like that I'm just remembering), and instead this time it seems like lean just goes "nope not even trying this time".

view this post on Zulip Reid Barton (Jun 12 2019 at 11:39):

Well because you don't even have an application of height

view this post on Zulip Keeley Hoek (Jun 12 2019 at 11:40):

aha! ok. Thanks! :)

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 01:39):

What's the right way to phrase a recursive show function like this one? I get a unexpected occurrence of recursive function error

import data.buffer.parser.basic

inductive tree
| leaf (s : string)
| branch (s : string) (l : list tree)

open tree

def tree.show : tree  list string
| (leaf   s)   := [s]
| (branch s l) := [s] ++ l.bind tree.show

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 01:42):

Or is this an issue of a nested inductive?

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 01:45):

I guess this is what is preferred:

import data.buffer.parser.basic

inductive tree
| leaf : string  tree
| branch : string  tree  tree  tree

open tree

def tree.show : tree  list string
| (leaf   s)       := [s]
| (branch s hd tl) := [s] ++ hd.show ++ tl.show

view this post on Zulip Greg Price (Apr 01 2021 at 02:37):

TPIL says that Lean supports type definitions like the one you originally wrote:
https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#mutual-and-nested-inductive-types

I don't know what that error means, though.

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 02:51):

I'm going to try lean4 later to see if it fares better here

view this post on Zulip Greg Price (Apr 01 2021 at 04:00):

Ah, there's also some perhaps helpful information in the previous history of this topic:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/unexpected.20occurrence.20of.20recursive.20function/near/167937423
(Which I happened to notice above this just now.)

view this post on Zulip Greg Price (Apr 01 2021 at 04:00):

In your example, I think the point is then that when Lean is looking at the definition of tree.show, it doesn't know that list.bind is itself a well-behaved recursive function that's compatible with the recursion you're doing here -- so it can't prove the recursion terminates

view this post on Zulip Greg Price (Apr 01 2021 at 04:08):

So one way you could resolve that is like so:

import data.buffer.parser.basic

inductive tree
| leaf (s : string)
| branch (s : string) (l : list tree)

open tree

mutual def tree.show, tree.show_list
with tree.show : tree  list string
| (leaf   s)   := [s]
| (branch s l) := [s] ++ tree.show_list l
with tree.show_list : list tree  list string
|  []      := []
| (h :: t) := tree.show h ++ tree.show_list t

#eval (branch "a" [leaf "b", leaf "c"]).show -- ["a", "b", "c"]

Basically inlining list.bind as part of a mutual recursion.

view this post on Zulip Greg Price (Apr 01 2021 at 04:13):

You may also be able to do it while using list.bind itself, if you can exhibit an appropriate well-founded relation. I haven't tried that feature of Lean, and I'm not sure if it's possible to apply in this situation.

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 04:28):

Mario has suggested to unravel mutual inductives into a plain inductive, and warns against nested inductives here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/nested.20recursion . Also, definitions based on wf aren't as compute friendly, so while this doesn't matter so much here, I do want to find a way to not have to rely on a wf proof.

view this post on Zulip Greg Price (Apr 01 2021 at 04:31):

Ah, I see:

Mario Carneiro said:

nested inductives are not really supported in lean, they are compiled (badly) to inductive types. It's better to roll your own inductive type if you want the right recursion principle

Good to know, then.

view this post on Zulip Greg Price (Apr 01 2021 at 04:32):

Later in the same thread Mario suggests another solution, if just running this code is what you're interested in and not proving theorems about it: you could use meta def for the function and then write the recursion however you like.

view this post on Zulip Yakov Pechersky (Apr 01 2021 at 04:36):

Right. I followed the second solution regarding unfolding. Since it's a simple type, I think it will be okay to have it unraveled (with an additional nil constructor). For reference, here is my lean4 attempt:

inductive tree
| leaf (s : String)
| branch (s : String) (l : List tree)

open tree

def tree.show (t : tree) : List String :=
  loop t
where
  loop := fun
    | leaf s      => [s]
    | branch s xs => [s] ++ xs.bind loop


-- fail to show termination for
--   show.loop
-- with errors
-- structural recursion cannot be used

-- well founded recursion has not been implemented yet

view this post on Zulip Mario Carneiro (Apr 01 2021 at 08:21):

I think this definition is more likely to work:

mutual
def tree.show : tree  List String
| leaf s      => [s]
| branch s xs => [s] ++ show_list xs

def tree.show_list : List tree  List String
| [] => []
| (t :: ts) => «show» t ++ show_list ts
end

but "mutual structural recursion" is not implemented yet


Last updated: May 15 2021 at 02:11 UTC