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

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

• 批准号: 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)というシステムとして実現している.これらを実際に使用した経験を基にして,本年度は単純表現理論を改良し,判断と導出の理論を再構築した.単純表現理論は抽象操作と具体化操作を備えた構造を持っているが,具体化操作は束縛変数の名前替えなしで行なわれ,環境の概念を拡張することによりその操作を簡潔に定義できることが特徴となっている.またこの単純表現理論はアリティという概念を持っているが,本年度は,それをさらに改良し,カテゴリーという概念を導入した.アリティは引数の個数を高階にしたものに相当する概念であるが,カテゴリーは引数の種類を高階にしたものに相当する概念であり,より豊富な数学の概念を表現できるようになった.また,単純表現理論をさらに拡張するときには,明示的代入を導入するのが自然である.しかし,明示的代入を有効に活用するには従来の合成規則では不十分であるので,明示的代入の合成規則を拡張する研究も行ない,これまでの合成規則ではできなかったメタレベルでの代入が体系内で実現でき,その強正規化性も証明した.

The purpose of this study is to describe the system of mathematics in the form of mathematics, which is the most important thing in this study. in this study, in the form of mathematics, which is in the form of mathematics, which is the most important thing in this study. On the basis of the mathematical theory, we can find out the record of the mathematics, and then we can get the definition of the definition in the theory group. The theory theory, the theory, the theory. The emacs lisp on the computer makes it possible for the computer to analyze the CAL, analyze the data, and determine the NF (Natural Framework). The international community is using information technology. This year, the table will be improved to determine whether the theory will be developed again. In the form of a table, abstract operations, specific operations, equipment, abstract operation, specific operation, specific operation, and environmental protection. In the course of this year, we will improve the concept of improvement and improve the concept of improvement. In terms of the number of arguments, the number of arguments, the concept of mathematics, mathematics. Please indicate that the theory is correct, that is, the explicit substitution of the word into the box is due to the nature. In this case, the explicit substitution has the ability to use the synthesis rules to improve the performance of the synthesis rules, the explicit substitution of the synthesis rules, the rules, the rules.

项目成果

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

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

• 发表时间: 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)
• 作者: 中澤 巧爾;龍田 真;佐藤 雅彦
• 通讯作者: 佐藤 雅彦