6 0 0 0 OA 線形論理の誕生
- 著者
- 照井 一成
- 出版者
- 一般社団法人 日本数学会
- 雑誌
- 数学 (ISSN:0039470X)
- 巻号頁・発行日
- vol.62, no.1, pp.115-132, 2010 (Released:2013-06-01)
- 参考文献数
- 6
6 0 0 0 OA 素朴集合論とコントラクション
- 著者
- 照井 一成
- 出版者
- 日本科学哲学会
- 雑誌
- 科学哲学 (ISSN:02893428)
- 巻号頁・発行日
- vol.36, no.2, pp.49-64, 2003-12-30 (Released:2009-05-29)
- 参考文献数
- 13
It is observed by Grishin that inconsistency of naive set theory can be avoided by restricting the logical law of contraction, as it is contraction that enables us to derive logical inconsistency from set-theoretic paradoxes such as Russell's paradox.In this paper, we examine Grishin's contraction-free naive set theory to better understand Russell's paradox and the naive comprehension principle from a purely formal standpoint. We study both static-propositional and dynamic-procedural aspects of naive comprehension and argue that it could lead to an ideal formalization of (part of) mathematics, where both propositional knowledge (theorems) and procedural knowledge (algorithms) reside in harmony.
1 0 0 0 充実期を迎えた線形論理の進化とその応用に関する研究
次の3点を中心に研究を進めた。1.証明論と意味論の統合的見方について研究を進めた。カット消去定理等の証明論の基本定理の成立条件がPhase semanticsによる意味論的分析により明らかになることを示した。又、Simple logic等の線形論理の基礎理論に対して、証明論と意味論の統合を進めた。さらに、直観主義論理Phase semanticsと古典論理Phase semanticsとの密接な関係を明らかにした。Phase semanticsの成果に基づいてカット消去定理の意味論的条件の研究を進めた。2.Reduction Paradigmによる計算モデルとProof-Search Paradigmによる計算モデルを統一的に分析できる論理的枠組の確立に向けた研究を進めた。ゲーム論的意味論等の観点からの分析も加えた。(岡田・Girard等フランスグループとの共同研究)これまでのReduction Paradigm(関数型言語の論理計算モデル)とProof-Search Paradigm(論理型言語や証明構成の計算モデル)の内的な統合を可能にするLudics等の新たな論理体系理論の分析をGirardグループらと共同で行なった。3.線形論理的概念がプログラミング言語理論やソフトウェア形式仕様・検証理論、計算量理論等にどのように応用され得るかのケーススタディーを行なった。例えば昨年に引き続き、ダイナミック実時間システムのシステマティックな設計・検証や認証プロトコル安全性証明等を例にとり、線形論理的観点や手法の応用可能性を示した。この目的でフランス及び米国共同研究グループとの共同研究を行なうとともに、計3回の成果報告会を日仏共同で行った。
1 0 0 0 構成的集合と余帰納的定義を用いたプログラム合成
本研究の目的は、構成的集合と余帰納的定義をもつ構成的論理を構築し、この論理体系を用いて、余帰納型を用いたプログラムの性質を明らかにし、また、構成的集合と余帰納的定義を用いたプログラム合成システムを試作することであった。次のような3つの研究成果を得た。(1)論理式Aが長D-正規証明をもつならば、Aの長正規証明が唯一であることを証明した。(2)古典二階自然演繹の強正規化可能性の証明に関して、CPS変換を用いた従来の証明が本質的誤っていることを主補題に対する反例をあげて示し、この原因が継続消滅の現象によることを指摘し、オグメンテーションの概念を用いてこの証明を完成させた。例外処理ラムダ計算や値呼びラムダミュー計算など他の類似の体系のCPS変換を用いた強正規化可能性の従来の証明が、継続証明により同様にして本質的に誤っていることを指摘した。(3)構成的二階自然演繹に置換簡約を追加した論理体系の強正規化可能性の簡明な証明を与えた。従来知られている証明は、Prawitzによる証明だけであり、これは記述が不完全であり、また複雑な帰納法を必要とした。原子選言論理のアイデアを用い、構成的二階自然演繹に置換簡約を追加した論理体系が原子選言論理に簡約を保存して翻訳できること、原子選言論理は飽和集合が定義でき飽和集合を用いた強正規化可能性の証明方法が使えることの2つから、新しい簡明な証明を得た。