「　みんな大好き　ラムダ計算　の辞書編だぜ☆
そこらへんの知らん人が書いた　ブログ記事　を読むときに　索引引きできるように　アルファベット順に書くぜ☆」

「　お父んが　自分の記事を　ぐちゃぐちゃに　してしまったからな☆」

「　ぱーっ　と　項目に飛べるようにしなさいよ。　ここは　ハイパーテキストなのよ？」

「　なんで　ぐちゃぐちゃになったんだろな☆？」

「　お父んの頭が　ぐちゃぐちゃ　だからだぜ☆」

「　項目で　関連　の内容に触れてはいけないの！　読者が嫌がっても　たらい回し　にリンクで　別項　に飛ばしなさい！」

https://crieit.net/posts/504fe6cd1464cf678c942c45ef473f45#alpha-conversion

「　しかし記事のタイトルを みんな大好きラムダ計算☆ｍ９（＾～＾） にしてしまったので
URL　が　むちゃくちゃ　で　Base64　だか　ランダム16進数　みたいになってしまったぜ☆
わたしは　こんな世界が嫌いだぜ☆　宇宙を滅ぼして歴史を作り直そうぜ☆？」

abstraction

lambda abstraction、ラムダ抽象、アブストラクション

「　↑上式でいうと、どこを指して　アブストラクション　って言ってるの？」

「　ここだな☆
丸かっこは　付けたり省いたり　するので、　含めないと考えた方が　すっきりするだろう☆」

「　どうやって見分けるの？」

「　左の隅っこに　ペンギン　みたいなやつがいるだろ☆
こいつは　ギリシャ文字の１１番目の文字　ラムダ　だぜ☆」

「　ペンギンの左隣に　開き丸かっこ　があれば、それに対応する　閉じ丸かっこ　までの中身が　アブストラクション　だぜ☆
ペンギンの左隣に　開き丸かっこ　がなければ、全体が　アブストラクション　だろう☆」

「　もう少し　要点を伝えると☆、」

「　アブストラクションの真ん中には　ドット　が置いてあって、左側と右側を分けているぜ☆」

「　今どきよく見かけるプログラム言語の用語で表すと、
ドットの左側は　パラメーター・リスト（Parameter list; 仮引数リスト）、
ドットの右側は　返り値（Returns a value; 戻り値）　だぜ☆」

「　ラムダ計算の用語で表すと、
ドットの左側は　変数（Variable; バリアブル）、
ドットの右側は　Ｍ（エム）　だぜ☆」

alpha-conversion

α-conversion、α変換、アルファ変換

「　式の答えを変えずに、評価しやすいように　式の見た目を変えることを　conversion(変換) とか redex(簡約) と呼んでいる☆
つまり　アルファ変換　は　評価ではなく　式の整理だぜ☆　詳しく見ていこう☆」

「　じゃあ、　ｘ　を　ｚ　に　アルファ変換　してみようぜ☆？」

「　ｚ　なんて　どこにあるの？　上図には　ｘ　と　ｙ　しか見えないけど？」

「　ｚ　が　あるつもりで☆」

= (λx.x)y
= (λz.z)y
    ^ ^

「　仮引数　　ｘ　を　ｚ　に変えたのなら、アブストラクションの　ｘ　も　ｚ　に変えるのよね」

「　そうだぜ☆　プログラム中の　ここらへんの　ｘ　は　ｙ　に置き換える、ぐらいの感じだぜ☆」

「　まるで　文字列置換ね」

「　まったく　文字列置換だぜ☆」

「　なんで　こんなこと　するの？」

「　変数のアルファベットは　２６個しかないのに、使い回すからな☆
名前が衝突するのを　防ぐだけ　だぜ☆」

「　これは　計算　なの？」

「　筆算で間違えないためにプロセスで行われるテクニック　は　計算の本質　だぜ☆
答えだけ欲しけりゃ　答えだけ書いて中間・期末試験で正解し続けて　受験で間違えろだぜ☆」

application

アプリケーション、適用

「　↑上式でいうと、どこを指して　アプリケーション　って言ってるの？」

「　これはもう　アプリケーション　されてるなあ☆」

「　↑２つのラムダ項を　１つの式にするのが　アプリケーション（Application; 適用）　だぜ☆」

  ((λx.x+1)(y*2))
!=((y*2)(λx.x+1))

「　右にくっついている方が　左のパラメーターに渡されるんで、　逆にすると　評価の結果は変わってくるぜ☆」

「　本当か☆？　やってみろだぜ☆」

「　評価は　めんどくさいのに……☆」

=((λx.    x+1)(y*2))
 ((λ_.(y*2)+1)_____)
    ^ ^^^^^   ^^^^^  # β-redex
 ((λ .(y*2)+1)     )
 ((λy.(y*2)+1)     )
    ^                # Bind the variable
 ((λy.(y*2)+1)     )
= (λy.(y*2)+1)     
 ^                 ^ # Erase paren

=((   y*2)(λx.x+1))
 ((λy.y*2)(λx.x+1))
   ^^^                 # Bind the variable
 ((λy.    y*2)(λx.x+1))
 ((λ_.(x+1)*2)________)
    ^ ^^^^^   ^^^^^^^^ # β-redex
 ((λ .(x+1)*2))
 ((λx.(x+1)*2))
    ^                  # Bind the variable
 ((λx.(x+1)*2))
= (λx.(x+1)*2)
 ^            ^        # Erase paren

「　例えば　変数に３を入れてみろだぜ☆　７と　８、違うぜ☆」

「　先に＋１　するのと、　後で＋１　するのとじゃ　結果が違うのよ！」

