A study on duality-based program transformation
| Project/Area Number |
17500004
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
FUJITA Ken-etsu GUNMA UNIVERSITY, Department of Computer Science, Associate Professor, 工学部, 助教授 (30228994)
|
|---|
| Project Period (FY) |
2005 – 2006
|
| Project Status |
Completed (Fiscal Year 2006)
|
| Budget Amount *help |
¥1,800,000 (Direct Cost: ¥1,800,000)
Fiscal Year 2006: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2005: ¥900,000 (Direct Cost: ¥900,000)
|
|---|
| Keywords | lambda calculus / polymorphism / abstract data types / Galois connection / continuation / CPS-translation / ガロア対応・埋め込み / 証明双対性 / 簡約対応 |
|---|
| Research Abstract |
(1) Galois embedding from polymorphic lambda-calculus into existential calculus :
We have defined a duality-based program transformation from polymorphic lambda-calculus into existential calculus. Then under the translation, it is shown that there exists a Galois connection between the calculi, and moreover a Galois embedding from polymorphic lambda-calculus into existential calculus.
(2) Sound and complete OPS-translation for type-free lambda-mu-calculus and abstract machine :
We have provided a sound and complete CPS-translation from type-free lambda-mu-calculus into lambda-calculus with surjective pair. Following the CPS-translation, we also introduced an abstract machine which executes CPS-codes and explicitly handles environment associated with substitution.
(3) CPS-translation as adjoint :
We have defined the duality-based program transformation (CPS-translation) for polymorphic lambda-calculus with extensionality. Then under the pre-order defined by the reflexive and transitive closure of the reduction, the translation can be expounded as an adjoint. That is, an inverse can be defined by the maximum element of an inverse image of a principal down-set under the pre-order, so that given the duality-based translation the inverse translation can be uniquely determined.
As a by-product of this project, we have introduced a new type system, as far as we know, called an existential calculus. This calculus models abstract data types and has a Galois connection to polymorphic lambda-calculus. We hope that revealing the fundamental property of the calculus gives a new and interesting viewpoint to calculi involving polymorphic calculus as a subsystem.
|
Report
(3 results)
Research Products
(11 results)
