web系な現場に回されて数ヶ月。phpで頑張るお仕事かとおもいきや、デザイナー不在でフロントエンドやらされる現場だった。40過ぎるときついのよね新しいことさせられんの。jsとphpはロジックだからまあいい。HTMLとcssは食わず嫌いで今まで来たもんだから、…

http://js-next.hatenablog.com/entry/2014/11/01/034607phpやったときも思ったけど、classの何がいいのか。しかも動的言語で。javascriptは Good Partsとグラフィックスの本とで洗脳されてるため javascriptでnew?馬鹿じゃねーのというくらい思考が歪んでい…

最近スマホのインターネットラジオを聞いてる。SkyFM mostly classicという番組が、ひたすらバロックから古典派前期くらいの曲を何のナレーションも入れずに、しかし曲名はネットラジオの通知欄で全部出してくれるという私にとって完璧な仕様。外国語で何や…

$h); echo $a['h']->v; // OK echo ($a['h'])->v; // シンタックスエラー 上記、意味が分かりません。どーゆーパースしてるんだろうか。あと、 constにarrayとかobjectは指定出来なくて、スカラ値しか指定出来ないとか、 殆ど同じであろう連想配列とオブジ…

さっきの記事だと、親が抽象クラスだとFatalエラーになるので、少し直した。

次の仕事はなかなか始まらない。 しかたがないので、PHPの勉強でもするために、プログラミングPHPという本を読んでいるが、この本へんだよ。サンプル動かないよ。古い本だから仕方ないのかと思って奥付みたら、2014/3/24て書いてある。

いろいろやる気は起こらないが、簡単そうなものならば読めそうなので、OCaml入門とか読む。http://www.fos.kuis.kyoto-u.ac.jp/~t-sekiym/classes/isle4/mltext/ocaml.html「関数適用と評価戦略」を読んで、初めて、 値呼び (Call by Value) 名前呼び (Call …

Software Foundations の ImpParserがあまりに分からなくてつらいので、コンパイラ方面のページを最近あちこち漁っていた。llvmというのがよいらしい。http://peta.okechan.net/blog/llvm%E3%81%AB%E3%82%88%E3%82%8B%E3%83%97%E3%83%AD%E3%82%B0%E3%83%A9%E…

http://cs.brown.edu/~sk/Publications/Books/ProgLangs/ を読んで、コードを実行したい場合。 DrRacketをインストールします。 メニューの「ファイル」->「install package」を選択。 Package Sourceというエディットボックスに、plai-typed と入力してOKを…

PHPプログラマがなんかソシャゲバブルの影響で数が足らんそうですよ。単価はJavaプログラマより安いらしいけど。

突然いろいろやる気を失なった。Coqむず杉。関数型言語ってよく知らんからその勉強がてら読みはじめたのが去年の今ごろだった。SoftwareFoundationsそもそも読み初めようと思ったのは、SICP読んでて、4章でprologっぽいものが出てきて、ここで扱われてる論理…

久し振りに見たら、While言語の問題が運営により？解禁されてた。Software FoundationのImp.vとほぼ同じ構造だったが、演習の問題が簡単すぎますわ。 もそっとだけ難しいの希望。 それはともかく、あのCoPLのオンライン演習は面白すぎるので、いにしえの昔の…

リストなどの構造に対する帰納というのがいまいち分かってない。チュートリアルみたいな簡単なのは出来るんだけど、ちょいと難しくなるとお手上げ。 というより、真ん中の難しさというのが、初学者にたいして何時も存在しない気がする。 はるか昔、Cを学んだ…

Imp.v 初めて読むところが多くなってきたので読むスピードが落ちる。 スピードが0になったら終わり。一度手動で全部書いてからでないと、「便利なタクティカル」とやらをちっともどうやって使ったらいいのか分からない。いずれ慣れるのだろうか。プログラミ…

Software Foundations Imp.v 全開前回挫折したとこまで再び到達。前よりは若干分かってる感じもする。http://d.hatena.ne.jp/morita_non/20130928/1380366939 で書いた、関係 bevalR のどこが間違ってるとか。関係なのに、関数aevalと混ぜたらあかんやろ。 R…