beta-redex

β-redex、β簡約、ベータ簡約

「　式の答えを変えずに、評価しやすいように　式の見た目を変えることを　conversion(変換) とか redex(簡約) と呼んでいる☆
つまり　ベータ簡約　は　評価ではなく　式の整理だぜ☆　詳しく見ていこう☆」

「　じゃあ、　とりあえず　λｘ　を　ベータ簡約　してみようぜ☆？」

「　この　電池　みたいな図は　何なのか……☆？」

= (λx.    x+1)(y*2)3
  (λ_.(y*2)+1)_____3
    ^ ^^^^^   ^^^^^

「　仮引数ｘを消して、第一実引数に置き換えましょう」

= (λx.    x+1)(y*2)3
  (λ_.(y*2)+1)_____3
= (λy.(y*2)+1)     3
    ^

「　このとき、自由変数ｙは　束縛されるわね」

= (λx.    x+1)(y*2)3
  (λ_.(y*2)+1)_____3
= (λy.(y*2)+1)     3
  (λ_.(3*2)+1)     _
    ^  ^           ^

「　仮引数ｙを消して、第二実引数に置き換えましょう」

= (λx.    x+1)(y*2)3
  (λ_.(y*2)+1)_____3
= (λy.(y*2)+1)     3
  (λ_.(3*2)+1)     _
= (_ _(3*2)+1)
   ^ ^

「　実引数が無くなったので　ラムダ式　は消えるわね」

「　じゃあ　答えは　６　だな☆」

= (λx.    x+1)(y*2)3
  (λ_.(y*2)+1)_____3
= (λy.(y*2)+1)     3
  (λ_.(3*2)+1)     _
= (_ _(3*2)+1)
= (   (  6)+1)
       ^^^
= (         7)
      ^  ^^^^
=            7
  ^         ^^

「　７ね」

eta-conversion

η-conversion、η変換、イータ変換

「　式の答えを変えずに、評価しやすいように　式の見た目を変えることを　conversion(変換) とか redex(簡約) と呼んでいる☆
つまり　イータ変換　は　評価ではなく　式の整理だぜ☆　詳しく見ていこう☆」

「　じゃあ、　ｙ＋０　は　イータ変換　できるんで、やってくれだぜ☆」

「　イータ変換できることが分かってるのなら　この　イータ変換　の項目なんか　要らないんだけどな☆」

= (λx.x+1)(y+0)3
           ^^^

「　y+0　って、なんの働きもしなくない！？」

= (λx.x+1)(y+0)3
= (λx.x+1)_____3
          ^^^^^

「　ベータ簡約するのも　しちめんどうくさい　から消しちゃいましょう」

= (λx.x+1)(y+0)3
= (λx.x+1)_____3
= (λx.x+1)3
          ^^^^^^

「　これでも何も結果は変わらないのよ！」

「　これは　計算　なのかだぜ☆？」

「　式の整理　は、計算の本質だぜ☆
１＋１＝２　とか　誰かが立てた式の評価　ばかりしていては　寿命が尽きてしまう……☆
式を立てろだぜ☆」

「　なんの働きもしない　というのが　何のことか分かっていない読者もいるだろ☆　説明がいるのでは☆？」

「　しちめんどくさいわね！」

= (λx.    x+1)(y+0)3
  (λ_.(y+0)+1)     3
    ^ ^^^^^   ^^^^^

「　xをベータ簡約しましょう」

= (λx.    x+1)(y+0)3
  (λ_.(y+0)+1)     3
= (λy.(y+0)+1)     3
    ^

「　ｙを束縛しましょう」

= (λx.    x+1)(y+0)3
  (λ_.(y+0)+1)     3
= (λy.(y+0)+1)     3
= (λy._y+0_+1)     3
      ^   ^
= (λy. y__ +1)     3
        ^^
= (λy. ___y+1)     3
       ^^^^

「　丸かっこを整理して　四則演算を評価しましょう」

= (λx.x+1)(y+0)3
= (λy.y+1)     3

「　この２つの式は同値だけど、 y を x に　α変換　しましょう」

= (λx.x+1)(y+0)3
= (λy.y+1)     3
    ^ ^
= (λx.x+1)     3

「　ということは」

= (λx.x+1)(y+0)3
= (λx.x+1)     3

「　y+0　は　有っても無くても　同じなのよ！」

「　何でだぜ☆？」

「　ぬぎぎぎぎぎ！」

「　α変換　してんのと同じなら　省いていいだろ☆」

「　そうなのよ！」

「　分かったぜ☆」

variable

「　ヴェリアボー　って何だぜ☆？」

「　そんな棒はない☆」

「　基本的に　パラメーター（Parameter; 仮引数）のことを　Variable　と呼んでいるが、
仮引数以外のところにも　Variable　はいる☆」

「　例えば　Returns a value（返り値; Ｍ）のところにいる　ｘ☆
仮引数に並んでいるので　Bounds variable（束縛変数）だぜ☆」

「　例を少し変えよう☆」

「　↑上図で　Returns a value（返り値; Ｍ）のところに　ｙ　がいるとしよう☆
仮引数には並んでいないし、　特にｙがローカル変数と宣言はしていないので　Free variable（自由変数）だぜ☆」

「　このｙは何なの？」

「　例えば　グローバル変数　かも知れないな☆
この式の中に　ｙとは何か、が書かれていない　本当の引数、本当の変数だぜ☆」

「　じゃあ　束縛変数は　ウソの変数か☆？」

「　式をたどっていけば　どこかに　ｘ　に入る数や　関数があるかもしれない☆」

＜おわり＞