2003 Fiscal Year Final Research Report Summary
Calculi and Logic of Environment and Context
| Project/Area Number |
13480082
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
SATO Masahiko Kyoto University, Graduate School of Informatics, Professor, 情報学研究科, 教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
NAKAZAWA Koji Kyoto University, Graduate School of Informatics, Research Associate, 情報学研究科, 助手 (80362581)
IGARASHI Atsushi Kyoto University, Graduate School of Informatics, Lecturer, 情報学研究科, 講師 (40323456)
|
|---|
| Project Period (FY) |
2001 – 2003
|
| Keywords | Object Language / Meta Language / Syntactic Object / Meta Variable / Variable Collision / Context |
|---|
| Research Abstract |
The aim of this research project was to construct calculi containing environments and contexts as first-class objects, and to study these calculi from a logical point of view. The main results are summarized as follows.
・Calculi of first-class environments and contexts
We have developed calculus systems of environments and contents. Though environments and contexts are notions outside a formal system, we can handle environments and contexts as first-class objects in these systems. We have constructed the systems as formal type systems, and proved subject reduction, confluence, strong normalizability and conservativity of the systems.
・Calculi of meta-variables
We have developed calculus systems of meta-variables. In these systems, each variable is given a level, which classifies variables into object variables (level 0), meta-variables (level 1), metameta-variables (level 2) and so on. By this notion of level, we can treat textual substitution in these systems, and express insertion of programs into holes of contexts, which may generate new variable binding. We have shown that these systems also can express composition of contexts, which the systems above cannot. We have also proved subject reduction, confluence and strong normalizability. of the systems of meta-variables.
|
