Qiita Teams that are logged in
You are not logged in to any team

Log in to Qiita Team
Community
OrganizationEventAdvent CalendarQiitadon (β)
Service
Qiita JobsQiita ZineQiita Blog
15
Help us understand the problem. What is going on with this article?

More than 1 year has passed since last update.

プログラミング言語においてシンプルな言語仕様というのはやはり魅力的ですよね。大域脱出やコルーチン、非同期処理の取り回しなど、多くの言語機能は継続という一つの概念で記述することができることが知られています。この記事で、言語処理系を自作するときに少しでも言語仕様を小さくするために継続を導入することをお勧めするために書きました。以降、少し堅苦しい文体になってしまいますが、お付き合いください。

前提知識

本項はSchemeおよび継続に対する基本的な事項は知っているものとする。まだ知らない場合はなんでも継続などを読み継続について理解してから読むことを推奨する。

以下では継続をプログラミング言語に実装する方法について解説する。たびたび議論に上がるCPS変換に対して、あまり話題にならない逆方向の変換であるDS変換を紹介することが本項の目的である。また$\lambda$計算を議論するにあたって、その評価戦略は正格評価とする。

ラムダ式

$v_1,v_2,\dots$を変数項とする。$\lambda$と$.$をラムダ抽象の記号とする。また、式の結合順位を定めるため括弧$()$を適宜用いる。このときラムダ式の集合$\Lambda$を次の様に帰納的に定義する。

$$
\begin{aligned}
v_i &\in\Lambda &&(i=1,2,\dots) \\
\lambda v_i . M &\in\Lambda &&(M\in\Lambda,\quad i=1,2,\dots)\\
MN &\in \Lambda &&(M\in\Lambda, N\in\Lambda)
\end{aligned}
$$

ラムダ式の計算は本項とは関係がないため、その評価戦略が正格評価を採用していることを述べるに留めておく。詳しく知りたい場合は適宜教科書を参考にしてほしい。

継続渡し形式(Continuation Passing Style, CPS)

各ラムダ項の継続を束縛変数$k$として参照することができるような形式を継続渡し形式と呼び、次の変換により定義される。

$$
\begin{align}
[ v_1 ] &= \lambda k . k(v_1)\\
[ \lambda v_1 . M ] &= \lambda k. k(\lambda v_2.[M]) \\
[ M N ] &= \lambda k_1. [ M ]\,(\lambda k_2 . [N]\,(\lambda k_3. k_2k_3k_1))
\end{align}
$$

この変換により各ラムダ式は、その継続を束縛変数$k$として参照できるようになる。

直接渡し形式(Direct Style, DS)

CPS変換が定義できたところでCPS変換した式を元の形式に戻すことについて述べる。例えばCPS変換をすると前節のように元の式よりも$\lambda$項のネストが深くなるためスタックを大量に消費することになるが、CPS変換した後必要な計算(簡約)を行いCPS変換からDSに戻すことができれば計算機のリソースの消費を抑えることができる。このためDS変換は実際の計算においても非常に重要な意味を持つものである。DS変換$[\cdot]$は、4つの変換$[\cdot]^E,[\cdot]^R,[\cdot]^T,[\cdot]^C$の組み合わせで構成されており、ラムダ式の形に応じて再帰的に変換する。ラムダ式の形は次のBNFによって定義される。

$$
\begin{align}
\eta &::= \rho\gamma\mid\gamma\tau\\
\rho &::= \lambda k. \eta\mid\tau\tau \\
\tau &::= v\mid v'\mid\lambda v'.\gamma \\
\gamma &::= k \mid\lambda v.\eta
\end{align}
$$
ここで$v,v',k$は、異なる変数項とする。
上記の定義の分類に従って変換$[\cdot]^E,[\cdot]^R,[\cdot]^T,[\cdot]^C$を下記のように定義する。

$$
\begin{align}
[\lambda k . \eta] &= [\eta]^E_{(\bot, \bullet)} \\

[\rho\gamma]^E_{(s,\eta)} &= [\gamma]^C_{(s, [\rho]^R_{(s, \bullet)})} \\
[\gamma\tau]^E_{(s, \eta)} &=[\gamma]^C_{(s, [\tau]^T_{(s, \bullet)})} \\
[v]^T_{({\eta_1::s},\eta_2)} &= (s,\eta_1) \\
[v']^T_{(s,\eta)} &= (s, v') \\
[\lambda v'.\rho]^T_{(s_1,\eta_1)} &= (s_1, \lambda v'.\eta_2) &&\text{ ただし } (s_2, \eta_2) = [\rho]^R_{(\bot, \bullet)} \\
[\lambda k. \eta_1]^R_{(s,\eta_2)} &= (s, [\eta_1]^E_{(\bot,\bullet)}) \\
[\tau_1\tau_2]^R_{(s, \eta)} &= (s_2, \eta_1\eta_2) &&\text{ただし} (s_1, \eta_2) = [\tau_2]^T_{(s,\bullet)}, (s_2, \eta_1) = [\tau_1]^T_{(s_1, \bullet)} \quad {\tiny (\dagger)} \\
[k]^C_{(s,\eta)} &= \eta \\
[\lambda v.\eta_1]^C_{(s, \eta_2)} &= [\eta_1]^E_{(\eta_2::s, \bullet)}
\end{align}
$$

この変換では、各変換でその式よりも上位のスタック$s$と下位の直接渡し形式の計算$\eta$が対象となるラムダ式と共に渡され変換されている。各変換の役割として変換$[\cdot]^T,[\cdot]^R$がスタックの順番を変換し、変換$[\cdot]^E,[\cdot]^C$が式の形を変換している。

この変換を施すことで、継続渡し形式に変換されたものを再び直接渡し形式に戻すことができる。

実装

上記の計算を実行するラムダ計算用のバイトコードコンパイラと仮想マシンをScalaで実装した。( 参考 )
この仮想マシンでは評価戦略自体をScalaのライブラリCatsにおけるBimonadとしてEvalに渡しバイトコードで渡すことができ、$\Lambda$式の評価自体は正格および非正格評価が可能である。バイトコードコンパイラにおけるCPS/DS変換は正格評価向けに実装しており、非正格向けのCPS/DS変換は今後の課題である。

余談

この様にCPS変換の定義を追うと継続とは特別なオブジェクトとしてではなく単なる式の変換によって現れる関数であることが分かる。とくに処理系を実装するなどした時は、継続の実装と聞くと身構えてしまうが構文木をうまく変換する操作を定義するだけで十分である。もちろん効率的な実装をする場合、FFIなどCPS変換できない部分がある場合など状況によって自分で継続渡し形式の定義を作り直す必要があるが、一度CPS変換を手で実装したことがあれば実はそんなに難しくなかったりする。それでもうまく行かない時や効率を求める時は、上記の方法以外にもなんでも継続にあるようなメモリのダンプを使うなどの方法もある。継続はどこにでも現れるし、定義するのは簡単である。筆者としては一つでも継続がネイティブに実装されたプログラミング言語が増えることを望む。

参考文献

  • Lasse R. Nielsen, "A simple Correctness Proof of the Direct-Style Transformation", BRICS Report Series, RS-02-2, January 2002.
15
Help us understand the problem. What is going on with this article?
Why not register and get more from Qiita?
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away
15
Help us understand the problem. What is going on with this article?