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

[Gabriel Scherer]

Dear types,

A small follow-up on new answers to my question of decidability of order-1
recursive schemes.

Sylvain Salvati has pointed out a practical algorithm to compute the
normalization of the recursive definitions by interpreting them in a domain
O with two values {⊥,⊤} ordered by ⊥≤⊤, where ⊥ interprets non-terminating
terms and ⊤ interprets terminating terms. Decidability of normalization
comes from the fact that fixpoints on this domain (or on first-order
function domains Oⁿ→O) are clearly decidable/computation.
Sylvain has published a 2015 paper with Igor Walukiewicz on framing not
just termination but also richer properties (captured by special classes of
automata) in this style, that they call "model construction", where
decidability results come with practical decision algorithms.

  Using models to model-check recursive schemes
  Sylvain Salvati and Igor Walukiewicz, 2015
  https://urldefense.com/v3/__https://lmcs.episciences.org/1567__;!!IBzWLUs!XjE1I-g2pV_7mCFIAzkrwCGm50p8Vrlkz1waEeD80ZBquELVXDyN5lU1qHMHejCvG6FFKHL-OdJz0aNmv74BCOcKc-Jw-aF5tkGFdA$ 


Gordon Plotkin also sent me a reference to a paper of his on this topic:

  Recursion does not always help
  Gordon Plotkin, 1982 or 2022
  https://urldefense.com/v3/__https://arxiv.org/abs/2206.08413__;!!IBzWLUs!XjE1I-g2pV_7mCFIAzkrwCGm50p8Vrlkz1waEeD80ZBquELVXDyN5lU1qHMHejCvG6FFKHL-OdJz0aNmv74BCOcKc-Jw-aGHxiWJCg$ 

This 2022 paper is a rewritten version of notes that Gordon wrote in 1982
and apparently forgot about for a while. It makes a similar observation
that we can use the two-element domain to interpret termination of terms of
order 0 (of base type in the simply-typed formulation). When applying the
fixpoint operator Y at an arbitrary higher-order type σ, Gordon shows that
it suffices to iterate/unfold the fixpoint computation at most h(σ) time
where h is the height of σ seen as a lattice.

In particular, note that this proves decidability of termination of the
pure simply-typed lambda-calculus with recursion, without any first-order
restriction.

I found this paper by Gordon a pleasant/easy read for someone with
experience in programming languages and some type theory (but not automata
etc.): if you don't know what "the model-checking problem for MSO" means,
start with Gordon's paper. (It also mentions a 2004 paper by Richard
Statman also establishing the decidability of termination in the
higher-order case, but that paper was not as easy to read for me.)


Finally: in my previous email I sent a high-level explanation on the proof
argument of Zurab Khasidashvil in the first-order case:

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

Unfortunately, this explanation is false. The cited proof (
https://urldefense.com/v3/__https://www.viam.science.tsu.ge/Ami/2020_2/5_zura.pdf__;!!IBzWLUs!XjE1I-g2pV_7mCFIAzkrwCGm50p8Vrlkz1waEeD80ZBquELVXDyN5lU1qHMHejCvG6FFKHL-OdJz0aNmv74BCOcKc-Jw-aGYdfPejQ$  ) is correct, only my
summary wasn't. The proof crucially relies on expanding some terms during
termination checking, which is more expressive than the "static" algorithm
I sketched above. Consider for example the following order-0 recursion
scheme:

  f(x) = erase(g(x))
  g(y) = f(y)
  erase(z) = stop()

With the algorithm sketched in my summary, one would wrongly determine that
(f, g) form a cycle and introduce non-termination, but all three functions
are in fact terminating. The "real" proof does follow a topological order,
but at each step it also performs some computation (it normalizes with
respect to functions already found terminating) and this may refine the
dependency order by erasing some subterms.

The algorithm underlying Zurab's proof can be understood as a fixpoint
computation as presented by Sylvain Salvati. On the example above:
- on the first iteration of the computation, we can compute stop() as ⊤
- on the second iteration, we thus get (erase(z) = ⊤)
- on the third iteration, we thus get (f(x) = ⊤)
- finally we can deduce g(y) = ⊤, showing that all functions are terminating

(In this example, the interpretation of all functions are constant
functions, but this is not necessarily the case, for example (id(x) = x) is
interpreted by the identity on the domain O.)

On Fri, Feb 17, 2023 at 2:54 PM Gabriel Scherer <gabriel.scherer at gmail.com>
wrote:

> 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:
>
>   c <https://urldefense.com/v3/__https://listes.ens-lyon.fr/sympa/info/rewriting/__;!!IBzWLUs!XjE1I-g2pV_7mCFIAzkrwCGm50p8Vrlkz1waEeD80ZBquELVXDyN5lU1qHMHejCvG6FFKHL-OdJz0aNmv74BCOcKc-Jw-aHF0pgglg$ >
>
> 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!XjE1I-g2pV_7mCFIAzkrwCGm50p8Vrlkz1waEeD80ZBquELVXDyN5lU1qHMHejCvG6FFKHL-OdJz0aNmv74BCOcKc-Jw-aH7lmFnWQ$ 
>
> 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!XjE1I-g2pV_7mCFIAzkrwCGm50p8Vrlkz1waEeD80ZBquELVXDyN5lU1qHMHejCvG6FFKHL-OdJz0aNmv74BCOcKc-Jw-aELJNJf9A$  .
>
>
> 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!XjE1I-g2pV_7mCFIAzkrwCGm50p8Vrlkz1waEeD80ZBquELVXDyN5lU1qHMHejCvG6FFKHL-OdJz0aNmv74BCOcKc-Jw-aGYdfPejQ$ 
>
> 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
>>
>