Avendia19
English

日記 (2020 年 7 月 8 日)

7 月 5 日7 月 6 日で、 継続を言語内で扱うためのラムダ計算の拡張として λc-計算を扱った。 今日は、 これとは別の方法で継続を扱えるようにした拡張である λμ-計算について触れていく。 λμ-計算は、 Parigot2 によって古典論理に対応する計算体系として導入されたものである。 古典論理との対応は次回扱うことにして、 今日は純粋に計算体系であるとして見ていくことにする。

λμ-計算では、 通常のラムダ計算での変項に相当するものが 2 種類あり、 片方は通常通り変項と呼び、 もう片方は名前と呼ぶ。 変項が項を表す一方で、 名前は継続を表すものと見なすことができる。 また、 変項に相当するものが 2 種類になったのを受けて、 それを束縛する構文も 2 種類あり、 片方は通常通り λ で表されて関数を作り、 もう片方は μ で表されて名前を束縛する。

定義 3.1

計算体系 λμ の言語を以下のように定める。 可算集合 󱀕󱀍 を固定し、 この元をそれぞれ変項variable名前name と呼ぶ。 さらに、 変項と名前をそれぞれメタ変項 xa で表すことにし、 その上で、 M ::= xλx.MMMμa.M{a}M V ::= xλx.M とする。 このとき、 MV で定まるものをそれぞれtermvalue という。

項のうち、 μa.M の形のものは μ-抽象と呼ぶことがあり、 {a}M の形をしたものは名前付き項と呼ぶことがある。

なお、 同じ記号が複数の意味合いで使われすぎるのを防ぐため、 通常の慣習から以下の 2 点について記号を変えた。 まず、 名前付き項における名前は角括弧で囲むのが普通だが、 角括弧は代入や環境で用いるので、 それと区別するために波括弧に変更した。 さらに、 名前はギリシャ小文字で書くのが普通だが、 ギリシャ小文字は後に型を導入する際に基本型の記号として使う予定なので、 ここではラテン小文字を使うことにした。

ここで、 いくつか記号を用意しておく。 まずは自由変項に関する記号について述べる。 通常のラムダ計算と同様に、 λμ-計算には変項の概念とそれを束縛する構文 (λ-抽象) があるので、 項の中にある変項に対して束縛されているか自由であるかのどちらかが定まる。 そこで、 項 M に対して、 そこに現れる変項のうち自由であるものの全体の集合を、 通常の慣習に従って FV(M) で表す。 さらに、 λμ-計算には名前の概念とそれを束縛する構文 (μ-抽象) もあるので、 これと同様のことは名前に対しても言える。 項 M に現れる名前のうち自由であるものの全体の集合は、 FN(M) で表すことにする。

次は代入に関してである。 通常のラムダ計算では、 ある項 M の中に含まれる変項 x に別の項 N を (新たな束縛を回避しつつ) 代入する操作が定義されていて、 その結果は M[x:=N] で表された。 λμ-計算でも同じ記号を用いることにする。 これに加えて、 λμ-計算には変項に相当するものとして名前もあるので、 名前に別の何かを代入する操作も考えられる。 項の定義を見ると、 名前を名前以外のもので置き換えてしまうと不正な項になってしまうので、 名前には名前しか代入できない。 そのような、 ある項 M に含まれる名前 a を別の名前 b で置き換えたものは、 変項への代入と同様の記号で M[a:=b] で表すことにする。

λμ-計算では、 今説明した 2 種類の代入以外に考えなければならない代入がもう 1 種類ある。 それを定義するには環境の概念が必要なので、 まずはそれを定義する。

定義 3.2

計算体系 λμ において、 項に含まれるある部分項を記号 [] に置き換えて得られるものを環境environment という。

これは定義 1.2 の評価環境に似ているが、 ここでの環境は [] の外側がどんな形をしていても良い点が異なる。 評価環境のときと同様に、 環境 E と項 M に対し、 E に含まれる [] を機械的に M に置き換えて得られる項を E[M] で表す。

定義 3.3

