Towards the average-case analysis of substitution resolution in $\lambda$-calculus

TL;DR

This paper provides an average-case analysis of substitution resolution in lambda calculus by studying the probabilistic normalization behavior of terms in an extended calculus, revealing limiting distributions as term size grows.

Contribution

It introduces a novel probabilistic framework and hierarchical grammars to analyze the average-case complexity of substitution resolution in lambda calculus extensions.

Findings

Probability of normalization in n steps converges to a computable limit as term size increases.

Hierarchical grammars partition terms based on their normalization steps.

Inductive construction of grammars inspired by unification algorithms.

Abstract

Substitution resolution supports the computational character of $\beta$-reduction, complementing its execution with a capture-avoiding exchange of terms for bound variables. Alas, the meta-level definition of substitution, masking a non-trivial computation, turns $\beta$-reduction into an atomic rewriting rule, despite its varying operational complexity. In the current paper we propose a somewhat indirect average-case analysis of substitution resolution in the classic $\lambda$-calculus, based on the quantitative analysis of substitution in $\lambda\upsilon$, an extension of $\lambda$-calculus internalising the $\upsilon$-calculus of explicit substitutions. Within this framework, we show that for any fixed $n \geq 0$, the probability that a uniformly random, conditioned on size, $\lambda\upsilon$-term $\upsilon$-normalises in $n$ normal-order (i.e. leftmost-outermost) reduction steps tends to a computable limit as the term size tends to infinity. For that purpose, we establish an effective hierarchy $\left(\mathscr{G}_n\right)_n$ of regular tree grammars partitioning $\upsilon$-normalisable terms into classes of terms normalising in $n$ normal-order rewriting steps. The main technical ingredient in our construction is an inductive approach to the construction of $\mathscr{G}_{n+1}$ out of $\mathscr{G}_n$ based, in turn, on the algorithmic construction of finite intersection partitions, inspired by Robinson's unification algorithm. Finally, we briefly discuss applications of our approach to other term rewriting systems, focusing on two closely related formalisms, i.e. the full $\lambda\upsilon$-calculus and combinatory logic.

Tables

Table 1. Table 1 . ` ​ y ` 𝑦 `y -rewriting rules with respective templates and production schemes.

	Rewriting rule	Template $\phi$	Production scheme ${\Delta }_{\phi }^n\mapsto \left(G_{n+1}\to \gamma \right)$
(App)	$\left(ab\right)\left[s\right]\to a\left[s\right]\left(b\left[s\right]\right)$	$T\left[S\right]\left(T\left[S\right]\right)$	$\alpha \left[{\tau }_1\right]\left(\beta \left[{\tau }_2\right]\right)\left[{\sigma }_1\right]\cdots \left[{\sigma }_w\right]\mapsto \left(\alpha \beta \right)\left[\tau \right]\left[{\sigma }_1\right]\cdots {\left[{\sigma }_w\right]}^{†}$
(Lambda)	$\left(`la\right)\left[s\right]\to `l\left(a\left[\Uparrow \left(s\right)\right]\right)$	$`l\left(T\left[\Uparrow \left(S\right)\right]\right)$	$`l\left(\alpha \left[\Uparrow \left(\sigma \right)\right]\right)\left[{\sigma }_1\right]\cdots \left[{\sigma }_w\right]\mapsto \left(`l\alpha \right)\left[\sigma \right]\left[{\sigma }_1\right]\cdots \left[{\sigma }_w\right]$
(FVar)	$\text{0}[a/]\to a$	$T$	see 5.8
(RVar)	$\left(\text{S}\text{n}\right)[a/]\to \text{n}$	$N$	$\alpha \left[{\sigma }_1\right]\cdots \left[{\sigma }_w\right]\mapsto \left(\text{S}\alpha \right)[T/]\left[{\sigma }_1\right]\cdots \left[{\sigma }_w\right]$
(FVarLift)	$\text{0}\left[\Uparrow \left(s\right)\right]\to \text{0}$	0	$\text{0}\left[{\sigma }_1\right]\cdots \left[{\sigma }_w\right]\mapsto \text{0}[\Uparrow \left(S\right)]\left[{\sigma }_1\right]\cdots \left[{\sigma }_w\right]$
(RVarLift)	$\left(\text{S}\text{n}\right)\left[\Uparrow \left(s\right)\right]\to \text{n}\left[s\right][\uparrow ]$	$N\left[S\right][\uparrow ]$	$\alpha \left[\sigma \right][\uparrow ]\left[{\sigma }_1\right]\cdots \left[{\sigma }_w\right]\mapsto \left(\text{S}\alpha \right)[\Uparrow \left(\sigma \right)]\left[{\sigma }_1\right]\cdots \left[{\sigma }_w\right]$
(VarShift)	$\text{n}[\uparrow ]\to \text{S}\text{n}$	$\text{S}N$	$\left(\text{S}\alpha \right)\left[{\sigma }_1\right]\cdots \left[{\sigma }_w\right]\mapsto \alpha [\uparrow ]\left[{\sigma }_1\right]\cdots \left[{\sigma }_w\right]$

Equations

$$\begin{array}{rl}t& ::=\text{mbox}\text{text@underline}\mathsf{n}\text{leavevmode}|\text{leavevmode}‘lt\text{leavevmode}|\text{leavevmode}tt\text{leavevmode}|\text{leavevmode}t[s]\\ s& ::=t/\text{leavevmode}|\text{leavevmode}\Uparrow (s)\text{leavevmode}|\text{leavevmode}\uparrow \\ \text{mbox}\text{text@underline}\mathsf{n}& ::=\text{mbox}\text{text@underline}0\text{leavevmode}|\text{leavevmode}\text{mbox}\mathsf{S}\text{mbox}\text{text@underline}\mathsf{n}.\end{array}$$

$$(‘la)b$$

$$(ab)[s]$$

$$(‘la)[s]$$

$$\text{mbox}\text{text@underline}0[a/]$$

$$(\text{mbox}\mathsf{S}\text{mbox}\text{text@underline}\mathsf{n})[a/]$$

$$\text{mbox}\text{text@underline}0[\Uparrow (s)]$$

$$(\text{mbox}\mathsf{S}\text{mbox}\text{text@underline}\mathsf{n})[\Uparrow (s)]$$

$$\text{mbox}\text{text@underline}\mathsf{n}[\uparrow ]$$

$$\begin{array}{rl}\left(‘l‘l\text{mbox}\text{text@underline}0\text{mbox}\text{text@underline}1\right)K& \to \left(‘l\text{mbox}\text{text@underline}0\text{mbox}\text{text@underline}1\right)[K/]\to \left(‘l\left(\text{mbox}\text{text@underline}0\text{mbox}\text{text@underline}1\right)[\Uparrow (K/)]\right)\to ‘l\left(\text{mbox}\text{text@underline}0[\Uparrow (K/)]\right)\left(\text{mbox}\text{text@underline}1[\Uparrow (K/)]\right)\\ & \to ‘l\left(\text{mbox}\text{text@underline}0\left(\text{mbox}\text{text@underline}1[\Uparrow (K/)]\right)\right)\to ‘l\left(\text{mbox}\text{text@underline}0\left(\text{mbox}\text{text@underline}0[K/][\uparrow ]\right)\right)\to ‘l\left(\text{mbox}\text{text@underline}0\left(K[\uparrow ]\right)\right).\end{array}$$

$$\begin{array}{rl}K[\uparrow ]& =\left(‘l‘l\text{mbox}\text{text@underline}1\right)[\uparrow ]\to ‘l\left((‘l\text{mbox}\text{text@underline}1)[\Uparrow (\uparrow )]\right)\to ‘l‘l\left(\text{mbox}\text{text@underline}1[\Uparrow (\Uparrow (\uparrow ))]\right)\\ & \to ‘l‘l\left(\text{mbox}\text{text@underline}0[\Uparrow (\uparrow )][\uparrow ]\right)\to ‘l‘l\left(\text{mbox}\text{text@underline}0[\uparrow ]\right)\\ & \to ‘l‘l\text{mbox}\text{text@underline}1=K\end{array}$$

$$\begin{array}{rl}T& \to N\text{leavevmode}|\text{leavevmode}‘lT\text{leavevmode}|\text{leavevmode}TT\text{leavevmode}|\text{leavevmode}T[S]\\ S& \to T/\text{leavevmode}|\text{leavevmode}\Uparrow (S)\text{leavevmode}|\text{leavevmode}\uparrow \\ N& \to \text{mbox}\text{text@underline}0\text{leavevmode}|\text{leavevmode}\text{mbox}\mathsf{S}N.\end{array}$$

$$\begin{array}{rl}{G}_0& \to N\text{leavevmode}|\text{leavevmode}‘l{G}_0\text{leavevmode}|\text{leavevmode}{G}_0{G}_0\\ N& \to \text{mbox}\mathsf{S}N\text{leavevmode}|\text{leavevmode}\text{mbox}\text{text@underline}0.\end{array}$$

$${\mathcal{G}}_n=(G_n,{\mathcal{N}}_n,\mathcal{F},{\mathcal{P}}_n)$$

$$G_k\to ‘l{G}_k\text{leavevmode}|\text{leavevmode}{G}_0{G}_k\text{leavevmode}|\text{leavevmode}{G}_k{G}_0$$

$$\begin{array}{rl}{G}_k& \to ‘l{G}_k\text{leavevmode}|\text{leavevmode}{G}_0{G}_k\text{leavevmode}|\text{leavevmode}{G}_k{G}_0\\ T& \to ‘lT\text{leavevmode}|\text{leavevmode}TT\text{leavevmode}|\text{leavevmode}T[S]\end{array}$$

$$\begin{array}{rl}S& \to \text{leavevmode}\Uparrow (S)\\ N& \to \text{mbox}\mathsf{S}N\end{array}$$

$$\begin{array}{rl}{\text{fip}}_k(f(f(X)),f(X))& \to {\text{fip}}_k(f(X),X)\\ & \to {\text{fip}}_k(X,f(X))\\ & \to {\text{fip}}_k(f(f(X)),f(X))\\ & \to \cdots \end{array}$$

$${\delta }_1=\text{mbox}\text{text@underline}0[\Uparrow (\uparrow )]\text{whereas}{\delta }_{n+1}=\text{mbox}\text{text@underline}0[{\delta }_n/].$$

$${\Delta }_{\phi }(\gamma [{\sigma }_1]\cdots [{\sigma }_w])=\Pi (\gamma [{\sigma }_1]\cdots [{\sigma }_w],\chi [{\tau }_1]\cdots [{\tau }_d]\underset{w-d\text{ times}}{\underbrace{[S]\cdots [S]}})$$

$${\Delta }_{\phi }^n=\bigcup \{{\Delta }_{\phi }(\gamma )\text{leavevmode}|\text{leavevmode}{G}_n\to \gamma \in {\mathcal{G}}_n\}.$$

