nptclのブログ

Common Lisp処理系nptの開発メモです。https://github.com/nptcl/npt

Scheme R7RSの形式意味論を読んでいく3

続きです

Scheme R7RSの形式意味論を見て行きます。

前回の続きとなります。
Scheme R7RSの形式意味論を読んでいく2 - nptclのブログ

7.2.3. Semantic functions

意味関数はSchemeの中核です。
式を受け取りどのように実行するかを表します。

意味関数は次のような型になります。

 {\cal K} : {\rm Con} \to {\rm E}
 {\cal E} : {\rm Exp} \to {\rm U} \to {\rm P} \to {\rm K} \to {\rm C}
 {\cal E^*} : {\rm Exp^*} \to {\rm U} \to {\rm P} \to {\rm K} \to {\rm C}
 {\cal C} : {\rm Com^*} \to {\rm U} \to {\rm P} \to {\rm C} \to {\rm C}

簡単に説明します。

 \cal K は、1つの引数 \rm Con を受け取り、 \rm E を返却する関数です。
目的は定数を \rm E に変換することです。

 \cal E は、4つの引数 {\rm Exp}, {\rm U}, {\rm P}, {\rm K} を受け取り、  \rm C を返却する関数です。
この関数がSchemeの本体と言ってもいいほど重要なものです。

 \cal E^* は、4つの引数 {\rm Exp^*}, {\rm U}, {\rm P}, {\rm K} を受け取り、  \rm C を返却する関数です。
目的は関数呼び出し時の全要素を評価するときに使われます。

 \cal C は、4つの引数 {\rm Com^*}, {\rm U}, {\rm P}, {\rm C} を受け取り、  \rm C を返却する関数です。
この関数は、返却値が無視できる式の評価を行う時に使用します。
具体的に言うと、lambda式のbody部の最後以外の式です。

この4つの関数は特殊であり、例えば次のような定義がされます。

 {\cal E} [\![{\rm K}]\!] = \lambda \rho \omega \kappa \: . \cdots

他にも

 {\cal E} [\![{\rm I}]\!] = \lambda \rho \omega \kappa \: . \cdots
 {\cal E} [\![{\rm E_0 \: {\rm E^*}}]\!] = \lambda \rho \omega \kappa \: . \cdots

のような定義がたくさんあります。
ここに現れる関数は、引数の数が4つではなく3つであることに注意して下さい。

もし {\cal E} [\![\epsilon]\!] \rho \omega \kappa のように実行された場合は、  {\cal E} \epsilon \rho \omega \kappa のように関数が呼び出されたかのようにふるまい、 さらに第一引数の \epsilon の形式によって呼ばれる関数が分岐します。
例えば \epsilon  \rm K であった場合は、  {\cal E} [\![{\rm K}]\!] で宣言された関数が呼び出されることになります。

 {\cal E} [\![\epsilon]\!] とは、 \epsilon を評価するという意味です。
評価とは、evalのことです。

評価の例を見てみましょう。

 {\cal E} [\![100]\!]

引数の100は定数なので、 {\cal E} [\![{\rm K}]\!] が呼ばれます。
次の例を見てみます。

 {\cal E} [\![({\tt lambda} \: (x) \: 10 \: 20 \:30)]\!]

引数はlambda式なので、  {\cal E} [\![({\tt lambda} \; ({\rm I^*}) \; {\rm \Gamma^*} \: {\rm E_0})]\!] が呼ばれます。

では \cal E の定義を全部見て行きましょう。

 {\cal E} [\![{\rm K}]\!]

定義を示します。

 {\cal E} [\![{\rm K}]\!] = \lambda \rho \omega \kappa \: . \:
  {\rm send} \: ({\cal K} [\![{\rm K}]\!]) \: \kappa

 \rm K は定数なので、 \cal E で定数を評価したときの振る舞いになります。
例えばこんな感じです。

 {\cal E} [\![100]\!]

では内容を見て行きます。

 \lambda \rho \omega \kappa \: . \:
  {\rm send} \: ({\cal K} [\![{\rm K}]\!]) \: \kappa

まず {\cal K} [\![{\rm K}]\!] ですが、 仕様書に \cal K の定義は面倒なので省略しますと書かれています。
難しいものではなく、受け取った定数 \rm K を、 何とかして \rm E にして返却するというものです。
処理系を作る人が適当に作ってくださいね、ということなのでしょう。

