今日一日で勉強した個人的なメモ．厳密な定義等を記すためではなく自身の理解の一助となるための記事であることを付け加えておく．
むしろだれか厳密性のあるつっこみとか下さい,おそらく間違えまくりです．
まず初めに，この記事で紹介されてるリンクがとっても素晴しかったです．
独学でラムダ記法学びたい人これを参考にしたほうがいいかも
「ラムダ計算」を独学で学習するための，講義ノートやPDFのリンク集 （復習用の問題付き）
定義をどっか参照しながらとかじゃなくて勢いとうろ覚えで書いた記事なのでいくつかの
函数間違っているかも
ラムダ記法
f(x) = x+2みたいなのをλx.x+2と表す
f(3) = 3+2 =5は
(λx.x+2)(3) -> 3+2 -> 5という風なかんじ
ラムダ項
計算可能な無限集合を<identify>としたとき次の3つがラムダ項<expr>
自由変数と束縛変数
とあるラムダ項Mについて，
λx.Mというラムダ項があるとき，Mの中の変数xは束縛されている．
このときMの中のx以外の変数は束縛されていない(=自由変数)
カリー化
f(x,y)=xという函数はλ式で
λxy.xと記すことができる．
これは略記であり
λx.(λy.x)と記すことができる．
これは引数xを受けとると引数yをとってxを返す函数を返す函数(=高階函数)になっている．
こういう風に複数の変数の函数を1変数函数の高階函数の形にすることがカリー化(だよね?)
α変換
λx.x+2とλy.y+2は変数の名前が違うだけで函数のやってることは一緒．
これは同値になっている.これを直感ではなくキチンと同値と言うために
λx.x+2 ->α λy.y+2
というふうになる
なんでも変数を別名に変更できるわけではなく，喩えば，
λy.x のxをyに置き換えると
λy.y になり変数がλyに束縛されてしまうために，λy.xとλy.yはあきらかに同値ではない
これはα変換とはいえない
β簡約
ラムダ項M,Nがあるとき，
(MN) -> M'と表せるとき
(MN) ->β M' はβ簡約という
簡単にいうと函数適用をワンステップ行なう
たとえば
(λf.f*2)(λx.x+3)をβ簡約すると
λx.(x+3)*2となる
これ以上簡約できない状態をもつこと->β正規形
β正規形を持たないラムダ項は端的にいって無限ループとか
ex. (λx.xx)(λx.xx) ->β (λx.xx)(λx.xx) ->β ...
η簡約というのもあるそうです
べんりなラムダ項
S:=λxyz.xz(yz)
K:=λxy.x
I:=λx.x
有名なSKIコンビネータ，これでいろいろ記述できる
Iは恒等函数，Kは定数函数で見たままだけれどもSがわかりにくい．
これは，xyzの3つ引数を取るとラムダ項xにzを適用するのとラムダ項yにzを適用する2つの函数適用を返す函数
実はIコンビネータはSコンビネータとKコンビネータだけで書ける
SKK -> (λxyz.xz(yz))(λxy.x)(λxy.x)
-> (λyz.(λxy.x)z(yz))(λxy.x)
->λz.(λxy.x)z((λxy.x)z)
-> λz.(λy.z)(λy.z)
-> λz.(λy.z)z
-> λz.(λz.z)
-> λz.z = I
ちなみにLinuxの有名な日本語変換エンジンのibus上でのSKK IMEの実装であるibus-skkは，
ツールバー上のアイコンがSKK=Iとなってます．イカしてますね．使いましょう．
ラムダ式は函数中に自身の函数を書くことができません．
そこで不動点コンビネータを使います．
不動点はf(x)=xとなるxのことだそうです
高階函数gについて，
任意の関数fをつかってf(g(f)) = g(f)
となる不動点を考えると再帰ができる模様．
ここで不動点コンビネータはいろいろあるけれど一番シンプルといわれるYコンビネータは
Y:=S(K(SII))(S(S(KS)K)(K(SII)))です．
シン……プル……?
ラムダ式でYコンビネータを表すと
Y:=λf.(λx.f(xx))(λx.f(xx))
シンプルですね．
証明
gY = (λf.(λx.f(xx))(λx.f(xx))g
-> (λx.g(xx))(λx.g(xx))
-> g((λx.g(xx))(λx.g(xx))
-> g(Yg)
再帰してますね.
SKIコンビネータのほうでのYコンビネータも
S(K(SII))(S(S(KS)K)(K(SII)))g -> K(SII)g(S(S(KS)K)(K(SII))g) -> SII(S(S(KS)K)(K(SII))g)
-> I(S(S(KS)K)(K(SII))g)I(S(S(KS)K)(K(SII))g) -> (S(S(KS)K)(K(SII))g)(S(S(KS)K)(K(SII))g)
-> S(KS)KgK(SII)g(S(S(KS)K)(K(SII))g) -> KSg(Kg)K(SII)g((S(S(KS)K)(K(SII))g)
-> S(Kg)K(SII)g(S(S(KS)K)(K(SII))g) -> Kg(SII)K(SII)g(S(S(KS)K)(K(SII))g)
-> gSII(S(S(KS)K)(K(SII))g) -> g(Yg)
ちゃんとなってますね! (この簡約があってるかどうかすっごい自信ないです)
次はデータについて
自然数もλ式だけで表せます．チャーチエンコーディングというそうです
0:=λsz.z
1:=λsz.sz
2:=λsz.s(sz)
3:=λsz.s(s(sz))
以下略
ここでnを受けとってn+1を返す函数を
Succ:=λnsz.s(nsz)とする
例
Succ2 -> (λnsz.s(nsz))(2) -> (λnsz.s(nsz))(λsz.s(sz))
-> λsz.s((λsz.s(sz))sz)
-> λsz.s((λz.s(sz))z)
-> λsz.s(s(sz)) = 3
また，
Add:=λmnsz.ms(nsz) = λmn.m Succ n
Mult:= λmns.m(ns) = λmn.m(Add n) 0
のように四則演算もラムダ式で定義できる
例 2+3
Add 2 3 -> (λmnsz.ms(nsz))(2)(3) -> (λmnsz.ms(nsz))(λsz.s(sz))(λsz.s(s(sz)))
-> λnsz.(λsz.s(sz))s(nsz)(λsz.s(s(sz)))
-> λsz.(λsz.s(sz))s((λsz.s(s(sz)))sz)
-> λsz.(λz.s(sz))(λz.s(s(sz)))z)
-> λsz.(λz.s(sz))(s(s(sz)))
-> λsz.s(s(s(s(sz)))) = 5
チャーチ論理値
真偽値もラムダ式で
T:=λxy.x (True)
F:=λxy.y (False)
ラムダ項TはKと，ラムダ項FはKIと等しい
if X then Y else ZはXYZと表記 (X,Y,Zはラムダ項で，Xは簡約したらTかFになる)
TYZ -> (λxy.x)YZ -> λy.Y(Z) -> Y
FYZ -> (λxy.y)YZ -> λy.y(Z) -> Z
ちゃんとif X then Y else Zの動作になる
このif X then Y else Zを使って
And:= λxy.xyF
Or:= λxy.xTy
Not:= λx.xFT
という論理演算も定義できる
データ構造
順序対をタプルという．
2つのラムダ項M,Nに対しタプルを<M,N>と表す．ラムダ項で表現されたタプルはチャーチ対とも．
<M,N>:=λx.xMN
ここで，順序対の最初の項を取り出すFstと最後の項を取り出すSndを定義すると
Fst:=λt.tT
Snd:=λt.tF
となる．
例
Fst<M,N> = λt.tT(λx.xMN)
->(λx.xMN)T -> TMN -> M
Snd<M,N> = λt.tF(λx.xMN)
->(λx.xMN)F -> FMN -> N
これでわかったのは手続き型言語と真逆で，
一切データをや値がなくとも函数の定義と適用だけでプログラムが組めるということである
(値はチャーチ数があるし，データ構造も函数で表現できるし，あとはif文もループ(Yコンビネータで再帰を使う)も函数で表現できる)
いままでラムダ記法は知っていたしJavaScriptの無名函数やC++11,Java8などでlambda式として
それら表記が行えることは聞いていたが，
その高階函数やラムダ記法ができて何が嬉しいかあまりわかってなかった．
チャーチ数やチャーチ論理値，チャーチ対といったプログラミングに必要なプリミティブな要素まで徹底してデータを排除して函数で表記できるのを初めて知って，とてつもなく感動した．
なるほど函数型言語のオモシロさはこういうところにあるのだなーと勝手に納得した日でした．
ちなみに，普通タプルときたらリストだとおもうけれど(Lispなんかで使われるconsとかcarとかcdrとかもラムダ記法でもちろん表現できる),私の理解がおっつきませんでした．理解に良い記事をだれか教えてください
追記:
チャーチ対のFstをCar,SndをCdrとして，
リスト終端を表わすNil:=F
チャーチ対を生成する函数Consを
Cons:=λmn.(λt.tmn)
とすると
(Cons X (Cons Y (Cons Z Nil)))
で
λt.tX(λt'.Y(λt''.ZF))
とかいうリストがつくれる……かな?あってるといいけど
むしろだれか厳密性のあるつっこみとか下さい,おそらく間違えまくりです．
まず初めに，この記事で紹介されてるリンクがとっても素晴しかったです．
独学でラムダ記法学びたい人これを参考にしたほうがいいかも
「ラムダ計算」を独学で学習するための，講義ノートやPDFのリンク集 （復習用の問題付き）
定義をどっか参照しながらとかじゃなくて勢いとうろ覚えで書いた記事なのでいくつかの
函数間違っているかも
ラムダ記法
f(x) = x+2みたいなのをλx.x+2と表す
f(3) = 3+2 =5は
(λx.x+2)(3) -> 3+2 -> 5という風なかんじ
ラムダ項
計算可能な無限集合を<identify>としたとき次の3つがラムダ項<expr>
<expr> := <identify> (変数)
<expr> := λ<identify>.<expr> (ラムダ抽象)
<expr> := <expr><expr> (関数適用)
自由変数と束縛変数
とあるラムダ項Mについて，
λx.Mというラムダ項があるとき，Mの中の変数xは束縛されている．
このときMの中のx以外の変数は束縛されていない(=自由変数)
カリー化
f(x,y)=xという函数はλ式で
λxy.xと記すことができる．
これは略記であり
λx.(λy.x)と記すことができる．
これは引数xを受けとると引数yをとってxを返す函数を返す函数(=高階函数)になっている．
こういう風に複数の変数の函数を1変数函数の高階函数の形にすることがカリー化(だよね?)
α変換
λx.x+2とλy.y+2は変数の名前が違うだけで函数のやってることは一緒．
これは同値になっている.これを直感ではなくキチンと同値と言うために
λx.x+2 ->α λy.y+2
というふうになる
なんでも変数を別名に変更できるわけではなく，喩えば，
λy.x のxをyに置き換えると
λy.y になり変数がλyに束縛されてしまうために，λy.xとλy.yはあきらかに同値ではない
これはα変換とはいえない
β簡約
ラムダ項M,Nがあるとき，
(MN) -> M'と表せるとき
(MN) ->β M' はβ簡約という
簡単にいうと函数適用をワンステップ行なう
たとえば
(λf.f*2)(λx.x+3)をβ簡約すると
λx.(x+3)*2となる
これ以上簡約できない状態をもつこと->β正規形
β正規形を持たないラムダ項は端的にいって無限ループとか
ex. (λx.xx)(λx.xx) ->β (λx.xx)(λx.xx) ->β ...
η簡約というのもあるそうです
べんりなラムダ項
S:=λxyz.xz(yz)
K:=λxy.x
I:=λx.x
有名なSKIコンビネータ，これでいろいろ記述できる
Iは恒等函数，Kは定数函数で見たままだけれどもSがわかりにくい．
これは，xyzの3つ引数を取るとラムダ項xにzを適用するのとラムダ項yにzを適用する2つの函数適用を返す函数
実はIコンビネータはSコンビネータとKコンビネータだけで書ける
SKK -> (λxyz.xz(yz))(λxy.x)(λxy.x)
-> (λyz.(λxy.x)z(yz))(λxy.x)
->λz.(λxy.x)z((λxy.x)z)
-> λz.(λy.z)(λy.z)
-> λz.(λy.z)z
-> λz.(λz.z)
-> λz.z = I
ちなみにLinuxの有名な日本語変換エンジンのibus上でのSKK IMEの実装であるibus-skkは，
ツールバー上のアイコンがSKK=Iとなってます．イカしてますね．使いましょう．
ラムダ式は函数中に自身の函数を書くことができません．
そこで不動点コンビネータを使います．
不動点はf(x)=xとなるxのことだそうです
高階函数gについて，
任意の関数fをつかってf(g(f)) = g(f)
となる不動点を考えると再帰ができる模様．
ここで不動点コンビネータはいろいろあるけれど一番シンプルといわれるYコンビネータは
Y:=S(K(SII))(S(S(KS)K)(K(SII)))です．
シン……プル……?
ラムダ式でYコンビネータを表すと
Y:=λf.(λx.f(xx))(λx.f(xx))
シンプルですね．
証明
gY = (λf.(λx.f(xx))(λx.f(xx))g
-> (λx.g(xx))(λx.g(xx))
-> g((λx.g(xx))(λx.g(xx))
-> g(Yg)
再帰してますね.
SKIコンビネータのほうでのYコンビネータも
S(K(SII))(S(S(KS)K)(K(SII)))g -> K(SII)g(S(S(KS)K)(K(SII))g) -> SII(S(S(KS)K)(K(SII))g)
-> I(S(S(KS)K)(K(SII))g)I(S(S(KS)K)(K(SII))g) -> (S(S(KS)K)(K(SII))g)(S(S(KS)K)(K(SII))g)
-> S(KS)KgK(SII)g(S(S(KS)K)(K(SII))g) -> KSg(Kg)K(SII)g((S(S(KS)K)(K(SII))g)
-> S(Kg)K(SII)g(S(S(KS)K)(K(SII))g) -> Kg(SII)K(SII)g(S(S(KS)K)(K(SII))g)
-> gSII(S(S(KS)K)(K(SII))g) -> g(Yg)
ちゃんとなってますね! (この簡約があってるかどうかすっごい自信ないです)
次はデータについて
自然数もλ式だけで表せます．チャーチエンコーディングというそうです
0:=λsz.z
1:=λsz.sz
2:=λsz.s(sz)
3:=λsz.s(s(sz))
以下略
ここでnを受けとってn+1を返す函数を
Succ:=λnsz.s(nsz)とする
例
Succ2 -> (λnsz.s(nsz))(2) -> (λnsz.s(nsz))(λsz.s(sz))
-> λsz.s((λsz.s(sz))sz)
-> λsz.s((λz.s(sz))z)
-> λsz.s(s(sz)) = 3
また，
Add:=λmnsz.ms(nsz) = λmn.m Succ n
Mult:= λmns.m(ns) = λmn.m(Add n) 0
のように四則演算もラムダ式で定義できる
例 2+3
Add 2 3 -> (λmnsz.ms(nsz))(2)(3) -> (λmnsz.ms(nsz))(λsz.s(sz))(λsz.s(s(sz)))
-> λnsz.(λsz.s(sz))s(nsz)(λsz.s(s(sz)))
-> λsz.(λsz.s(sz))s((λsz.s(s(sz)))sz)
-> λsz.(λz.s(sz))(λz.s(s(sz)))z)
-> λsz.(λz.s(sz))(s(s(sz)))
-> λsz.s(s(s(s(sz)))) = 5
チャーチ論理値
真偽値もラムダ式で
T:=λxy.x (True)
F:=λxy.y (False)
ラムダ項TはKと，ラムダ項FはKIと等しい
if X then Y else ZはXYZと表記 (X,Y,Zはラムダ項で，Xは簡約したらTかFになる)
TYZ -> (λxy.x)YZ -> λy.Y(Z) -> Y
FYZ -> (λxy.y)YZ -> λy.y(Z) -> Z
ちゃんとif X then Y else Zの動作になる
このif X then Y else Zを使って
And:= λxy.xyF
Or:= λxy.xTy
Not:= λx.xFT
という論理演算も定義できる
データ構造
順序対をタプルという．
2つのラムダ項M,Nに対しタプルを<M,N>と表す．ラムダ項で表現されたタプルはチャーチ対とも．
<M,N>:=λx.xMN
ここで，順序対の最初の項を取り出すFstと最後の項を取り出すSndを定義すると
Fst:=λt.tT
Snd:=λt.tF
となる．
例
Fst<M,N> = λt.tT(λx.xMN)
->(λx.xMN)T -> TMN -> M
Snd<M,N> = λt.tF(λx.xMN)
->(λx.xMN)F -> FMN -> N
これでわかったのは手続き型言語と真逆で，
一切データをや値がなくとも函数の定義と適用だけでプログラムが組めるということである
(値はチャーチ数があるし，データ構造も函数で表現できるし，あとはif文もループ(Yコンビネータで再帰を使う)も函数で表現できる)
いままでラムダ記法は知っていたしJavaScriptの無名函数やC++11,Java8などでlambda式として
それら表記が行えることは聞いていたが，
その高階函数やラムダ記法ができて何が嬉しいかあまりわかってなかった．
チャーチ数やチャーチ論理値，チャーチ対といったプログラミングに必要なプリミティブな要素まで徹底してデータを排除して函数で表記できるのを初めて知って，とてつもなく感動した．
なるほど函数型言語のオモシロさはこういうところにあるのだなーと勝手に納得した日でした．
ちなみに，普通タプルときたらリストだとおもうけれど(Lispなんかで使われるconsとかcarとかcdrとかもラムダ記法でもちろん表現できる),私の理解がおっつきませんでした．理解に良い記事をだれか教えてください
追記:
チャーチ対のFstをCar,SndをCdrとして，
リスト終端を表わすNil:=F
チャーチ対を生成する函数Consを
Cons:=λmn.(λt.tmn)
とすると
(Cons X (Cons Y (Cons Z Nil)))
で
λt.tX(λt'.Y(λt''.ZF))
とかいうリストがつくれる……かな?あってるといいけど