この記事は，IQ1の2まいめっ Advent Calendar 2018の2日目の記事です．

5秒でわかるさくらんぼ $\lambda$ 計算

f:id:JXCgaKA6uGAhLMhi:20181125181540p:plain

導入

さくらんぼ計算の例です． f:id:JXCgaKA6uGAhLMhi:20181125181502p:plain

さくらんぼ計算は，計算の定義をよく知らないんですが，たぶん以下のような命題を使った計算方法だと思います．

任意の自然数 $k,n, m$ が $n \le k \land k - n \le m$ を満たすとき，以下の条件を満たす自然数 $m_1, m_2$ が存在する: 1. $m_1 + m_2 = m$ 2. $n + m_1 = k$

しかも，このような自然数 $m_1, m_2$ は一意に定まる．

証明:

2.より $m_1 = k - n$ であり， $n \le k$ であるから， $m_1 \in \mathbb{N}$ である．また，1.より $m_2 = n + m - k$ であり， $k - n \le m$ であるから， $m_2 \in \mathbb{N}$ である．しかも， $m_1, m_2$ は自然数 $n, m, k$ を決めると，一意に定まる．

上の命題をさくらんぼ補題と呼ぶことにします． $k=10$ のときのさくらんぼ補題を使って，繰り上がりのある自然数の足し算をやろう!みたいなプリントが話題になっていましたね．さくらんぼ補題は，ある群の任意の元を群の二項演算を使って分解できる，ことしか言ってない気がしますが，よくわからないのでやりません．

さて，さくらんぼ補題は自然数の計算で使うものなんですが， $\lambda$ 計算でも似たようなことができるのか気になりますね．単純型付き $\lambda$ 計算では，項を簡約基とそれ以外に分解できる性質があります:

$\vdash M:A$ ならば，以下のどちらかが成り立つ．

$M$ は値である．
一意な評価文脈 $E[\;]$ , 項 $(\lambda x. N)V$ が存在して， $M \equiv E[(\lambda x.N)V]$ が成り立つ．

これを使って，項を分解したのが，上の図です． $\lambda$ 計算のさくらんぼ補題は，進行定理(Progress Theorem)としてよく知られている定理の言い換えです．

残りの部分で， $\lambda$ 計算のさくらんぼ補題の説明をやっていきます．

後書き

単純型付き計算
- 構文
- 簡約
- 評価文脈(Evaluation Context)
- 型付け
さくらんぼ $\lambda$ 計算
まとめ

気持ち

結構雑にやっていくので，ちゃんと知りたい人はちゃんとしたやつ読んでください．

単純型付き $\lambda$ 計算

単純型付き $\lambda$ 計算とは，単純型がついた $\lambda$ 計算です🤔 どこまでが単純なのかよく知らないんですが，今回は関数型と基底型だけを型にもつような $\lambda$ 計算を考えます．

本節では，今回使う $\lambda$ 計算の定義をやっていきます．名前がないと不便なので， $\lambda_\to$ と呼ぶことにします．

構文

型

まず，型を定義します．基底型を指すメタ変数として $A, B, C$ などを，型を指すメタ変数として $T, S$ などを使います．

$\lambda_\to$ の型 $T$ を，以下のように帰納的に定義します: ${\displaystyle T := A \text{ (基底型)} \mid T \to T \text{ (関数型)} \ \text{where } A \in \mathcal{A} }$

例えば，基底型 $A, B$ について， $A \to B$ とか $A$ とか $((A \to B) \to A) \to A$ とかが型になります．基底型は，関数型の再帰のベースケースになる型で，IntとかBool, Stringとかのイメージです．関数型は，そのまま関数の型です．たとえば，

def add3(x: Int): Int = x + 3

int add3(int x) {
    return x + 3;
}

とかの関数の型はどちらもint -> intになります(雑シンタックスです)．

note: 見やすさのため，型 $A \to (A \to (A \to A))$ を $A \to A \to A \to A$ と書くことにします．つまり， $- \to -$ は右結合です．

項

$x, y, z$ とかを変数を指すメタ変数として， $M, N$ とかを項を指すメタ変数として使います．