$$G_n\to ‘l{G}_n\text{leavevmode}|\text{leavevmode}{G}_0{G}_n\text{leavevmode}|\text{leavevmode}{G}_n{G}_0.$$

$$\begin{array}{rl}{G}_1& \to ‘l{G}_1\text{leavevmode}|\text{leavevmode}{G}_0{G}_1\text{leavevmode}|\text{leavevmode}{G}_1{G}_0\\ & |\text{leavevmode}\text{mbox}\text{text@underline}0[(G_0{G}_0)/]\text{leavevmode}|\text{leavevmode}\text{mbox}\text{text@underline}0[‘l{G}_0/]\text{leavevmode}|\text{leavevmode}\text{mbox}\text{text@underline}0[N/]\\ & |\text{leavevmode}(\text{mbox}\mathsf{S}N)[T/]\text{leavevmode}|\text{leavevmode}\text{mbox}\text{text@underline}0[\Uparrow (S)]\text{leavevmode}|\text{leavevmode}N[\uparrow ].\end{array}$$

$$[z^n]f(z)\underset{n\to \infty }{\to }{\zeta }^{-n}\frac{n^{-3/2}g(\zeta )}{\Gamma (-\frac{1}{2})}.$$

$$|\text{mbox}\text{text@underline}\mathsf{n}|$$

$$|‘la|$$

$$|ab|$$

$$|a[s]|$$

$$|a/|$$

$$|\Uparrow (s)|$$

$$|\uparrow |$$

$$L_{\infty }(z)=\frac{1-z-\sqrt{\frac{1-3z-z^2-z^3}{1-z}}}{2z}.$$

$$T(z)=\frac{1-\sqrt{1-4z}}{2z}-1,S(z)=\frac{1-\sqrt{1-4z}}{2z}\left(\frac{z}{1-z}\right)\text{and}N(z)=\frac{z}{1-z}.$$

$$G_k(z)=\frac{1}{1-z-2z{L}_{\infty }(z)}\sum _{G_k\to \gamma \in {\Phi }_k}{G}_{\gamma }(z)$$

$$G_{\gamma }(z)=z^{\zeta (\gamma )}{T(z)}^{\tau (\gamma )}{S(z)}^{\sigma (\gamma )}{N(z)}^{\nu (\gamma )}\prod _{0\le i<k}{G_i(z)}^{{\rho }_i(\gamma )}$$

$$G_k(z)=z{G}_k(z)+2z{G}_0(z)G_k(z)+\sum _{G_k\to \gamma \in {\Phi }_k}{G}_{\gamma }(z).$$

Full text

In the current paper we propose a somewhat indirect average-case analysis of substitution resolution in the classic $`l$-calculus, based on the quantitative analysis of substitution in $`l`y$, an extension of $`l$-calculus internalising the $`y$-calculus of explicit substitutions. Within this framework, we show that for any fixed $n\geq 0$, the probability that a uniformly random, conditioned on size, $`l`y$-term $`y$-normalises in $n$ normal-order (i.e. leftmost-outermost) reduction steps tends to a computable limit as the term size tends to infinity.

For that purpose, we establish an effective hierarchy $\left(\mathscr{G}_{n}\right)_{n}$ of regular tree grammars partitioning $`y$-normalisable terms into classes of terms normalising in $n$ normal-order rewriting steps. The main technical ingredient in our construction is an inductive approach to the construction of $\mathscr{G}_{n+1}$ out of $\mathscr{G}_{n}$ based, in turn, on the algorithmic construction of finite intersection partitions, inspired by Robinson’s unification algorithm.

Finally, we briefly discuss applications of our approach to other term rewriting systems, focusing on two closely related formalisms, i.e. the full $`l`y$-calculus and combinatory logic.

1. Introduction

Traditional, machine-based computational models, such as Turing machines or RAMs, admit a natural notion of an atomic computation step, closely reflecting the actual operational cost of executing the represented computations. Unfortunately, this is not quite the case for computational models based on term rewriting systems with substitution, such as the classic $`l$-calculus. Given the (traditionally) epitheoretic nature of substitution, the single rewriting rule of $`b$-reduction $(`lx.a)b\to_{\beta}a[x:=b]$ masks a non-trivial computation of resolving (i.e. executing) the pending substitution of $b$ for occurrences of $x$ in $a$. Moreover, unlike machine-based models, $`l$-calculus (as other term rewriting systems) does not impose a strict, deterministic evaluation mechanism. Consequently, various strategies for resolving substitutions can be used, even more obfuscating the operational semantics of $`b$-reduction and hence also its operational cost. Those subtle nuances hidden behind the implementation details of substitution resolution are in fact one of the core issues in establishing reasonable cost models for the classic $`l$-calculus, relating it with other, machine-based computational models, see [14].

In order to resolve this apparent inadequacy, Abadi et al. proposed to refine substitution in the classic $`l$-calculus and decompose it into a series of atomic rewriting steps, internalising in effect the calculus of executing substitutions [1]. Substitutions become first-class citizens and, in effect, can be manipulated together with regular terms. Consequently, the general framework of explicit substitutions provides a machine-independent setup for the operational semantics of substitution, based on a finite set of unit rewriting primitives. Remarkably, with the help of linear substitution calculus (a resource aware calculus of explicit substitutions) Accattoli and dal Lago showed recently that the leftmost-outermost $`b$-reduction strategy is a reasonable invariant cost model for $`l$-calculus, and hence it is able to simulate RAMs (or equivalent, machine-based models) within a polynomial time overhead [2].

Various subtleties of substitution resolution, reflected in the variety of available calculi of explicit substitutions, induce different operational semantics for executing substitutions in $`l$-calculus. This abundance of approaches is perhaps the main barrier in establishing a systematic, quantitative analysis of the operational complexity of substitution resolution and, among other things, a term rewriting analogue of classic average-case complexity analysis. In the current paper we propose a step towards filling this gap by offering a quantitative approach to substitution resolution in Lescanne’s $`l`y$-calculus of explicit substitutions [15]. In particular, we focus on the following, average-case analysis type of question. Having fixed arbitrary non-negative $n$, what is the probability that a (uniformly) random $`l`y$-term of given size is $`y$-normalisable (i.e. can be reduced to a normal form without explicit substitutions) in exactly $n$ leftmost-outermost reduction steps? Furthermore, how does this probability distribution change with the term size tending to infinity?

We address the above questions using a two-step approach. First, we exhibit an effective (i.e. computable) hierarchy $\left(\mathscr{G}_{n}\right)_{n}$ of unambiguous regular tree grammars with the property that $\mathscr{G}_{n}$ describes the language of terms $`y$-normalising in precisely $n$ leftmost-outermost $`y$-rewriting steps. Next, borrowing techniques from analytic combinatorics, we analyse the limit proportion of terms $`y$-normalising in $n$ normal-order steps. To that end, we construct appropriate generating functions and provide asymptotic estimates for the number of $`l`y$-terms $`y$-normalising in $n$ normal-order reduction steps. As a result, we base our approach on a direct quantitative analysis of the $`y$ term rewriting system, measuring the operational cost of evaluating substitution in terms of the number of leftmost-outermost rewriting steps required to reach a ($`y$-)normal form.

The paper is structured as follows. In Section 2 we outline $`l`y$-calculus and the framework of regular tree grammars, establishing the necessary terminology for the reminder of the paper. Next, in Section 3, we prepare the background for the construction of $\left(\mathscr{G}_{n}\right)_{n}$. In particular, we sketch its general, intuitive scheme. In Section 4 we introduce the main tool of finite intersection partitions and show that it is indeed constructible in the context of generated reduction grammars. Afterwards, in Section 5, we show how finite intersection partitions can be used in the construction of new productions in $\mathscr{G}_{n+1}$ based on productions in the grammar $\mathscr{G}_{n}$. Having constructed $\left(\mathscr{G}_{n}\right)_{n}$ we then proceed to the main quantitative analysis of $`y$-calculus using methods of analytic combinatorics, see Section 6. Finally, in Section 7 we discuss broader applications of our technique to other term rewriting systems, based on the examples of $`l`y$-calculus and combinatory logic, and conclude the paper in the final Section 8.

2. Preliminaries

2.1. Lambda upsilon calculus

$`l`y$ (lambda upsilon) is a simple, first-order term rewriting system extending the classic $`l$-calculus based on de Bruijn indices [11] with the calculus of resolving pending substitutions [15, 16]. Its formal terms, so-called $`l`y$-terms, are comprised of de Bruijn indices n, application, abstraction, together with an additional, explicit closure operator $[\cdot]$ standing for unresolved substitutions. De Bruijn indices are represented in unary base expansion. In other words, n is encoded as an $n$-fold application of the successor operator $\operatorname*{\mbox{\sf S}}$ to zero 0. Substitutions, in turn, consist of three primitives, i.e. a constant shift $\uparrow$, a unary lift operator $\Uparrow$, mapping substitutions onto substitutions, and a unary slash operator $/$, mapping terms onto substitutions. Terms containing closures are called impure whereas terms without them are said to be pure. Figure 1 summarises the formal specification of $`l`y$-terms and the corresponding rewriting system $`l`y$.

Example 2.1**.**

Note that the well-known combinator $K=`lxy.x$ is represented in the de Bruijn notation as $`l`l\mbox{\text@underline{\sf 1}}$. The reverse application term $`lxy.yx$, on the other hand, is represented as $`l`l\mbox{\text@underline{\sf 0}}\mbox{\text@underline{\sf 1}}$. Consequently, in a single $`b$-reduction step, it holds $\left(`l`l\mbox{\text@underline{\sf 0}}\mbox{\text@underline{\sf 1}}\right)K\to_{\beta}`l\left(\mbox{\text@underline{\sf 0}}K\right)$.

In $`l`y$, however, this single $`b$-reduction is decomposed into a series of small rewriting steps governing both the $`b$-reduction as well as the subsequent substitution resolution. For instance, we have

[TABLE]

Furthermore,

[TABLE]

hence indeed $\left(`l`l\mbox{\text@underline{\sf 0}}\mbox{\text@underline{\sf 1}}\right)K$ rewrites to $`l\left(\mbox{\text@underline{\sf 0}}K\right)$.

Let us notice that in the presence of the erasing (RVar) and duplicating (App) rewriting rules, not all reduction sequences starting with the same term have to be of equal length. Like in the classic $`l$-calculus, depending on the considered term, some rewriting strategies might be more efficient then others.

