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.