さくらんぼλ計算
この記事は,IQ1の2まいめっ Advent Calendar 2018の2日目の記事です.
5秒でわかるさくらんぼ計算
導入
さくらんぼ計算の例です.
さくらんぼ計算は,計算の定義をよく知らないんですが,たぶん以下のような命題を使った計算方法だと思います.
任意の自然数がを満たすとき,以下の条件を満たす自然数が存在する: 1. 2.
しかも,このような自然数は一意に定まる.
証明:
2.よりであり,であるから,である. また,1.よりであり,であるから,である. しかも,は自然数を決めると,一意に定まる.
上の命題をさくらんぼ補題と呼ぶことにします. のときのさくらんぼ補題を使って,繰り上がりのある自然数の足し算をやろう!みたいなプリントが話題になっていましたね. さくらんぼ補題は,ある群の任意の元を群の二項演算を使って分解できる,ことしか言ってない気がしますが,よくわからないのでやりません.
さて,さくらんぼ補題は自然数の計算で使うものなんですが,計算でも似たようなことができるのか気になりますね. 単純型付き計算では,項を簡約基とそれ以外に分解できる性質があります:
ならば,以下のどちらかが成り立つ.
- は値である.
- 一意な評価文脈, 項が存在して,が成り立つ.
これを使って,項を分解したのが,上の図です. 計算のさくらんぼ補題は,進行定理(Progress Theorem)としてよく知られている定理の言い換えです.
後書き
Contents
- 単純型付き計算
- 構文
- 簡約
- 評価文脈(Evaluation Context)
- 型付け
- さくらんぼ計算
- まとめ
気持ち
結構雑にやっていくので,ちゃんと知りたい人はちゃんとしたやつ読んでください.
単純型付き計算
単純型付き計算とは,単純型がついた計算です🤔 どこまでが単純なのかよく知らないんですが,今回は関数型と基底型だけを型にもつような計算を考えます.
本節では,今回使う計算の定義をやっていきます. 名前がないと不便なので,と呼ぶことにします.
構文
型
まず,型を定義します. 基底型を指すメタ変数としてなどを,型を指すメタ変数としてなどを使います.
の型を,以下のように帰納的に定義します:
例えば,基底型について,とかとかとかが型になります. 基底型は,関数型の再帰のベースケースになる型で,IntとかBool, Stringとかのイメージです. 関数型は,そのまま関数の型です.たとえば,
def add3(x: Int): Int = x + 3
int add3(int x) { return x + 3; }
とかの関数の型はどちらもint -> int
になります(雑シンタックスです).
note: 見やすさのため,型をと書くことにします.つまり,は右結合です.
項
とかを変数を指すメタ変数として,とかを項を指すメタ変数として使います.
の項を帰納的に定義します:
それぞれの項は,だいたい以下のような意味になります:
- 変数: プログラミング言語における仮引数.
- 抽象(抽象): 関数を表現する.は変数をとって項を実行する関数.
- 適用: 関数に引数を渡す.は,引数に項を渡す.
関数を返す関数も項です.これは,変数をとって,関数を返す関数ぐらいの意味になります. 例えば,, , , は項です.
note: 以下のような雑記述を使います😃:
- のような,が続くケースでは,省略してと書くことにします.
- は,と解釈します.つまり,抽象はなるべく右にまで伸ばして解釈して,適用は左結合とします.
簡約
簡約とは,項をルールに従って書き直すことです(たぶん). この書き直しによって,計算を表現します.
の簡約規則の前に,一般的な簡約規則の話をします.
簡約を以下のように定義する:
]は,代入です. 項の中の全ての自由変数をで置き換える操作です. ただ,自由変数を定義するのがめんどくさいので,いい感じに動くことにします1
値
の値を以下のように定義する:
値とは,それ以上計算できない項のことです. なんらかの計算をして,変数か関数になったら計算を止めて,それを結果として受け取ります. ちょっと紛らわしいですが,値も項に含まれることに注意してください.
評価戦略
さきほどの簡約規則だけに従うと,例えばのような項は簡約できません. はの構造になっていないからです. このままだと簡単な例しかかけないので,もう少し簡約規則を拡張します. ちなみに,は,型がついた項であれば,どのような簡約順でも必ず簡約が停止して(強正規化可能)かつ,どのような簡約順であっても計算結果が一致する(合流性)はずです. 今回は,多くのプログラミング言語で採用されているcall-by-valueを採用します.
の評価を以下のように定める:
それぞれの評価の意味は以下の通りです:
- Eval: 項がの形なら簡約を行う.簡約の規則に制限を加えて,評価に持ち上げたもの.
- Eval: 項が適用の形かつ左側()が評価できるなら,左側を評価して(),項全体の評価をにする.
- Eval: 項が適用の形かつ左側が値かつ右側()が評価できるなら,右側を評価して(),項全体の評価をにする.
以上の規則からわかるのは,1)項は(ASTの)左側から評価されること,2)簡約で代入される項は値だけであること,3)評価規則は再帰になっていて,基底ケースはEvalになっていることです.
例えば,整数の足し算を+で書くとして,の簡約は以下のように進みます:
引数が先に評価されるので,関数内で変数が2回以上使われていても,引数の評価が一度で済みます.
評価文脈(Evaluation Context)
さっき書いた評価規則なんですが,3つあると面倒なので(🤔),どうにか1つにまとめることを考えます. 要は次に簡約が行われる部分(評価でなく簡約です)と,それ以外の部分に分けたら良いです. 評価文脈という穴つきの項を導入して,この問題を解決します.
評価文脈を以下のように定義する:(BNFで書いたら表示されなかったので,箇条書きで書きます)
- hole: 1つの評価文脈に正確に1つ穴が空いていて,そこに項を入れる.
- E: Evalに対応する.
- E: Evalに対応する.
評価文脈の意味は以下のようになります:
評価文脈の穴を項で埋めたとき,と書くことにします.このときは項になります. 以下に評価文脈と,それを項で埋めた例を書きます.
- (とは同一視することにします)
上記の評価文脈を使うことで,3つの評価規則を1つにまとめることができます:
の評価は以下のように定義される:
紛らわしいですが,holeの括弧と代入の括弧に同じ括弧を用いています.
型付け
このままだと,評価できないが値ではない項が存在してしまうので,あんまり嬉しくないです.
例えば,のような項を考えます. このとき,項は1引数の関数がに渡されることを期待しているのですが,変数が渡されています.この変数が1引数の関数になっているかは,書いた人が何を渡すのかに依存しています. 人間は信用できないので,こういう項が書けないような仕組みが欲しくなります.
そこで,項にお気持ちを書ける機能,型を導入します.
の型付け規則を以下のように定義する:
は,型付け文脈のもとで,項は型を持つ,と読みます.
型付け文脈というのは,変数と型の組の列のようなもので,例えばであれば,変数は型で...という意味になります.項に登場する変数のうち,型が既にわかっているものをメモして置くことで,あとで変数の型に矛盾がないか調べることができます.
各規則の意味は以下のとおりです:
- var: 変数が型を持つことが型付け文脈に記録されているならば(規則の上側),のもとで項は型を持つ.
- abs: 型付け文脈のもとで,項が型であるなら,のもとで項は型を持つ.
- app: 型付け文脈のもとで,項が型を持ち,かつ型付け文脈のもとで,項が型を持つならば,のもとで,項は型を持つ.
さくらんぼ計算
ならば,以下のどちらかが成り立つ.
- は値である.
- 一意な評価文脈, 項が存在して,が成り立つ.
証明: の型導出に関する帰納法による.
a) が変数のとき
仮定が空のとき,は導出できないので,は変数になりえない.
b) が抽象のとき
抽象は全て値であるので,直ちに成り立つ.
c) が適用のとき
導出木は以下の形になっています.
このとき帰納法の仮定により,項について命題の主張が成り立つ. 以下では,さくらんぼ補題の主張2.の項をと書くことにします. について場合分けを行う.
c-1) が値でないとき
帰納法の仮定により,となる評価文脈,項が存在する. このとき,として,が成り立つ. しかもは一意である.
c-2) が値かつ,が値でないとき
c-1)と同様に成り立つ.
c-3) がともに値であるとき
が値かつ変数ではないので,の形をしている. よって,として,が成り立つ.
若干怪しい気がしますが,だいたいこんな感じで示せると思います.
冒頭でも述べたように,この命題は,型付き計算の進行定理を別の形に書き直したものです. 進行定理は,型がついた閉じた項ならば,項は値であるか評価が必ず1ステップ進むことを保証してくれます. TaPL2でもっと詳しい説明がなされているので,そちらを読んでください.
-
詳しくはcapture avoiding substitutionでぐぐってください.wikipediaにも書いてありました.https://en.wikipedia.org/wiki/Lambda_calculus#Capture-avoiding_substitutions↩