$`l`y$ enjoys a series of pleasing properties. Most notably, $`l`y$ is confluent, correctly implements $`b$-reduction of the classic $`l$-calculus, and preserves strong normalisation of closed terms [3]. Moreover, the $`y$ fragment, i.e. $`l`y$ without the (Beta) rule, is terminating. In other words, each $`l`y$-term is $`y$-normalising as can be shown using, for instance, polynomial interpretations [9]. In the current paper we focus on the normal-order (i.e. leftmost-outermost) evaluation strategy of $`y$-reduction. For convenience, we assume the following notational conventions. We use lowercase letters $a,b,c,\ldots$ to denote arbitrary terms and $s$ (with or without subscripts) to denote substitutions. Moreover, we write $a\downarrow_{n}$ to denote the fact that $a$ normalises to its $`y$-normal form in $n$ normal-order $`y$-reduction steps. Sometimes, for further convenience, we also simply state that $t$ normalises in $n$ steps, without specifying the assumed evaluation strategy nor the specific rewriting steps and normal form.

2.2. Regular tree languages

We base our main construction in the framework of regular tree languages. In what follows, we outline their basic characteristics and that of corresponding regular tree grammars, introducing necessary terminology. We refer the curious reader to [10, Chapter II] for a more detailed exposition.

Definition 2.2** (Ranked alphabet).**

A ranked alphabet $\mathscr{F}$ is a finite set of function symbols endowed with a corresponding arity function $\operatorname*{\mbox{\sf arity}}\colon\mathscr{F}\to\mathbb{N}$. We use $\mathscr{F}_{n}$ to denote the set of function symbols of arity $n$, i.e. function symbols $f\in\mathscr{F}$ such that $\operatorname*{\mbox{\sf arity}}(f)=n$. Function symbols of arity zero are called constants. As a notational convention, we use lowercase letters $f,g,h,\ldots$ to denote arbitrary function symbols.

Definition 2.3** (Terms).**

Let $X$ be a finite set of variables. Then, the set $\mathscr{T}_{\mathscr{F}}(X)$ of terms over $\mathscr{F}$ is defined inductively as follows:

1. (1)

$X,\mathscr{F}_{0}\subset\mathscr{T}_{\mathscr{F}}(X)$; 2. (2)

If $f\in\mathscr{F}_{n}$ and $\alpha_{1},\ldots,\alpha_{n}\in\mathscr{T}_{\mathscr{F}}(X)$, then $f(\alpha_{1},\ldots,\alpha_{n})\in\mathscr{T}_{\mathscr{F}}(X)$.

Terms not containing variables, in other words elements of $\mathscr{T}_{\mathscr{F}}(\varnothing)$, are called ground terms.

As a notational convention, we use lowercase Greek letters $\alpha,\beta,\gamma,\ldots$ to denote arbitrary terms. Whenever it is clear from the context, we use the word term both to refer to the above structures as as well as to denote $`l`y$-terms.

Definition 2.4** (Regular tree grammars).**

A regular tree grammar $\mathscr{G}=(S,\mathscr{N},\mathscr{F},\mathscr{P})$ is a tuple consisting of:

1. (1)

an axiom $S\in\mathscr{N}$; 2. (2)

a finite set $\mathscr{N}$ of non-terminal symbols; 3. (3)

a ranked alphabet $\mathscr{F}$ of terminal symbols such that $\mathscr{F}\cap\mathscr{N}=\varnothing$; and 4. (4)

a finite set $\mathscr{P}$ of productions in form of $N\to\alpha$ such that $N\in\mathscr{N}$ and $\alpha\in\mathscr{T}_{\mathscr{F}}(\mathscr{N})$.

A production $N\to\alpha$ is self-referencing if $N$ occurs in $\alpha$. Otherwise, if $N$ does not occur in $\alpha$, we say that $n\to\alpha$ is regular. As a notational convention, we use capital letters $X,Y,Z\ldots$ to denote arbitrary non-terminal symbols.

Definition 2.5** (Derivation relation).**

The derivation relation $\to_{\mathscr{G}}$ associated with the grammar $\mathscr{G}=(S,\mathscr{N},\mathscr{F},\mathscr{P})$ is a relation on pairs of terms in $\mathscr{T}_{\mathscr{F}}(\mathscr{N})$ satisfying $\alpha\to_{\mathscr{G}}\beta$ iff there exists a production $N\to\gamma$ in $\mathscr{P}$ such that after substituting $\gamma$ for some occurrence of $N$ in $\alpha$ we obtain $\beta$. Following standard notational conventions, we use $\xrightarrow[]{*}_{\mathscr{G}}$ to denote the transitive closure of $\to_{\mathscr{G}}$. Moreover, if $\mathscr{G}$ is clear from the context, we omit it in the subscript of the derivation relations and simply write $\to$ and $\xrightarrow[]{*}$.

A regular tree grammar $\mathscr{G}$ with axiom $S$ is said to be unambiguous iff for each ground term $\alpha\in\mathscr{T}_{\mathscr{F}}(\varnothing)$ there exist at most one derivation sequence in form of $S\to\gamma_{1}\to\cdots\to\gamma_{n}=\alpha$. Likewise, $N$ is said to be unambiguous in $\mathscr{G}$ iff for each ground term $\alpha\in\mathscr{T}_{\mathscr{F}}(\varnothing)$ there exist at most one derivation sequence in form of $N\to\gamma_{1}\to\cdots\to\gamma_{n}=\alpha$.

Definition 2.6** (Regular tree languages).**

The language $L(\mathscr{G})$ generated by $\mathscr{G}$ is the set of all ground terms $\alpha$ such that $S\xrightarrow[]{*}\alpha$ where $S$ is the axiom of $\mathscr{G}$. Similarly, the language generated by term $\alpha\in\mathscr{T}_{\mathscr{F}}(\mathscr{N})$ in $\mathscr{G}$, denoted as $L_{\mathscr{G}}(\alpha)$, is the set of of all ground terms $\beta$ such that $\alpha\xrightarrow[]{*}\beta$. Finally, a set $\mathscr{L}$ of ground terms over a ranked alphabet $\mathscr{F}$ is said to be a regular tree language if there exists a regular tree grammar $\mathscr{G}$ such that $L(\mathscr{G})=\mathscr{L}$.

Example 2.7**.**

The set of $`l`y$-terms is an example of a regular tree language. The corresponding regular tree grammar $\Lambda=(T,\mathscr{N},\mathscr{F},\mathscr{P})$ consists of

• •

a set $\mathscr{N}$ of three non-terminal symbols $T$, $S$, $N$ intended to stand for $`l`y$-terms, substitutions, and de Bruijn indices, respectively, with $T$ being the axiom of $\Lambda$;

• •

a set $\mathscr{F}$ of terminal symbols, comprised of all the symbols of the $`l`y$-calculus language, i.e. term application and abstraction, closure $\cdot[\cdot]$, slash $\cdot/$, lift $\Uparrow(\cdot)$ and shift $\uparrow$ operators, and the successor $\operatorname*{\mbox{\sf S}}(\cdot)$ with the constant 0; and

• •

a set $\mathscr{P}$ of productions

[TABLE]

Let us notice that (4) consists of five self-referencing productions, three for $T$ and one for each $S$ and $N$. Moreover, $L(N)\subset L(T)$ as $\mathscr{P}$ includes a production $T\to N$.

3. Reduction grammars

We conduct our construction of $\left(\mathscr{G}_{n}\right)_{n}$ in an inductive, incremental fashion. Starting with $\mathscr{G}_{0}$ corresponding to the set of pure terms (i.e. $`l`y$-terms without closures) we build the $(n+1)$st grammar $\mathscr{G}_{n+1}$ based on the structure of the $n$th grammar $\mathscr{G}_{n}$. First-order rewriting rules of $`l`y$-calculus guarantee a close structural resemblance of both their left- and right-hand sides, see 1(b). Consequently, with $\mathscr{G}_{n}$ at hand, we can analyse the right-hand sides of $`y$ rewriting rules and match them with productions of $\mathscr{G}_{n}$. Based on their structure, we then determine the structure of productions of $\mathscr{G}_{n+1}$ which correspond to respective left-hand sides. Although such a general idea of constructing $\mathscr{G}_{n+1}$ out of $\mathscr{G}_{n}$ is quite straightforward, its implementation requires some careful amount of detail.

For that reason, we make the following initial preparations. Each grammar $\mathscr{G}_{n}$ uses the same, global, ranked alphabet $\mathscr{F}$ corresponding to $`l`y$-calculus, see 2.7. The standard non-terminal symbols $T,S$, and $N$, together with their respective productions (4), are pre-defined in each grammar $\mathscr{G}_{n}$. In addition, $\mathscr{G}_{n}$ includes $n+1$ non-terminal symbols $G_{0},\ldots,G_{n}$ (the final one being the axiom of $\mathscr{G}_{n}$) with the intended meaning that for all $0\leq k\leq n$, the language $L_{\mathscr{G}_{k}}(G_{n})$ is equal to the set of terms $`y$-normalising in $k$ normal-order steps. In this manner, building $\left(\mathscr{G}_{n}\right)_{n}$ amounts to a careful, incremental extension process, starting with the initial grammar $\mathscr{G}_{0}$ comprised of the following extra, i.e. not included in (4), productions:

[TABLE]

In order to formalise the above preparations and the overall presentation of our construction, we introduce the following, abstract notions of $`y$-reduction grammar and later also their simple variants.

