权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

古典論理に基づく計算系とその性質の検証

基于经典逻辑的计算系统及其属性的验证

基本信息

批准号：
17K00005
负责人：
桜井貴文
金额：
$ 2.5万
依托单位：
Chiba University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2017
资助国家：
日本
起止时间：
2017-04-01 至 2024-03-31
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-17K00005/
关键词：
古典論理ラムダ計算 α同値証明検証系 minlog 直観主義論理数理論理学検証

项目摘要

本研究の目的は古典論理に基づくの計算系に関する様々な性質を研究することであるが、本研究代表者は、これまでの研究で古典論理の計算系を型付ラムダ計算に翻訳する新しい変換を考え、その変換が簡約を保存するという性質を持つことを示した。具体的には、古典論理の計算系 lambda-bar-mu やその変種の lambda-bar-mu-tilde-CBN を lambda-conj-neg に翻訳する変換および lambda-conj-neg を型付ラムダ計算に翻訳する簡単な変換を考え、それらの変換を合成することで新しい変換を得ることができた。本研究では、それらの古典論理の計算系から型付ラムダ計算への翻訳に関する性質を計算機上の証明検証系で証明することを最初の目標としており、そのためにminlogという証明検証系を使っている。本研究代表者は平成29年度に開始した「クラス理論に基づく自己拡張可能なソフトウェア検証体系の深化」(代表者:佐藤雅彦)という科研費の研究課題の分担者になっていたが、その研究課題では、ラムダ計算を改良・発展させた計算系を開発するためにminlogを使ってその計算系の性質を証明している。さらにその研究課題ではminlogを使ってその計算系と伝統的ラムダ計算の関係を明かにした。伝統的ラムダ計算は古典論理の計算系 lambda-bar-mu に含まれるので、その研究で開発している技術は本研究に応用できるという見込みの下にその分担研究課題に取り組んだ。令和3年度までに伝統的なラムダ計算について様々な性質を証明してきて一段落したと思ったが、令和4年度にα簡約が同値関係になるというよく知られた定理に新しい証明があることに気付き、その証明に取り組むことに注力した。

The purpose of this study is to study the properties of classical logic computing system, and to demonstrate the properties of classical logic computing system. The specific classical logic calculation system lambda-bar-mu-tilde-CBN lambda-conj-neg is transformed into lambda-conj-neg. The classical logic calculation is transformed into lambda-bar-mu-tilde-CBN lambda-conj-neg. In this paper, the classical logic calculation system is studied from the type of calculation to the nature of the proof system on the computer. The representative of this research began in the 29th year of Heisei to "deepen the verification system based on the theory of Kourasi and expand the possibilities of it"(representative: Masahiko Sato). Ito is a contributor to the research project of scientific research funding, and his research topic is to prove the nature of the computing system by improving and developing the computing system. The research topic of this paper is to clarify the relationship between computing system and computing system. The classical logic calculation system lambda-bar-mu contains the following research topics: In the third year of the order, the calculation of the system was carried out, and the property was proved. In the fourth year of the order, the α reduction was carried out, and the same value relationship was carried out. In the fourth year, the theorem was proved.

项目成果

期刊论文数量（0）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Polymorphic computation systems: Theory and practice of confluence with call-by-value

多态计算系统：按值调用融合的理论与实践

DOI：
10.1016/j.scico.2019.102322
发表时间：
2020
期刊：
Science of Computer Programming
影响因子：
1.3
作者：
Makoto Hamana;Tatsuya Abe;Kentaro Kikuchi
通讯作者：
Kentaro Kikuchi

Parallel Closure Theorem for Left-Linear Nominal Rewriting Systems

左线性标称重写系统的并行闭包定理

DOI：
10.1007/978-3-319-66167-4_7
发表时间：
2017
期刊：
Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017)
影响因子：
0
作者：
Kentaro Kikuchi;Takahito Aoto and Yoshihito Toyama
通讯作者：
Takahito Aoto and Yoshihito Toyama

無限のデータを含む等式に対する帰納的定理証明

涉及无限数据的方程的归纳定理证明