形式言語と数理論理学

機械学習技術 Clojure デジタルトランスフォーメーション技術 人工知能技術 セマンティックウェブ技術 オントロジー技術 確率的生成モデル サポートベクトルマシン スパースモデリング トピックモデル Python  プログラミング技術 深層学習 自然言語処理 ITシステム 機械学習における数学 本ブログのナビ

形式言語と数理論理学

以前述べたプログラミング言語は、形式言語と呼ばれる言語の一種となる。形式言語とは、もとになる記号の集合（アルファベット等）と，生成規則（文法）から，生成することの出来る文字列（言葉）の集合をいい、数理論理学と呼ばれる数学が理論的基盤となる。

数理論理学は数学の基礎となるもので、集合論や証明論等を用いて数学のありとあらゆるものを定義したり証明したりする学問である。有名なものではZFC公理系を用いた古典数学体系の証明などがある。ここで行われていることは大雑把に言うと、基本パーツを定義して、それらを組み合わせて、大きな世界を構築していくことになる。

これを言語の世界に適用すると、記号の集合と生成規則(文法)を定義して、文字列(言葉)を生成することになる。実際のプログラミング言語の例では、例えばLISP言語において、Y Combinatorを創立したことでも有名なポール・グレアムによる古典「onLISP」の中で、少数の関数(単語)をベースに残り全ての関数(LISPにおけるプログラミング言語)が構築できることが述べられている。

ON LISP

言語には、構造を生成する「シンタックス」と意味を評価する「セマンティクス」がある。前述の例は主に言葉を形作る「シンタックス」の話になる。後者の「セマンティクス」を考える学問としては「意味論」があり、数理論理学での意味論は命題(言っていること)が真であれば意味があるとの定義で議論が進められている。

意味論での「あるものが真かどうか」というイメージと、現実世界での「意味」と言う言葉が持つイメージとの間にギャップがあり、しばらく違和感を感じていた。実際に、「意味がある」と言う言葉を辞書で引くと「物事を行うことが自分にとってためになる」「物事が重要性を持っているさま」「それを行うことに一定の価値があるさま」となり、数理論理学の意味である「それが真であるかどうか」とは異なる意味を持つことが分かる。両者は全く同じものではないが、「ためになる」とか「重要性を持つ」とか「価値がある」と言うものと「それが真である」との間には後者が前者の前提になると言うこともでき、これでイメージギャップのもやもやは少し収めることができた。

プログラミングの意味論の参考書としては横内寛文氏による「プログラム意味論」がある。目次としては、第1章 表示的意味論の考え方、第2章 ラムダ計算の基礎、第3章 領域理論の基礎、第4章　関数型言語の意味論、第5章 カテゴリ理論の基礎、第6章 領域方程式、第7章 ラムダ計算の意味論となっており、少し古い本だが、ラムダ計算やカテゴリ理論等のLISPの本を読んでいても現れる理論の基礎が学べる。

更に深く意味論に入るには、吉本啓氏、中村裕昭氏による「現代意味論入門」もおすすめだ。こちらは目次としては、第1章 イントロダクション、第2章 意味論の道具箱—集合と関数、第3章 命題論理、第4章 述語論理、第5章 句構造文法，カテゴリー文法およびタイプ理論、第6章 内包論理と可能世界意味論、第7章 モンタギュー意味論、第8章 ダイナミック意味論、第9章 おわりにとなっており、数理論理の基礎的なところから、論理学者ソール・クリプキが高校生の頃に思い付いた様相論理の意味論である可能世界意味論、そして最近の理論であるダイナミック意味論まで網羅された内容となっている。

真と偽しかない世界ではなく色々な可能性の世界を仮定して考えればいいよね、と言うクリプキの考え方は、数理論理学の「意味」と、現実世界の「意味」とのギャップを埋めるものとなる。

これらの論理学に関しては”論理学をつくる 第1部論理学をはじめる 読書メモ“等で、更に数学的な基礎としては”集合論の概要と参考図書“に記載している集合論、あるいは”構造とアルゴリズムと関数“で述べている代数学等も参照のこと。

以前紹介したClojureを使ったプログラミングを選択しているのは、LISPがこれらの数学的な理論の裏付けのある言語であるからと言う理由もある。人工知能のゴールの一つであるプログラムの自動生成を考える際に、「シンタックス」側のアプローチはLISPを使うことでの実現手段がイメージできるが、それに密接に関係する「セマンティクス」のアプローチは未だ十分にイメージできていない。今後もそれらに関しては考えていければと思う。

次回は形式言語とは対極にある自然言語処理について述べてみたい。