Definition 3.1** ($`y$-reduction grammars).**

Let $\Lambda=(T,\mathscr{N},\mathscr{F},\mathscr{P})$ be the regular tree grammar corresponding to $`l`y$-terms, see 2.7. Then, the regular tree grammar

[TABLE]

with

• •

$\mathscr{N}_{n}=\mathscr{N}\cup\{G_{0},G_{1},\ldots,G_{n}\}$; and

• •

$\mathscr{P}_{n}$ being a set of productions such that $\mathscr{P}\subset\mathscr{P}_{n}$

is said to be a $`y$-reduction grammar, $`y$-RG in short, if for all $0\leq k\leq n$, the non-terminal $G_{k}$ is unambiguous in $\mathscr{G}_{n}$, and moreover $L(G_{k})$ is equal to the set of $`l`y$-terms $`y$-normalising in $k$ normal-order $`y$-steps.

Definition 3.2** (Partial order of sorts).**

The partial order of sorts $(\mathscr{N}_{n},\preceq)$ is a partial order (i.e. reflexive, transitive, and anti-symmetric relation) on non-terminal symbols $\mathscr{N}_{n}$ satisfying $X\preceq Y$ if and only if $L_{\mathscr{G}_{n}}(X)\subseteq L_{\mathscr{G}_{n}}(Y)$. For convenience, we write $X\varcurlywedge Y$ to denote the greatest lower bound of $\{X,Y\}$. Figure 2 depicts the partial order $(\mathscr{N}_{n},\preceq)$.

Remark 3.3**.**

Let us notice that given the interpretation of $L(G_{0}),\ldots,L(G_{n})$, the partial order of sorts $(\mathscr{N}_{n},\preceq)$ captures all the inclusions among the non-terminal languages within $\mathscr{G}_{n}$. However, in addition, if $X$ and $Y$ are not comparable through $\preceq$, then $L(X)\cap L(Y)=\varnothing$ as each term $`y$-normalises in a unique, determined number of steps.

Definition 3.4** (Simple $`y$-reduction grammars).**

A $`y$-RG $\mathscr{G}_{n}$ is said to be simple if all its self-referencing productions are either productions of the regular tree grammar corresponding to $`l`y$-terms, see 2.7, or are of the form

[TABLE]

and moreover, for all regular productions in form of $G_{k}\to\alpha$ in $\mathscr{G}_{n}$, it holds $\alpha\in\mathscr{T}_{\mathscr{F}}(\mathscr{N}\cup\{G_{0},\ldots,G_{k-1}\})$, i.e. $\alpha$ does not reference non-terminals other than $G_{0},\ldots,G_{k-1}$.

Remark 3.5**.**

Let us note that, in general, $`y$-reduction grammars do not have to be simple. Due to the erasing (RVar) rewriting rule, it is possible to construct, inter alia, more involved self-referencing productions. Nonetheless, for technical convenience, we will maintain the simplicity of constructed grammars $\left(\mathscr{G}_{n}\right)_{n}$.

Also, let us remark that the above definition of simple $`y$-reduction grammars asserts that if $\mathscr{G}_{n+1}$ is a simple $`y$-RG, then, by a suitable truncation, it is possible to obtain all the $`y$-reduction grammars $\mathscr{G}_{0}$ up to $\mathscr{G}_{n}$. Consequently, $\mathscr{G}_{n+1}$ contains, in a proper sense, all the proceeding grammars $\mathscr{G}_{0},\ldots,\mathscr{G}_{n}$.

4. Finite intersection

partitions

The main technical ingredient in our construction of $\left(\mathscr{G}_{n}\right)_{n}$ are finite intersection partitions.

Definition 4.1** (Finite intersection partition).**

Let $\alpha,\beta$ be two terms in $\mathscr{T}_{\mathscr{F}}(X)$. Then, a finite intersection partition, FIP in short, of $\alpha$ and $\beta$ is a finite set $\Pi(\alpha,\beta)=\{\pi_{1},\ldots,\pi_{n}\}\subset\mathscr{T}_{\mathscr{F}}(X)$ such that $L(\pi_{i})\cap L(\pi_{j})=\varnothing$ whenever $i\neq j$, and $\bigcup_{i}L(\pi_{i})=L(\alpha)\cap L(\beta)$.

Let us note that, a priori, it is not immediately clear if $\Pi(\alpha,\beta)$ exists for $\alpha$ and $\beta$ in the term algebra $\mathscr{T}(\mathscr{N}_{n})$ associated with the simple $`y$-RG $\mathscr{G}_{n}$ nor whether there exists an algorithmic method of its construction. The following result states that both questions can be settled in the affirmative.

Lemma 4.2** (Constructible finite intersection partitions).**

Assume that $\mathscr{G}_{n}$ is a simple $`y$-reduction grammar. Let $\alpha,\beta$ be two (not necessarily ground) terms in $\mathscr{T}(\mathscr{N}_{n})$ where $\mathscr{N}_{n}$ is the set of non-terminal symbols of $\mathscr{G}_{n}$. Then, $\alpha$ and $\beta$ have a computable finite intersection partition $\Pi(\alpha,\beta)$.

In order to prove 4.2, we resort to the following technical notion of term potential used to embed terms into the well-founded set of natural numbers.

Definition 4.3** (Term potential).**

Let $\alpha\in\mathscr{T}(\mathscr{N}_{n})$ be a term and $\mathscr{G}_{n}$ be a simple $`y$-RG. Let ${\sf Prod}_{\mathscr{G}_{n}}(X)$ denote the set consisting of right-hand sides of regular productions in form of $X\to\beta$ in $\mathscr{G}_{n}$. Then, the potential $\pi(\alpha)$ of $\alpha$ in $\mathscr{G}_{n}$ is defined inductively as follows:

• •

If $\alpha=f(\alpha_{1},\ldots,\alpha_{m})$, then $\pi(\alpha)=1+\displaystyle\sum_{i=1}^{m}\pi(\alpha_{i})$;

• •

If $\alpha=X\in\{T,S,N\}$, then $\pi(\alpha)=1+\displaystyle\max\{\pi(\gamma)\leavevmode\nobreak\ |\leavevmode\nobreak\ \gamma\in{\sf Prod}_{\mathscr{G}_{n}}(X)\}$;

• •

If $\alpha=G_{k}$ for some $0\leq k\leq n$, then $\pi(\alpha)=1+\displaystyle\max\{\pi(\gamma)\leavevmode\nobreak\ |\leavevmode\nobreak\ \gamma\in\bigcup_{i=0}^{k}{\sf Prod}_{\mathscr{G}_{n}}(G_{i})\}$.

Let us note that $\pi$ is well-defined as, by assumption, ${\sf Prod}_{\mathscr{G}_{n}}(X)\neq\varnothing$ for all simple $`y$-reduction grammars $\mathscr{G}_{n}$; otherwise $L(G_{k})$ could not span the whole set of $`l`y$-terms $`y$-normalising in $k$ normal-order steps. Moreover, $\pi$ has the following crucial properties:

• •

For each term $\alpha$ we have $\pi(\alpha)\geq 1$;

• •

If $\alpha$ is a proper subterm of $\beta$, then $\pi(\alpha)<\pi(\beta)$;

• •

If $X\to\alpha$ is a regular production, then $\pi(\alpha)<\pi(X)$; and

• •

For each $G_{i}$ and $G_{j}$, it holds $\pi(G_{i})\leq\pi(G_{j})$ whenever $i\leq j$.

Example 4.4**.**

Note that the term potential of $N$ associated with de Bruijn indices is equal to ${\pi(N)=2}$ as $\pi(\mbox{\text@underline{\sf 0}})=1$. Since $T\to N$ is the single regular production starting with $T$ on its left-hand side, the potential $\pi(T)$ is therefore equal to $3$. Consequently, we also have $\pi(S)=5$ as witnessed by the regular production $S\to T/$. Finally, since $\pi(N)=2$ it holds $\pi(G_{0})=3$ and so, for instance, we also have $\pi(G_{0}G_{0})=7$.

Productions of a simple $\mathscr{G}_{n}$ cannot reference non-terminals other than $G_{0},\ldots,G_{n}$. Since the potential of $G_{k+1}$ is defined in terms of the potential of its regular productions, this means that $\pi(G_{k+1})$ depends, in an implicit manner, on the potentials $\pi(G_{0}),\ldots,\pi(G_{k})$. Note that this constitutes a traditional inductive definition. In order to compute the potential of a given term $\alpha$, we start with computing the potential of associated non-terminals. In particular, we find the values $\pi(G_{0}),\ldots,\pi(G_{n})$ in ascending order. Afterwards, we can recursively decompose $\alpha$ and calculate its potential based on the potential of non-terminal symbols occurring in $\alpha$. Note that the same scheme holds, in particular, for the right-hand sides of self-referencing productions.

Definition 4.5** (Conservative productions).**

A self-referencing production $X\to f(\alpha_{1},\ldots,\alpha_{n})$ is said to be conservative if $\pi(\alpha_{i})\leq\pi(X)$ for all $1\leq i\leq n$.

Remark 4.6**.**

Conservative productions play a central role in the algorithmic cosntruction of finite intersection partitions $\Pi(\alpha,\beta)$. In particular, let us remark that all self-referencing productions of a simple $`y$-RG $\mathscr{G}_{n}$, as listed in Figure 3, are at the same time conservative.

With the technical notions of term potential and conservative productions, we are ready to present a recursive procedure $\texttt{fip}_{k}$ constructing $\Pi(\alpha,\beta)$ for arbitrary terms $\alpha,\beta$ within the scope of a simple $`y$-RG $\mathscr{G}_{k}$. Figure 4 provides the functional pseudocode describing $\texttt{fip}_{k}$.

Proof.

(of 4.2) Induction over the total potential of $\alpha$ and $\beta$.

Let us start with the base case $\pi(\alpha)+\pi(\beta)=2$. Note that both $\alpha$ and $\beta$ have to be constant ground terms (the potential of non-terminals in $\mathscr{N}_{k}$ is at least $2$). If $\alpha\neq\beta$, then certainly $L(\alpha)\cap L(\beta)=\varnothing$ and so $\Pi(\alpha,\beta)=\varnothing$, see Line 4. Otherwise if $\alpha=\beta$, then both $L(\alpha)\cap L(\beta)=\Pi(\alpha,\beta)=\{\alpha\}=\{\beta\}$; hence, $\texttt{fip}_{k}$ returns a correct intersection partition $\Pi(\alpha,\beta)$, see Line 4. And so, assume that $\pi(\alpha)+\pi(\beta)>2$. Depending on the joint structure of both $\alpha$ and $\beta$ we have to consider three cases.

Case 1.

Suppose that $\alpha=f(\alpha_{1},\ldots,\alpha_{n})$ and $\beta=g(\beta_{1},\ldots,\beta_{m})$ for some function symbols $f$ and $g$ with $n,m\geq 0$. Certainly, if either $f\neq g$ or $n\neq m$, then $L(\alpha)\cap L(\beta)=\varnothing$. In consequence, $\varnothing$ is the sole valid FIP of both $\alpha$ and $\beta$, see Line 4.

So, let us assume that both $f=g$ and $n=m$. Moreover, we can also assume that $n,m\geq 1$ as the trivial case $n=m=0$ cannot occur under the working assumption $\pi(\alpha)+\pi(\beta)>2$. Take an arbitrary $\delta\in L(\alpha)\cap L(\beta)$. Note that $\delta$ takes the form of $\delta=f(\delta_{1},\ldots,\delta_{n})$ for some ground terms $\delta_{1},\ldots,\delta_{n}$. By induction, for all $1\leq i\leq n$, the recursive call $\texttt{fip}_{k}\,\alpha_{i}\,\beta_{i}$ yields a finite intersection partition $\Pi(\alpha_{i},\beta_{i})$ of $\alpha_{i}$ and $\beta_{i}$. Since $\delta_{i}\in L(\alpha_{i})\cap L(\beta_{i})$ there exists a unique $\pi_{i}\in\Pi(\alpha_{i},\beta_{i})$ such that $\delta_{i}\in L(\pi_{i})$. Accordingly, for $\delta=f(\delta_{1},\ldots,\delta_{n})$ there exists a unique term $\pi=f(\pi_{1},\ldots,\pi_{n})$ in $\texttt{fip}_{k}\,\alpha\,\beta$ such that $\delta\in L(\pi)$.

Conversely, take an arbitrary ground term $\delta=f(\delta_{1},\ldots,\delta_{n})\in L(\pi)$ for some $\pi\in\texttt{fip}_{k}\,\alpha\,\beta$. Note that $\pi$ takes the form $\pi=f(\pi_{1},\ldots,\pi_{n})$, see Line 4. Since $\delta\in L(\pi)$, we know that $\delta_{i}\in L(\pi_{i})$, for each $1\leq i\leq n$. Moreover, $\pi_{i}\in\Pi_{i}$ by the construction of $\texttt{fip}_{k}\,\alpha\,\beta$, see Line 4. Following the inductive hypothesis that $\Pi_{i}$ is a FIP of $\alpha_{i}$ and $\beta_{i}$, we notice that $L(\pi_{i})\subseteq L(\alpha_{i})\cap L(\beta_{i})$. Consequently, $\delta_{i}\in L(\alpha_{i})\cap L(\beta_{i})$ and so $\delta\in L(\alpha)\cap L(\beta)$.

Case 2.

Suppose that $\alpha=X$ and $\beta=Y$ are two non-terminal symbols in $\mathscr{N}_{k}$, see Line 4. Let us consider the sort poset $(\mathscr{N}_{k},\preceq)$ associated with $\mathscr{G}_{k}$. Assume that $X$ and $Y$ are comparable through $\preceq$ (w.l.o.g. let $X\preceq Y$). Consequently, $L(X)\subseteq L(Y)$ and so $X\varcurlywedge Y=X$. Clearly, $\{X\}$ is a valid FIP, see Line 4. On the other hand, if $X$ and $Y$ are incomparable in the sort poset associated with $\mathscr{G}_{k}$, it means that $L(X)\cap L(Y)=\varnothing$ and so $\Pi(\alpha,\beta)=\varnothing$, see 3.3.

Case 3.

Suppose w.l.o.g that $\alpha=X$ and $\beta$ takes the form $\beta=f(\beta_{1},\ldots,\beta_{n})$ with $n\geq 0$. Note that $\texttt{fip}_{k}$ flips its arguments if necessary, see Line 4. Take an arbitrary $\delta\in L(\alpha)\cap L(\beta)$. Note that from the form of $\beta$ we know that $\delta=f(\delta_{1},\ldots,\delta_{n})$ for some ground terms $\delta_{1},\ldots,\delta_{n}$ ($n\geq 0$). Since $\alpha=X$ is a non-terminal symbol which, by assumption, is unambiguous in $\mathscr{G}_{k}$, there exists a unique production $X\to\gamma$ such that $\delta\in L(\gamma)$.

If $X\to\gamma$ is regular (i.e. $X$ does not occur in $\gamma$), then $\pi(\gamma)<\pi(X)$ and so $\pi(\gamma)+\pi(\beta)<\pi(X)+\pi(\beta)$. Hence, by induction, $\texttt{fip}_{k}\,\gamma\,\beta$ constructs a finite intersection partition $\Pi(\gamma,\beta)$ with a unique $\pi\in\Pi(\gamma,\beta)\subset\Pi(X,\beta)$ such that $\delta\in L(\pi)$, see Line 4.

Let us therefore assume that $X\to\gamma$ is not regular, but instead self-referencing (i.e. $X$ occurs in $\gamma$). In such a case $\pi(X)\leq\pi(\gamma)$ and so we cannot directly apply the induction hypothesis to $\texttt{fip}_{k}\,\gamma\,\beta$. Note however, that since $\delta\in L(\gamma)\cap L(\beta)$ and $\gamma\neq X$, the term $\gamma$ must be of form $\gamma=f(\gamma_{1},\ldots,\gamma_{n})$ as otherwise $\delta\not\in L(\gamma)$. Furthermore if $n=0$, then trivially $\gamma=\beta=f$, see Line 4. Hence, let us assume that $n\geq 1$. It follows that $\texttt{fip}_{k}$ proceeds to construct finite intersection partitions for respective pairs of arguments $\gamma_{i}$ and $\beta_{i}$. However, since $X\to f(\gamma_{1},\ldots,\gamma_{n})$ is conservative (see 4.6), it holds $\pi(\gamma_{i})\leq\pi(X)$. At the same time, $\pi(\beta_{i})<\pi(\beta)$; hence, by induction we can argue that $\texttt{fip}_{k}\,\gamma_{i}\,\beta_{i}$ constructs a proper intersection partition $\Pi(\gamma_{i},\beta_{i})$ for each $1\leq i\leq n$, see Line 4. There exists therefore a unique term $\pi=f(\pi_{1},\ldots,\pi_{n})\in\texttt{fip}_{k}\,X\,\beta$ such that $\delta\in L(\pi)$, see Line 4 and Line 4.

Conversely, take an arbitrary ground term $\delta=f(\delta_{1},\ldots,\delta_{n})\in L(\pi)$ for some $\pi\in\texttt{fip}_{k}\,X\,\beta$ $(n\geq 0)$. By definition, $\texttt{fip}_{k}$ proceeds to invoke itself on pairs of arguments $\gamma$ and $\beta$ where $\gamma$ is the right-hand side of a production $X\to\gamma$ in $\mathscr{G}_{k}$, see Line 4, and returns the set-theoretic union of recursively obtained outcomes. There exists therefore some $\gamma$ such that $\pi\in\texttt{fip}_{k}\,\gamma\,\beta$. If $X\to\gamma$ is regular, then by induction, $\texttt{fip}_{k}\,\gamma\,\beta$ constructs a FIP for both $\gamma$ and $\beta$. Consequently, it holds $\delta\in L(\pi)\subset L(\gamma)\cap L(\beta)\subset L(X)\cap L(\beta)$. Assume therefore that $X\to\gamma$ is not regular, but instead self-referencing. As before, we cannot directly argue about $\texttt{fip}_{k}\,\gamma\,\beta$ since the total potential of $\gamma$ and $\beta$ exceeds the potential of $X$ and $\beta$. However, since $\pi\in\texttt{fip}_{k}\,\gamma\,\beta$ and $\gamma\neq X$, we note that $\gamma$ takes form $\gamma=f(\gamma_{1},\ldots,\gamma_{n})$, see Line 4. If $f$ is a constant symbol, then certainly $\texttt{fip}_{k}\,\gamma\,\beta$ outputs a proper FIP. Otherwise, $\texttt{fip}_{k}$ proceeds to invoke itself recursively on respective pairs of arguments $\gamma_{i}$ and $\beta_{i}$. Since $X\to f(\gamma_{1},\ldots,\gamma_{n})$ is conservative, we know that, by induction, $\texttt{fip}_{k}\,\gamma_{i}\,\beta_{i}$ constructs finite intersection partitions $\Pi(\gamma_{i},\beta_{i})$ for all pairs $\gamma_{i}$ and $\beta_{i}$. Certainly, $\delta_{i}\in L(\pi_{i})$ for some $\pi_{i}\in\Pi(\gamma_{i},\beta_{i})$; hence $\delta\in L(\pi)$ where $\pi=f(\pi_{1},\ldots,\pi_{n})\in\texttt{fip}_{k}\,\gamma\,\beta$. It follows that $\delta\in L(\pi)\cap L(\beta)\subset L(X)\cap L(\beta)$, which finishes the proof. ∎

Remark 4.7**.**

Note that the termination of $\texttt{fip}_{k}$ is based on the fact that all self-referencing productions of simple $`y$-reduction grammars are at the same time conservative. Indeed, $\texttt{fip}_{k}$ does not terminate in the presence of non-conservative productions. Consider the non-conservative production $X\to f(f(X))$. Note that

[TABLE]

Remark 4.8**.**

It is possible to optimise $\texttt{fip}_{k}$, as presented in Figure 4, and (potentially) shrink the size of $\Pi(\alpha,\beta)$ by including an additional pattern in form of

$T$, $f(\alpha_{1},\ldots,\alpha_{n})$ $\Rightarrow$ $\{f(\alpha_{1},\ldots,\alpha_{n})\}$

Remark 4.9**.**

Our finite intersection partition algorithm resembles a variant of Robinsons’s unification algorithm [17] applied to many-sorted term algebras with a tree hierarchy of sorts, as investigated by Walther, cf. [19]. It becomes even more apparent once the correspondence between sorts, as stated in the language of many-sorted term algebra, and the tree-like hierarchy of non-terminal symbols in $`y$-reduction grammars is established, see Figure 2.

5. The construction of simple $`y$-reduction grammars

Equipped with constructible, finite intersection partitions, we are now ready to describe the generation procedure for $\left(\mathscr{G}_{n}\right)_{n}$. We begin with establishing a convenient verbosity invariant maintained during the construction of $\left(\mathscr{G}_{n}\right)_{n}$.

Definition 5.1** (Closure width).**

Let $\alpha$ be a term in $\mathscr{T}_{\mathscr{F}}(X)$ for some finite set $X$. Then, $\alpha$ has closure width $w$, if $w$ is the largest non-negative integer such that $\alpha$ is of form $\chi[\sigma_{1}]\cdots[\sigma_{w}]$ for some term $\chi$ and substitutions $\sigma_{1},\ldots,\sigma_{w}$. For convenience, we refer to $\chi$ as the head of $\alpha$ and to $\sigma_{1},\ldots,\sigma_{w}$ as its tail.

Definition 5.2** (Verbose $`y$-reduction grammars).**

A $`y$-RG $\mathscr{G}_{n}$ is said to be verbose if none of its productions takes the form $X\to G_{k}[\sigma_{1}]\cdots[\sigma_{w}]$ for some arbitrary non-negative $w$ and $k$.

Simple, verbose $`y$-reduction grammars admit a neat structural feature. Specifically, their productions preserve closure width of generated terms.

Lemma 5.3**.**

Let $\mathscr{G}_{n}$ be a simple, verbose $`y$-RG. Then, for each production $G_{n}\to\chi[\sigma_{1}]\cdots[\sigma_{w}]$ in $\mathscr{G}_{n}$ such that its right-hand side is of closure width $w$, either $\chi=N$ or $\chi$ is in form $\chi=f(\alpha_{1},\ldots,\alpha_{m})$ for some non-closure function symbol $f$ of arity $m$.

Proof.

Suppose that neither $\chi=N$ nor $\chi=f(\alpha_{1},\ldots,\alpha_{m})$. Since $\mathscr{G}_{n}$ is simple, it follows that either $\chi=T$ or $\chi=G_{k}$ for some $0\leq k\leq n$. However, due to the verbosity of $\mathscr{G}_{n}$ we know that $\chi\neq G_{k}$ and so it must hold $\chi=T$. Consider the following inductive family of terms:

[TABLE]

By construction, we note that $\delta_{n}\downarrow_{n}$. Let $s_{1},\ldots,s_{w}$ be substitutions satisfying $s_{i}\in L(\sigma_{i})$. Note that $\delta:=\delta_{n+1}[s_{1}]\cdots[s_{w}]\in L(T[\sigma_{1}]\cdots[\sigma_{w}])$; hence, simultaneously $\delta$ reduces in $n$ steps, as $\delta\in L(G_{n})$, and in at least $n+1$ steps, contradiction. ∎

Lemma 5.4**.**

Let $\mathscr{G}_{n}$ be a simple, verbose $`y$-RG. Then, for each production $G_{n}\to\chi[\sigma_{1}]\cdots[\sigma_{w}]$ in $\mathscr{G}_{n}$ such that its right-hand side is of closure width $w$, and ground term $\delta\in L(\chi[\sigma_{1}]\cdots[\sigma_{w}])$ it holds that $\delta$ is of closure width $w$.

Proof.

Direct consequence of 5.3. ∎

The following $\varphi$-matchings are the central tool used in the construction of new reduction grammars. Based on finite intersection partitions, $\varphi$-matchings provide a simple template recognition mechanism which allows us to match productions in $\mathscr{G}_{n}$ with right-hand side of $`y$ rewriting rules.

Definition 5.5** ($\varphi$-matchings).**

Let $\mathscr{G}_{n}$ be a simple, verbose $`y$-RG and $\varphi=\chi[\tau_{1}]\cdots[\tau_{d}]\in\mathscr{T}(\mathscr{N}_{n})$ be a template (term) of closure width $d$. Assume that $X\to\gamma[\sigma_{1}]\cdots[\sigma_{w}]$ is a production of $\mathscr{G}_{n}$ which right-hand side has closure width $w$. Furthermore, let

[TABLE]

be the set of $\varphi$-matchings of $\gamma[\sigma_{1}]\cdots[\sigma_{w}]$.

Then, the set $\Delta_{\varphi}^{n}$ of $\varphi$-matchings of $\mathscr{G}_{n}$ is defined as

[TABLE]

For further convenience, we write $\varphi_{\langle i\rangle}$ to denote the template $\varphi=\chi[\tau_{1}]\cdots[\tau_{d}]$ with $i$ copies of $[S]$ appended to its original tail, i.e. $\varphi_{\langle i\rangle}=\chi[\tau_{1}]\cdots[\tau_{d}]\underbrace{[S]\cdots[S]}_{i\leavevmode\nobreak\ \text{times}}$.

In what follows we use computable intersection partitions in our iterative construction of $\left(\mathscr{G}_{n}\right)_{n}$. Recall that if $\mathscr{G}_{n}$ is simple then, inter alia, self-referencing productions starting with the non-terminal $G_{n}$ take the form

[TABLE]

If $t\downarrow_{n}$ (for $n\geq 1$) but it does not strat with a head $`y$-redex, then it must be of form $t=`la$ or $t=ab$. In the former case, it must hold $a\downarrow_{n}$; hence the pre-defined production $G_{n}\to`lG_{n}$ in $\mathscr{G}_{n}$. In the latter case, it must hold $a\downarrow_{k}$ whereas $b\downarrow_{n-k}$ for some $0\leq k\leq n$. And so, it means that we have to include productions in form of $G_{n}\to G_{k}G_{n-k}$ for all $0\leq k\leq n$ in $\mathscr{G}_{n}$; in particular, the already mentioned two self-referencing productions, see (12).

Remaining terms have to start with head redexes. Each of these head $`y$-redexes is covered by a dedicated set of productions. The following 5.6 demonstrates how $\varphi$-matchings and, in particular, finite intersection partitions can be used for that purpose.

Lemma 5.6**.**

Let $\varphi=`l(T[\Uparrow(S)])$ be the template corresponding to the (Lambda) rewriting rule, see Table 1, and $t=(`la)[s][s_{1}]\cdots[s_{w}]$. Then, $t\downarrow_{n+1}$ if and only if there exists a unique term $\pi=\left(`l(\alpha[\Uparrow(\sigma)])\right)[\sigma_{1}]\cdots[\sigma_{w}]\in\Delta_{\varphi}^{n}$ such that $t\in L((`l\alpha)[\sigma][\sigma_{1}]\cdots[\sigma_{w}])$.

Proof.

Let $t=(`la)[s][s_{1}]\cdots[s_{w}]\downarrow_{n+1}$ where $w\geq 0$. Since $t$ admits a head $`y$-redex, we note that $t\to t^{\prime}=\left(`l(a[\Uparrow(s)])\right)[s_{1}]\cdots[s_{w}]\downarrow_{n}$. By assumption, $\mathscr{G}_{n}$ is simple, hence there exists a unique production $G_{n}\to\gamma$ in $\mathscr{G}_{n}$ such that $t^{\prime}\in L(\gamma)$. Consider the set $\Delta_{\varphi}^{n}$. Since $G_{n}\to\gamma$ is the unique production satisfying $t^{\prime}\in L(\gamma)$, it follows that for each production $G_{n}\to\gamma^{\prime}$ in $\mathscr{G}_{n}$ such that $\gamma^{\prime}\neq\gamma$ and all $\pi\in\Delta_{\varphi}(\gamma^{\prime})$ it holds $t^{\prime}\not\in L(\pi)$. Let us therefore focus on the set $\Delta_{\varphi}(\gamma)$ of $\varphi$-matchings limited to $\gamma$.

By assumption, $\mathscr{G}_{n}$ is not only simple but also verbose. Consequently, we know that $\gamma$ retains the closure width of generated terms, see 5.4. It follows that $\gamma$ has closure width $w$ and takes the form $\gamma=\chi[\tau_{1}]\cdots[\tau_{w}]$. Certainly, $t^{\prime}\in L(\varphi_{\langle w\rangle})$. Moreover, $\Delta_{\varphi}(\gamma)=\Pi(\gamma,\varphi_{\langle w\rangle})$. There exists therefore a unique $\pi\in\Pi(\gamma,\varphi_{\langle w\rangle})$ such that $t^{\prime}\in L(\pi)$. Given the fact that the head of $\varphi_{\langle w\rangle}$ is equal to $\varphi=`l(T[\Uparrow(S)])$ we note that $\pi$ must be of form $\pi=`l(\alpha[\Uparrow(\sigma)])[\sigma_{1}]\cdots[\sigma_{w}]$. However, since $t^{\prime}=(`la[\Uparrow(s)][s_{1}]\cdots[s_{w}])\in L(\pi)$ it also means that $a\in L(\alpha)$, $s\in L(\sigma)$, and $s_{i}\in L(\sigma_{i})$ for all $1\leq i\leq w$. Consequently, $t\in L((`l\alpha)[\sigma][\sigma_{1}]\cdots[\sigma_{w}])$ as required.

Conversely, let $\pi=`l(\alpha[\Uparrow(\sigma)])[\sigma_{1}]\cdots[\sigma_{w}]$ be the unique term in the $\varphi$-matching family $\Delta_{\varphi}^{n}$ such that $t\in L((`l\alpha)[\sigma][\sigma_{1}]\cdots[\sigma_{w}])$. Note that $a\in L(\alpha)$, $s\in L(\sigma)$, and $s_{i}\in L(\sigma_{i})$ for all $1\leq i\leq w$. Since $t$ has a head $`y$-redex, after a single reduction step $t$ reduces to $t^{\prime}=`l(a[\Uparrow(s)])[s_{1}]\cdots[s_{w}]\in L(\pi)$. By construction of $\Delta_{\varphi}^{n}$, it means that there exists a production $G_{n}\to\gamma$ in $\mathscr{G}_{n}$ such that $L(\pi)\subset L(\gamma)$ and hence $t^{\prime}\downarrow_{n}$. Certainly, it follows that $t\downarrow_{n+1}$. ∎

