On equal \(\mu \)-terms (Q549186)

From the text: ``The paper studies a particular orthogonal higher-order rewrite system that we will call \(R_\mu\), containing terms built from some constants, variables, a binary function symbol \texttt{F}, and a higher-order symbol \(\mu\) allowing to construct terms such as \(\mu x. {\mathtt F}(x,{\mathtt c})\), where \texttt{c} is a constant. Everything in this paper generalizes to a more general first-order signature \(\Sigma\), but for our purposes, with recursive types as main application, the specific signature as mentioned will be assumed. There is a single rewrite rule, the \(\mu\)-rule, which reads \(\mu x.M \rightarrow M, x:=\mu x.M\) (in meta-notation using the schematic variable \(M\) and meta-substitution). The rewrite system \(R_\mu\) embodies the recursion principle in a most concentrated form, replacing the fixed point combinators \(Y\) as employed in \(\lambda\)-calculus. In fact, we can consider \(R_\mu\) to be a sub-calculus of \(\lambda\)-calculus, via the translation replacing \(\mu\) by \(Y\circ\mu\) for some fixed point combinator \(Y\); the \(\mu\)-rule then becomes a derived rule. [...] This translation preserves unsolvability; meaningless terms are carried over to unsolvables in the \(\lambda\)-calculus. Just as we can view \(\lambda\)-calculus from the finitary or the infinitary perspective, the latter leading to semantical notions such as Böhm trees, its subsystem \(R_\mu\) can also be viewed finitary or infinitary. The infinitary perspective of \(R_\mu\) is in fact rather well known, as it pertains to tree unwinding semantics of e.g. recursive types [\textit{H. P. Barendregt}, \textit{W. J. M. Dekkers} and \textit{R. Statman}, Lambda Calculus with Types. Perspectives in Logic. Cambridge: Cambridge University Press (2011; Zbl 1347.03001)]. The ensuing equality is called `strong equality' in [Barendregt et al., loc. cit.], holding when \(\mu\)-terms \(M,N\) have the same possibly infinite tree unwinding. There are many proof systems for strong equality, and many algorithms for deciding strong equality. However, the finitary aspects of \(R_\mu\) are much less known. In our first decidability proof for weak \(\mu\)-equality we have adopted the commitment to treat matters \(\alpha\)-free, and clearly separating \(\alpha\)-renaming and \(\mu\)-reduction, extending the proof method of \textit{F. Cardone} and \textit{M. Coppo} [Lect. Notes Comput. Sci. 2841, 242--255 (2003; Zbl 1257.68056)]. It is also adopted in our third decidability proof, which uses tree automata techniques, made possible by our `first-order rendering' of \(\mu\)-terms. Our second decidability proof is under the regime of the commitment to work all the way with \(\alpha\)-equivalence classes and a corresponding notion of \(\mu\)-reduction. It still follows the proof strategy of [Cardone and Coppo, loc. cit.], but now in a pure higher-order setting, so that \(\mu\)-terms are \(\alpha\)-equivalence classes. The advantage is that we do not have to deal with reduction modulo \(\alpha\); this is seamlessly integrated in the notion of reduction in higher-order rewriting. Here a certain disadvantage is that the higher-order setting is less concrete, and also less well known. Summing up, we advocate the adagium that \(\alpha\)-freeness entails a first-order setting. In our paper we have endeavored to put light on the decidability question for weak \(\mu\)-equality from both paradigm perspectives, \(\alpha\)-free with the ensuing first-order setting, and higher-order, with ensuing built-in \(\alpha\)-equivalence. This is the rationale for the different proofs that we have developed. An interesting meta-observation about the inclusion of the core system \(R_\mu\) in the full \(\lambda\)-calculus, is that while in the \(\lambda\)-calculus `every interesting property is undecidable', as validated for many instances by Scott's theorem, in the core system \(R_\mu\) by contrast `every interesting property is decidable'. To substantiate this informal slogan, we have included proofs of decidability of reachability \(\rightarrow\!\!\!\!\rightarrow_{\mu/\alpha}\), and also of unsolvability, and of upward-joinability \(\uparrow_{\mu/\alpha}\).''