語句の真相とあやまち

なにもないことにまつわるあれこれとか関係のないこととか

そしてResolution

Juliaで論理式を表す方法について、ずっと試行錯誤している。

いまは、parse("[x,y].[+P(x,f(x)),-Q(x,y)]") のようにparse()を使うことにして、Exprベースで式を扱っている。

内部で[x,y] と :([+(P(x,f(x)),-(Q(x,y))] に分けているのだけれど、これも[:(+(P(x,f(x)))), :(-(Q(x,y))]にしたほうがいいかもしれない。

 

Resolutionについては、だいぶ忘れてしまったので、思い出すためにいろいろ調べているけれど、今のAIブームの中では自動証明はほとんど話題になっていないように見える。

 ニューラルネットと自動証明はAIの両輪のような気がするけれど、そうでもないのかもしれない。そもそもAIという言葉も意味不明ではあるけど。

 

話題がそれたので戻すと、unificationはできていて、単体のResolutionもできているはず。

あとはclause集合からcontradictionを導出するtactics/strategyをどうするか・・・

 

まず、命題論理でgoalからの証明の枠組みを作り、一階でその証明にmguが存在するかどうかでステップの刈り込みを行う。

このとき、繰り返される証明ステップパターンが無限の証明になるのをどうするか。

 

これは先の場合と同じく、

  • 世界の事実(Fact)をground unit clauseの集合で表し
  • それに対する仮説(理論, Theory)を変数を含むclauseの集合で表す
  • queryはいまのところunit clauseを想定

というようなもの。

仮説は、すべてのFactについて成立するものを考えているので、少なくとも

Fact + Theory は無矛盾にしたい。これは、Theoryの各clauseをFactに加えたとき矛盾がでないことで分かるが、たぶん有限時間に検証できるだろう。

複数のTheoryの間の矛盾は有限時間では分からないかもしれない。たぶん分からない。

 

 

 

それから Resolutionにいたるまで

JuliaでResolutionをしたいと思っていたのだけれど、式の表現でSymbolを使うといちいち:なんとかと書かなくてはならないことや、Lispだとlistにするところをベクトルにした場合の表現方法などで悩んで、手がつかなかったのが、去年のどこかでそのあたりがわかったので、いろいろとプログラムを作っている。

最初に作ったのは、非常に単純なものというか制限をつけたもので、それがだいたいできた段階で、真面目に1階述語のResolutionを作った。

 

今は、Unit resolutionあるいはLinear Resolutionで証明(あるいは反証)を作るあたりを考えている。

 

最初に作ったものでは

1. 世界の事実を記述したUnit Clauseの集合に対して、Queryとしての論理式が与えられると、その変数に対する代入を解=モデルを求めるというもの。

DBのQueryみたいなものだ(歴史的には逆か)

 

事実は変数を含まないので、resolutionも一方向の代入だけを考えればよく、事実の全Factを列、QueryのClauseの各Literalを行とし、成分にmguをとるような行列を考える。

その行列を元に、代入の積を使ってQuery全体で成立するモデルを絞り込むというようなもの。

いくつかサンプルをやってみると、あまり深い答えはでなかった。

これはこれで面白いのだけれど、まともな一階述語論理のシステムにしてみようと思うようになったという次第。

 

計算のこと

クラスにもとづくオブジェクト指向は、計算というか関数を整理するための仕組みだと思う。前にも書いたかもしれない。

 

同じアルゴリズムオブジェクト指向で書いたり、Cで書いたりして、それを同じアルゴリズムだと区別できるのだから、そういうことだろう。

 

COMMON LISPのgeneric functionやその他、型ベースでメソッドをディスパッチするタイプのオブジェクト指向(というよりただの型か)の方式もそう見られる。

 

計算の方式自体が違うとしても、時系列上で実行される処理が同じなのだから、それは計算の表現の違いと考えるべきで、結局、こまぎれにしたメソッドをどう管理するかという問題だと見られる。

 

Apple Dylanの開発環境では、メソッドをデータベースで管理していたけれど、まさにそういうことではないのだろうか。

 

 

Project EulerをJuliaでやる

Projct EulerをJuliaで解いてみる。

以前は、RubyかRかで20個くらい解いたあと、問題が面倒臭いのばかりで放棄していたのだけれど、途中で言語を変えるのもおもしろくないから、改めてJuliaで解くためにアカウントを新調してみた。

 

解法をブログに書くのは問題があるのでしないけれど、思ったことなどをここに書くことにしよう。

 

問題1を解いて思ったのは、私にとってプログラムまたはプログラミングとは、問題あるいは解法を明瞭に記述することのようで、手順で書くよりも関係で書くほうを好んでいるらしい。ちがうかもしれない。

 

問題11までは、すぐに答えがでたのだけれど問題12は時間がかかっている。これはプログラムの実行時間のこと。

 49.8分かかった。

 

プログラムを書くまでにかかる時間は、問題にもよるわけで、もしもJuliaやそのパッケージで使えるものがあれば使っているので、ときどき、問題の意図と違う解法をしているのかと思わなくもないけれど、違う言語を使うと言うことはそういうことだと思う。細かいアルゴリズムで解きたくなることもあるので、そういうときはそうするかもしれない。

 

 

Julia save&loadはJLD

packageがある。

HDF5も使うようだ。

 

HDF5は、MochaでMNISTのデータを保存するために使っていた。

これはOSによるファイルシステムの違いを吸収する仕組みのようにみえる。一般的な仕様。

 

CouseraでJuliaのコース

CourseraからのアナウンスでJuliaのコースがあったので、受講した。

いままで動かなくて往生していたことも、解決せざるをえず、うまくいくようになったと思う。

 

・演習はIJuliaのnotebookで提出するので、使えるようになった。

 JuliaBoxが簡単に使える。しかし、notebookをCouseraにアップロードすると、読み込めなかったりしていろいろトラブルがあった。JuliaBox自体は問題ないし、どこでも同じ環境が支えて便利。

 JuliaBoxは、今は無料だが、いずれ有料コースもできるみたい。無料では使用時間が3時間に限定されている。たぶん、一回のセッションが3時間なのではないだろうか。そんなに使わないので、わからない。残り時間が3時間からカウントダウンされているのでそう思った。

 ローカルのJuliaでもnotebookを動かすためにはIJuliaが必要だが、これがなかなかうまくいかなかった。IJuliaのgithubのドキュメントをみると、minicondaをインストールせよとあって、指定のURLにはminicondaがみあたらなかったが、anacondaをインストールして解決した。

 Anacondaににあるnotebookだったかな、それを使っているらしい。Python使う場合は、これも便利そう。(僕はPythonを使っていない。Rは使っている)

 

 コースでは、pyplot(だったかな)やGadflyを使ってグラフを書いた。DataFramesも使った。散布図の放物線によるフィッティングなど面白かった。型のあたりも一人でやっていると退屈だが、講義だと聞ける。

 

 今回受講してみて、思ったのは、Juliaのパッケージの使い方に関する情報がなかなかみつからないので、こういう機会があるとありがたいなということ。

 

 ちなみに、Couseraのコースは無料だが、その場合はアクセスできるリソースに制限があるので、5000円くらい出して全部できるようにした。5000円なら1.5冊くらい本が買えるので、ちょっと高い気もするが、まずまず満足。

 

僕の環境はMacOS。会社ではWindowsLinuxだが、Proxy経由の場合の使い方がうまくわからず、ローカル環境では使えない。そんなときは、JuliaBoxがいいかなと思う。秘密情報は置けないけれど。

 

 

 

 

The Little Prover

これは、LISPSchemeに対する、The Little LisperやThe Little Schemerのような関係にある Coqに対するThe Little Proferらしい。

 

まだ最初の方しか読めていない。ややこしい。

focusをあてている部分にルールを適用するその仕方を繰り返し説明しているのだけれど、なんだかよくわからない。英語の読解力がないからだろう。

 

もう少し読み続けてみよう。

 とはいえ、Juliaが優先だと思う。