| Project/Area Number |
19540145
|
|---|
| 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 | Okinawa Institute of Science and Technology (2008-2009)
Keio University (2007) |
|---|
Principal Investigator |
HAMANO Masahiro Okinawa Institute of Science and Technology, 大学院・情報理工学系研究科, 客員研究員 (50313705)
|
|---|
| Project Period (FY) |
2007 – 2009
|
| Project Status |
Completed (Fiscal Year 2009)
|
| Budget Amount *help |
¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000)
Fiscal Year 2009: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2008: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2007: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
|---|
| Keywords | linear logic / denotational semantics / polarized category / full completeness / relational category / indexed linear logic / polarity / topological semantics / second order linear logic / polarized linear logic / focalization / topological phase space / enriched phase space / interior / closure operators / Indexed linear logic / Relational semantics / Pointed relation / Polarized linear logic / Denotational completeness / Phase semantics / Topological semantics / Second order linear logic / pre*-autonomous category / bimodule / double gluing / Chu space |
|---|
| Research Abstract |
We investigate semantcal structures of computations arising from polarized linear logic. A categorical model is constructed to model computations by employing modules and adjunction between two contravariant categories of dual polarities. To model computability for the second order logic, we accommodate a topological structure for the polarities to a (non-polarized) algebraic semantics. Using the topological semantics, we solve a second order conservation theorem of linear logic over its polarized fragment. To make a relationship between these two kind of semantics of computations and of computability, we present an indexed system for polarized logic and characterize a denotational completeness in terms of the system.
|
