プログラム・チェッカーに関する基礎的研究

点击翻译按钮获取中文摘要

静的なプログラム・チェッカーが構成可能な関数fのクラスは,"関数制限対話型証明"を用いることで特徴付られることが知られている.この特徴付けは,関数fに対するプログラムP_fが静的に動作するという条件に強く依存しており,同様な方法でこれを動的なプログラム・チェッカーが構成可能な関数fのクラスの特徴付けに拡張することは極めて困難である.そこで我々は,動的なプログラム・チェッカーが構成可能な関数のクラスを特徴付けるために,(1)最も自然な計算モデルとして"競合的対話型証明"を取り上げ;(2)競合的対話型証明を"関数型"競合的対話型証明に変換する手法-より具体的には,競合的対話型証明における証明者が言語Lに問い合わせる質問を検証者に代行させ,証明者は言語Lの所属問題のみに対してその解を返すというプロトコル変化-を開発した.そしてこの関数型競合的対話型証明を用いることで,動的なプログラム・チェッカーが構成可能な言語Lのクラスは,言語Lとその補言語L^^-がともに関数型競合的対話型証明を持つことであることを明らかにした.ここで,静的なプログラム・チェッカーを持つことが動的なプログラム・チェッカーを持たない関数fの存在が考えられることから,そのような関数fに対して動的なプログラム・チェッカーが構成可能となるような新しい計算モデル-関数fに対する動的なプログラムP_fのコピーをk【greater than or equal】2個用意し,関数fに対するプログラム・チェッカーC_fがそのk【greater than or equal】2個のプログラムP_fをサブルーチンとする-を導入した.そしてこのモデル上で,動的なプログラム・チェッカーが構成可能な言語のクラスの特徴付け-(3)全ての静的なプログラム・チェッカーが構成可能な言語に対して,k【greater than or equal】2個のプログラムを持つ動的なプログラム・チェッカーが構成可能であること;(4)関数fに対し,k【greater than or equal】2個のプログラムを持つ動的なプログラム・チェッカーC_f存在するならば,2個のプログラムを持つ動的なプログラム・チェッカーC'_fが存在すること-を与え,上記のモデルの