Let us remark that almost all of the rewriting rules of $`l`y$ exhibit a similar construction scheme; the exceptional (App) and (FVar) rewriting rules are discussed in 5.7 and 5.8, respectively. Given a rewriting rule, we start with the respective template $\varphi$ (see Table 1) and generate all possible $\varphi$-matchings in $\mathscr{G}_{n}$. Intuitively, such an operation extracts unambiguous sublanguages out of each production in $\mathscr{G}_{n}$ which match the right-hand side of the considered rewriting rule. Next, we consider each term $\pi\in\Delta_{\varphi}^{n}$ and establish new productions $G_{n+1}\to\gamma$ in $\mathscr{G}_{n+1}$ out of $\pi$. Assuming that $\mathscr{G}_{n}$ is a simple and verbose $`y$-RG, the novel productions generated by means of $\Delta_{\varphi}^{n}$ cover all the $`l`y$-terms reducing in $n+1$ normal-order steps, starting with the prescribed head rewriting rule. Since the head of each so constructed production either starts with a function symbol or is equal to $N$, cf. Table 1, the outcome grammar is necessarily verbose. Moreover, if we complete the production generation for all rewriting rules, by construction, the grammar $\mathscr{G}_{n+1}$ must be, at the same time, simple. Consequently, the construction of the hierarchy $\left(\mathscr{G}_{n}\right)_{n}$ amounts to an inductive application of the above construction scheme.

Remark 5.7**.**

While following the same pattern for the (App) rule, we notice that the corresponding construction requires a slight modification. Specifically, while matching $\varphi=T[S](T[S])$ with a right-hand side $\gamma$ of a production $G_{n}\to\gamma$ in $\mathscr{G}_{n}$ we cannot conclude that $\pi\in\Delta_{\varphi}^{n}$ takes the form $\pi=\alpha[\sigma](\beta[\sigma])[\sigma_{1}]\cdots[\sigma_{w}]$. Note that, in fact, $\pi=\alpha[\tau_{1}](\beta[\tau_{2}])[\sigma_{1}]\cdots[\sigma_{w}]$ however perhaps $\tau_{1}\neq\tau_{2}$. Nonetheless, we can still compute $\Pi(\tau_{1},\tau_{2})$ and use $\tau\in\Pi(\tau_{1},\tau_{2})$ to generate a finite set of terms in form of $\pi=\alpha[\tau](\beta[\tau])[\sigma_{1}]\cdots[\sigma_{w}]$. Using those terms, we can continue with our construction and establish a set of new productions in form of $G_{n}\to(\alpha\beta)[\tau][\sigma_{1}]\cdots[\sigma_{w}]$ meant to be included in $\mathscr{G}_{n+1}$.

Remark 5.8**.**

Let us also remark that the single rewriting rule which has a template $\varphi$ not retaining closure width is (FVar). In consequence, the utility of $\Delta_{T}(\gamma)$ is substantially limited. If $t=\mbox{\text@underline{\sf 0}}[a/][s_{1}]\cdots[s_{w}]\downarrow_{n+1}$, then $t\to t^{\prime}=a[s_{1}]\cdots[s_{w}]$ which, in turn, satisfies $t^{\prime}\downarrow_{n}$. Note that if $\gamma$ is the right-hand side of a unique production $G_{n}\to\gamma$ in $\mathscr{G}_{n}$ generating $t^{\prime}$, then we can match $T$ with any non-empty prefix of $\gamma$. The length of the chosen prefix influences what initial part $\alpha$ of $\gamma$ is going to be placed under the closure in $G_{n+1}\to\mbox{\text@underline{\sf 0}}[\alpha/][\sigma_{1}]\cdots[\sigma_{w}]$.

This motivates the following approach. Let $G_{n}\to\gamma^{\prime}=\chi[\sigma_{1}]\cdots[\sigma_{w}]$ be an arbitrary production in $\mathscr{G}_{n}$ of closure width $w$. If $t^{\prime}\in L(\gamma^{\prime})$ and $t\to t^{\prime}$ in a single head (FVar)-reduction, then $t\in L(\mbox{\text@underline{\sf 0}}[\chi[\sigma_{1}]\cdots[\sigma_{d}]/][\sigma_{d+1}]\cdots[\sigma_{w}]$ for some $0\leq d\leq w$. Therefore, in order to generate all productions in $\mathscr{G}_{n+1}$ corresponding to $`l`y$-terms $`y$-normalising in $n+1$ steps, starting with a head (FVar)-reduction, we have to include all productions in form of $G_{n+1}\to\mbox{\text@underline{\sf 0}}[\chi[\sigma_{1}]\cdots[\sigma_{d}]/][\sigma_{d+1}]\cdots[\sigma_{w}]$ for each production $G_{n}\to\gamma^{\prime}$ in $\mathscr{G}_{n}$.