仮に {\cal K} [\![{\rm K}]\!] の値が \rm E_K だとしたとき、

 \lambda \rho \omega \kappa \: . \: {\rm send} \: {\rm E_K} \: \kappa

になります。
この関数の引数は \rho, \omega, \kappa の3つあるのですが、 今は \kappa しか使っていません。
 \cal E の引数の形式が決まっているため、自由に変更できないのです。

sendの定義は前に説明しましたが再掲します。

 {\rm send} \: : \: \rm E \to K \to C
 {\rm send} \: = \:
 \lambda \epsilon \kappa \: . \: \kappa \langle \epsilon \rangle

内容の \kappa \langle \epsilon \rangle というのは、  \rm E_K を列 \langle {\rm E_K} \rangle にして、継続 \kappa を呼び出すということです。

例えば {\cal E} [\![100]\!] の場合を考えます。
 {\cal K} [\![100]\!] の結果を \rm E_{100} とした場合、  {\cal E} [\![100]\!] の実行は

 \kappa  \: \langle {\rm E_{100}} \rangle

になります。
つまりは継続 \kappa を引数 \langle {\rm E_{100}} \rangle で 呼び出すということになります。
Schemeで考えれば分かりますが、100と書かれたら 継続に100を渡すということです。
そのままですね。

sendの存在意義は、たった1つの値を継続に渡すことです。
継続の関数である \kappa は、引数に列を受け取る関数です。
つまり \kappa \:\langle 10, 20, 30, 40 \rangle みたいな呼び出し方ができます。
もしたった1つだけ値を継続に渡したいなら、 つまり \kappa \:\langle 10 \rangle みたいになるのですが、 それをsendという関数で実現したということです。

 {\cal E} [\![{\rm I}]\!]

定義を示します。

 {\cal E} [\![{\rm I}]\!] = \lambda \rho \omega \kappa \: . \:
{\rm hold} \: ({\rm lookup} \: \rho {\rm I})
 \qquad \qquad \qquad \qquad \,\,
({\rm single} \: (\lambda\epsilon \: . \: \epsilon = {\rm undefined} \to
 \qquad \qquad \qquad \qquad \qquad
  {\rm wrong} \: "{\tt undefined \: variable}",
 \qquad \qquad \qquad \qquad \qquad
  {\rm send} \: \epsilon \kappa))

 {\cal E} [\![{\rm I}]\!] は 変数が評価されたときの処理です。
 \rm I  \rm Ide 型なので、つまりは変数です。

いろいろと説明されてない関数があります。
lookup, single, wrong, holdくらいでしょうか。
ちゃんと説明して行きます。

lookup関数は、変数の表から位置を取得します。
第1引数が変数表 \rm U 、第2引数が変数である \rm Ide 、返却値が位置 \rm L です。

 {\rm lookup} : {\rm U} \to {\rm Ide} \to {\rm L}
 {\rm lookup} = \lambda \rho {\rm I} \: . \: \rho {\rm I}

引数 \rho  \rm I を受け取り、 実行が \rho {\rm I} だと何の意味があるんだという話になりますが、 lookup関数を使うことで、索引からアドレスを引いているんですよ、 分かりやすくするためなのかもしれません。
実行部の \rho {\rm I} は、 関数 \rho を引数 \rm I で呼び出すという処理です。

さて問題はsingleです。
定義は下記の通り。

 {\rm single} : ({\rm E} \to {\rm C}) \to {\rm K}
 {\rm single} =
\lambda \psi {\epsilon^*} \: . \:
  \#{\epsilon^*} = 1 \to \psi ({\epsilon^*} \downarrow 1),
 \qquad {\rm wrong} \: {\tt "wrong \: number \: of \: return \: values"}

何が問題なのかはすでに説明しました。
「暗黙のlambda式」に該当するので、次のように書き換えられます。

 {\rm single} =
\lambda \psi \: . \: \lambda {\epsilon^*} \: . \:
  \#{\epsilon^*} = 1 \to \psi ({\epsilon^*} \downarrow 1),
 \qquad {\rm wrong} \: {\tt "wrong \: number \: of \: return \: values"}

変更点は「 \lambda \psi \epsilon^* 」の部分を 「 \lambda \psi \: . \: \lambda \epsilon^* 」にしただけです。

