The combinatorial enumeration model of functional programming languages and trace
Project/Area Number  17540102 
Research Category 
GrantinAid for Scientific Research (C)

Allocation Type  Singleyear Grants 
Section  一般 
Research Field 
General mathematics (including Probability theory/Statistical mathematics)

Research Institution  The University of Tokyo 
Principal Investigator 
HASEGAWA Ryu The University of Tokyo, Graduate School for Mathematical Sciences, Associate Professor, 大学院数理科学研究科, 助教授 (20243107)

CoInvestigator(Kenkyūbuntansha) 
HASEGAWA Masahito Kyoto University, Research Institute for Mathematical Sciences, Professor, 数理解析研究所, 教授 (50293973)

Project Period (FY) 
2005 – 2006

Project Status 
Completed(Fiscal Year 2006)

Budget Amount *help 
¥1,400,000 (Direct Cost : ¥1,400,000)
Fiscal Year 2006 : ¥600,000 (Direct Cost : ¥600,000)
Fiscal Year 2005 : ¥800,000 (Direct Cost : ¥800,000)

Keywords  linear logic / combinatorial enumeration model / fixed point combinator / 圏論モデル / トレース 
Research Abstract 
We adopt the secondorder 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 secondorder 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 coEilenbergMoore 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.

Report
(3results)
Research Products
(9results)