Welcome to Yamagu's Research Page
| |
 | |
論理系と計算機および推論について論理は思考を形式的に表現する方法である。 つまり、ものごとの関係などのさまざまな言明を、 ある規則にしたがって記号で表現する方法である。 言明を表現した上で、この表現をある規則にしたがって変形することで、 もとの言明から導かれる別の言明の表現を得ることができる。 これは「Aが正しければBが正しい」という理性的な思考を、 記号の変形によって表現しているともいえる。論理に見られるような記号の規則的な変形は、計算機を使って行うことができる。 これは、思考する機械を作ることができそうであるという期待につながり、 人工知能の分野では古くから自動推論や自動証明が研究されてきた。 また、論理における証明とプログラムが似た構造を持つことが知られている。 これは Curry-Howard 同型対応と呼ばれる性質である。 ある性質を持った値が存在することの構成的な証明には、 そのような値を具体的に計算するプログラムが対応するのである。 このことから、論理式が正しいことを自動的に証明する機械は、 プログラムを自動的に作り出すことができると期待できる。 さて、ものごとの因果関係を、「前提」と「規則」と「結果」の関係であると考えよう。 「前提が成り立っているとき、規則を適用すると、結果が得られる」という関係である。 この三つのうちの二つが分かっているとき、 残りの一つを導き出す思考過程を推論と呼ぶことにする。 すると、推論には三種類あることになる。 この三種類のうち、規則を導き出そうとする推論を、帰納推論と呼ぶ。 帰納推論は、学習の基礎であり、自然科学の方法論でもある。 線形論理上の帰納推論論理というと、数学の基礎となっている論理体系のことを指すことが多い。 数学的に厳密な言明は、正しいか正しくないかのどちらかであって、 そのような正しさについての形式的な体系が、いわゆる論理（古典論理ともいう）である。 しかし古典論理とは異なる正しさの表現を対象とするさまざまな論理体系が発明されている。 線形論理はその一つで、substructural logic と呼ばれるものの先駆けである。線形論理は、論理式が増減するような推論規則を制限しており、 論理式の個数に意味がある論理系となっている。 線形論理の論理式には、標準形を定義することが難しく、 推論を行うアルゴリズムには標準形を使わずに推論をする工夫が必要となる。 線形論理式の部分式を変形することで、標準形を使わずに、 帰納推論を行う方法を提案する研究を行った。 また、線形論理の式の意味を多重集合の集合で与え、その意味論の上で、 提案アルゴリズムが正しい帰納推論をすることを示した。 これらの研究は、International Journal of Theoretical Physics や、 人工知能学会誌に掲載された。 プロセス代数式の帰納合成プロセス代数というのは、 並列または並行に実行されるプログラムやその動作を形式的に表現した系で、 二つのプロセスの動作が等価であることを証明できる記述力などを持っている。 このような代数系で対象（プロセス）を表現するプロセス代数式は、 並行に動作するプログラムの骨格を表していると言える。線形論理の論理式とプロセス代数式、線形論理の証明とプロセス代数の計算が、 それぞれ対応することが知られている。そこで、 論理式を作り出す推論を自動的に行うことで、 プロセス代数式（すなわち並行計算のプログラム）が作りだせると考えた。 線形論理とプロセス代数の対応関係から、線形論理上の帰納推論は、 プロセスの振舞いからプロセス代数式を推定することに対応すると分かる。 帰納推論は、古典的には、可能な式をすべて数え上げることで定式化されてきたが、 論理式の伴意関係を参考にすることで、 数え上げるべき式の個数を大幅に減らすことができる。 このような推論の効率化は、 帰納論理プログラミングという分野で盛んに研究されており、 プロセス代数式の帰納合成にも同様の考え方が使えることを示す研究成果となった。 線形論理上の帰納推論関連研究発表
参考文献
|
