語句の真相とあやまち

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

これからしたいこと

真偽値が確率であるような論理を考える 時間によって変化する公理系の満たすべき条件を考える 命題論理との融合(?) 命題レベルで全証明をとらえて(SAT solverなのか) それを制約条件として一階の全証明(=mgu)をとらえる そのとき、は命題レベルでは見えなく…

ニューラルネットで個体という概念を学習できるのだろうか

ニューラルネットで画像認識をした場合、二つの像が似ていることは学習できるけれど、その二つの像の示す個体の同一性までは学習できていないと思う。 たとえば、セキュリティで同じ人間かどうかは判定するとき、顔や指紋に基づいて処理するが、それは同一人…

量子計算と論理について考え始める

ある像aがNNでカテゴリーPに属する確率をrと判定されたとき、P(a,r)と書くとすると事実は+P(a,r)として得られる。 では-P(a,1-r)なのかというと違うような気がする。 否定と確率の関係を理解するために、あれこれ考えているうちに、量子計算が関係するかもし…

今後したいことの整理

確率と否定 P(a,r) でrをP(a)である確率だとする。 このとき、¬P(a,r)はP(a,1-r)と同じではないみたいだ。 ¬P(a,1-r)を含めた四つの関係は? 量子計算-トポス-論理-確率と否定 全proofの有限表現と操作 証明のカバリング proofの情報とはなにか? Capical変数…

λ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)であるということで、存在が重要。 存在を全称にしてしまってこれをc…

Factのadjustについて

Factの述語記号P、定数記号cとし、FactにP(c)が含まれていないとき Pが2つに一つだったら、-P(c)を加えてもいいはず。つまり、G(x)が'xは少女'という意味なら、FactにG(c)が含まれていなければ'-G(c)'にしても、だいたい正しい 一方で、友達を表す'F(x,y)'に…

こんな証明はできないのか

clauseの集合を {P(a), Q(a), Q(b)} としたとき any x. P(x) → Q(x) は証明できるのか? できないみたい。 Herbrand Universeで成り立っても、必ずしも成り立たないようなかんじ。 もしも、 {P(a), P(f(x))} で P(f(x)) の証明は当然できる。

そしてResolution

Juliaで論理式を表す方法について、ずっと試行錯誤している。 いまは、parse("[x,y].[+P(x,f(x)),-Q(x,y)]") のようにparse()を使うことにして、Exprベースで式を扱っている。 内部で[x,y] と :([+(P(x,f(x)),-(Q(x,y))] に分けているのだけれど、これも[:(+…

それから Resolutionにいたるまで

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

計算のこと

クラスにもとづくオブジェクト指向は、計算というか関数を整理するための仕組みだと思う。前にも書いたかもしれない。 同じアルゴリズムをオブジェクト指向で書いたり、Cで書いたりして、それを同じアルゴリズムだと区別できるのだから、そういうことだろう…

Project EulerをJuliaでやる

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

Julia save&loadはJLD

packageがある。 HDF5も使うようだ。 HDF5は、MochaでMNISTのデータを保存するために使っていた。 これはOSによるファイルシステムの違いを吸収する仕組みのようにみえる。一般的な仕様。

CouseraでJuliaのコース

CourseraからのアナウンスでJuliaのコースがあったので、受講した。 いままで動かなくて往生していたことも、解決せざるをえず、うまくいくようになったと思う。 ・演習はIJuliaのnotebookで提出するので、使えるようになった。 JuliaBoxが簡単に使える。し…

The Little Prover

これは、LISPやSchemeに対する、The Little LisperやThe Little Schemerのような関係にある Coqに対するThe Little Proferらしい。 まだ最初の方しか読めていない。ややこしい。 focusをあてている部分にルールを適用するその仕方を繰り返し説明しているのだ…

Junoが使えない記録

JunoがAtomから使えるようになっていて、固有のGUIがみあたらない。これまでも何度かJunoを使おうとして、結局使えなかったのだけれど、今回はすこしまじめに取り組んだが、やはりだめみたいだという話。環境はMacOS/X 10.11.4, MacBookPro 1. Atomが古いと…

Deviant Moon Tarot Companion Book by Patrick Valenza

数日前にAmazon.co.jpから届けられたこの本は、思っていたよりも巨大。 しかし、大きな絵がとてもいい。 元のタロットは、従来のタロットとはまったく違う絵だと思う。 不思議な絵で、見ているといろんなストーリーが浮かんでくる。 時間がいくらでもすぎて…

プログラミング言語Julia

すこしJuliaの勉強を始めてひと月くらい。週末だけ。 ライブラリもいろいろあっておもしろい。 インタープリタ言語(という区分けに意味があるのかどうか)の中で最速というはなしだけれど、あんまり気にならない。 最近気がついたのは、デバツグ環境がないこ…