$\lambda_\to$ の項 $M$ を帰納的に定義します: ${\displaystyle M := x \text{ (変数)} \mid \lambda x.M \text{ (抽象)} \mid M M \text{ (適用)} }$

それぞれの項は，だいたい以下のような意味になります:

変数: プログラミング言語における仮引数．
抽象( $\lambda$ 抽象): 関数を表現する． $\lambda x. M$ は変数 $x$ をとって項 $M$ を実行する関数．
適用: 関数に引数を渡す． $(\lambda x. M)N$ は，引数 $x$ に項 $N$ を渡す．

関数を返す関数 $\lambda x.\lambda y. N$ も項です．これは，変数 $x$ をとって，関数 $\lambda y. N$ を返す関数ぐらいの意味になります．例えば， $x$ , $x y$ , $\lambda x \lambda y. y x$ , $(\lambda fgx. fx(gx))(\lambda x y. x)z$ は項です．

note: 以下のような雑記述を使います😃:

$\lambda x. \lambda y. M$ のような， $\lambda$ が続くケースでは，省略して $\lambda xy.M$ と書くことにします．
$\lambda x. M_1M_2M_3$ は， $(\lambda x.(M_1 M_2)M_3)$ と解釈します．つまり，抽象はなるべく右にまで伸ばして解釈して，適用は左結合とします．

簡約

簡約とは，項をルールに従って書き直すことです(たぶん)．この書き直しによって，計算を表現します．

$\lambda_\to$ の簡約規則の前に，一般的な簡約規則の話をします．

$\beta$ 簡約を以下のように定義する: ${\displaystyle (\lambda x. M) N \to^\beta M[N/x] }$

$M[N/x$ ]は，代入です．項 $M$ の中の全ての自由変数 $x$ を $N$ で置き換える操作です．ただ，自由変数を定義するのがめんどくさいので，いい感じに動くことにします¹

値

$\lambda_\to$ の値を以下のように定義する: ${\displaystyle V := x \mid \lambda x. M }$

値とは，それ以上計算できない項のことです．なんらかの計算をして，変数か関数になったら計算を止めて，それを結果として受け取ります．ちょっと紛らわしいですが，値も項に含まれることに注意してください．

評価戦略

さきほどの簡約規則だけに従うと，例えば $(\lambda xy.x)M_1 M_2$ のような項は簡約できません． $( (\lambda x y . x) M_{1} ) M_{2}$ は $(\lambda x. M) N$ の構造になっていないからです．このままだと簡単な例しかかけないので，もう少し簡約規則を拡張します．ちなみに， $\lambda_\to$ は，型がついた項であれば，どのような簡約順でも必ず簡約が停止して(強正規化可能)かつ，どのような簡約順であっても計算結果が一致する(合流性)はずです．今回は，多くのプログラミング言語で採用されているcall-by-valueを採用します．

$\lambda_\to$ の評価を以下のように定める:

${\displaystyle \frac{}{ (\lambda x.M)V \to M[V/x] } \text{ Eval}_\beta }$

${\displaystyle \frac{ M_1 \to M_1' }{ M_1 M_2 \to M_1' M_2 } \text{ Eval}_L }$

${\displaystyle \frac{ M \to M' }{ V M \to V M' } \text{ Eval}_R }$

それぞれの評価の意味は以下の通りです:

Eval $_\beta$ : 項が $(\lambda x. M) V$ の形なら $\beta$ 簡約を行う． $\beta$ 簡約の規則に制限を加えて，評価に持ち上げたもの．
Eval $_L$ : 項が適用の形かつ左側( $M_1$ )が評価できるなら，左側を評価して( $M_1'$ )，項全体の評価を $M_1' M_2$ にする．
Eval $_R$ : 項が適用の形かつ左側が値 $V$ かつ右側( $M$ )が評価できるなら，右側を評価して( $M'$ )，項全体の評価を $V M'$ にする．

以上の規則からわかるのは，1)項は(ASTの)左側から評価されること，2) $\beta$ 簡約で代入される項は値だけであること，3)評価規則は再帰になっていて，基底ケースはEval $_\beta$ になっていることです．

例えば，整数の足し算を+で書くとして， $(\lambda x. x + x)(1 + 2)$ の簡約は以下のように進みます:

