「再帰的定義を可能にする述語論理の証明支援系上の実装」

情報処理学会 第68回プログラミング研究会（＠日本IBM東京基礎研究所）で、上記の題で発表をすることになりました。3月17日（月）14:15-15:00の予定です。内容は業務研究の成果報告で、知識様相論理の充足関数を証明支援系に実装するさいの問題点を解決したという話です。要旨は以下の通り。

型付けを持つ証明支援系において、任意有限個の変数を持つ述語を含み、さらに量化子による変数の束縛が可能となる形式的体系（データ型やデータ構造）を定義することが困難であることはよく知られている。さらに、束縛された変数への具体的な値を代入する操作を証明支援系が解釈することにも困難が伴う。そのため、量化子を含む論理式によって関数を再帰的に定義しようとして、たとえそれが人間の目には十全な定義であっても、証明支援系はその関数の停止判定に失敗することが起こる。

本発表では、Martin-Lofの直観主義的型理論に基づいた厳格な型付けを持つ証明支援系Agda上で以上の点を解決した述語論理の実装例を紹介する。この例においては、多変数述語の実装は、依存型理論(dependent type theory)を使用した。すなわち、自由変数の個数と、そのうちの束縛された変数の個数を、同時に型に情報として含むように、多変数述語のデータ型を定義した。また、束縛された変数の個数の上での帰納法により、知識様相述語論理の充足関係を関数として定義した。このことにより、関数定義が明示的に有限回で停止することを証明支援系に理解させることができ、関数の停止判定に成功した。