Finally, note that it is, again, possible to optimise the (FVar) construction scheme with respect to the number of generated productions. For each $G_{n}\to\gamma$ in $\mathscr{G}_{n}$ the above scheme produces, inter alia, a production $G_{n+1}\to\mbox{\text@underline{\sf 0}}[\gamma/]$. Note that we can easily merge them into a single production $G_{n+1}\to\mbox{\text@underline{\sf 0}}[G_{n}/]$ instead.

Such a construction leads us to the following conclusion.

Theorem 5.9**.**

For all $n\geq 0$ there exists a constructible, simple $`y$-RG $\mathscr{G}_{n}$.

Example 5.10**.**

The following example demonstrates the construction of $\mathscr{G}_{1}$ out of $\mathscr{G}_{0}$. Note that $\mathscr{G}_{1}$ includes the following productions associated with the axiom $G_{1}$:

[TABLE]

The first three productions are included by default. The next three productions are derived from the (FVar) rule applied to all the productions of $G_{0}\to\gamma$ in $\mathscr{G}_{0}$. The final three productions are obtained by (RVar), (FVarLift), and (VarShift), respectively.

6. Analytic combinatorics and simple $`y$-reduction

grammars

Having established an effective hierarchy $\left(\mathscr{G}_{k}\right)_{k}$ of simple $`y$-reduction grammars, we can now proceed with their quantitative analysis. Given the fact that regular tree grammars represent well-known algebraic tree-like structures, our analysis is in fact a standard application of algebraic singularity analysis of respective generating functions [12, 13]. The following result provides the main tool of the current section.

Proposition 6.1** **(Algebraic singularity analysis, see [13], Theorem

VII.8).

Assume that $f(z)=\left(\sqrt{1-z/\zeta}\right)g(z)+h(z)$ is an algebraic function, analytic at [math], and has a unique dominant singularity $z=\zeta$. Moreover, assume that $g(z)$ and $h(z)$ are analytic in the disk $|z|<\zeta+\varepsilon$ for some $\varepsilon>0$. Then, the coefficients $[z^{n}]f(z)$ in the series expansion of $f(z)$ around the origin, satisfy the following asymptotic estimate

[TABLE]

In order to analyse the number of $`l`y$-terms normalising in $k$ steps, we execute the following plan. First, we use the structure (and unambiguity) of $\mathscr{G}_{k}$ to convert it by means of symbolic methods into a corresponding generating function $G_{k}(z)=\sum g^{(k)}_{n}z^{n}$ in which the integer coefficient $g^{(k)}_{n}$ standing by $z^{n}$ in the series expansion of $G_{k}(z)$, also denoted as $[z^{n}]G_{k}(z)$, is equal to the number of $`l`y$-terms of size $n$ normalising in $k$ steps. Next, we show that so obtained generating functions fit the premises of 6.1.

We start with establishing an appropriate size notion for $`l`y$-terms. For technical convenience, we assume the following natural size notion, equivalent to the number of constructors in the associated term algebra $\mathscr{T}_{\mathscr{F}}(\varnothing)$, see Figure 5.

The following results exhibit the closed-form of generating functions corresponding to pure terms as well as the general class of $`l`y$-terms and explicit substitutions.

Proposition 6.2** (see [5]).**

Let $L_{\infty}(z)$ denote the generating function corresponding to the set of $`l$-terms in $`y$-normal form (i.e. without $`y$-redexes). Then,

