Stream: General

Topic: Recursion theorem on some inductive datatype constructors

Ant S. (Mar 10 2026 at 13:17):

Suppose I have some inductive data type like a tree in a locale:

datatype tree =
        Leaf int
     |  Branch "tree" "'tree"

locale foo =
assumes recFn :: tree => nat
and bar = "recFn Leaf x = 0"

Is it possible to show that there exists some helper function f', whose type signature is tree => tree => int (or in general, for an inductive constructor X a b c that its signature is a => b => c => d, which I believe would need some sort of reflection on the types of the objects that an instance of X stores), that recursively calls recFn somewhere in its body? I believe this is how the Recursion Theorem works, although that is used in a set-theoretic context. Additionally, since I am "breaking apart" a type into its constituent components, would this notion be easier to represent using a codatatype. Can we construct f' in a way that its type can be inferred?

Fabian Huch (Mar 10 2026 at 14:14):

Your source code is ill-formed, but a statement that 'some function calls some other function' can't be expressed in HOL, unless you are talking about the semantics of some embedded language.

Ant S. (Mar 10 2026 at 14:18):

Sorry bout that, here's the example, with corrections:

datatype tree =
        Leaf int
     |  Branch "tree" "tree"

      locale foo =
      fixes recFn :: "tree ⇒ nat"
      assumes bar: "recFn (Leaf x) = 0"

(also, meta-question: why can't I edit prior messages?)
(well, I'm able to edit this message, but not the previous one)

Ant S. (Mar 10 2026 at 14:21):

Fabian Huch said:

some function calls some other function

How about a refinement: For the Branch constructor: ∃ f s.t. recFn (Branch x y) = f x y, or some generalized form of this for every constructor that is not the "base" constructor

Fabian Huch (Mar 10 2026 at 14:30):

I doubt that this is what you want since λ x y. recFn (Branch x y) is a trivial witness.

Last updated: Mar 20 2026 at 05:16 UTC