[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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.sche...@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 >