5 0 0 0 OA 文脈自由言語と超決定性言語の包含判定問題の決定可能性の型理論を用いた証明
- 著者
- 塚田 武志 小林 直樹
- 雑誌
- 情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)
- 巻号頁・発行日
- vol.4, no.2, pp.31-47, 2011-03-25
言語の包含判定問題とは,与えられた言語 L1 と L2 について L1 ⊆ L2 が成立するか否かを判定する問題であり,理論的な興味の対象であるだけでなく,プログラム検証などへの広い応用を持つ重要な問題である.この問題に関する既知の最も強い結果の 1 つが文脈自由言語と超決定性言語の包含判定の決定可能性である.このオリジナルの証明は,Greibach と Friedman によって与えられている.我々はこの問題に対して,小林らによって提案されている型に基づく言語の包含判定の手法を適用し,決定可能性に対する別証明を与えた.この手法は以下のような利点を持つ.(1) 部分型関係やポンプの補題などのよく知られた概念で理論が展開できる.(2) 型推論を効率的に行う方法は多数提案されており,それらを利用することができる.また,提案する証明は小林らのアイデアを正規言語よりも広いクラスに適用したはじめての例であり,その他の非正規言語クラスへの応用も期待される.
4 0 0 0 数学の自動化を推進するための機械学習を用いた定理自動証明手法
数学における証明のを計算機を用いて一部自動化することを目指します.本申請課題は,この最終目標に対する探索研究として,自然数に関する命題の証明の一部自動化を目指します.本申請課題では,証明が二者ゲームとして定式化でき,したがってゲーム AI の学習手法を証明ゲームに適用することで有能な自動証明アルゴリズムを錬成できるのではないか,というアイデアに基づいて研究を進めます.自動証明は様々なシステムが意図通りに動作することを保証するための要素技術として用いられており,その点で将来的に産業的なインパクト・貢献の可能性が期待できると考えています.
1 0 0 0 機械学習技術による高速な演繹的推論エンジンの開発
本研究では,近年著しい発展を遂げている機械学習技術を数理論理学的な問題に応用して,高効率な演繹的推論エンジンを構成することを目指す.機械学習技術は画像認識やゲームAIを含む様々な分野で著しい成功を遂げているが,証明などの演繹的推論が関わる分野には未だに古典的な演繹的推論技術が機械学習技術に優位である問題が多い.これまでの研究では解きたい問題を直接解く機械学習モデルを作る End-to-End の方法が主流であったが,本研究では解きたい問題ではなく機械学習に適した問題を学習させて,学習結果を演繹的推論エンジンで活用する.
1 0 0 0 OA AI時代を見据えたプログラム検証技術
プログラム検証とは、プログラムが正しく振る舞うかどうかを実行前に網羅的に検証する技術であり、ソフトウェアの信頼性向上のために欠かせないものである。本研究課題では、近年の機械学習技術の台頭とそれに伴うコンピュータによって制御されたシステムの社会への普及を踏まえ、(1)代表者らがこれまで研究を進めてきた高階モデル検査などの自動プログラム検証技術や理論をさらに発展させるとともに、(2)プログラム検証技術のさらなる飛躍のために機械学習技術を活用し、さらに(3)機械学習技術の台頭に伴うソフトウェアの質と量の変化に対応するための、新たなプログラム検証技術の確立を目指す。
- 著者
- 塚田 武志 小林 直樹
- 出版者
- 情報処理学会
- 雑誌
- 情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)
- 巻号頁・発行日
- vol.4, no.2, pp.31-47, 2011-03-25
言語の包含判定問題とは,与えられた言語 L1 と L2 について L1 ⊆ L2 が成立するか否かを判定する問題であり,理論的な興味の対象であるだけでなく,プログラム検証などへの広い応用を持つ重要な問題である.この問題に関する既知の最も強い結果の 1 つが文脈自由言語と超決定性言語の包含判定の決定可能性である.このオリジナルの証明は,Greibach と Friedman によって与えられている.我々はこの問題に対して,小林らによって提案されている型に基づく言語の包含判定の手法を適用し,決定可能性に対する別証明を与えた.この手法は以下のような利点を持つ.(1) 部分型関係やポンプの補題などのよく知られた概念で理論が展開できる.(2) 型推論を効率的に行う方法は多数提案されており,それらを利用することができる.また,提案する証明は小林らのアイデアを正規言語よりも広いクラスに適用したはじめての例であり,その他の非正規言語クラスへの応用も期待される.The language containment problem, which asks whether L1 ⊆ L2 for given languages L1 and L2, is an important problem in the field of formal language theory and has a variety of applications including program verification. One of the strongest result about this problem is the decidability for the case where L1 and L2 are context free and superdeterministic languages respectively, originally proved by Greibach and Friedman. In this paper, we give a new proof of the decidability, inspired by Kobayashi's type-based approach to language containment problems. The new proof has the following advantages. (1) The key notions and lemmas in the proof are well-known ones, such as subtyping and Pumping Lemma. (2) We can apply well-studied techniques for efficient typability checking. Furthermore, our proof is the first application of the type-based approach to the inclusion between non-regular languages and it seems applicable to other cases.