single関数は1つの引数 \psi を関数として受け取ります。
受け取る関数 \psi は、ひとつの引数 \epsilon^* を列として受け取ります。
この列は継続の値そのものの列であるvaluesだと思います。
もし \epsilon^* の長さが1だったら、その要素を引数に関数 \psi を呼び出して返却しますが、 もし \epsilon^* の長さが1では無かったらwrongでエラーになります。
型から考えるなら、関数 \psi の戻り値は継続のようです。

holdは非常に問題がある関数です。
まずは定義から。

 {\rm hold} : {\rm L} \to {\rm K} \to {\rm C}
 {\rm hold} = \lambda \alpha \kappa \sigma \: . \:
  {\rm send} \, (\sigma \alpha \downarrow 1) \kappa \sigma

引数の数が一致してないので、暗黙のlambda式になっています。
つまり次のように書き直します。

 {\rm hold} = \lambda \alpha \kappa \: . \: \lambda \sigma \: . \:
  {\rm send} \, (\sigma \alpha \downarrow 1) \kappa \sigma

send関数の引数の個数は2つということを考慮すると、 次のようになります。

 {\rm hold} = \lambda \alpha \kappa \: . \:
(\lambda \sigma \: . \:
{\rm send} \, (\sigma \alpha \downarrow 1) \kappa) \sigma

邪魔なので \lambda \sigma を消してしまいましょう。

 {\rm hold} = \lambda \alpha \kappa \: . \:
{\rm send} \, (\sigma \alpha \downarrow 1) \kappa

ここで気にして欲しいのは、 \sigma が残るということです。
 \alpha は位置なので、値を取り出すには、 メモリ \sigma が必要です。
何らかの形で、どうしても \sigma は必要になるのです。

hold関数は全体的におかしかったため、 暗黙のlambda式で \sigma を消してしまいましたが、 本来であれば \sigma は引数に必要です。
しかしhold関数に引数を追加した所で、 全体的に作りが \sigma を渡せるように設計されていないのです。
引数に \sigma が無いと、 後から説明する {\cal E} [\![({\tt lambda} \: \cdots)]\!] の ローカル変数の値を取り出せません。
どうしようもないので、 処理系実装者は適切な \sigma をどうにかして持ってきて下さい。
単純にグローバル変数にしてもダメです。

仕様書を全体で見ると、 \sigma の扱いはいつもなんかおかしいです。
実装する人はちゃんと考えて下さい。
そうじゃない人は適当に注意して下さい。

関数holdを改めて解説しますが、 まずは位置 \alpha と継続 \kappa を受け取ります。
位置 \alpha というのはポインタです。
メモリ \sigma を位置 \alpha で呼び出すと、 その位置にある情報が次のような列になって取得できます。

 \langle {\rm value}, {\rm bool} \rangle

第1要素の「value」が欲しいので、 \sigma \alpha \downarrow 1 により 「value」を取得します。
send関数は「value」と継続 \kappa を引数の実行されますので、 単純に継続 \kappa が「value」という値で呼び出されます。
まとめますと「位置 \alpha にある値を継続に渡す」。

 {\cal E} [\![{\rm E_0} \, {\rm E^*}]\!]

定義を示します。

 {\cal E} [\![{\rm E_0} \, {\rm E^*}]\!] =
\lambda \rho \omega \kappa \: . \:
{\cal E^*} \: ({\rm permute} (\langle {\rm E_0} \rangle \: \S \: {\rm E^*}))
 \qquad \qquad \qquad \qquad \qquad \rho
 \qquad \qquad \qquad \qquad \qquad \omega
 \qquad \qquad \qquad \qquad \qquad
(\lambda \epsilon^* \: . \: ((\lambda \epsilon^* \: . \:
  {\rm applicate} \: (\epsilon^* \downarrow 1) \:
      (\epsilon^* \dagger 1) \: \omega \kappa)
 \qquad \qquad \qquad \qquad \qquad \qquad \quad
({\rm unpermute} \: \epsilon^*)))

この関数の内容は、 \cal E^* 関数をただ呼んでいるだけです。
しかし \cal E^* の第1引数と第4引数には色々手を加えているのが分かります。

まず注目したいのは、 \rm E_0  \rm E^* は、 それぞれ要素と列を表していることです。
さらに、実行内容を見ると、 \S であったり、  \downarrow ,  \dagger の記号があります。
前に少し余談として出しましたが、

(car ε*)は、 \epsilon^* \downarrow 1
(cdr ε*)は、 \epsilon^* \dagger 1
(cons E0 E*)は、 \langle {\rm E_0} \rangle \: \S \: {\rm E^*}

