第６回です。５章のつづき。
前回「カットするかしら」とか話した部分になりました。型無しラムダでのいろんな表現。
引っ越して生活がかわってから、
ちょっと勉強時間が前ほど取れない感じになってしまっていたりします。つらさがある。
でははじまり。
前回のあらすじ：
「なんかラムダ式とかいうの来た」
「式の中にある文字と、外からその式の中に入っていく文字、みたいなルールだけある」
「それイジってたら真偽値とか論理演算とかできたｳﾞｫｰｰｰｰｰｽｹﾞｰｰｰｰｰｰ」
はい。
５章２節 ラムダ計算でのプログラミング
前回の真偽値、論理演算を超えて、更に発展していく話です。
ぶっちゃけどんどん難易度が上がっていく様子に自分はまるでついていけていませんし、
更にはこれを進めていく意味もあまり理解していません。そんなにピンときていない。
とりあえず「この計算体系だけでこんだけ色々表現できるんや、ヤバないか？」とだけ見ています。
というわけで、
「こういうのを満たす式、考えてみない？」
→考えてみる
→なんもわからん
→答えみる
→なんもわからん
を繰り返しがちな状況なので、書いてあることをぼちぼち紹介していくだけ説があります。ひどい。
2つ組
タプルっぽいもの。という理解。いや実際そうだと思います。
pair = λfsb. b f s
fst = λp. p tru
snd = λp. p fls
pair A Bとかって使う感じのヤツ。
fst (pair A B)とするとfstの中のpにpairが入って、中のtruによってAが選ばれる。
sndはflsを持っているのでBが選ばれる。
というかんじ。イメージできる。このへんまでギリギリついていけてるんですよね。
（truが手前、flsが後ろの引数を選ぶとかそういうのは前回を参照していく感じで...）
Church 数
値です。
値。数字。
C0 = λsz. z
C1 = λsz. s z
C2 = λsz. s (s z)
「0をzとして、sをｎ回適用したものを数値ｎとして扱いま～す」くらいの意味。
前回のtru、flsと同じですね。「とりあえずこの形をそう呼ぶことにするわ」っていう。
そう、前回と同じなんだよな・・・
↑図．思い起こされる「前回と同じ」
後者関数
まあこれは妥当な話題です。というかさっきから居るやつだと思う。（sのこと）
要は１コ後の値。３章あたりで通った話題な感がありますね。ただの別の表現。
（あえて言う必要があるか謎ながら、Church数のs,zは明らかにsucc,zeroですよねという話）
succ = λnsz. s (n s z)
考え方に慣れてたら簡単そう。
なお僕は「λn.s nでいんじゃね？」とか考えてました（不正解）
（ちなみにこの不正解にC2を入れたらs λsz.s (s z)とかになります）（処理が足りないね）
要はまあsを適用する回数を増やしたいのと、sとzを入れ直してあげようという図です。
それから、冊子上ではここの演習で別の形のsuccを求めるように言われていますが、
こっから先のこの手の演習がミリも解けねえんだよなあ・・・。
足し算
できるんすよ。聞いてみれば確かにというか。賢ければ思いつくなというか。
plus = λmnsz. m s (n s z)
うーんわかる。今聞くとわかる。
初めて読んだ当時の僕は、上の後者関数での間違いから日を跨いでここを読んでおり、
また「λmn. m s nじゃね？ micro soft networkじゃん」とか言っていました。
理屈としては単純で、「ゼロの部分に前の値を入れればいいじゃない」ということだと思います。
んで「前の値」というのは、ちゃんとsとzを入れた状態のヤツな、と。
あとは自動的に被加算値のsが適用されていきます。
これはs (s ...(s z)を見たら視覚的にさえわかりやすいレベル。
そんで。
掛け算
times = λmn. m (plus n) C0
た・・・ったしかに～～～？ うお？ おう？ たしかに～！？！？
みたいな。（みたいな。じゃなくてね）
足し算ができれば掛け算もできる。そうだねと思いますよ。
よくよく思えば「sをｎ回適用した式を値ｎとする」みたいな話でしたからね。
定義から掛け算だねみたいな。いやわかンねェし思いつかねェけど。
中身を話すと、
Cm = λsz. ナントカに対して、sにplus n、zにC0を渡しているわけですね。
したらあとは、わかりやすく算数の式にしますけど、
m * n = (n + (n + (n + (n + ...m回やる...(n + 0)))m個のカッコ))) //（あんまりピンと来ないながらマジで理解しようという方は、 // 手元で式変形をしてみて`plus n`を入れまくってみるといいと思う感じですよ）
となっておるわけですね。zに渡すのがzでなくてC0なのは、
plus nのもうひとつの引数になるからですね。そしてその答えがまた次の引数になる。
冪乗
やることが複雑化しているように感じてきました。勘弁してほしい。
pow = λmn. n (times m ) C1
といいつつわりと単純ではあるんですが。
ちょっと書き下すと、
// 2^3でもやるか（pow m n は m^n)
= pow C2 C3
= C3 (times C2) C1 // ↑の定義を展開してC3，C2を代入した
= (λsz. s (s (s z)) (times C2) C1 // C3を展開した
// = (2* (2* (2* 1) // 書くのしんどいしこっちのがわかりやすいかなと思って算数の式にした
となるわけで、まあ納得はしますけど、
Church数からここまで等速で進められる奴絶対天才だと思う。
そういうレベル。
とはいえ、自分でウンウン唸りながら手元の計算で遊びまくった上で記事を書いている今、
なんとなし考え方に追従できはじめたような気がしましたが、
なんか知らないうちに抽象化が進んでませんかね。ついてこれてますか。
ちなみに僕は今日の記事の内容だけで一週間とかかけてますからゆっくりでいいですよ。
そしてここからが本当の地獄だからな。
ゼロ判定
iszero = λm. m (λx. fls) tru
ぼく「？？？？？？？？？」
本「
Church数がゼロかどうかを判定するには、その情報を返すような適切な引数を二つ見つけなければならない。具体的には、
zzにssを1回以上適用するとfls、全く適用しないとtruを返すような二つの項zzとssを見つけ、それらに対して判定したいChurch数を適用する。明らかに、zzは単なるtruとすべきである。ssには、引数を無視して常にflsを返す関数を用いる。
」
本を読んでいた当時、僕のしがない認識ではこうです。
C0 = λsz. z
// これは fls と同じカタチなので (→第二引数を選ぶやつである)
iszero = λm. m (なんかflsになるやつ) tru
// 第二引数にtruを置いた 他の値を入れた時にtruを選びうる形があるのかとか謎
みたいな。みたいなとしか言えませんよ。なんせ大した理屈がない。
これに対して、えっとなんですか。
「適切な引数を二つ見つけなければならない」とか。勝手に（使命感）みたいになっちゃって。
そもそもzzとかssとか何なんですか。こちとらそういう話がしたい。
まあなんかssが(λx. fls)でzzがtruみたいですね。はい？
うお？
（記事を書きながら理解っぽいものを感じてしまい、書きかけの文をどうするか迷っている顔）
これはどうやら、
「C0だとtruで～」よりも「Cnだとflsで～」を考えたほうがよいやつな気がしてきました。
（当然のように書き続けることを選んだ顔）
C2 = λsz. s (s z)
ここから先、上の引用文を初めから読めていた人には完全にいらないトークになるんですけど、
どうやらこの(C2とかの)状況を思い浮かべながら読むとよいものだったみたいですね。
あと、「sには常に引数を1つ入る関数が入る」という認識があると尚よさそう。当然ですけど。
というわけでさっきの引用文がどういう話かというと、
s、zにまた何か入るわけやが、それぞれss、zzとして考えよか。
C0んときはzまんまやな。やったらそらzzはtruそのまま入れといたらエエな。
他の値だとsが出てくるから、こいつが絡むといっつもflsになるようにしよか。
そんならssはλx. flsとかでええんちゃうか。
という文章だと読み下せますね。（これを読み下しというのか？）
僕個人の理解しやすさベースで勝手に付け足すと、
実際
(ss zz)も(ss (ss zz)もfls返るな。勝ちや。
となりました。
今かなりのアハ体験を得ながら文章を書いています。自分の言葉で記事にするってしゅごい。
（マジで記事作成開始当初なんもわかってなかったんですよこのiszero）
（ていうか掛け算とかも記事を起こす前は今と比べて全然整理できてませんでしたからね・・・）
それではiszeroも紹介したところで次、と言いたいところですが、
なんか明日の業務に支障が出そうな時間帯になってきてしまったため今回はここでおわりです。
まだあと少し続きます。 続きの内容ですけど、引き続き、現状は理解している感が全然ありません。大丈夫か。
淡々とモノを紹介していくフェーズなために成果っぽいものがない回となりましたが、
ぶっちゃけボリュームとしてはいつもこんなんよな・・・という気持ちも込めて。
尻切れトンボなかんじなので、また早いうちに続きをしにきます。（希望）
では！おやすみなっさい～！（不特定時刻に読まれる記事で大胆な挨拶を書く行為）
