Zulip Chat Archive

Stream: general

Topic: unexpected occurrence of recursive function


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!

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.

Keeley Hoek (Jun 12 2019 at 11:36):

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

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)

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

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

Reid Barton (Jun 12 2019 at 11:39):

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

Keeley Hoek (Jun 12 2019 at 11:40):

aha! ok. Thanks! :)

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

Yakov Pechersky (Apr 01 2021 at 01:42):

Or is this an issue of a nested inductive?

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

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.

Yakov Pechersky (Apr 01 2021 at 02:51):

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

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

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

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.

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.

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.

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.

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.

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

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: Dec 20 2023 at 11:08 UTC