とみなすことができるます。
Lispの考え方が出来るのであれば、 たぶん列を再帰処理していくんだろうなあ、と予想することができます。

まだ説明していない関数は下記の通り。

  • permute
  • unpermute
  • applicate

それでは、それぞれを見て行きましょう。

 {\rm permute} : {\rm Exp^*} \to {\rm Exp^*}
 {\rm unpermute} : {\rm E^*} \to {\rm E^*}

これらの関数は並べ替えをするためのものです。
処理系実装者であるあなたが自由に作成する関数です。
よくわかんなかったら、引数をそのまま返却してください。

Schemeの関数が呼び出されるとき、各要素の評価順は決まっていません。
これはCommon Lispとは違っている部分です。
その評価順を変更するための関数が、 permuteとunpermuteになります。

Common Lispであれば、(aaa 10 20 30)という 関数呼び出しがあったとしたら、 10が評価され、20, 30と順番に評価した後に 関数aaaが呼び出されるのですが、 Schemeでは順番は未定です。
最初に20が評価されるかもしれませんし、そうじゃないかもしれません。
それを分かってもらおうとしてpermuteとunpermuteが制定されたとのこと。
面倒なら引数をそのまま返却するという実装でいいと思います。

 {\rm applicate} : {\rm E} \to {\rm E^*} \to {\rm P} \to {\rm K} \to {\rm C}
 {\rm applicate} = \lambda \epsilon \epsilon^* \omega \kappa \: . \:
  \epsilon \in {\rm F} \to (\epsilon \: | \: {\rm F} \downarrow 2)
  \epsilon^* \omega \kappa,
  \: {\rm wrong} \: {\tt "bad \: procedure"}

この関数は、関数を表す \epsilon を実行するという処理です。

まず引数が4つもあります。
とはいっても \omega, \kappa は実行に必要なものなので ただのたらいまわしです。

第1引数の \epsilon  \rm F であり、第2引数の \epsilon^* は引数の列です。
 \epsilon はいわゆる関数オブジェクトですが、 形式意味論でそのまま使える関数ではなく、 内容は \langle {\rm 位置L}, {\rm 関数} \rangle の列です。

処理の内容を見て行きましょう。
まずは \epsilon \in {\rm F} で、第1引数が \rm F かどうかの確認を行います。
もし \rm F じゃなかったらエラーが出て終わりです。

 (\epsilon \: | \: {\rm F} \downarrow 2) はどういう意味かというと、  \epsilon  \langle {\rm 位置L}, {\rm 関数} \rangle の列であるため、 その第2要素である関数を取り出すということです。
取り出した関数は、引数 \epsilon^* \omega \kappa を引数にして呼び出されます。

 {\cal E} [\![{\rm E_0} \, {\rm E^*}]\!] の説明に戻ります。
第1引数で実行されるpermuteは、要素の順番を変えるだけです。
面倒なら無視していいと思います。

4つ目の引数である

 (\lambda \epsilon^* \: . \: ((\lambda \epsilon^* \: . \:
  {\rm applicate} \: (\epsilon^* \downarrow 1) \:
      (\epsilon^* \dagger 1) \: \omega \kappa)
 \qquad \quad ({\rm unpermute} \: \epsilon^*)))

は少し複雑に見えます。
lambda式が2つあることに注意してください。
あと、どちらのlambda式の引数も \epsilon^* になっているので分かりづらいです。
こんな感じに変えてしまうことができます。

 (\lambda \epsilon^*_1 \: . \: ((\lambda \epsilon^*_2 \: . \:
  {\rm applicate} \: (\epsilon^*_2 \downarrow 1) \:
      (\epsilon^*_2 \dagger 1) \: \omega \kappa)
 \qquad \quad ({\rm unpermute} \: \epsilon^*_1)))

Schemeっぽく書き換えると次のようになります。

(lambda (e1)
  (let ((e2 (unpermute e1)))
    (applicate (↓ e2 1) († e2 1) ω κ)))

2つ目のlambdaをletにしてしまいました。
第一引数はこっちの計算の都合でpermuteを使って並び替えをしたのだから、 第四引数の継続内ではunpermuteを使ってちゃんと元の並び順に戻しましょうね、 という意味です。

参考までにpermuteを使用しない定義を示します。

 {\cal E} [\![{\rm E_0} \, {\rm E^*}]\!] =