[TABLE]

Proposition 6.3** (see [7]).**

Let $T(z)$, $S(z)$ and $N(z)$ denote the generating functions corresponding to $`l`y$-terms, substitutions, and de Bruijn indices, respectively. Then,

[TABLE]

With the above basic generating functions, we can now proceed with the construction of generating functions corresponding to simple $`y$-reduction grammars.

Proposition 6.4** (Constructible generating functions).**

Let $\Phi_{k}$ denote the set of regular productions in $\mathscr{G}_{k}$. Then, for all $k\geq 1$ there exists a generating function $G_{k}(z)$ such that $[z^{n}]G_{k}(z)$ (i.e. the coefficient standing by $z^{n}$ in the power series expansion of $G_{k}(z)$) is equal to the number of terms of size $n$ which $`y$-normalise in $k$ normal-order reduction steps, and moreover $G_{k}(z)$ admits a closed-form of the following shape:

[TABLE]

where

[TABLE]

and all $\zeta(\gamma)$, $\tau(\gamma)$, $\sigma(\gamma)$, $\nu(\gamma)$, and $\rho_{i}(\gamma)$ are non-negative integers depending on $\gamma$.

Proof.

Let $G_{k}\to\gamma$ be a regular production in $\mathscr{G}_{k}$. Since by construction $\mathscr{G}_{k}$ is simple, we know that $\gamma\in\mathscr{T}_{\mathscr{F}}(\mathscr{N}\cup\{G_{0},\ldots,G_{k-1}\})$. Following symbolic methods [13, Part A, Symbolic Methods] we can therefore convert each non-terminal $X\in\mathscr{N}\cup\{G_{0},\ldots,G_{k-1}\}$ occurring in $\gamma$ into an appropriate generating function $X(z)$. Likewise, we can convert each function symbol occurrence $f$ into an appropriate monomial $z$, see Figure 5. Finally, we group respective monomials together, and note that the generating function $G_{\gamma}(z)$ corresponding to $\gamma$ takes the form (18). Respective exponents denote the number of occurrences of their associated symbols.

Consider the remaining self-referencing productions $G_{k}\to\delta$. Again, since $\mathscr{G}_{k}$ is simple, we know that $\delta$ takes the form $`lG_{k}$, $G_{0}G_{k}$ or (symmetrically) $G_{k}G_{0}$. And so, as each $X\in\mathscr{N}_{n}$ is unambiguous in $\mathscr{G}_{k}$, by symbolic methods, it follows that $G_{k}(z)$ satisfies the following functional equation:

[TABLE]

Note that as no $G_{\gamma}(z)$ references the left-hand side $G_{k}(z)$, equation (19) is in fact linear in $G_{k}(z)$. Furthermore, as $G_{0}(z)=L_{\infty}(z)$ we finally obtain the requested form of $G_{k}(z)$, see (17). ∎

This brings us to our following, main quantitative result.

Theorem 6.5**.**

For all $k\geq 1$ the coefficients $[z^{n}]G_{k}(z)$ admit the following asymptotic estimate

[TABLE]

Proof.

We claim that for each $k\geq 1$ the generating function $G_{k}(z)$ can be represented as $G_{k}(z)=\sqrt{1-4z}P(z)+Q(z)$ where both $P(z)$ and $Q(z)$ are functions analytic in the disk $|z|<\frac{1}{4}+\varepsilon$ for some positive $\varepsilon$. The asserted asymptotic estimate follows then as a straightforward application of algebraic singularity analysis, see 6.1.

We start with showing that each $G_{k}(z)$ includes a summand in form of $\sqrt{1-4z}\,\overline{P}(z)+\overline{Q}(z)$ such that both $\overline{P}(z)$ and $\overline{Q}(z)$ are analytic in a large enough disk containing (properly) $|z|<\frac{1}{4}$. Afterwards, we argue that no summand has singularities in $|z|<\frac{1}{4}$. Standard closure properties of analytic functions with single dominant, square-root type singularities guarantee the required representation of $G_{k}(z)$.

Let $\varphi=N$ be the template corresponding to the (RVar) rule, see Table 1. Note that since $\mathscr{G}_{0}$ includes the production $G_{0}\to N$, the set of $\varphi$-matchings $\Delta_{\varphi}^{0}$ consists of the single term $N$. Hence, due to the respective production construction, it means that $G_{1}\to(\operatorname*{\mbox{\sf S}}N)[T/]$ is a production of $\mathscr{G}_{1}$, cf. 5.10. Moreover, as a consequence of the construction associated with the (FVar) rule, for each $G_{k}\to\gamma$ in $\mathscr{G}_{k}$ there exists a production $G_{k+1}\to\mbox{\text@underline{\sf 0}}[\gamma/]$ in the subsequent grammar $\mathscr{G}_{k+1}$. And so, each $\mathscr{G}_{k}$ includes among its productions one production in form of

[TABLE]

Denote the right-hand side of the above production as $\gamma$. Note that the associated generating function $G_{\gamma}(z)$, cf. (19), must therefore take form

[TABLE]

where both $P(z)$ and $Q(z)$ are analytic in $|z|<\frac{1}{4}+\varepsilon$ for some (determined) $\varepsilon>0$.

In order to show that no production admits a corresponding generating function with singularities in the disk $|z|<\frac{1}{4}$ we note that the single dominant singularity of $G_{0}(z)$, and so at the same time $L_{\infty}(z)$, is equal to the smallest positive real root $\rho$ of $1-3z-z^{2}-z^{3}$ which satisfies $\frac{1}{4}<\rho\approx 0.295598$, see 6.2. Due to the form of basic generating functions corresponding to $T$, $S$ and $N$, see 6.3, we further note that other singularities must lie on the unit circle $|z|=1$. And so, each $G_{k}(z)$ admits the asserted form

[TABLE]

for some functions analytic in a disk $|z|<\frac{1}{4}+\varepsilon$. ∎

Remark 6.6**.**

Consider the following asymptotic density of $`l`y$-terms $`y$-normalisable in $k$ normal-order reduction steps in the set of all $`l`y$-terms:

[TABLE]

