权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

A study on denotational semantics of λμ-calculus

λμ演算的指称语义研究

基本信息

批准号：
14540119
负责人：
FUJITA Ken-etsu
金额：
$ 1.86万
依托单位：
Gunma University (2004)Shimane University (2002-2003)
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2002
资助国家：
日本
起止时间：
2002 至 2004
项目状态：
已结题

项目摘要

A correspondence between Intuitionistic logic and typed λ-calculus is well-known as Curry-Howard isomorphism. M.Parigot (1992) has extended the correspondence and introduced λμ-calculus as a second-order classical logic. λμ-calculus is a natural extension of λ-calculus and the system itself is quite interesting as a functional computation model. In the last two years' project, we have investigated the following points :(1)CPS-translation from type-free and simply typed λμ-calculi intoλ-calculus ;(2)Continuation denotational semantics of λμ-calculus and C-monoid ;(3)Similarity relation on CPO between CPS-translation and continuation denotational semantics.In order to extend the results above, we introduced a new system, an existential type system λ∃. It is proved that there exist bijective translations between polymorphicλ-calculus and a subsystem of λ∃, which form a Galois connection and moreover Galois embedding. From a programming point of view, this result means that polymorphic functions can be represented by abstract data types.

直觉主义逻辑和类型化λ-演算之间的对应被称为Curry-Howard同构。M.Parigot（1992）扩展了对应关系，并引入λμ-演算作为二阶经典逻辑。λμ-演算是λ-演算的自然扩展，系统本身作为函数计算模型是非常有趣的。在过去的两年中，我们研究了以下几个问题：（1）从无类型和简单类型的λμ-演算到λ-演算的CPS-翻译;（2）λμ-演算和C-幺半群的延拓指称语义;（3）CPS-翻译与延拓指称语义在CPO上的相似关系。证明了多态λ-演算与λ-演算的一个子系统之间存在双射变换，它们构成一个Galois联络，进而构成一个Galois嵌入.从编程的角度来看，这个结果意味着多态函数可以用抽象数据类型表示。