シーケント計算に基づく型システムの研究

基于序贯演算的类型系统研究

• 批准号: 17700003
• 负责人: 菊池 健太郎
• 金额: $ 0.64万
• 依托单位: Tohoku University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Young Scientists (B)
• 财政年份: 2005
• 资助国家: 日本
• 起止时间: 2005 至 2006
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-17700003/
• 关键词: シーケント計算; カット除去手続き; カリーハワード対応; 合流性; 強正規化性; ラムダ計算; 明示的代入計算; 完全性; 数理論理学; プログラム理論

昨年度までの研究によって,古典論理の自然演繹における正規化手続きとシーケント計算におけるカット除去手続きの対応関係を明らかにすることができた.これを利用して,古典論理に対して,強正規化性と合流性をみたす局所ステップカット除去手続きを提案した.この結果は,国際ワークショップ(CL＆C'06)で発表し,現在,学術雑誌に投稿中である.一方,直観主義論理に対する通常のシーケント計算において,自然演繹の正規化手続きがどのようなカット除去手続きに対応するのかについても明らかにした.これにより,シーケント計算に対する項計算は,項構造と簡約関係の双方についてラムダ計算の保存拡大であることが明らかになった.この結果は,国際会議(LPAR'06)で発表した.このカット除去手続きは合流性をみたさないが,ラムダ計算のベータ簡約を模倣する能力を保ちつつ制限を加えたカット除去手続きの合流性を証明した.この結果は,国際会議(CiE'07)で発表する予定である.さらに,直観主義論理のシーケント計算から得られる項計算に対して,インターセクション型システムを定義し,その型付け可能性によって強正規化性を特徴づけることができることを示した.そこで用いられる手法は,従来知られていた明示的代入計算とインターセクション型に関する手法を大幅に簡略化したものである.この結果は,国際会議(RTA'07)で発表する予定である.この他,直観主義論理のクリプキ意味論を一般化することによって得られる様々な論理の述語拡大に対して,ツリーシーケント計算の手法を用いて完全性を証明した.この結果は,国際会議(TABLEAUX'07)と国際学術雑誌(Logic Journal of the IGPL)で発表する予定である.

通过去年的研究，我们已经弄清楚了经典逻辑中自然演绎中的归一化过程与序贯微积分中的切除去除过程之间的对应关系，我们提出了满足汇合的局部逐步切除去除过程。这个结果是。在国际研讨会 (CL&C'06) 上发表，目前正在提交给学术期刊。我们还澄清了自然演绎的归一化过程对应于普通序贯计算中的哪种割除过程。因此，序贯计算的项计算可以使用 lambda 计算来进行项结构和约简关系。这个结果是。在一次国际会议（LPAR'06）上宣布。虽然这种割除过程不满足汇合，但可以保留和扩展 lambda 演算。我们已经证明了删除过程的汇合，该过程在添加限制的同时保持了模拟数据缩减的能力。该结果将在国际会议（CiE'07）上展示。此外，从直觉逻辑的顺序演算我们定义了一个。交集类型系统用于所得项计算，并表明强标准化性可以通过其可打字性来表征。这是一种大大简化的计算赋值和交集类型的方法。结果将在国际会议（RTA'07）上公布。此外，我们将推广直觉逻辑的Kripke语义。我们使用树顺序计算方法来证明。得到的各种逻辑谓词扩展的完整性IGPL 杂志）。

项目成果

On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus

直觉序贯演算的局部步割消法

• 发表时间: 2006
• 期刊: Lecture Notes in Computer Science Vol. 4246
• 作者: Muraoka N;Shum L;Fukumoto S;Nomura T;Ohishi M;Nonaka K.;Kentaro Kikuchi
• 通讯作者: Kentaro Kikuchi

Call-by-Name Reduction and Cut-Elimination in Classical Logic

经典逻辑中的直呼名字减少和剪切消除

• 发表时间: 2006
• 期刊: Proceedings of the 1st International Workshop on Classical Logic and Computation
• 作者: Muraoka N;Shum L;Fukumoto S;Nomura T;Ohishi M;Nonaka K.;Kentaro Kikuchi;Kentaro Kikuchi
• 通讯作者: Kentaro Kikuchi