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

[Gabriel Scherer]

Dear types-list,

I have received excellent replies from Pablo Barenbaum and Martin Lester,
thanks to them both!


First: Delia Kesner advertized the "rewriting" list as a good place to ask
similar questions in the future:

  https://urldefense.com/v3/__https://listes.ens-lyon.fr/sympa/info/rewriting/__;!!IBzWLUs!UmE2Bk2_gj40xjyJ2PLWjqV16vC7YHWc7jvOD7Q8vrH6A9_c5dT1RApNIIjl4IMCRAJzGVKrF_pYsdIQ2ZjIRPDEgtQOd5FBykAaCQ$ 

Hopefully this can be useful to other list members as  well if they need a
rewriting fix.


Here is what I (re)learned from the replies:

- The "first-order calculus with recursion" I mentioned is a specific shape
of term rewriting systems that was central in the research on "recursive
program schemes" a few decades ago. It is attributed to Maurice Nivat in
1972, who called them "recursive applicative program schemes" and did
fruitful research with Bruno Courcelle on this topic.

- Since then there has been a very rich literature on *higher-order*
recursion schemes, which are not first-order in the sense above and allow
arguments to be functions themselves (of order strictly above 0). The
central question in this field is to decide equivalence of two recursion
schemes (rather than normalization or head normalization). There are rich
connections with automata theory, and important results of Kobayashi and
also Ong on higher-order model checking. In this context, the first-order
calculus with recursion corresponds to "recursive schemes of order 1".

Let me quote Martin's answer for the details:

    I think the property you are asking about is decidable as a specific
    case of Alternating Parity Tree automata/MSO model-checking of value
    trees generated by higher order recursion schemes (Luke Ong, LICS
    2006).

    However, your first order restriction makes it simpler. I guess you
    have an order 0 or order 1 recursion scheme, for which decidability
    will be simpler and will have been proved earlier. If you chase the
    references in the Introduction of this book chapter by Carayol and
    Serre, you may find the origin:

    https://urldefense.com/v3/__https://hal.science/hal-03176662/document__;!!IBzWLUs!UmE2Bk2_gj40xjyJ2PLWjqV16vC7YHWc7jvOD7Q8vrH6A9_c5dT1RApNIIjl4IMCRAJzGVKrF_pYsdIQ2ZjIRPDEgtQOd5HJEWUw_Q$ 

I can confirm that the introduction of the chapter above by Carayol and
Serre is a pleasant read and full of pointers into the connections between
higher-order recursion schemes and automata theory.
Looking at this (did not directly answer my question but) also reminded me
of previous work on the connection between higher-order model checking and
linear logic, see for example https://urldefense.com/v3/__https://arxiv.org/pdf/1501.04789.pdf__;!!IBzWLUs!UmE2Bk2_gj40xjyJ2PLWjqV16vC7YHWc7jvOD7Q8vrH6A9_c5dT1RApNIIjl4IMCRAJzGVKrF_pYsdIQ2ZjIRPDEgtQOd5EptWhkxw$  .


For the decidability of termination of full reduction of order-1 recursion
schemes, Pablo Barenbaum pointed me to the following simple proof (and was
kind enough to provide some user support for my questions):

  A short proof of the decidability of normalization in recursive program
schemes
  Zurab Khasidashvil, 2020
  https://urldefense.com/v3/__https://www.viam.science.tsu.ge/Ami/2020_2/5_zura.pdf__;!!IBzWLUs!UmE2Bk2_gj40xjyJ2PLWjqV16vC7YHWc7jvOD7Q8vrH6A9_c5dT1RApNIIjl4IMCRAJzGVKrF_pYsdIQ2ZjIRPDEgtQOd5Eu4Uz7jA$ 

My understanding of the proof uses a topological sort on recursive
functions for the dependency order (f <= g if the definition of g calls f).
If a recursive function belongs to a cycle for this dependency order, then
any call to this function gives a diverging term; same for any function
that is above such a cycle in the dependency order (reducing its calls
eventually reveals a function in a cycle). If a function is not above any
cycle (all its descending chains in the dependency order are finite), then
calling it with terminating arguments always terminates. A term is
terminating if and only all the bound functions it calls are terminating in
this sense.

For head reduction, one can probably make the same argument with a
restricted dependency order that does not consider function calls that are
"guarded" under a free function variable -- or, equivalently, erase the
arguments of free function variables and ask about normalization of full
reduction for the simplified system.


On Thu, Feb 16, 2023 at 11:23 PM Gabriel Scherer <gabriel.scherer at gmail.com>
wrote:

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