• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

The combinatorial enumeration model of functional programming languages and trace

Research Project

Project/Area Number 17540102
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field General mathematics (including Probability theory/Statistical mathematics)
Research InstitutionThe 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)
Keywordslinear 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)
  • 2006 Annual Research Report   Final Research Report Summary
  • 2005 Annual Research Report
  • Research Products

    (9 results)

All 2007 2006 2005

All Journal Article (9 results)

  • [Journal Article] 再帰プログラミングの意味論にっぃて2007

    • Author(s)
      長谷川真人
    • Journal Title

      数学 59

      Pages: 180-191

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2006 Final Research Report Summary
  • [Journal Article] Coherenco of the double involution on *-autonomous categories2006

    • Author(s)
      J.R.B.Cockeff, M.Hasegawa, R.A.G.Seely
    • Journal Title

      Theory and Applications of Categories 17

      Pages: 17-29

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2006 Final Research Report Summary
  • [Journal Article] Relational paramervicity and control.2006

    • Author(s)
      M.Hasegawa
    • Journal Title

      Logical methods in Computer Science. 2

      Pages: 1-22

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2006 Final Research Report Summary
  • [Journal Article] Coherence of the double involution on *-autonomous categories2006

    • Author(s)
      J.R.B.Cockett, M.Hasegawa, R.A.G.Seely
    • Journal Title

      Theory and Applications of Categories 17

      Pages: 17-29

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2006 Final Research Report Summary
  • [Journal Article] Relational parametricity and control2006

    • Author(s)
      M.Hasegawa
    • Journal Title

      Logical Methods in Computer Science 2

      Pages: 1-22

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      2006 Final Research Report Summary
  • [Journal Article] Coherence of the double involution on *-autonomous categories2006

    • Author(s)
      J.R.B.Cockett, M.Hasegawa, R.A.G.Seely
    • Journal Title

      Theory and Applications of Categories 17・2

      Pages: 17-29

    • Related Report
      2006 Annual Research Report
  • [Journal Article] Relational parametricity and control2006

    • Author(s)
      M.Haegawa
    • Journal Title

      Logical Methods in Computer Science 2・3:3

    • Related Report
      2006 Annual Research Report
  • [Journal Article] Classical linear logic of implications2005

    • Author(s)
      M.Hasegawa
    • Journal Title

      Mathematical Structures in Computer Science 15

      Pages: 323-342

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      2006 Final Research Report Summary
  • [Journal Article] Relational parametricity and control2005

    • Author(s)
      M.Hasegawa
    • Journal Title

      20th Annual IEEE Symposium on Logic in Computer Science

      Pages: 72-81

    • Related Report
      2005 Annual Research Report

URL: 

Published: 2005-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi