[TYPES] Reference request: decidability of head normalization for a pure first-order calculus with recursion

[Gabriel Scherer]

Dear types-list,

When working on something seemingly unrelated, I ended up writing what I
suspect is a decision procedure for termination of head reduction for the
first-order lambda-calculus with recursion -- see the details of the
calculus below.

This looks like a relatively natural problem that other people have
probably considered in the past. Would you know of previous work
establishing the decidability of whether a term has a head normal form?


## A first-order pure (untyped) calculus

Consider the pure untyped lambda-calculus (no other data structures than
functions):

  t ::=
      | x
      | t t
      | lambda x. t

Now consider the "first-order" restriction of this calculus, where
functions may not be passed as function parameters themselves. There are
two ways to capture this restriction:
- use a simple type discipline, where lambda arguments must have ground
type, or
- make a distinction in the grammar between function names and non-function
variables names.

Using the second approach, we can propose the following grammar for example:

  t ::=
      | x
      | let f(x1, x2, ...) = t in t
      | f(t1, t2, ...)

In this calculus, subterms of the form f(t1, t2...) are head
redexes if there is a definition of f in the surrounding
scope. Otherwise, if f is a free function variable, they are in
head normal form.

For example:

  let id(x) = x in id(id(y))

This first-order restriction is much less expressive: no church
integers, no conditionals, no elimination of pairs, etc. In
particular it can be proved normalizing by a direct structural
induction.


## First-order pure calculus with recursion

If we allow mutually-recursive functions, we immediately lose the
property that all terms are normalizing.

  t ::=
      | x
      | let rec f1(x1, x2, ...) = t1
            and f2(y1, y2, ...) = t2
            and ...
        in t
      | f(t1, t2, ...)

This term has no head normal form:

  let rec loop(x) = loop(x) in
  loop(y)

And this term has a head normal form, but no strong normal form:

  let rec nats_from(n) = cons(n, nats_from(s(n))) in
  nats_from(z())

its head normal form is

  cons(z(), s(nats_from(s(z()))))

and it reduces to the infinite stream

  cons(z(), cons(s(z()), cons(s(s(z())), ....)))


## Decidability of head normalization

Claim: for this pure first-order lambda-calculus with recursion, it is
decidable whether a given term has a head normal form.

Question: Do you know of a published proof of this result?

If the result is indeed true, I would assume that previous proofs exist,
because this is a relatively natural question. I looked for something like
this in particular in the literature on Term Rewriting Systems, but as a
non-expert I failed to find a proof of this result there.


Best