2004 Fiscal Year Final Research Report Summary
| Project/Area Number |
15500003
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
HASEGAWA Ryu The University of Tokyo, Graduate School of Mathematical Sciences, Assistant Professor, 大学院・数理科学研究科, 助教授 (20243107)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
HASEGAWA Masahito Kyoto University, Research Institute for Mathematical Sciences, Assistant Professor, 数理解析研究所, 助教授 (50293973)
|
|---|
| Project Period (FY) |
2003 – 2004
|
| Keywords | categorical semantics / linear logic / weak normalization / lambda calculus |
|---|
| Research Abstract |
We interprets categorical semantics of the intuitionistic linear logic as a reduction system. The categorical semantics is a basic machinery providing a mathematical support to the theory of typed lambda calculi. In effect, the calculi and the semantics are equivalcot in a suitable sense, and this well-known observation has yielded a number of fruitful results. The equivaleces is, however, achieved only if the reduction rules of the lambda calculus are viewed as equational rules. Namely, the reduction rules should be regarded as static rules if we want to have the equivalence. We conjecture that the equivalence remsins to hold if the reduction rules are regarded to be dynamic, that is, operational. But this approach faces difficulties if we stick to the typed lambda calcules.Therefore we switch to the intuitionistic liner logic, which is a refinement of the typed lambda calculus. We adopt the semantics by Ristmann et al.as the categorical semantics of the intuitionistic linear logic. We introduce reduction rules on the commutative diagrams occurring in the semantics. We observed the connection between the reduction rules on the categorical semantics and the corresponding operations on the intuitionistic linear logic. Toward appropriateness of the reduction system on the categorical semantics, we attempt to verify the Church-Roaser property and the normalization property. These properties are expected since they hold for many systems of the type theory. So far, as a partial result, we verified the weak normalization property. The intuitionistic linear logic is designed on the same basis as the computational model oriented to reflect implementation details, such as the explicit substitution and the Lamping graph. We compared our reduction system to these.
|