In other words, the limit $\mu_{k}$ of the probability that a uniformly random $`l`y$-term of size $n$ normalises in $k$ steps as $n$ tends to infinity. Note that for each $k\geq 1$, the asymptotic density $\mu_{k}$ is positive as both $[z^{n}]G_{k}(z)$ and $[z^{n}]T(z)$ admit the same (up to a multiplicative constant) asymptotic estimate. Moreover, it holds $\mu_{k}\xrightarrow[k\to\infty]{}0$ as the sum $\sum_{k}\mu_{k}$ is increasing and necessarily bounded above by one.

Each $`l`y$-term is $`y$-normalising in some (determined) number of normal-order reduction steps. However, it is not clear whether $\sum_{k}\mu_{k}=1$ as asymptotic density is, in general, not countably additive. Let us remark that if this sum converges to one, then the random variable $X_{n}$ denoting the number of normal-order $`y$-reduction steps required to normalise a random $`l`y$-term of size $n$ (i.e. the average-case cost of resolving pending substitutions in a random term of size $n$) converges pointwise to a discrete random variable $X$ defined as $\mathbb{P}(X=k)=\mu_{k}$. Unfortunately, the presented analysis does not determine an answer to this problem.

Remark 6.7**.**

Theorem 5.9 and Theorem 6.5 are effective in the sense that both the symbolic representation and the symbolic asymptotic estimate of respective coefficients are computable. Since $\Gamma(-1/2)=-2\sqrt{\pi}$ is the sole transcendental number occurring in the asymptotic estimates, and cancels out when asymptotic densities are considered, cf. (24), we immediately note that for each $k\geq 0$, the asymptotic density of terms $`y$-normalising in $k$ steps is necessarily an algebraic number.

Figure 6 provides the specific asymptotic densities $\mu_{0},\ldots,\mu_{10}$ obtained by means of a direct construction and symbolic computations111Corresponding software is available at https://github.com/maciej-bendkowski/towards-acasrlc. (numerical values are rounded up to the fifth decimal point).

7. Applications to other term rewriting

systems

Let us note that the presented construction of reduction grammars does not depend on specific traits immanent to $`l`y$, but rather on certain more general features of its rewriting rules. The key ingredient in our approach is the ability to compute finite intersection partitions for arbitrary terms within the scope of established reduction grammars, which themselves admit certain neat structural properties. Using finite intersection partitions, it becomes possible to generate new productions based on the structural resemblance of both the left-hand and right-hand sides of associated rewriting rules.

In what follows we sketch the application of the presented approach to other term rewriting systems, focusing on two examples of $`l`y$-calculus and combinatory logic. Although the technique is similar, some careful amount of details is required.

7.1. $`l`y$-calculus

In order to characterise the full $`l`y$-calculus, we need a few adjustments to the already established construction of $\left(\mathscr{G}_{k}\right)_{k}$ corresponding to the $`y$ fragment. Clearly, we have to establish a new production construction scheme associated with the (Beta) rewriting rule. Consider the corresponding template $\varphi=T[T/]$. Like the respective template for (FVar), cf. 5.8, the current template $\varphi$ does not retain closure width of generated ground terms. However, at the same time it is also amenable to similar treatment as (FVar).

Let $t=(`la)b[s_{1}]\cdots[s_{w}]\downarrow_{n+1}$. Note that $t\to a[b/][s_{1}]\cdots[s_{w}]\downarrow_{n}$. Consequently, one should attempt to match $\varphi$ with all possible prefixes of $\gamma$ in all productions $G_{n}\to\gamma$ instead of merely their heads, as in the case of $\Delta_{\varphi}^{n}$. Let $\gamma=\chi[\sigma_{1}]\cdots[\sigma_{d}]$ be of closure width $d$ and $\delta=\chi[\sigma_{1}]\cdots[\sigma_{i}]$ be its prefix ($1\leq i\leq d$). Note that, effectively, $\Pi(\delta,T[T/])$ checks if $[\sigma_{i}]$ takes form $\beta/$ for some term $\beta$. Hence, for each $\pi\in\Pi(\delta,T[T/])$ we have $\pi=\alpha[\tau_{1}]\cdots[\tau_{i-1}][\beta/]$ for some terms $\alpha$, $\tau_{1},\ldots,\tau_{i-1}$, and $\beta$. Out of such a partition $\pi$ we can then construct the production $G_{n+1}\to(`l\alpha[\tau_{1}]\cdots[\tau_{i-1}])\beta[\tau_{i+1}]\cdots[\tau_{d}]$ in $\mathscr{G}_{n+1}$.

However, with the new scheme for (Beta) we are not yet done with our construction. Note that due to the new head redex type, we are, inter alia, forced to change the pre-defined set of productions corresponding to $`l`y$-terms without a head redex. Indeed, note that if $t$ does not start with a head redex, then it must be of form $(`la)$ or $(ab)$ where in the latter case $a$ cannot start with a leading abstraction. This constraint suggests the following approach. We split the set of productions in form of $G_{n}\to\gamma$ into two categories, i.e. productions whose right-hand sides are of form $`l\gamma^{\prime}$ and the reminder ones. Since both sets are disjoint, we can group them separately and introduce two auxiliary non-terminal symbols $G_{n}^{(`l)}$ and $G_{n}^{(\neg`l)}$ for terms starting with a head abstraction and for those without a head abstraction, respectively, with the additional productions $G_{n}\to G_{n}^{(`l)}\leavevmode\nobreak\ |\leavevmode\nobreak\ G_{n}^{(\neg`l)}$. In doing so, it is possible to pre-define the all the productions corresponding to terms without head redexes using productions in form of

[TABLE]

This operation, however, requires a minor adjustment of the term potential, see 4.3, accounting for the new non-terminal symbols $G_{k}^{(`l)}$ and $G_{k}^{(\neg`l)}$ occurring in the right-hand sides of grammar productions. Once updated, we can reuse it in showing that finite intersection partitions are, again, computable and can serve as a tool in the construction of new productions in $\mathscr{G}_{n+1}$ out of $\mathscr{G}_{n}$.

7.2. $SK$-combinators

Using a similar approach, it becomes possible to construct reduction grammars for $SK$-combinators. In particular, our current technique (partially) subsumes, and also simplifies, the results of [6, 4]. With merely two rewriting rules in form of

[TABLE]

we can use the developed finite intersection partitions and $\varphi$-matchings to construct a hierarchy $\left(\mathscr{G}_{n}\right)_{n}$ of normal-order reduction grammars for $SK$-combinators. The rewriting rule corresponding to $K$ is similar to (FVar) whereas the respective rule for $S$ resembles the (App) rule; as in this case, we have to deal with variable duplication on the right-hand side of the rewriting rule. Instead of closure width, we use a different normal form of terms, and so also productions, based on the sole binary constructor of term application. Consequently, a combinator is of application width $w$ if it takes the form $X\alpha_{1}\ldots\alpha_{w}$ for some primitive combinator $X\in\{S,K\}$.

Consider the more involved case of productions corresponding to head $S$-redexes. Let $t=Sxyz\alpha_{1}\ldots\alpha_{w}$ be a term of application width $w+3$ where $w\geq 0$. Note that

[TABLE]

Let us rewrite the right-hand side of (27) as $t^{\prime}=Xx_{1}\ldots x_{k}z(yz)\delta_{1}\ldots\delta_{w}$ where $x=Xx_{1}\ldots x_{k}$ and $X$ is a primitive combinator. Assume that $\gamma$ is the right-hand side of the unique production $G_{n}\to\gamma$ in $\mathscr{G}_{n}$ such that $t^{\prime}\in L(\gamma)$. Note that the shape of $t^{\prime}$ suggests a construction scheme similar to the already discussed (App), see 5.7, where we first have to match the pattern $\varphi=T(TT)$ with some argument of $\gamma$ and subsequently attempt to extract a finite intersection partition $\Pi(\alpha,\beta)$ of respective subterms $\alpha$ and $\beta$ so that for each $\pi\in\Pi(\alpha,\beta)$ we have $z\in L(\pi)$. With appropriate terms at hand, we can then construct corresponding productions in the next grammar $\mathscr{G}_{n+1}$.

8. Conclusions

Quantitative aspects of term rewriting systems are not well studied. A general complexity analysis was undertaken by Choppy, Kaplan, and Soria who considered a class of confluent, terminating term rewriting systems in which the evaluation cost, measured in the number of rewriting steps required to reach the normal form, is independent of the assumed evaluation strategy [8]. More recently, typical evaluation cost of normal-order reduction in combinatory logic was studied by Bendkowski, Grygiel and Zaionc [6, 4]. Using quite different, non-analytic methods, Sin’Ya, Asada, Kobayashi and Tsukada considered certain asymptotic aspects of $`b$-reduction in the simply-typed variant of $`l$-calculus showing that, typically, $`l$-terms have exponentially long $`b$-reduction sequences [18].

Arguably, the main novelty in the presented approach lies in the algorithmic construction of reduction grammars $\left(\mathscr{G}_{k}\right)_{k}$ based on finite intersection partitions, assembled using a general technique reminiscent of Robinson’s unification algorithm applied to many-sorted term algebras, cf. [17, 19]. Equipped with finite intersection partitions, the construction of $\mathscr{G}_{k+1}$ out of $\mathscr{G}_{k}$ follows a stepwise approach, in which new productions are established on a per rewriting rule basis. Consequently, the general technique of generating reduction grammars does not depend on specific features of $`l`y$, but rather on more general traits of certain first-order rewriting systems. Nonetheless, the full scope of our technique is yet to be determined.

Although the presented construction is based on the leftmost-outermost evaluation strategy, it does not depend on the specific size notion associated with $`l`y$-terms; in principle, more involved size models can be assumed and analysed. The assumed evaluation strategy, size notion, as well as the specific choice of $`l`y$ are clearly arbitrary and other, equally perfect choices for modelling substitution resolution could have been made. However, due to merely eight rewriting rules forming $`l`y$, it is one of the conceptually simplest calculus of explicit substitutions. Together with the normal-order evaluation tactic, it is therefore one of the simplest to investigate in quantitative terms and to demonstrate the finite intersection partitions technique.

Due to the unambiguity of constructed grammars $\left(\mathscr{G}_{k}\right)_{k}$ it is possible to automatically establish their corresponding combinatorial specifications and, in consequence, obtain respective generating functions encoding sequences $\left(g^{(k)}_{n}\right)_{n}$ comprised of numbers $g^{(k)}_{n}$ associated with $`l`y$-terms of size $n$ which reduce in $k$ normal-order rewriting steps to their $`y$-normal forms. Singularity analysis provides then the means for systematic, quantitative investigations into the properties of substitution resolution in $`l`y$, as well as its machine-independent operational complexity. Finally, with generating functions at hand, it is possible to undertake a more sophisticated statistical analysis of substitution (in particular $`y$-normalisation) using available techniques of analytic combinatorics, effectively analysing the average-case cost of $`l$-calculus and related term rewriting systems.