λx,z,E.y F(x,y),F(y,z)→F(x,z)
clause形に変換するとき、違うclauseの変数は独立になる。
λx,z,E.y F(x,y),F(y,z)→F(x,z)
は、全順序のようにも見えるが本当は、友達の友達は友達の関係。
ここでは、yが存在すればF(x,z)であるということで、存在が重要。
存在を全称にしてしまってこれをclauseにすると
¬F(x,y),¬F(y,z),F(x,z)
となり、これの否定は
F(x,y),F(y,z),¬F(x,z)
になる。
この否定が矛盾を導けば、元の主張は正しいということになる。
Fact1={F(a,b), F(b,c),F(a,c)}
のとき、確かに反証できる。
しかし、
Fact2={F(a,b), F(d,c), F(a,c)}
でも成り立ってしまうのはおかしい。
これはおそらく、yは存在なのでclauseを超えて同じ値にならなくてはならないということではないだろうか。
もともとclause formにするとき存在変数は定数に置き換えられることになるので、同一性は必要とされる。しかし、定数では代入ができないのでこの問題が解決できない。
mguを代入とだけ考えるのではなく、{x←t}を{x=t}という条件と考えれば、対処できるとは思う。
いずれにせよ、存在変数(とは呼ばないと思うが)は、clauseを超えた変数の同一性と考えればいいのではないか。
あるいは問題の視点が間違っているかも。
Factのadjustについて
Factの述語記号P、定数記号cとし、FactにP(c)が含まれていないとき
- Pが2つに一つだったら、-P(c)を加えてもいいはず。
つまり、G(x)が'xは少女'という意味なら、FactにG(c)が含まれていなければ'-G(c)'にしても、だいたい正しい - 一方で、友達を表す'F(x,y)'について、Factの中で、F(a,b), F(b,c)からF(a,c)が導けるかどうかを判定しようとしてるときに、勝手にF(a,c)を加えてはならない。
こんな証明はできないのか
clauseの集合を
{P(a), Q(a), Q(b)}
としたとき
any x. P(x) → Q(x)
は証明できるのか?
できないみたい。
Herbrand Universeで成り立っても、必ずしも成り立たないようなかんじ。
もしも、
{P(a), P(f(x))}
で
P(f(x))
の証明は当然できる。
Project EulerをJuliaでやる
Projct EulerをJuliaで解いてみる。
以前は、RubyかRかで20個くらい解いたあと、問題が面倒臭いのばかりで放棄していたのだけれど、途中で言語を変えるのもおもしろくないから、改めてJuliaで解くためにアカウントを新調してみた。
解法をブログに書くのは問題があるのでしないけれど、思ったことなどをここに書くことにしよう。
問題1を解いて思ったのは、私にとってプログラムまたはプログラミングとは、問題あるいは解法を明瞭に記述することのようで、手順で書くよりも関係で書くほうを好んでいるらしい。ちがうかもしれない。
問題11までは、すぐに答えがでたのだけれど問題12は時間がかかっている。これはプログラムの実行時間のこと。
49.8分かかった。
プログラムを書くまでにかかる時間は、問題にもよるわけで、もしもJuliaやそのパッケージで使えるものがあれば使っているので、ときどき、問題の意図と違う解法をしているのかと思わなくもないけれど、違う言語を使うと言うことはそういうことだと思う。細かいアルゴリズムで解きたくなることもあるので、そういうときはそうするかもしれない。
Deviant Moon Tarot Companion Book by Patrick Valenza
数日前にAmazon.co.jpから届けられたこの本は、思っていたよりも巨大。
しかし、大きな絵がとてもいい。
元のタロットは、従来のタロットとはまったく違う絵だと思う。
不思議な絵で、見ているといろんなストーリーが浮かんでくる。
時間がいくらでもすぎてゆく。
そのCompanion Bookなので期待している。英語なのでいつになったら読めるのやら。
