The combinatorial enumeration model of functional programming languages and trace
| Project/Area Number |
17540102
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year 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)
|
|---|
| Co-Investigator(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 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.
|
Report
(3 results)
Research Products
(9 results)
