Rustの並列処理を学ぼうぜ☆（＾～＾）？＜その８＞
＜前回の記事＞
「 ラムダ計算 を特集する☆」
「 寝てればいいのに……☆」
(λx.x) 2
「 この 適用（application） は？」
「 ベータ簡約（β-redex） するだけじゃないの？」
= (λx.x) 2
(λ .x) 2
^
「 実引数ｘを消して、」
= (λx.x) 2
(λ .x) 2
(λ .2)
^ ^
「 アブストラクションのｘを 2 に置き換えて、」
= (λx.x) 2
(λ .x) 2
(λ .2)
= 2
^^ ^ ^
「 丸かっこと λと ．を消して、２よ」
「 I Combinator なんか計算しても おもんないぜ☆」
(λxy.x) 2 7
「 じゃあ、この適用は？」
= (λxy.x) 2 7
(λ y.2) 7
^ ^ ^
「 ベータ簡約で x を消して、」
= (λxy.x) 2 7
(λ y.2) 7
(λ .2)
^ ^
「 y は束縛されてないから 7 と一緒に消えて、」
= (λxy.x) 2 7
(λ y.2) 7
(λ .2)
= 2
^^ ^ ^
「 丸かっこと λと ．を消して、２よ」
(λxy.x) (λy.y+1) 5
「 じゃあ、この適用は？」
「 y が 衝突（collision） しそうだから、α変換しましょう」
= (λxy.x) (λy.y+1) 5
(λxy.x) (λz.z+1) 5
^ ^
「 ↑ 片方の y を z に α変換 して……」
= (λxy. x ) (λy.y+1) 5
(λxy. x ) (λz.z+1) 5
(λ y.(λz.z+1)) 5
^ ^^^^^^^^ ^^^^^^^^
「 ↑左結合だから ここが先に β簡約」
= (λxy. x ) (λy.y+1) 5
(λxy. x ) (λz.z+1) 5
(λ y.(λz.z+1)) 5
(λ .(λz.z+1))
^ ^
「 ↑もう１回 β簡約。ｙはどこにも使われていないから 5 と一緒に消えるだけね」
= (λxy . x ) (λy.y+1) 5
(λxy . x ) (λz.z+1) 5
(λ y .(λz.z+1)) 5
(λ .(λz.z+1))
= (λ z.z+1 )
^^^ ^
「 ↑実引数が空っぽの （λ ．） が１個浮いているから消しちゃいましょう」
「 これ以上 β簡約 できないから、 ベータ正規形（beta normal form） よ」
「 仮引数 z を消すには、実引数が １個 足りなかったな☆
設問を作ったやつが あんぽんたん だったんだぜ☆」
「 そうだったのかだぜ☆」
「 まあ、実引数を付ければ それが ＋１ されるだろう☆」
「 K Combinator なんか計算しても おもんないぜ☆」
(λxyz.xz(yz)) (λx.x+1) (λy.y-1) 3 5 7
「 じゃあ、この適用は？」
「 x と y が 衝突（collision） しまくりそうだから、α変換しましょう」
= (λxyz.xz(yz)) (λx.x+1) (λy.y-1) 3 5 7
= (λxyz.xz(yz)) (λv.v+1) (λw.w-1) 3 5 7
^ ^ ^ ^
「 片方の x を v に、 片方の ｙ を ｗ に α変換 して……」
= (λxyz. xz(yz)) (λx.x+1) (λy.y-1) 3 5 7
= (λxyz. xz(yz)) (λv.v+1) (λw.w-1) 3 5 7
= (λ yz.(λv.v+1)z(yz)) (λw.w-1) 3 5 7
^ ^^^^^^^^ ^^^^^^^^
「 ↑左結合だから 最初に x が β簡約」
= (λxyz. xz( yz)) (λx.x+1) (λy.y-1) 3 5 7
= (λxyz. xz( yz)) (λv.v+1) (λw.w-1) 3 5 7
= (λ yz.(λv.v+1)z( yz)) (λw.w-1) 3 5 7
= (λ z.(λv.v+1)z((λw.w-1)z)) 3 5 7
^ ^^^^^^^^ ^^^^^^^^ ^^^^^^^^
「 ↑左結合だから 次に y が β簡約」
= (λxyz. xz( yz)) (λx.x+1) (λy.y-1) 3 5 7
= (λxyz. xz( yz)) (λv.v+1) (λw.w-1) 3 5 7
= (λ yz.(λv.v+1)z( yz)) (λw.w-1) 3 5 7
= (λ z.(λv.v+1)z((λw.w-1)z)) 3 5 7
(λ .(λv.v+1)3((λw.w-1)3)) 5 7
^ ^ ^ ^
= (λv.v+1)3((λw.w-1)3) 5 7
^^ ^ ^
「 ↑次に z が β簡約。
実引数が空っぽになったから ラムダ式 が１個消えるわよ」
「 左結合だから 次に消える実引数は v かしらねぇ？」
= (λxyz. xz( yz)) (λx.x+1) (λy.y-1) 3 5 7
= (λxyz. xz( yz)) (λv.v+1) (λw.w-1) 3 5 7
= (λ yz.(λv.v+1)z( yz)) (λw.w-1) 3 5 7
= (λ z.(λv.v+1)z((λw.w-1)z)) 3 5 7
(λ .(λv.v+1)3((λw.w-1)3)) 5 7
= (λv.v+1)3((λw.w-1)3) 5 7
= (λ .3+1) ((λw.w-1)3) 5 7
^ ^ ^
= (λ . 4) ((λw.w-1)3) 5 7
= 4 ((λw.w-1)3) 5 7
「 ↑次に ｖ を β簡約。
あらっ、ラムダ式が消えて ４ になったわよ？ 左結合できないんじゃないの？」
「 あれま☆」
「 設問したやつが あんぽんたん だったんだぜ☆」
「 そうだったのかだぜ☆」
(λxyz.xz(yz)) (λx.x+1) (λy.y-1) (λz.z*2) 5 7
「 じゃあ これでやり直しで☆ × は ｘ と見間違えるので ＊ とするぜ☆」
「 x と y と ｚ が 衝突（collision） しまくりそうだから、α変換しましょう」
= (λxyz.xz(yz)) (λx.x+1) (λy.y-1) (λz.z*2) 5 7
= (λxyz.xz(yz)) (λu.u+1) (λv.v-1) (λw.w*2) 5 7
^ ^ ^ ^ ^ ^
「 片方の x を ｕ に、 片方の ｙ を ｖ に、 片方の ｚ を ｗ に α変換 して……」
= (λxyz. xz(yz)) (λx.x+1) (λy.y-1) (λz.z*2) 5 7
= (λxyz. xz(yz)) (λu.u+1) (λv.v-1) (λw.w*2) 5 7
= (λ yz.(λu.u+1)z(yz)) (λv.v-1) (λw.w*2) 5 7
^ ^^^^^^^^ ^^^^^^^^
「 ↑左結合だから 最初に x が β簡約」
= (λxyz. xz( yz)) (λx.x+1) (λy.y-1) (λz.z*2) 5 7
= (λxyz. xz( yz)) (λu.u+1) (λv.v-1) (λw.w*2) 5 7
= (λ yz.(λu.u+1)z( yz)) (λv.v-1) (λw.w*2) 5 7
= (λ z.(λu.u+1)z((λv.v-1)z)) (λw.w*2) 5 7
^ ^^^^^^^^ ^^^^^^^^
「 ↑次に ｙ が β簡約」
= (λxyz. x z( y z)) (λx.x+1) (λy.y-1) (λz.z*2) 5 7
= (λxyz. x z( y z)) (λu.u+1) (λv.v-1) (λw.w*2) 5 7
= (λ yz.(λu.u+1) z( y z)) (λv.v-1) (λw.w*2) 5 7
= (λ z.(λu.u+1) z((λv.v-1) z)) (λw.w*2) 5 7
(λ .(λu.u+1)(λw.w*2)((λv.v-1)(λw.w*2))) 5 7
^ ^^^^^^^^ ^^^^^^^^ ^^^^^^^^
= (λu.u+1)(λw.w*2)((λv.v-1)(λw.w*2)) 5 7
^^ ^ ^
「 ↑次に ｚ が β簡約。
実引数が無くなったから ラムダ式が１個消えるわよ」
= (λxyz. x z( y z)) (λx.x+1) (λy.y-1) (λz.z*2) 5 7
= (λxyz. x z( y z)) (λu.u+1) (λv.v-1) (λw.w*2) 5 7
= (λ yz.(λu. u +1) z( y z)) (λv.v-1) (λw.w*2) 5 7
= (λ z.(λu. u +1) z((λv.v-1) z)) (λw.w*2) 5 7
(λ .(λu. u +1)(λw.w*2)((λv.v-1)(λw.w*2))) 5 7
= (λu. u +1)(λw.w*2)((λv.v-1)(λw.w*2)) 5 7
(λ .(λw.w*2)+1) ((λv.v-1)(λw.w*2)) 5 7
^ ^^^^^^^^ ^^^^^^^^
= (λw.w*2)+1 ((λv.v-1)(λw.w*2)) 5 7
^^ ^ ^
「 ↑左結合だから とりあえず 次に ｕ を β簡約 しましょう。
実引数が無くなったから ラムダ式が１個消えるわよ」
「 +1 が飛び出た☆」
「 なんで飛び出たんだぜ☆？」
「 じゃあ 飛び出なけりゃいいんでしょ」
= (λxyz. x z( y z)) (λx.x+1) (λy.y-1) (λz.z*2) 5 7
= (λxyz. x z( y z)) (λu.u+1) (λv.v-1) (λw.w*2) 5 7
= (λ yz.(λu. u +1) z( y z)) (λv.v-1) (λw.w*2) 5 7
= (λ z.(λu. u +1) z((λv.v-1) z)) (λw.w*2) 5 7
(λ .(λu. u +1)(λw.w*2)((λv.v-1)(λw.w*2))) 5 7
= (λu. u +1)(λw.w*2)((λv.v-1)(λw.w*2)) 5 7
(λ .(λw.w*2)+1) ((λv.v-1)(λw.w*2)) 5 7
(λw.w*2)+1 ((λv.v-1)(λw.w*2)) 5 7
= (λw.w*2 +1) ((λv.v-1)(λw.w*2)) 5 7
^ ^
「 アブストラクション が丸かっこの中に入るようにしましょう」
「 適当だな☆」
「 あらっ？！ ｗ が collision しそうな気がするけど。 どこで分裂したのかしら？」
「 ｚ が２つあったのねぇ」
= (λxyz. x z( y z)) (λx.x+1) (λy.y-1) (λz.z*2) 5 7
= (λxyz. x z( y z)) (λu.u+1) (λv.v-1) (λw.w*2) 5 7
= (λ yz.(λu. u +1) z( y z)) (λv.v-1) (λw.w*2) 5 7
= (λ z.(λu. u +1) z((λv.v-1) z)) (λw.w*2) 5 7
(λ .(λu. u +1)(λw.w*2)((λv.v-1)(λw.w*2))) 5 7
= (λu. u +1)(λw.w*2)((λv.v-1)(λw.w*2)) 5 7
(λ .(λw.w*2)+1) ((λv.v-1)(λw.w*2)) 5 7
(λw.w*2)+1 ((λv.v-1)(λw.w*2)) 5 7
= (λw.w*2 +1) ((λv.v-1)(λw.w*2)) 5 7
= (λw.w*2 +1) ((λv.v-1)(λt.t*2)) 5 7
^ ^
「 ↑片方の ｗ は ｔ に α変換 しましょう」
= (λxyz. x z( y z)) (λx.x+1) (λy.y-1) (λz.z*2) 5 7
= (λxyz. x z( y z)) (λu.u+1) (λv.v-1) (λw.w*2) 5 7
= (λ yz.(λu. u +1) z( y z)) (λv.v-1) (λw.w*2) 5 7
= (λ z.(λu. u +1) z((λv.v-1) z)) (λw.w*2) 5 7
(λ .(λu. u +1)(λw.w*2)((λv.v-1)(λw.w*2))) 5 7
= (λu. u +1)(λw.w*2)((λv.v-1)(λw.w*2)) 5 7
(λ .(λw. w*2)+1) ((λv.v-1)(λw.w*2)) 5 7
(λw. w*2)+1 ((λv.v-1)(λw.w*2)) 5 7
= (λw. w*2 +1) ((λv.v-1)(λw.w*2)) 5 7
= (λw. w*2 +1) ((λv.v-1)(λt.t*2)) 5 7
(λ .((λv.v-1)(λt.t*2))*2 +1) 5 7
^ ^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^
「 ↑左結合だから 次は ｗ を β簡約 しましょう」
「 豪快にいったなご主人☆」
= (λxyz. x z( y z)) (λx.x+1) (λy.y-1) (λz.z*2) 5 7
= (λxyz. x z( y z)) (λu.u+1) (λv.v-1) (λw.w*2) 5 7
= (λ yz.(λu. u +1) z( y z)) (λv.v-1) (λw.w*2) 5 7
= (λ z.(λu. u +1) z((λv.v-1) z)) (λw.w*2) 5 7
(λ .(λu. u +1)(λw.w*2)((λv.v-1)(λw.w*2))) 5 7
= (λu. u +1)(λw.w*2)((λv.v-1)(λw.w*2)) 5 7
(λ .(λw. w*2)+1) ((λv.v-1)(λw.w*2)) 5 7
(λw. w*2)+1 ((λv.v-1)(λw.w*2)) 5 7
= (λw. w*2 +1) ((λv.v-1)(λw.w*2)) 5 7
= (λw. w*2 +1) ((λv.v-1)(λt.t*2)) 5 7
(λ .((λv.v-1)(λt.t*2))*2 +1) 5 7
((λv.v-1)(λt.t*2))*2 +1 5 7
^^ ^ ^
? (((λv.v-1)(λt.t*2))*2 +1) 5 7
^ ^
「 ↑ 仮引数の無くなった （λ．） を消そうにも、＋１ が飛び出て うまく収まんないわねぇ」
「 丸かっこの内側のラムダ式の アブストラクション と うまく くっつかないかだぜ☆？」
「 手順前後だったのでは☆ どんな手順に入れ替えてもいいのが チャーチ・ロッサー性 なのに……☆」
= (λxyz. x z( y z)) (λx.x+1) (λy.y-1) (λz.z*2) 5 7
= (λxyz. x z( y z)) (λu.u+1) (λv.v-1) (λw.w*2) 5 7
= (λ yz.(λu. u +1) z( y z)) (λv.v-1) (λw.w*2) 5 7
= (λ z.(λu. u +1) z((λv.v-1) z)) (λw.w*2) 5 7
(λ .(λu. u +1)(λw.w*2)((λv.v-1)(λw.w*2))) 5 7
= (λu. u +1)(λw.w*2)((λv.v-1)(λw.w*2)) 5 7
(λ .(λw. w*2)+1) ((λv.v-1)(λw.w*2)) 5 7
(λw. w*2)+1 ((λv.v-1)(λw.w*2)) 5 7
= (λw. w*2 +1) ((λv.v-1)(λw.w*2)) 5 7
= (λw. w*2 +1) ((λv.v-1)(λt.t*2)) 5 7
(λ .((λv. v-1)(λt.t*2))*2 +1) 5 7
((λv. v-1)(λt.t*2))*2 +1 5 7
? (((λv. v-1)(λt.t*2))*2 +1) 5 7
(((λ .(λt. t*2)-1) )*2 +1) 5 7
^ ^^^^^^^^^^ ^^^^^^^^
= (λt.((t*2 -1) *2 +1)) 5 7
^^^^ ^ ^^ ^ ^ ^
「 ↑ ｖ を β簡約 しましょう。
かっこをうまく動かせないわねぇ」
「 かなり うさんくさく かっこ を移動したりしていたが、まあいいだろう見逃そう☆」
= (λxyz. x z( y z)) (λx.x+1) (λy.y-1) (λz.z*2) 5 7
= (λxyz. x z( y z)) (λu.u+1) (λv.v-1) (λw.w*2) 5 7
= (λ yz.(λu. u +1) z( y z)) (λv.v-1) (λw.w*2) 5 7
= (λ z.(λu. u +1) z((λv.v-1) z)) (λw.w*2) 5 7
(λ .(λu. u +1)(λw.w*2)((λv.v-1)(λw.w*2))) 5 7
= (λu. u +1)(λw.w*2)((λv.v-1)(λw.w*2)) 5 7
(λ .(λw. w*2)+1) ((λv.v-1)(λw.w*2)) 5 7
(λw. w*2)+1 ((λv.v-1)(λw.w*2)) 5 7
= (λw. w*2 +1) ((λv.v-1)(λw.w*2)) 5 7
= (λw. w*2 +1) ((λv.v-1)(λt.t*2)) 5 7
(λ .((λv. v-1)(λt.t*2))*2 +1) 5 7
((λv. v-1)(λt.t*2))*2 +1 5 7
? (((λv. v-1)(λt.t*2))*2 +1) 5 7
(((λ .(λt. t*2)-1) )*2 +1) 5 7
= (λt.((t*2 -1) *2 +1)) 5 7
(λ .((5*2 -1) *2 +1)) 7
^ ^ ^
(λ .(( 9) *2 +1)) 7
(λ . 19 ) 7
? 19 7
「 ↑ ｔ を β簡約 しましょう」
「 １９ と ７ が残ったんだけど」
「 設問を作ったやつが あんぽんたん だったんだぜ☆」
「 そうだったのかだぜ☆」
「 実引数は いくつだったら いいんだぜ☆？」
(λxyz.xz(yz))
「 一番左に 仮引数を３つもった ラムダ式があるということは……☆」
(λxyz.xz(yz)) u v w
「 ｘ、ｙ、ｚに対応する実引数 ｕ、ｖ、ｗ と……☆」
(λxyz.xz(yz)) u v w 7
「 ナンバーが何か１個 要るんじゃないか☆？」
「 そうなのかだぜ☆」
「 S Combinator なんか計算しても おもんないぜ☆」
「 さっきの式の答えは ほんとうに 19 なのか検算しておくかだぜ☆」
(λxyz.xz(yz)) (λx.x+1) (λy.y-1) (λz.z*2) 5
「 ↑こういう形にすればよかったのかだぜ☆」
= (λxyz.xz(yz)) (λx. x+1) (λy. y-1) (λz.z*2) 5
? (λxy .x (y )) (λ .(λz.z*2)+1) (λ .(λz.z*2)-1) 5
^ ^ ^ ^ ^^^^^^^^ ^ ^^^^^^^^ ^^^^^^^^
(λxy .x (y )) (λ z.z*2 +1) (λ z.z*2 -1) 5
^^^ ^ ^^^ ^
「 ↑計算順序を無視して ｚ を先に消してみるぜ☆」
「 また そういう 基礎を疎かにした 手抜きをする……☆」
= (λxyz.xz(yz)) (λx. x+1) (λy. y-1) (λz.z*2) 5
? (λxy .x (y )) (λ .(λz.z *2)+1) (λ .(λz.z*2)-1) 5
(λxy .x (y )) (λ z.z *2 +1) (λ z.z*2 -1) 5
? (λx .x ) (λ .(λz.z*2 -1)*2 +1) 5
^ ^^^^ ^ ^^^^^^^^^^^ ^^^^^^^^^^^^^^^
「 ↑計算順序を無視して ｙ を先に消してみるぜ☆」
「 またまた 自分流でやられると、目が追い付いていかないぜ☆」
= (λxyz.xz(yz)) (λx. x+1) (λy. y-1) (λz.z*2) 5
? (λxy .x (y )) (λ .(λ z. z *2)+1) (λ .(λz.z*2)-1) 5
(λxy .x (y )) (λ z. z *2 +1) (λ z.z*2 -1) 5
? (λx .x ) (λ .(λz. z*2 -1)*2 +1) 5
? (λ .(λz. z*2 -1)*2 +1) 5
(λ z.(z*2 -1)*2 +1) 5
^^^^^^^^^^^^^ ^^^ ^
「 ↑計算順序を無視して （λｘ．ｘ） を消してしまおうぜ☆ 丸かっこも整理☆」
「 またまたまた そういう 勝手なことをする……☆」
= (λxyz.xz(yz)) (λx. x+1) (λy. y-1) (λz.z*2) 5
? (λxy .x (y )) (λ .(λ z. z *2)+1) (λ .(λz.z*2)-1) 5
(λxy .x (y )) (λ z. z *2 +1) (λ z.z*2 -1) 5
? (λx .x ) (λ .(λz. z*2 -1)*2 +1) 5
? (λ .(λz. z*2 -1)*2 +1) 5
(λ z.(z*2 -1)*2 +1) 5
? (λ .(5*2 -1)*2 +1)
^ ^ ^
(λ .( 9)*2 +1)
(λ . 19)
19
「 ↑ｚに５を入れてみようぜ☆
19 になってそうだけどな☆」
「 しかし 計算順序を ぐちゃぐちゃ にして出したものは 答えと言えるのか……☆？」
「 計算順序を ぐちゃぐちゃ にしても 結果が合流するのが 強味なんだけどな☆」
＜次の記事へ＞
光速のアカウント凍結されちゃったんで……。ゲームプログラムを独習中なんだぜ☆電王戦IIに出た棋士もコンピューターもみんな好きだぜ☆▲(パソコン将棋)WCSC29一次予選36位、SDT5予選42位▲(パソコン囲碁)AI竜星戦予選16位
Crieitは誰でも投稿できるサービスです。 是非記事の投稿をお願いします。どんな軽い内容でも投稿できます。
また、「こんな記事が読みたいけど見つからない！」という方は是非記事投稿リクエストボードへ！
こじんまりと作業ログやメモ、進捗を書き残しておきたい方はボード機能をご利用ください。
ボードとは？
コメント