Calculi and Logic of Environment and Context

环境和语境的演算和逻辑

• 批准号: 13480082
• 负责人: SATO Masahiko
• 金额: $ 4.67万
• 依托单位: Kyoto University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2001
• 资助国家: 日本
• 起止时间: 2001 至 2003
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-13480082/
• 关键词: Object Language; Meta Language; Syntactic Object; Meta Variable; Variable Collision; Context; 環境; 合流性; 強正規化性; 型理論; 計算体系

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 contextsWe 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-variablesWe 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.

本研究的目的是构造包含环境和上下文作为第一类对象的演算，并从逻辑的角度研究这些演算。主要结果总结如下。·第一类环境和上下文的微积分我们开发了环境和内容的微积分系统。虽然环境和上下文是形式系统之外的概念，但我们可以将环境和上下文作为这些系统中的第一类对象来处理。我们将系统构造为形式类型系统，并证明了系统的主题约简、合流、强规范化和保守性。元变量的微积分我们已经开发了元变量的微积分系统。在这些系统中，每个变量都被赋予一个层次，它将变量分为对象变量（层次0）、元变量（层次1）、元变量（层次2）等，通过这个层次的概念，我们可以处理这些系统中的文本替换，并表示程序插入到上下文的空洞中，从而产生新的变量绑定。我们已经证明，这些系统也可以表达上下文的组合，这是上述系统不能表达的。我们还证明了主题的减少，融合和强大的规范化。元变量系统。

项目成果

Azza A.Taha, Masahiko Sato, Yukiyoshi Kameyama: "A Second-order Context Calculus"JSSST Computer Software. 19(3). 2-19 (2002)

Azza A.Taha、Masahiko Sato、Yukiyoshi Kameyama：“二阶上下文微积分”JSSST 计算机软件。

Azza A.Taha: "A Second-order Context Calculus"コンピュータソフトウェア. 19・3. 2-19 (2002)

Azza A. Taha：“二阶上下文微积分”计算机软件 19・3（2002）。

Masahiko SATO, Yukiyoshi KAMEYAMA, TAKEUTI Izumi: "CAL : A computer Assisted Learning System for Computation & Logic"EUROCAST. Lecture Notesin Computer Science. 2178. (2001)

Masahiko SATO、Yukiyoshi KAMEYAMA、TAKEUTI Izumi：“CAL：计算机辅助计算学习系统

Atsushi Igarashi: "A Generic Type System for the Pi-Calculus"Theoretical Computer Science. 311・1-3. 121-163 (2004)

Atsushi Igarashi：“Pi 演算的通用类型系统”理论计算机科学 311・1-163（2004）。

Masahiko Sato, Takafumi Sakurai, Yukiyoshi Kameyama: "A Simply Typed Context Calculus with First-class Environments"Journal of Functional and Logic Programming. Vol.2002, No.4. 1-41 (2002)

Masahiko Sato、Takafumi Sakurai、Yukiyoshi Kameyama：“具有一流环境的简单类型上下文演算”函数与逻辑编程杂志。