Is recursion exclusive to inductive types that are datatype?

Stream: lean4

[nrs]

I could not fit the plural of datatypes in the title hehe. From #lean4 > Are all recursive functions implemented with .brecOn? and reading the new manual's section on structural recursion, I just wanted to confirm: it seems to me that there is a distinction between recursion and induction, where induction is something that can happen on dataless types. Would it be correct to say that the Lean kernel or compiler only needs to support/involve recursion (or derecursification) when eliminating inductive types that contain data? I think maybe the following question captures the essence of what I'm trying to ask:

Is recursion in Lean exclusively a phenomenon that occurs when eliminating a type that is not in Prop?

[nrs]

A stricter definition of datatype could be an Encodable type (maybe?)

[Kyle Miller]

I'm not sure what you mean about a difference between recursion and induction, or what you mean precisely by a dataless type (do you mean a type that's Prop-valued? a type that only eliminates to Prop? a type that contains no computationally relevant fields?)

The following is a theorem proved using recursion, and you can see it uses P.brecOn like any other structural recursion.

inductive P : Nat → Prop
  | one : P 1
  | succ (n : Nat) : P n → P (n + 1)

theorem test (n : Nat) (h : P n) : 1 ≤ n :=
  match h with
  | .one => le_refl 1
  | .succ n h => Nat.le_step <| test n h

[nrs]

hm right... that does generate a brecOn definition

[nrs]

I'm trying to determine whether recursion is exclusively something that occurs wrt types that contain as you say "computationally relevant fields", but I don't have a very good definition of what this might mean. I just infer there must be such a difference because .rec can be used to eliminate values without at times seemingly needing to perform any sort of recursive computation

[nrs]

Also from that fact that in sources about type theory there is always a disclaimer that the name "recursor" might be confusing as there may not be recursion involved at all (understandably so, as a type's "recursor" is just the name for the eliminator of the values/terms for a particular type)

[Kyle Miller]

Where do you see a distinction between recursion and induction in Lean?

[nrs]

I am not sure I can pinpoint it, but it seems to me it would explain the need for explicitly needing to compile .rec to use it in a definition, and the insufficiency of .rec to define functions that use instead .brecOn

[nrs]

that is, if the distinction between recursion and induction is one of "dataful" vs "dataless" elimination

[Kyle Miller]

Needing to explicitly compile .rec is just that the compiler doesn't compile it by default. The runtime semantics of recursors is also a bit unclear, since naively you might always evaluate the base case. They're not like normal functions.

[Kyle Miller]

This is not any sort of fundamental theory about recursors. My understanding is that the next code generator will handle them.

[Kyle Miller]

It's a design decision to have the compiler consume elaborated match expressions rather than recursors. In fact, the code generator does not support brecOn either.

inductive MyNat where
  | zero
  | succ (n : MyNat)

def f : MyNat → MyNat := (fun n => (MyNat.brecOn n (fun t _ => t) : MyNat))
/-  ~
code generator does not support recursor 'MyNat.brecOn' yet,
consider using 'match ... with' and/or structural recursion
-/

[nrs]

hm I will be thinking about your comments, tyvm for taking the time!