相互再帰を導入した。 ((式1=>SとかKとか) (式2) ...) のような式に対応した。 (use srfi-11) (define (cutlist size car_l result_size l) (if (or (= size 0) (null? l)) (values (reverse car_l) l result_size) (cutlist (- size 1) (cons (car l) car_l…

S (式1) (式2) が S (式1') (式2') (式3) になることはありえない気がする。気がするだけなのが弱い。結局、((式1) (式2) (式3)) みたいなの((式1)を簡約するとSになるようなやつ)には対応せず。つーか (else (map expand-combinator-one seq))を (else (exp…

ラムダ式をSKIコンビネータにバラすプログラムを書いてはみたものの、本当に正しく動いてんのか不安になって、(実際最初は間違ってたし。)逆を行なうプログラムを書いてみた。 (define (construct-S p1 p2 p3 rest) (if (not (pair? p1)) `(,p1 ,p3 ,(if (no…

鳥(コンビネータ)を全て1引数の関数として実装して、schemeで動かそうとすると、どうしても余計に(主観だけど)括弧がついてしまう。 (define I (lambda (x) x)) (define K (lambda (x) (lambda (y) x))) (define T (lambda (x) (lambda (y) (y x)))) (define…

先日のschemeのプログラムは色々間違ってた。x消去で、xを含まない合成手続きXを K X と処理すべきが、 S (K Y) (K Z) になってた。コンビネータとしては冗長だけど、間違ってはいない。といいわけしておく。 ついでにutil.matchを使って書き直してみた。(中…

SKIコンビネータをばらすプログラムをgauche書いた。やっぱものまね鳥の本はすごいと思う。初心者でもこんなことが出来るようになるとは。てゆーかアルゴリズムがまんま書いてくれてあるだけだが。(toSK '(x y) '(x y y)) => (S S (K I)) (toSK '(x y) '(y x…

SICPの遅延評価版schemeで、LによるYコンビネータは上手くいった。 (define L (lambda (x) (lambda (y) (x (y y)))) (define Y (lambda (f) ((L f) (L f)))) ((Y (lambda (f) (lambda (n) (if (= n 1) 1 (+ n (f (- n 1))))))) 10) # => 55 Uコンビネータが…

あいかわらずものまね鳥の本はよー分からんが、Yコンビネータの構成方法は分かった。Lxy = x(yy) という Lコンビネータ(Lark ヒバリ)を使用した Lx(Lx) // x(Lx(Lx)) または以下のチューリングコンビネータを使用した Uxy=y(xxy) UUx // x(UUx) schemeなどの…

ものまね鳥のカリーの森がゲロ吐きそうなレベルで何が書いてあるか分からん。

squid ATSとかvarnishのようなキャッシュサーバって、デフォルトでは不特定多数にキャッシュを消させないようにしてるけど、なんでや？DoS攻撃対策?

デフォルトの設定で、普通に並列に取得してくれた。

なんでか知らんが、ESI(edge side include)について調べていた。 最初Ajaxでクライアント通信でええやんという感じだったんではあるが、 調べたところ、上手く使えば、確かに通信量が削減されていいかもしらん。 (あくまで上手く使えばである。最初聞かされ…

チャーチの森で、SとTとMとIが基底とされてるけど、チョウゲンポウ Kはいません!と書かれてる。なんでいないのかしら。

P102の 20 コマドリで書かれている、ルリムクドリという鳥は、ルリツグミの間違い？ルリムクドリなんて出てこないよな？

タイトルの横に書いてある、POD版の意味を最近ようやく知った。 注文してから一部ずつ刷ってんのね。最後の一冊でラッキーとか書いてはずかしー。

Pである鳥 Aがいて、Qである鳥 Bがいる場合 Xである鳥がいることを示せ。みたいな問題で、 (exists A, P A) -> (exists B, Q B) -> exists C, X C.のように立式してたけど、 forall A B, P A -> Q B -> exists C, X C.でいいのか？ 証明も少し楽だ。 destruc…

そういや、: の左は、値。右は型。だった。 あるいは、: の左は証明。右は命題。 あるいは、: の左は命題。 右は命題型。つまり、 なんらかの命題 : Prop右に命題を書いてしまえば、左はその証明を用意しなくちゃならない。

Aに向ってBと呼びかければ、Aは同じ鳥Bの名を呼びもどすかもしれない。 その場合、鳥Aは鳥Bが好きであるという。 記号だと、AB = Bあらゆる鳥はすくなくとも一羽の鳥が好き。coqで。 Theorem any_bird_is_fond_of_least_one_bird : forall A, exists B, B = …

ひいた。正月そうそう縁起が悪い。

鳥xは自分自身が好きであれば、すなわちxのxへの応答がxであれば、自己中心的と呼ばれる。 記号的には、xx = x である。結合条件とものまね鳥がいる条件のもとで、少なくとも一羽の鳥は自己中心的であることを示せ。coqで。とりあえず。 Theorem there_is_eg…

正しくは、こうであった。 Axiom bird_composition : forall A B : Bird, exists C : Bird, forall x : Bird, bird_respond C x = bird_respond A (bird_respond B x).Coqで証明出来るということから逆算した正しさに過ぎないけどな!しかし、世の数学の偉い…

この森の任意の鳥A,Bに対して、任意の鳥xを取れば、Cx = A(Bx)となるような鳥Cがいる。 任意の鳥A,Bに対して,AとBを結合する鳥Cが存在する。 Axiom bird_composition : forall A B : Bird, exists C : Bird, forall x : Bird, bird_respond C x = bird_respo…

ものまね鳥は任意の鳥xに対して、次の条件が成り立つような鳥Mのことである。Mx = xxMに対してxと呼んでも、xに対しxと呼んでも同じ応答が得られる。そうな。 Axiom there_is_mockingbird : exists M, forall x, bird_respond x x = bird_respond M x.疲れた…

たぶんすぐ飽きる。というか分からなくなって投げだすと思うが、真似てみる。この本の9章。 ある森に鳥たちが住んでる。任意の鳥AとBがいるとして、Aに向かってBの名を呼べば、Aは、何かしら鳥の名前を返事として応答する。そのとき返事として応答された鳥の…

#coq 去年末、スマリヤンのコンビネータ論理を使ったパズル本を手に入れて、これcoqで出来るんかもかもと試してみた。 出来んかった・・・本の回答だと、 forall x : Bird, exists C : Bird, bird_respond C x = bird_respond A (bird_respond M x)で xにCを…

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エラーになるので、少し直した。