The combinatorial enumeration model of functional programming languages and trace

我们采用二阶线性逻辑作为函数式程序设计语言的语法模型。如果我们把逻辑看作一个忽略逻辑系统方面的计算系统，那么不动点组合器作为一种支持递归程序设计的结构是必不可少的。因此，我们考虑由不动点组合子扩充的二阶线性逻辑系统。我们的目标是探索作为函数式编程语言计算模型的系统结构。定点组合子的存在使模型的构造变得极其困难，同时也使模型的结构变得极其丰富。我们针对与定点组合子的解释相关的各种性质。我们分析了组合子在抽象范畴模型中的行为及其在具体模型中的实现。在一般范畴模型中，对于线性逻辑范畴模型中的指数组合，不动点组合子的解释是由无余余代数的co-Eilenberg-Moore范畴的迹算子导出的。从这个角度来看，我们前面构造的跟踪操作符是自然重建的。作为一般设置的一个具体例子，我们根据一种名为孪生数的新的数学概念构建了一个模型。我们分析了该模型中定点组合子的解释结构。双胞胎与枚举组合学理论中使用的母函数密切相关。这意味着我们可以使用列举组合学中使用的数学方法来分析我们的模型。从这个角度出发，我们探讨了不动点组合子的解释。其结果是，与解释定点组合子的孪生子相关联的母函数对应于被称为Cayley函数的幂函数。

We adopt the second-order linear logic as a syntactic model of functional programming languages. If we regard the logic as a computational system ignoring the aspect of a logical system, the fixed point combinator is indispensable as a structure to support recursive programming. We therefore consider the system of the second-order linear logic augmented by the fixed point combinator. Our goal is to explore the structure of the system as a computational model of functional programming languages. Existence of the fixed point combinator makes the construction of models extremely difficult as well as it makes the structure of the models extremely rich. We target the various properties related to interpretation of the fixed point combinator. We analyze both the behavior of the combinator in abstract categorical models and its realization in a concrete model. In general categorical models, the interpretation of the fixed point combinator is induced from the trace operator in the subcategory of the co-Eilenberg-Moore category of the cofree coalgebras for the exponential comonad in the categorical models of the linear logic. The trace operator we constructed earlier is rebuilt naturally from this perspective. As a concrete example for the general setting, we construct a model from a novel mathematical notion called twiners. We analyze the structure of the interpretation of the fixed point combinator in this model. The twiners are intimately related to the generating functions used in the theory of the enumerative combinatorics. This signifies that we can employ the mathematical methods used in the enumerative combinatorics also in the analysis of our model. From this view, we explore the interpretation of the fixed point combinator. A result is that the generating function associated to the twiner interpreting the fixed point combinator corresponds to the power series known as the Cayley function.