変数の動的束縛機構をもつ新しいソフトウェアの理論的研究

动态变量绑定机制的新软件理论研究

• 批准号: 16016245
• 负责人: 佐藤 雅彦
• 金额: $ 3.84万
• 依托单位: Kyoto University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research on Priority Areas
• 财政年份: 2004
• 资助国家: 日本
• 起止时间: 2004 至 2005
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-16016245/
• 关键词: 表現理論; 抽象操作; 具体化操作; α同値性; 判断; 導出; 明示的代入; 合成規則; 表現の理論; 変数参照; Natural Framework

本研究は何年かに渡って継続して行っているが,その最終的な目標は数学を形式的に記述するための体系を構築することであり,そのためにいくつかの層に分けて理論を構築している.一番上のレベルである数学(特に論理および計算)の理論は導出ゲームという形で記述し,その導出ゲームは判断と導出の理論という枠組の中で定義されている.そしてその判断と導出の理論は単純表現理論という理論を使って定義されている.これらの理論は計算機上でemacs lispを使ってインプリメントしており,単純表現理論はCAL,判断と導出の理論はNF(Natural Framework)というシステムとして実現している.これらを実際に使用した経験を基にして,本年度は単純表現理論を改良し,判断と導出の理論を再構築した.単純表現理論は抽象操作と具体化操作を備えた構造を持っているが,具体化操作は束縛変数の名前替えなしで行なわれ,環境の概念を拡張することによりその操作を簡潔に定義できることが特徴となっている.またこの単純表現理論はアリティという概念を持っているが,本年度は,それをさらに改良し,カテゴリーという概念を導入した.アリティは引数の個数を高階にしたものに相当する概念であるが,カテゴリーは引数の種類を高階にしたものに相当する概念であり,より豊富な数学の概念を表現できるようになった.また,単純表現理論をさらに拡張するときには,明示的代入を導入するのが自然である.しかし,明示的代入を有効に活用するには従来の合成規則では不十分であるので,明示的代入の合成規則を拡張する研究も行ない,これまでの合成規則ではできなかったメタレベルでの代入が体系内で実現でき,その強正規化性も証明した.

这项研究已经持续了好几年，最终目标是构建一个形式化描述数学的系统，为此，我们将理论分为几个层次的数学（特别是逻辑和计算）。 ）以推导博弈的形式进行描述，推导博弈是在判断和推导理论的框架内定义的。判断和推导理论是使用简单表示论的理论来定义的，这些理论可以用于。使用 emacs 的计算机。使用lisp实现，简单表示理论为CAL，判断推导理论为NF（Natural基于实际使用这些系统的经验，今年我们改进了简单表示论，重建了判断和推导的理论。简单表示论是基于抽象运算和具体的具有运算的结构，但具体化运算是边界。它的特点是不需要重命名变量，并且可以通过扩展环境的概念来简洁地定义其操作。此外，这个简单的表示理论有元数的概念，今年我们将重点关注这个概念。我们进一步改进了这一点并引入了类别的概念。属性是对应于高阶数的参数的概念，而类别是对应于高阶参数类型的概念，并且在扩展时可以表达更丰富的数学概念。简单表示论更进一步，有必要引入显式赋值。然而，由于传统的组合规则不足以有效地利用显式赋值，我们还进行了研究以扩展显式赋值的组合规则，并且能够做到以前的元级替换规则无法做到的事情。可以在系统内实现，并且其强大的规范性也得到了证明。

项目成果

選言を含む自然演繹古典論理の強正規化性

包括析取在内的自然演绎经典逻辑的强规范化

• 发表时间: 2006
• 期刊: 第8回プログラミング言語およびプログラミング言語ワークショップ(PPL2006)論文集
• 作者: 中澤 巧爾;龍田 真
• 通讯作者: 龍田 真

Axiomatizing Higher Level Delimited Continuation

公理化更高层定界延拓

• 发表时间: 2004
• 期刊: Proc. ACM SIGPLAN Workshop CW'04
• 作者: 中澤 巧爾;龍田 真;佐藤 雅彦;Masahiko Sato;Yukiyoshi Kameyama
• 通讯作者: Yukiyoshi Kameyama

Axioms for Delimited Continuations in the CPS Hierarchy

CPS 层次结构中定界延续的公理

• 发表时间: 2004
• 期刊: Proc. Computer Science Logic 2004,LNCS 3210
• 作者: 中澤 巧爾;龍田 真;佐藤 雅彦;Masahiko Sato;Yukiyoshi Kameyama;Yukiyoshi Kameyama
• 通讯作者: Yukiyoshi Kameyama

Axioms for Control Operators in the CPS Hierarchy

CPS 层次结构中控制运算符的公理

• 期刊: Higher-Order and Symbolic Computation (to appear)
• 作者: 中澤 巧爾;龍田 真;佐藤 雅彦;Masahiko Sato;Yukiyoshi Kameyama;Yukiyoshi Kameyama;Yukiyoshi Kameyama
• 通讯作者: Yukiyoshi Kameyama

フレーゲの計算機科学への影響

弗雷格对计算机科学的影响

• 发表时间: 2005
• 期刊: 科学哲学 38(2)
• 作者: 中澤 巧爾;龍田 真;佐藤 雅彦
• 通讯作者: 佐藤 雅彦