Normal-order reduction grammars

TL;DR

This paper introduces an algorithm to generate unambiguous regular tree grammars that characterize combinatory logic terms requiring a specific number of normal-order reduction steps, enabling precise counting and analysis.

Contribution

It provides the first recursive method to construct grammars for normalizing combinatory logic terms and analyzes their size with a primitive recursive bound.

Findings

Generated grammars precisely characterize normalizing terms.

Recursive formulas count combinators by reduction steps.

Size of grammars has a primitive recursive upper bound.

Abstract

We present an algorithm which, for given $n$, generates an unambiguous regular tree grammar defining the set of combinatory logic terms, over the set $\{S,K\}$ of primitive combinators, requiring exactly $n$ normal-order reduction steps to normalize. As a consequence of Curry and Feys's standardization theorem, our reduction grammars form a complete syntactic characterization of normalizing combinatory logic terms. Using them, we provide a recursive method of constructing ordinary generating functions counting the number of $S K$-combinators reducing in $n$ normal-order reduction steps. Finally, we investigate the size of generated grammars, giving a primitive recursive upper bound.