型推論は、型を推論するものである。多相的な型の型パラメータの値は、推論される型じゃないので省略出来ない。 Inductive list (X:Type) : Type := | nil : list X | cons : X -> list X -> list X.の Xみたいなやつね。型パラメータを持つ多相的な型のコン…

Lists.v 自分で問題を考えましょう。 - [cons] （[::]）、 [snoc]、 [append] （[++]） に関する、自明でない定理を考えて書きなさい。 とかいう問題が一番なにしたらいいか分からない。 定理ってどうやって思い付けばいいの？ Lemma nil_rev : forall l : n…

関数を宣言するときに型パラメータを暗黙に指定させてしまうことも出来るようだ。 Fixpoint length {X:Type} (l:list X) : nat := match l with | nil => 0 | cons h t => S (length'' t) end.{X:Type}のように中括弧で宣言すると型パラメータは実際に書かな…

再読中。 ここをあーはいはいリストね。ペアね。ってな感じで流し読みしたことが あとでつまった原因の一つだと思われる。出来ない人間が挫折する理由は無限にあるし、教育者ってたいへんだなと思う。 まあ出来ないやつはほっとかれるだけであろうが。

二進数のnormalizeに関して、normalizeした二進数が必ずnormalizeする前のものより短くなることを証明してみた。 証明することは出来たが、命題に対する帰納法ってやつをあんまり理解していないことが分かった。(最初、n S n 帰納法でやってしまって泥沼に嵌…

coqのワイルドカードって、データしかあかんのか？ Fixpoint bin_len (b : bin) : nat := match b with | Q => O | T b' => S (bin_len b') | F b' => S (bin_len b') end.を Fixpoint bin_len (b : bin) : nat := match b with | Q => O | _ b' => S (bin_l…

http://d.hatena.ne.jp/propella/20090215/p1 Coq < Parameter a b :nat. a is assumed b is assumed Coq < Print plus. plus = fix plus (n m : nat) {struct n} : nat := match n with | 0 => m | S p => S (plus p m) end : nat -> nat -> nat Argument s…

SF Induction.v #coqnormalizeにて、Prove It. とだけ書いてあるんですが、何を証明すればよいのでしょうか。これ？ 取り敢えず、normalizeする前の二進数とした後の二進数で、同じ自然数に変換出来ることは証明したけど、 これって意味あるんだろうか？そも…

Coqコマンドの Print/Locateを教えてもらった。 チュートリアルの一番最初にのっけておいて欲しかった。途中で挫折して読めてない後ろの方に載ってんのかもしらんが。 Check 式の型を表示。 Print 関数や型の定義を表示。 Locate Notation を展開して表示。N…

オンライン演習も終ったし、仕事がヒマな内に、Coqに戻るかと思ったけど、やはりもう色々忘れてていろいろいやになる。年とるのってやだねえ。しかし若いころは経験と理解力と忍耐力が足らんかったから余り変わってないかもしれん。 Software Foundation Bas…

最近あらゆる義務を放棄してこればっかりやってたけど、おわた。 残念だ。あと100問くらいあってもいいのに。 こんなに熱中したのは10年くらい前のガンパレ以来かもしらんやはり、再代入はプログラミングにおいて必要かもしらんが、悪であると断言する。 参…

137問まで来た。 http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/CoPL/index.cgi?command=stats のページを見てニヨニヨするのがここ最近の楽しみだったんだけども。最近はあまり順位が変動しなくて寂しい。何問も解かないと順位があがらないし。佐野さんとい…

「別に「副作用」の発生が悪い，というわけではなく，単に，主たる効果が，値の計算・実行の終了であるとした時には，そう呼べる，といういわば相対的な概念である．現実世界で意味のあるプログラムの動作のほとんどは副作用である，という見方も可能である」

継続に入った。 schemeで、Gauche入門本で、全然分からんかった継続が、http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/CoPL/chap11.pdf を読んで、演習問題を解いて初めて分かった気がした。継続のことが書かれた文書を読んだだけで理解しようというのは間違…

似非科学を批判したり、 渋滞を研究したり、 テルミン弾いたり 不完全性定理について本を書いてたり、 半導体設計したりと とてつもなくすごい人なんだなあと思ってたんですが、 私のなかで三人くらい混ってたみたいだ。すんませんでした。

第9章の多相的型システムに入って本格的に何が書いてあるか分かんなくなったぞ。分かんなくても演習問題を解くことは出来るぞ。なんでか知らんが。115番。114番と同じ？出題ミス？とか思ったら全然違う。泣ける。114 |- let twice = fun f -> fun x -> f (f …

なんで、PolyTypingML4 から、T-Times が 唐突に T-Multになるねんな。「掛ける」だけ動詞のtimes で、「足す」と「引く」がplus/minusとかなのは違和感があった。timesなら、「足す」「引く」もadd/subにせんとあかんのと違う？

100問突破! 飽きっぽい私としてはめずらしいことよ。 単純型システムに入った時、intのつもりで、natと書いてしまっており、なんで通らないんじゃーと一時間くらい無駄にした。97問目 k2の型は int->???->int のような形になるけど、真ん中に何を入れても成…

関数適用がなんで、+や*より強いのか、それは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演習をやってみて、やはりあんまり自分が理解してない。ということが分かった。 とくに、 命題とブール値の違い 命題とブール値は、一見とてもよく似ているように見えます。しかしこの二つは根本的に違うものです！ ・ブール値は、「計算の世界における値…