一句话:提出为给定 n 生成无歧义正则树文法,刻画恰需 n 步正规序归约的 SK 组合子项。
本文研究如何句法刻画在组合逻辑中恰需 n 步正规序归约才能规范化的 SK 组合子项。作者提出一个算法:对给定 n 生成无歧义正则树文法,其语言正是这类项;借助 Curry 与 Feys 的标准化定理,该文法给出所有可规范化 SK 组合子项的完全句法刻画。进一步地,作者由这些文法递归构造普通生成函数,用于计数恰需 n 步正规序归约的 SK 组合子项,并考察所生成文法的规模,给出原始递归上界。
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 SK -combinators reducing in n normal-order reduction steps. Finally, we investigate the size of generated grammars giving a primitive recursive upper bound.