型システム入門を読んでいます（第５回）

当ブログのメインコンテンツこと（？）、型システム入門読書回です。

５章 ラムダ計算に入りました。
テンションが上がり気味な内容になっています。

ではどうぞ。

第5章 型無しラムダ計算

早速。

ええと"ラムダ"という単語が出ました。おネツですねこの単語。
色々調べましたが、フタを開けたら「関数のこと」みたいな感覚でよさそうです。
「慣習として関数に対してこの文字λ使うわ」くらいの歴史があって、
以降、関数っぽいもの(処理部分があってそこに値を代入する感じの)には
とりあえずラムダラムダ言っとけという感じ。（ホントか？？）

なんか突然カッコイイ名前が付いてるんで何か特有の概念があるのかと思ったんですが、
どうやらそうではないよということで。
ちなみに、「この文字λ使うわ」の段階の採用経緯は、
「諸説あります」レベルでしかないっぽいです。

総和での∑みたいなわかりやすい理由？とかがあったら、
色々腑に落ちてうれしかったんですが。まあよし。
（∑がギリシャ文字におけるＳで、Summation(合計)の頭文字として・・・みたいな）

というわけで、かつてC#とかF#とかで「ラムダ式」という単語に出くわして
「なんやねんこいつ・・・やってんのはプチ関数用意するくらいだけど・・・名前何・・・」
となっていた過去の自分に対しては
「関数式って名前だと思ってエエで」
と伝えてやりたい所存です。そんなかんじ。

同じようなモニョりを抱える人がいたらと思ってここまで書きましたけど、
皆そういうの気にするかしら。ワカンナイッスネ！

---

5.1 基礎

というわけでラムダ計算はじまります。今までのやつ章タイトルだけに対する文章かよ。
ラムダ計算というのは、プログラマ各位が関数関数と呼ぶ奴らのご先祖さんと言う感じ。

～ここからなのやつ氏の感想（実際に正しいかしらんやつ）～
実際のところ関数。
みんなが知ってる「関数」を究極にシンプルにしたもんだと考えてよさそう。
is Aのやつ。ラムダイズ関数。けど関数イズラムダかというとちがう。みたいな。
～ここまでなのやつ氏の感想（実際に正しいかしらんやつ）～

では定義。

  t ::=       // 項：
       x      // 変数
       λx.t   // ラムダ抽象
       t t    // 関数適用

はい。

F#もそうですけど、関数型言語の文法っていうのはこういうところから来ているんだなーと思った所存。
（関数適用らへんにフォーカスして発言しています）

それぞれ書くと、

• 変数
  変数。プログラミング的にはその中になんか値が入っていそうですが、
  今はこの文字そのものが値です。（？）
• ラムダ抽象
  ちょっと面倒めな単語を使っていますが、まあ(関数)式のことです。
  λの後の文字が引数変数。
  たとえば↑のtの中身がxだとしたら、λx.xとなって、
  これは「引数をもらってそのまま返す関数」みたいな。
• 関数適用
  引数に代入したらよろしい。
  ↑のt tをt1 t2として、t1がλx.x、t2がyだとしたら、
  (λx.x) yとなってyがxに入り、結果はyですと。
  いきなりやりましたけれど、操作としては
  「いちばん近い引数を突っ込んで、λ*の文字を消す」
  感じだと思っておいてよさそう。あとは実践。

と。
最後微妙に詳しく書き気味でしたが、なぜかと言うと、
この後に続くラムダの文法っぽい話をスキップするためです。

見ての通りカッコとかで補足しないと曖昧な表記になるわけですが、
5.1基礎の続きではそのへんに対する記述がありました。

まあまとめておくと、

• 書いた式は簡約(＝評価)していくやで
• 関数適用は左から順にやってくやで（カッコが要る部分要らない部分の話）
  →関数M 引数A 引数B 引数C...とあったらAから入っていく
• 簡約にはいろんなやり方があるけどこっから先はこういう手法を使うやで
  →色々紹介されたものの、最終形には特に差がない。
  　ぶっちゃけ自分はあまり気にしていません
• 実は引数１コしか取れんのやけど、ラムダ抽象をまたラムダ抽象でくくれば解決するやで
  →式：x y z に対して、(λz.λy.λx.x y z)と書けば3引数取れる(→高階関数)
  　(λz.λy.λx.x y z) a b cを簡約したら、
  　zにa、yにb...となって、c b aになる

こんなくらい。
まあ「こんなことやるよ～」と構文を定義してからの、ルールとかを詳しく書くフェイズなので、
あんまり学問的な脳みそでない僕とかは、
「なにを必要以上に小難しく言うてんねん？？？」となるやつです。大丈夫だろうかその理由。

---

5.2 ラムダ計算でのプログラミング

で。やっと。
やっとここ。

この　節　is　神　。 (誇張表現)