${\displaystyle (\lambda x. x + x)(1 + 2) \to (\lambda x. x + x)\;3 \to 3 + 3 \to 6 }$

引数が先に評価されるので，関数内で変数が2回以上使われていても，引数の評価が一度で済みます．

評価文脈(Evaluation Context)

さっき書いた評価規則なんですが，3つあると面倒なので(🤔)，どうにか1つにまとめることを考えます．要は次に $\beta$ 簡約が行われる部分(評価でなく簡約です)と，それ以外の部分に分けたら良いです．評価文脈という穴つきの項を導入して，この問題を解決します．

評価文脈 $E[\;]$ を以下のように定義する:(BNFで書いたら表示されなかったので，箇条書きで書きます)

hole: $[\;]$ 1つの評価文脈に正確に1つ穴が空いていて，そこに項を入れる．
E $_L$ : $E[\;]M$ Eval $_L$ に対応する．
E $_R$ : $V E[\;]$ Eval $_R$ に対応する．

評価文脈の意味は以下のようになります:

評価文脈 $E[\;]$ の穴を項 $M$ で埋めたとき， $E[M]$ と書くことにします．このとき $E[M]$ は項になります．以下に評価文脈と，それを項 $M$ で埋めた例を書きます．

$[\;] \mapsto [M] \equiv M$ ( $[M]$ と $M$ は同一視することにします)
$[\;](\lambda x y. x) \mapsto M(\lambda x y. x)$
$( (\lambda z. z) [\;] ) (\lambda f g. f g) \mapsto ( (\lambda z. z) M ) (\lambda f g. f g)$

上記の評価文脈を使うことで，3つの評価規則を1つにまとめることができます:

$\lambda_\to$ の評価は以下のように定義される: ${\displaystyle E[(\lambda x. M)V] \to E[M[V/x]] }$

紛らわしいですが，holeの括弧と代入の括弧に同じ括弧を用いています．

型付け

このままだと，評価できないが値ではない項が存在してしまうので，あんまり嬉しくないです．

例えば， $(\lambda f x. f (f x))h(\lambda y. y)$ のような項を考えます．このとき，項 $\lambda f x.f (f x)$ は1引数の関数が $f$ に渡されることを期待しているのですが，変数 $h$ が渡されています．この変数が1引数の関数になっているかは，書いた人が何を渡すのかに依存しています．人間は信用できないので，こういう項が書けないような仕組みが欲しくなります．

そこで，項にお気持ちを書ける機能，型を導入します．

$\lambda_\to$ の型付け規則を以下のように定義する:

${\displaystyle \frac{x: A \in \Gamma}{\Gamma \vdash x: A}\text{ (var)} }$

${\displaystyle \frac{\Gamma, x:A \vdash M: B}{\Gamma \vdash \lambda x.M: A \to B}\text{ (abs)} }$

${\displaystyle \frac{\Gamma \vdash M_1: A \to B \quad \quad \Gamma \vdash M_2: A}{\Gamma \vdash M_1 M_2:B}\text{ (app)} }$

$\Gamma \vdash M:A$ は，型付け文脈 $\Gamma$ のもとで，項 $M$ は型 $A$ を持つ，と読みます．

型付け文脈というのは，変数と型の組の列のようなもので，例えば $\Gamma = x:A, y:B, f: A \to B$ であれば，変数 $x$ は型 $A$ で...という意味になります．項に登場する変数のうち，型が既にわかっているものをメモして置くことで，あとで変数の型に矛盾がないか調べることができます．

各規則の意味は以下のとおりです:

var: 変数 $x$ が型 $A$ を持つことが型付け文脈 $\Gamma$ に記録されているならば(規則の上側)， $\Gamma$ のもとで項 $x$ は型 $A$ を持つ．
abs: 型付け文脈 $\Gamma, x : A$ のもとで，項 $M$ が型 $B$ であるなら， $\Gamma$ のもとで項 $\lambda x. M$ は型 $A \to B$ を持つ．
app: 型付け文脈 $\Gamma$ のもとで，項 $M_1$ が型 $A \to B$ を持ち，かつ型付け文脈 $\Gamma$ のもとで，項 $M_2$ が型 $A$ を持つならば， $\Gamma$ のもとで，項 $M_1 M_2$ は型 $B$ を持つ．