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）。

Atsushi Igarashi, Naoki Kobayashi: "A Generic Type System for the Pi-Calculus"TCS. Vol.311(1-3). 121-163 (2004)

Atsushi Igarashi、Naoki Kobayashi：“Pi 微积分的通用类型系统”TCS。