いや、突然何かという話ですけどね。
↑で色々定義したじゃないですか。こいつ。λナントカ。

ぶっちゃけた話ですけど、

「で、コレが何になんの？　値入れるだけしか無いんか？　よっわ（笑」

みたいな気持ちありませんか。僕はあったんですけど。

ここからもうなんかヤバいんですよ。見ててくださいよ。
ヤバい。天才しかいないので。（語彙の喪失）

まず、いきなりtru,flsを定義し始めます。

  tru = λt.λf.t
  fls = λt.λf.f

いや意味わかんないですよね。
TRUE,FALSE言いたいんやろけど何やねんそれみたいな。どこが真で偽やねんと。
実際この段階では「この形λA.λB.AだったらTRUEってことにしとこ」でしかないんですが、
こいつが飛躍的な進化をします。

そこからノータイムでいきなり出てくるのがこちら。

  test = λl.λm.λn.l m n

は？？って感じじゃないですか。
またこれよく見たらクッソ単純な式ですよ。ていうかtestって名前何。
これにですね、さっきのtruとかflsとかを入れるわけですね。

  test tru A B                      // 引数にtruとなんかの値A,B
= (λl.λm.λn.l m n) tru A B          // testを展開した
= (λm.λn.tru m n) A B               // lに入っていく
= tru A B                           // m,nに入っていく
= (λt.λf.t) A B                     // truを展開した
= (λf.A) B                          // tに入っていく
= A                                 // 引数fを取る関数の中にfがおらんかったらそらなんもせず引数は消える

  test fls A B                      // 引数にflsとなんかの値A,B
= (λl.λm.λn l m n) tru A B          // testを展開した
= (λm.λn.fls m n) A B               // lに入っていく
= fls A B                           // m,nに入っていく
= (λt.λf.f) A B                     // flsを展開した
= (λf.f) B                          // 今回はここで引数が使われていないので消えていく
= B                                 // で、fに入っていく

おわかりいただけただろうか。 if式んなっとるぞこれ・・・・・・・・・・・・・・・・・。

衝撃は止まりません。
どうやら論理演算ができる模様。

  and = λb.λc.b c fls

「んなアホな（笑」感のある式ですけど。

  and tru fls
= (λb.λc.b c fls) tru fls
= tru fls fls
= (λt.λf.t) fls fls
= (λf.fls) fls
= fls

  and tru tru
= (λb.λc.b c fls) tru tru
= tru tru fls
= (λt.λf.t) tru fls
= (λf.tru) fls
= tru

ヒエッ・・・

天才じゃない？？？？天才ですよね？？？？？？
なんかチャーチさん？Churchさんって人が考えたらしいんですよこれ。天才でしょ。

僕らやってたのアレですよ、なんか文字並べて、どこにどれを入れるかしてただけ。
それがなんか意味を帯び始めてるんですよ。僕はビビってますよ。
伝わりますか？伝わってますね？こんなんおかしい。

いやまあどうやら世の中にはそういうものがあるというのはわかります。経験があります。
論理回路って言うんですけどね、要するにコンピュータのゼロイチと電気の話です。
電気回路みたく線を繋いで行って、その線の中身は電流ON,OFFのどちらか、
つまりはゼロイチのどちらかということだけが決まっていて、
なんかそれを組み合わせていくとANDとかORとか数字とかになる。
似てますね。似てませんか。まあ似てるかどうかはどうでもいいんですけど、
かつてそれをお勉強した時と同じ気持ちになりました。僕は。
このChurchさんの示したラムダ計算体系で。

というのを感動として伝えたかった。僕からは以上です。
ぶっちゃけ型システム入門のこの部分を読んでビビリ散らかしたのは10月6日頃なんですが、
10月20日現在も未だにラムダ計算のトリコかもしれません。ひたすら考えている。

オススメはCombinator Birdsというこのページです。
その元ネタらしきものまね鳥をまねるという本↓も興味がありすぎてたまらんのですが、

数学パズル ものまね鳥をまねる―愉快なパズルと結合子論理の夢の鳥物語

どうやらKindle版がないので手をこまねいています。
なのでKindle化リクエストを押してください。（ダイレクトマーケティング）（オチ）

---

第５回はこんなところで。

次回に続きますが、
この後のラムダ計算によるいろんなモノの表現を1つ1つ書いていくかは怪しい所です。
（本の内容を全部書き下すことになっちゃうし）

流して見ている感じ、あと10ページくらいの間は
ラムダ計算体系の拡張とかが続く(今回ビビリ散らかした部分は２ページ分)ので、
まだまだ先は長いなと思いながら、ラムダ計算体系の実装を待ち遠しく進めていく感じです。

ちなみに、冊子全体のページ番号では今回の内容で４６ページです。マジでなげえ。

おまけ：iPadにつらつら書いていた計算跡

おわり！