MoreInd.v 帰納法のための明示的な証明オブジェクト を読む。目的の集合を数え上げ尽すことが出来れば、コンストラクタは何でもよい。という意味だと理解。そういうわけで、以前の l=rev l -> pal l も、 list Xのコンストラクタを変えて、新たな帰納法の原…

PHPについて少し調べてる。次の仕事がそれだし。 何か作るのがいいんだろうけど、何か作りあげるような根性とか意欲はもちろんない。pukiwikiって現在のPHP5.x系で動かないんだね。あれ結構使ったのに。直系のアプリもなさそう。みんなWiki記法なんてものは…

ついったで(Coq方面の)その筋の人らをフォローしてると、たまに「面白い証明を求む」とか、それくらいの証明じゃ面白くないとか、そういう呟きが流れてくることがある。しかし、面白い証明っていったい何なの？ 難しかったり、アクロバティックだったりする…

ProofObject.v これこそが知りたかったことだけど、すでに前の版で大半は日本語訳されてた。例とかは少ないけど。 以前読んだときは目に入ってなかったのか、理解出来てなかっただけか、両方か。しかし、Printとかの使い方はなかった気もする。 Theorem b_ti…

MoreLogic.v 練習問題。all_forallbようやっと、Coqで仕様を記述し、証明する。という本来の目的のモノが出てくる。問題は、「仕様とは何か？」ということが分かってないことだが。とりあえず、allを以下のように書く。これはこれで間違ってはいない・・・と…

Rel.v 反射推移閉包とかこれ何かの役に立つんじゃろか。関係をラップするとか。clos_refl_transとかrefl_step_closureとかまったく意図とか分かってないけど、だいたいこんな感じだろうというレバガチャで証明は出来た。何の役に立つとか、読み進めたら出て…

Prop.v *** Exercise: 3 stars, optional (R_fact) にて、That is, if R m n o is true,って書いてあるけど、R m n oは命題なんだから、Trueじゃね？と思う。 でもSoftwareFoundations/coqの世界のなかで、Trueとは、 True : Prop := I : True.でしかないか…

Software Foundations Rel.vより Definition partial_function {X: Type} (R: relation X) := forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2. Theorem le_not_a_partial_function : ~ (partial_function le). Proof. unfold not. unfold partial_functio…

途中ちょっとしたコードを保存するために、gistを使ってみた。 わりいいけど、大きなファイルを何度も書き換えたりする用途には、githubでリポジトリにファイル置くのがよいっぽい。

Software Foundationsを読んでると、時々、「なんか自明でない定理考えて証明しろ」とか無茶振りしてくるけど、数学に慣れてない人間にんなこと言われても途方に暮れるわけだ。そもそも、何か命題があって、それを証明する必要があるかどうか、ということが…

Inductive 型とか命題の定義を行う。 回文の定義で、 Inductive pal {X:TYpe} : list X -> Prop := | p_zero: pal [] | p_one : forall x:X, pal [x] | p_2 : forall l, pal (l ++ (rev l)) | p_3 : forall l1 l2, pal l2 -> pal (l1 ++ l2 ++ (rev l1)).と…

Software Foundation Prop.v forall l, l = rev l -> pal l.どっから手をつけたらいいかすら分からん・・・前問の forall l, pal l -> l = rev l.ならば、"pal l"という命題を定義してあるから、そのコンストラクタに応じて場合わけして、それぞれが l = rev…

Logic.v 証明オブジェクトがどんなかたちになるかについて、 全然イメージが湧かない。 あいかわらずレバガチャ状態ではある。 Theorem or_distributes_over_and_2 : forall P Q R : Prop, (P \/ Q) /\ (P \/ R) -> P \/ (Q /\ R).とか。scriptモードでも、…

どれが型で、値で、という区別。 どれが命題で、証明で、という区別。 慣れるしかないとはいえつらい。しばしば出て来る数学用語についても、もう少し知っておく必要がある。直積、関係、反射的、推移的、対称的、etc...学がないとつらいね。SoftwareFoundat…

Logic.v証明オブジェクトが良くわからん。論理積の交換で、Logic.vに載ってるやり方だと以下のような証明オブジェクトが作られる。 Theorem and_commut : forall P Q : Prop, P /\ Q -> Q /\ P. Proof. intros P Q H. inversion H. split. apply H1. apply H…