計算体系 λμ を考える。 項 M と環境 E と名前 a,b に対し、 項 M[a:=bE] を以下によって定義する。 まず、 簡単のため、 ME の束縛変項を適切に置き換えて全て異なるようにしておき、 束縛名前についても全て異なりかつ a,b のどちらでもないようにしておく。 その上で、 x[a:=bE] x (λx.P)[a:=bE] λx.P[a:=bE] (PQ)[a:=bE] (P[a:=bE])(Q[a:=bE]) (μc.P)[a:=bE] μc.P[a:=bE] ({c}P)[a:=bE] { {b}E[P[a:=bE]] (ca) {c}P[a:=bE] (ca) と再帰的に定める。 このとき、 M から M[a:=bE] を得る操作を混合代入mixed substitution という。

直観的には、 M の中の {a}P という形の部分項を全て {b}E[P] に置き換えて得られる項が M[a:=bE] である。

以上の準備のもと、 λμ-計算の簡約を定義する。 ここでは、 前回までに引き続き、 値呼びをベースとした簡約を考えることにする。 なお、 Parigot によるオリジナルの定義は (論文中でそう明言されているわけではないが) 名前呼びの体系であり、 ここで定義する値呼びの体系は Ong–Stewart1 によるものである。

定義 3.4

計算体系 λμ の項の上の関係 を、 項 M,N と値 V に対し、 (λx.M)V M[x:=V] {b}(μa.M) M[a:=b] μa.{a}M M (aFN(M)) (μa.M)N μb.M[a:=b[]N] (bFN(M)FN(N)) V(μa.M) μb.M[a:=bV[]] (bFN(M)FN(V)) で定める。 さらに、 関係 の合同閉包として定め、 これを値呼び簡約call-by-value reduction という。

ここで、 λμ-計算の項の直観を簡単に述べよう。 μa.M という項は、 この項が置かれている環境を a という名前に束縛する役割をもっている。 それに対して {a}M という項は、 μ-抽象によって a に束縛された環境に M が置かれているものとして評価を行うという意味がある。 λc-計算では、 評価環境 (つまり継続) は暗黙的に取り出されて cont という演算子の引数に引数として渡されていたが、 λμ-計算では、 μ-抽象によって継続が名前に束縛される。 これによって、 λμ-計算ではより直接的な形で一級継続が実現されているのである。

次に、 λμ-計算の簡約規則について解説しよう。 λμ-計算の簡約規則を詳しく見る前に、 まずは定義 2.2 λc-計算の局所的な簡約規則 (L で書いたもの) を思い出そう。 そこには、 (contM)Ncont(λk.M(λx.k(xN))) という規則があった。 定理 2.3 によってこの規則が想定通りの振る舞いをすることは示されているが、 次のような観察をしてももっともらしいことが分かる。 この式の右辺を簡単に contX と書くことにする。 右辺の contX と左辺の contM の継続関数をそれぞれ QQ󰎘 で表すと、 Q󰎘 はまず N を適用してから Q に渡すという形になっているはずなので、 Q󰎘λx.Q(xN) という関係が成り立つ。 ここで、 contM はこれが置かれている場所における継続を M に引数として渡す項であった。 すなわち、 M は引数として Q󰎘 を受け取ることを想定している。 そこで、 上の式の右辺に簡約した後でも MQ󰎘 すなわち λx.Q(xN) が渡されるようにしないとおかしなことになる。 この Q は上式の右辺において X の引数として渡されるので、 X の形としては、 まず Q を受け取るためにラムダ抽象 λk から始め、 Mλx.k(xN) を渡すという項を書いたものが適切だと考えられ、 実際にそうなっている。

この観察のもと、 λμ-計算の (μa.M)Nμb.M[a:=b[]N] を見てみよう。 右辺は簡単に μb.X と書くことにする。 左辺の M の中に現れる {a}P という形の項は、 すでに述べたように μa.M が置かれている環境での P を表している。 このことは、 上の式の右辺に簡約した後でも成立しなければならない。 右辺で μb.X が置かれている環境は、 左辺では N を引数として適用した後に μa.M が置かれている環境に渡すというものである。 したがって、 左辺で {a}P が表していたものと同じものを右辺でも実現するには、 {b}PN という形に置き換えなければならない。 ところで、 X の定義である M[a:=b[]N] という混合代入は、 まさにそれを行う操作であった。 以上のように考えると、 上記の簡約規則がもっともらしいと感じられるだろう。

最後に、 λc-計算が λμ-計算の中でシミュレートできることを述べて、 今日の内容を終わりとする。 λμ-計算において、 abort λm.μb.m cont λm.μa.m(λx.μb.{a}x) とおく。 すると、 任意の値呼び評価環境 E と項 M と名前 k に対して、 {k}E[abortM] M {k}E[contM] M(λx.abort{k}E[x])) が成り立つことが、 E に関する帰納法で簡単に示せる。 これは、 評価環境の先頭に {k} が付いていることを除けば、 λc-計算の簡約規則と同一である。 先頭に {k} が必要なのは、 μ-抽象は名前付き項にされないと簡約が進まないというテクニカルな理由によるものである。

参考文献

  1. C.-H. L. Ong, C. A. Stewart (1997) 「A Curry-Howard foundation for functional computation with control」 『Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on principles of programming languages』 215–227
  2. M. Parigot (1992) 「λμ-calculus: an algorithmic interpretation of classical natural deduction」 『Lecture Notes in Artificial Intelligence』 624:190–201