\lambda \rho \omega \kappa \: . \:
{\cal E^*} \: (\langle {\rm E_0} \rangle \: \S \: {\rm E^*}) \: \rho \: \omega \:
(\lambda \epsilon^* \: . \: {\rm applicate}
  (\epsilon^* \downarrow 1) \: (\epsilon^* \dagger 1) \: \omega \kappa)

それでは、 \cal E^* を見て行きましょう。
呼び出される関数 \cal E^*  \cal E とは別物なので、 ちゃんと定義を見て行かなければなりません。
 \cal E^* は何をするのかというと、 関数呼び出しのカッコの中を再帰呼出で評価するというものです。
例えば

(list 10 20 30)

という関数呼び出しのリストがあった場合は、 それを先頭から順番に評価していきます。
でもSchemeは関数の呼び出し順序は不定なんじゃ?
というときのためのpermuteであって、

(30 20 10 list)

とか

(list 30 20 10)

みたいに好きに並び順を変えればいいのです。
もうめちゃくちゃに変えたっていいですけど、 ちゃんとunpermuteで元に戻せるようにして下さい。

 \cal E^* は、列の全ての要素を、単純に評価していくだけです。
それでは定義を見て行きましょう。

 {\cal E^*}[\![\:]\!] = \lambda \rho \omega \kappa \: . \: \kappa \langle \rangle

この定義は再帰呼出の最後に使われるものです。
何もない場合は、継続 \kappa に長さ0の列 \langle \rangle を渡します。

 {\cal E^*}[\![{\rm E_0} \, {\rm E^*}]\!] = \lambda \rho \omega \kappa \: . \:
{\cal E}[\![{\rm E_0}]\!] \: \rho \: \omega \:
 \qquad \qquad \qquad \quad
({\rm single} \: (\lambda \epsilon_0 \: . \:
{\cal E^*}[\![{\rm E^*}]\!] \: \rho \: \omega \:
(\lambda \epsilon^* \: . \: \kappa \:
(\langle \epsilon_0 \rangle \: \S \: \epsilon^*))))

どんどん行きたい所ですが、lambda式が3つもありますね。
この関数は、つまりは \rm E_0 を評価するために、  {\cal E}[\![{\rm E_0}]\!] を実行しているだけです。

 {\cal E}[\![{\rm E_0}]\!] は3つの引数を取る関数なので、 引数に \rho  \omega と、そして関数である継続を渡しています。
継続は次の文で作られます。

 {\rm single} \: (\lambda \epsilon_0 \: . \:
{\cal E^*}[\![{\rm E^*}]\!] \: \rho \: \omega \:
(\lambda \epsilon^* \: . \: \kappa \:
(\langle \epsilon_0 \rangle \: \S \: \epsilon^*)))

singleは、継続からひとつの値をとりだす関数です。
その値は \epsilon_0 に渡されます。 返却値もまた継続になります。

singleの引数である

 {\cal E^*}[\![{\rm E^*}]\!] \: \rho \: \omega \:
(\lambda \epsilon^* \: . \: \kappa \:
(\langle \epsilon_0 \rangle \: \S \: \epsilon^*))

は何なのかというと、 残りの列である \rm E^* 再帰処理に渡して、 すでに評価した \rm E_0 の値 \epsilon_0 を、 継続内で結合して返却するというものです。

もっと分かりやすく言うとmap関数です。
 {\cal E^*} とは、再帰処理を使ってmap関数をやっています。

例えば入力の値が

 {\rm E_X} = \langle \rm E_0, E_1, E_2 \rangle

であった場合、 {\cal E^*}[\![{\rm E_X}]\!] は次のようになります。

 {\cal E^*}[\![{\rm E_X}]\!] = \langle
{\cal E}[\![{\rm E_0}]\!],
{\cal E}[\![{\rm E_1}]\!],
{\cal E}[\![{\rm E_2}]\!]
\rangle

ただそれだけです。
よくある再帰関数なので、まあまあ理解しやすいと思います。

この辺りまで見ると、評価には常に継続があり、 変数の返却は当たり前のように継続に渡されていることが分かりました。
そりゃSchemeなんだからそんなもんだろうと思ってはいましたが、 ここまでちゃんと書かれていると作る方は楽だと思います。

続きます

次の投稿に続きます。
Scheme R7RSの形式意味論を読んでいく4 - nptclのブログ