型システム入門を読んでいます（第７回）
～～ぜんかいのなのやつさん～～
尻切れトンボなかんじなので、また早いうちに続きをしにきます。（希望）
～～３週間経過～～
ホントそういうの勘弁しろよ。
はいそういうかんじで。こんにちはこんばんは。（動画配信者感）
その、実は今実質一人暮らしではなくなっていたりして、
ちょっとばかり家で一人の時間を確保しにくくなっていたりするんですよね。
以上言い訳でした。レッツTaPL。
前回までのあらすじ。
「ラムダ式で色々表現してんで」
「わりと式変形が板についてきたんちゃうか」
「ゼロ判定なんもわからん」
「この先のやつらもっとわからんな」
「引き続きいろいろ表現するフェイズ（たぶん今回で一区切り）」
前者関数
TaPL的には、減算の定義をしようとして
驚くことに、Church数を使った減算は、加算よりもかなり難しい。以下のかなりややこしい「前者関数」を用いれば可能ではある。
とか言って出てくる感じです。
遂にこの本がかなり難しいとかかなりややこしいとか言い出した。心を折りに来ている。
それで、出てくるもの。
zz = pair C0 C0
ss = λ.p pair (snd p) (plus C1 (snd p))
prd = λm. fst (m ss zz)
今導きたいものがprdですね。定義としてはprd C0 = C0でprd (Cn) = (Cn-1)。
なんかよくわかんないですけど簡約？代入？していきますか。ていうかssヤベエな。
// とりあえず使うやつ（前回の記事からコピペ）（tru,flsあたりは覚えたということで・・・）
pair = λfsb. b f s
fst = λp. p tru
snd = λp. p fls
plus = λmnsz. m s (n s z)
prd N //なんかの値N
= fst (N ss zz)
// Cn ss zz でpairの形(次元？型？まあなんか引数の数とかの形)に一致するらしいな～という雰囲気
= (λp. p tru) (N ss zz)
= (N ss zz) tru
// Nをなんかの値にせなあかんっぽいので C3 = λsz. (s (s (s z)) とかにする
= (ss (ss (ss zz) tru
式としてはここで既にいい感じの意味になっているはずだと読んだので止めました。
いい感じの意味というのは、λsz.(s (s z))に落ちる流れが見て取れるはず・・・みたいな。
やまあ雰囲気なわけですけど。
// (ss zz) を見ていく所存
ss = λ.p pair (snd p) (plus C1 (snd p))
zz = pair C0 C0
ss zz
= pair (snd (pair C0 C0)) (plus C1 (snd pair(C0 C0)))
// 'snd (pair C0 C0)' に 'C0' と書く以上の意味があるのか謎すぎてしんどくなっているなのやつ氏
= pair (C0) (plus C1 C0)
// なので丸めた
これのpairの中にtruが乗るので、確かに左側が選ばれてC0で、C1の1コ前だなとなりました。
それから、最後にtruがかかって選ばれるということで、
zz = pair C0 C0もたぶんそういう形。（たぶんそういう形ってなんだ）
しんどいですけど、もう一回ssをかけてみます。（prd C2相当）
= (ss (pair (C0) plus C1 C0)) tru
= (λp. pair (snd p) (plus C1 (snd p)))
(pair C0 plus C1 C0)
tru
まとめ。
前回ほどの深いわかりはないんですが、
ゼロをzzのpair型として扱い始めることで、
ssをかけて「そのままの値＆１コ増やした値」の組にできて、
元のChurch数のsの回数によってなんかそういうのが組み立てられて、
途中の計算のほうには後ろの「１コ増やした値の方 」を(sndで)使いつつ、
最後にはfstで手前のほうを選ぶと値が１コ減る・・・らしい。らしい。
言われていた通り複雑度が高くて「ヨッシャ理解した」感が薄いんですが、
理屈は↑の通りだと思います。たぶんこれ以上に理屈はなさそう。
これで「ヨッシャ理解した」とならないのは、
頭の方に修行が足りない気がします。（辛辣）（自分の首を絞める）
引き算
で、これがあると引き算ができるらしいです。理屈はわかるような？
１コ減らすやつ(prd)があるので、減数のsの数ぶんprdが増えるようにして、
それを被減数にかければよいのでは？というかんじ。
ただし式はわからん。
minus m n = λmn. (n prd m)
なんかこんなん。（イメージ）
答えをみた。（減算関数の導出は演習方式でした）
解答 5.2.5.
substract1 = λm. λn. n prd m
合っとる・・・・・・・・・・・。
これでいいということにしてほしい。（ボロが出がち）
等価関数 equal
Church値を2つ渡して、同じ値だったらtru、違う値だったらflsを返すやつ。
しれっと演習として出題されている。のに見事にわからん。すごい。
equal C3 C3
= λtf.t
equal C2 C3
= λtf.f
こういう。
引き算してゼロ判定でもするか・・・？（メッチャ無駄そう）
こたえ。
解答 5.2.7.
equal = λmn. and (iszero (m prd n)) (iszero (n prd m))
・・・？？？？？？？？？？？？
(m-n)がゼロか見る(n-m)がゼロか見る- そいつらの論理積
そうかC3-C5とかしてもC0なのか・・・この世界・・・。
なので、C5-C3(C2になる)も確認して、それから論理積でした。
（メッチャ無駄そう）とか言ったやつ誰だよ
等価演算ってムズいんですね・・・（？）
でもこれ、この形式の数値にだけ通じる評価ですね。
等価そのものの複雑さよりは、Church数が等価確認と相性が悪い、みたいな感じがある。わからん。
こんなもんにしといたろ（瀕死）
実はだいたいここまででラムダ式列挙タイムが一旦終了です。
次回以降、「計算体系の拡張」としてプリミティブな値とかが混ざってくる模様。
今回のお勉強は前回ほど「言葉にしてたらなんかメッチャ掴めたわ」という感が薄いですが、
それでもそれぞれ整理しながら行けたかなという感じです。
11月以降、ひどくゆっくり進行になってしまっていますが、
引き続きボチボチやっていきます。F#書きてえな・・・。
では！
