関数適用がなんで、+や*より強いのか、それはEvalMl3のどこ見たら分かるのか。が分からんわー。項の名無し表現で、再帰関数の書き換えが圧倒的に楽になったぞ。なんでや？ No69

No53は、実際のＭＬ上でも型チェックに通らないものらしいし、取り敢えずあとまわしにした。 6章の「静的有効範囲と名前無し表現への変換」に入る。名前無し表現が何のためのものかよく分からんかったけど、バイナリコードとか中間形式への変換の定式化とか…

似たような箇所を不用意にコピーして、構造が崩れて死んだ。後から解析出来ねー。手動でやる場合、同じレベルの変換を終わらせずに、下位のレベルの変換に行くとどこやってなかったか分からなくなって死ぬ。 No53でYコンビネータっぽいのが出て来た。 フツー…

エディタを比較的慣れてるviに切り替えて再挑戦。viで正規表現前方後方参照とか始めて使った。使いかたも知らんかった。てゆーか、そもそも正規表現て良く知らない。それでも大量の文字列に埋まった評価結果だけをハイライトしてくれるだけで大分楽だ。 /\v(…

例の演習を馬鹿正直に手でやってると、コンピュータの気持が分かる気がしないでもない。No 47 |- let twice = fun f -> fun x -> f (f x) in twice twice (fun x -> x * x) 2 evalto 65536 by E-Let { |- fun f -> fun x -> f (f x) evalto ()[fun f -> fun …

5章あたりから急激に難しくなってきた感じ。 もうすこしやる。 難しいけど麻薬的だ。プチプチ？的な。 難しそうに聞こえないけど。

39問までやった。 少しパターンマッチ力(ぢから)が上った気がする。

パターンマッチ力(ぢから)が欲しい。

第11問 S(S(Z)) is less than S(S(S(Z)))を 導出システム CompareNat3 で判断 CompareNat3 を適用する余地がない・・・ S(Z) is less than S(S(S(Z)))なら分かるけど。 誰かemacsのこれを支援してくれるモードとか書いてないかしら。 ruby-modeで代用中

課題12 難しすぎ。先人のを参考に丸写し。あとで見直す。http://homepage2.nifty.com/magicant/programmingmemo/coq/byhyp.html http://homepage2.nifty.com/magicant/programmingmemo/coq/bygoal.htmlあらためて読んで、代数的データ型というものをちっとも…

http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/CoPL/ というのもあるのか。登録だけしてみた。

Coq演習をやってみて、やはりあんまり自分が理解してない。ということが分かった。 とくに、 命題とブール値の違い 命題とブール値は、一見とてもよく似ているように見えます。しかしこの二つは根本的に違うものです！ ・ブール値は、「計算の世界における値…

出来た。紙に書いて落ち着いて考えるの大事だ。

Lemma inv_r : forall x, x * / x = 1. Proof. intros. assert(H: //x/x=1). rewrite inv_l. reflexivity. (* 1 subgoals, subgoal 1 (ID 150) x : G H : / / x / x = 1 ============================ x / x = 1 ここで、//x = xが示せれば、証明終わりなん…

仕事の現場がまた変わるらしい。なんで私だけなのか。 文句ばっかり言ってたから外されたのかしら。その仕事自体がぽしゃったっぽい。 今の仕事楽だからいいんだけど、あまり長くいたくない。腐りそうだし。

第二回 数学が分からん。群というのはぐぐる限りかなり基礎的なことであるようだ。 http://maldoror-ducasse.cocolog-nifty.com/blog/2006/12/post_f319.html a*/a = (1*a)*/a = [{/(/a)*/a}*a]*/a = {/(/a)*1}*/a＝/(/a)*/a = 1 ですね。ですね。とか言われ…

http://qnighy.github.io/coqex2014/ なんてものがあった。第一回をやってみた。 試行錯誤してなんとか証明出来たけど、 あいかわらず、いまいち何かが分かっている感がない。#coq 論理学／数学を分かってないせいか。 Theorem tautology: forall P : Prop, …