続きです

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

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

形式意味論の関数

話しを続ける前に、形式意味論でよく使われる「関数」について説明しておく必要があります。
関数というのは、Lispを使う人ならみんな大好きなlambda式のことです。

lambda式とは、形式意味論だと「 $\lambda$ 」という記号であらわされます。
意味は関数そのものです。
Schemeでいう(lambda ...)さえ知っていれば理解できると思います。

どうも形式意味論では、関数の作成と定義ができるようで、当然呼び出すこともできます。
なんなら再帰呼出もバリバリ使っています。

関数の作成はこんな感じです。

$\lambda \; {\rm args} \; . \; {\rm body}$

argsは引数であり、bodyが実行部分です。
argsには変数がそのまま並べられます。
よく

$\lambda \rho \omega \kappa \; . \; {\rm body}$

のような表記が、本当にいっぱい出てきますが、これはSchemeでいうところの、

(lambda (ρ ω κ)
  body)

となります。
日本語で意味を書くならば「この関数は $\rho, \omega, \kappa$ の3つの引数を取る関数であり、実行内容はbodyです」となります。

関数定義は、次のように記載されます。

${\rm name} \: : \: \cdots$
${\rm name} \: = \lambda \: {\rm args} \: . \; {\rm body}$

これだけ見てもよくわからないので、具体的な例を仕様書から抜き出します。
send関数の定義をどうぞ。

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

関数定義は、上記のように2行によって行われます。
最初の行は関数の型についての定義です。
そして次の行が関数の実行内容です。

まずは下の方の関数の定義から見て行きますが、

$\lambda \epsilon \kappa \: . \: \kappa \langle \epsilon \rangle$

というのはつまりSchemeで書くと

(lambda (ε κ)
  (κ (list ε)))  ;; 関数呼び出し

なので、sendの定義は次のように書くことができます。

(define (send ε κ)
  (κ (list ε)))

Common Lispっぽく書くとこんな感じです。

(defun send (ε κ)
  (funcall κ (list ε)))

日本語で書くならば「send関数は、 $\epsilon$ と $\kappa$ の2つの引数を取り、 $\kappa$ 関数を引数 $\langle \epsilon \rangle$ で呼び出します」という意味です。

では上の行である

${\rm send} \: : \: \rm E \to K \to C$

はどういう意味なのでしょうか。
次のように覚えてください。

「第一引数の $\epsilon$ は $\rm E$ 型、第二引数の $\kappa$ は $\rm K$ 型であり、その結果 $\rm C$ 型の値を返却」

つまり、引数の型を示してから、一番最後に関数の返却値の型を表しています。
この場所に現れる矢印「 $\to$ 」は関数を意味しています。

いま出てきた $\rm E$ は、 ${\rm E} \in {\rm Exp}$ の $\rm E$ ではなく、これからまた別に定義する集合のことです。
ややこしいですね。
$\rm K$ なんかは、定数ではなく継続です。
同じ記号なのに、変数と集合のどちらも定義されているので注意して下さい。
（ちょっと話題に出しましたが継続はケーではなくKappaなんだと思います）

では話を続けます。
違う例の場合を考えましょう。

${\rm applicate} : {\rm E} \to {\rm E^*} \to {\rm P} \to {\rm K} \to {\rm C}$

applicate関数は、4つの引数を ${\rm E}, {\rm E^*}, {\rm P}, {\rm K}$ の順に受け取り、 $\rm C$ を返却するという意味です。
続いて、次の例を考えます。

${\rm single} : ({\rm E} \to {\rm C}) \to {\rm K}$

かっこが現れた場合は、中に矢印があるかどうかを確認してください。
矢印がある場合は関数の型であることを意味しています。
$({\rm E} \to {\rm C})$ は「引数 $\rm E$ を1つ受け取り、 $\rm C$ を返却する関数」です。

${\rm single} : (\cdots) \to {\rm K}$

なのでsingle関数が受け取る引数の個数は1つです。
つまり「引数に $({\rm E} \to {\rm C})$ の関数を1つ受け取り、 $\rm K$ を返却する関数」です。

以上で関数定義の説明は全てですが、これだと説明できない例は多々あります。
正直意味が分からない部分があるので、問題がありそうな部分は、説明の時にその都度話題にあげます。

では関数を呼び出すときはどうしたらいいでしょうか。
呼び出しは引数をただ横に並べるだけです。
例えばsend関数を呼び出す場合は次のようになります。

${\rm send} \: \epsilon \: \kappa$

実行した結果は $\kappa \langle \epsilon \rangle$ になるので、ここからさらに関数 $\kappa$ が実行されます。

例にあげたsend関数は「補助関数」という章に記載されているものでしたが、形式意味論の中核となる「意味関数」なるものの関数定義も一つだけ見てみましょう。

${\cal E}: {\rm Exp} \to {\rm U} \to {\rm P} \to {\rm K} \to {\rm C}$
${\cal E} [\![{\rm K}]\!] = \lambda \rho \omega \kappa \: . \: {\rm send} \: ({\cal K}[\![{\rm K}]\!]) \: \kappa$

まず ${\cal E} [\![{\rm K}]\!]$ とは何なのか、特に $[\![{\rm K}]\!]$ の部分を説明しなければなりません。

$\cal E$ はひとつの関数です。
そして $[\![\cdots]\!]$ で囲まれた部分の内容を元に、さらに条件が分岐して関数が呼び出される仕組みになっています。
今回のケースでは ${\cal E} [\![{\rm K}]\!]$ であるため、 $\rm K$ が渡された場合についての定義でしたが、他にも ${\cal E} [\![{\rm I}]\!]$ の定義も存在します。

${\cal E} [\![{\rm K}]\!]$ は、 $\rm K$ を評価するという意味です。
評価とは、すなわちevalのことです。
${\cal E} [\![{\rm K}]\!]$ の定義では、引数が $\rho, \omega, \kappa$ の3つであり、内容はsend関数を呼び出すというものです。

では型の方はどうなっているでしょか。

${\cal E}: {\rm Exp} \to {\rm U} \to {\rm P} \to {\rm K} \to {\rm C}$

$\rm Exp$ から $\to$ を経由して、 $\rm C$ まで5つの型（集合）がつあります。
つまり $\cal E$ 関数は4つの引数を取るということです。
しかし、 ${\cal E} [\![{\rm K}]\!]$ の $\lambda$ は 3つの引数を取る定義のため数があっていません。
$\rho$ は $\rm U$ 型、 $\omega$ は $\rm P$ 型、 $\kappa$ は $\rm K$ 型、返却は $\rm C$ 型なので、最初の $\rm Exp$ は何だということになります。

関数 $\cal E$ は4つの引数を取りますが、最初の引数の型に応じて呼び出す関数が分岐します。
オブジェクト指向のジェネリック関数といよりは、 Schemeのマクロの方が近いかもしれません。
もし、 ${\cal E} \: \epsilon \rho \omega \kappa$ という関数呼び出しがされたとき、第一引数である $\epsilon$ の内容を調べて、もし $\epsilon \in {\rm K}$ であるならば、 ${\cal E} [\![{\rm K}]\!] \: \rho \omega \kappa$ を呼び出します。

上記の説明は覚えておいてください。
実際に結構変な関数の呼び出し方がされています。

【注意】暗黙のlambda式

いくつか注意するべき点がありますので説明します。
たまに引数の数が一致してないことがあります。

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"}$

single関数の型についてはすでに説明しましたが、 $({\rm E} \to {\rm C}) \to {\rm K}$ なので、引数に関数を1つ受け取り、 $\rm K$ を返却するというものです。
ところが定義を見ると、関数の定義が $\lambda \psi {\epsilon^*}$ であるため、 $\psi$ と $\epsilon^*$ の2つの引数を受け取るようになっています。
引数の数に不一致が生じているのです。

こんな場合は、大抵は $\lambda$ が省略されています。
正しくは下記のようになります。

${\rm single} : ({\rm E} \to {\rm C}) \to {\rm K}$
${\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^*$ 」にしただけです。
ひとつの関数を受け取って、ひとつの関数を返すという意味になるので、型の個数と内容が一致します。

このような書き換えは、本当に合っているのか正直わかりません。
SchemeやCommon Lispならばこの書き換えで正しいのですが、もしかしたら形式意味論特有の何かがあるかもしれません。

関数の引数の数が型と一致していないものは結構あります。
他の例もひとつあげますと、例えばtwoargがあります。

${\rm twoarg} : ({\rm E} \to {\rm E} \to {\rm P} \to {\rm K} \to {\rm C}) \to ({\rm E^*} \to {\rm P} \to {\rm K} \to {\rm C})$
${\rm twoarg} = \lambda \zeta {\epsilon^*} \omega \kappa \: . \: \# {\epsilon^*} = 2 \to \zeta ({\epsilon^*} \downarrow 1) ({\epsilon^*} \downarrow 2) \omega \kappa,$
$\qquad \qquad \qquad {\rm wrong} \: {\tt "number \: of \: arguments"}$

型が長々と書かれていますが、結局のところtwoargの引数はたった1つです。
引数に1つの関数を受け取り、返却されるのも関数です。
しかし $\lambda$ を見ると、引数は4つも記載されていますので合っていません。
次のように書き換えるのが正解です。

${\rm twoarg} = \lambda \zeta \: . \; \lambda {\epsilon^*} \omega \kappa \: . \: \# {\epsilon^*} = 2 \to \zeta ({\epsilon^*} \downarrow 1) ({\epsilon^*} \downarrow 2) \omega \kappa,$
$\qquad \qquad \qquad {\rm wrong} \: {\tt "number \: of \: arguments"}$

変更は「 $\lambda \zeta {\epsilon^*} \omega \kappa$ 」から「 $\lambda \zeta \: . \; \lambda {\epsilon^*} \omega \kappa$ 」です。
twoarg関数は、引数の個数のチェックを行うときに役立つものです。
他にもoneargやthreeargなど存在しますが、どれもこれも同じような問題を抱えていますので注意してください。

【注意】lambda式とマッカーシーの条件

次の式は理解できるでしょうか。

$\lambda \sigma \: . \: {\rm body} \: \sigma$

カッコをつけると理解できると思います。

$(\lambda \sigma \: . \: {\rm body}) \: \sigma$

カッコ内のlambda式は関数であり、その関数をすぐに $\sigma$ という引数で呼び出しているという文です。
次のように書き換えることができます。

$\rm body$

こんな書き方を好んですることはないと思います。
それでは、次の文を見てみましょう。

$\lambda \sigma \: . \: x \to {\rm body1} \: \sigma_1, {\rm body2} \: \sigma_2$

この書き方はかなり使われます。
そしてLispに慣れている人たちにとっては、なんなのこれ？ってなりませんか？

マッカーシーの条件により、 $x$ の値によって条件が分岐します。
もし $x$ がtrueなら $(\lambda \sigma \: . \: {\rm body_1}) \: \sigma_1$ が実行されます。
もし $x$ がfalseなら $(\lambda \sigma \: . \: {\rm body_2}) \: \sigma_2$ が実行されます。

これって文法的に合ってるんでしょうか。
次のように書き直した方が自然なように思えます。

$x \to \lambda \sigma \: . \: {\rm body1} \: \sigma_1, \lambda \sigma \: . \: {\rm body2} \: \sigma_2$

この書き方に気が付かないと、とにかく意味が分からなくなります。
後々で次のような文が出てきたら注意してください。

$({\rm update} \: ({\rm new} \: \sigma \: | \: {\rm L}) \epsilon \sigma)$
${\rm wrong} \: {\tt "out \: of \: memory"} \: \sigma$

updateの方は、それ自体が $\sigma$ なので、lambda式の引数扱いになります。
wrongの方は、文字列の後にある $\sigma$ がlambda式の引数になります。

私はこれに気が付かず、ずっと悩んでました。
みなさんも注意してください。

7.2.2. Domain equations

ここでは、よく使われる変数と型（集合）を定義しています。
上から順番に説明して行きたいのですが、説明の都合上いろいろと前後します。

$\alpha \in {\rm L}$ , locations

$\rm L$ は位置をあらわす型です。
つまりアドレスのことです。
$\alpha$ は位置の変数です。
よく関数の引数なんかに $\alpha$ が使われます。

$\nu \in {\rm N}$ , natural numbers

$\rm N$ は自然数の型です。
$\nu$ は自然数を格納する変数です。

${\rm T} = \{ {\rm false}, {\rm true}\}$ , booleans

$\rm T$ はブール値です。
見てわかる通り、trueかfalseのどちらかの値を取ります。
ちなみに結構出てきます。
Schemeでいう、#false, #trueのことです。

$\rm Q$ , symbols

シンボルです。

$\rm H$ , characters

文字です。
文字列ではなく、ひとつの文字を表します。

$\rm R$ , numbers

数です。
整数やら実数やら複素数やら全部含みます。

$\rm E_p = {\rm L} \times {\rm L} \times {\rm T}$ , pairs

$\rm E_p$ はペアです。
ペアとはつまりコンスです。
(car . cdr)みたいなやつです。

ここで分からなかったのが「 $\times$ 」です。
なんで外積？とずっと悩んでいたのですが、そうではないようです。
前に形式意味論とは集合論に関わりがあることを言いました。
集合論では外積ではなく「直積」を意味します。
$\rm L$ は位置でありつまりポインタなので、ペアがcarとcdrの2つの位置を保有するという意味であるならば、 ${\rm L} \times {\rm L}$ の直積の集合は、あらゆるcarとcdrの2つの位置の集合という意味になります。

ではさらにブール値の $\rm T$ の直積を取っていますが、これどうなるの？
純粋に何やってるのか分かりませんでした。
確認のために次のような場合を考えます。

${\rm L_1} = \{a, b, c\}$
${\rm L_2} = \{1, 2\}$

まずは上記二つの直積を計算します。

${\rm L_1} \times {\rm L_2} = \{(a, 1), (a, 2), (b, 1), (b, 2), (c, 1), (c, 2)\}$

さらに $\rm T$ の直積を取るってこうなるの？

${\rm L_1} \times {\rm L_2} \times {\rm T} = \{$
$\quad ((a, 1), true), \: ((a, 2), true), \: ((b, 1), true),$
$\quad ((b, 2), true), \: ((c, 1), true), \: ((c, 2), true),$
$\quad ((a, 1), false), \: ((a, 2), false), \: ((b, 1), false),$
$\quad ((b, 2), false), \: ((c, 1), false), \: ((c, 2), false)$
$\}$

そうじゃなくてこんな感じ？

${\rm L_1} \times {\rm L_2} \times {\rm T} = \{$
$\quad (a, 1, true), \: (a, 2, true), \: (b, 1, true),$
$\quad (b, 2, true), \: (c, 1, true), \: (c, 2, true),$
$\quad (a, 1, false), \: (a, 2, false), \: (b, 1, false),$
$\quad (b, 2, false), \: (c, 1, false), \: (c, 2, false)$
$\}$

これについての回答は、直積集合で検索したら出てきました。

直積集合
https://ja.wikipedia.org/wiki/%E7%9B%B4%E7%A9%8D%E9%9B%86%E5%90%88

厳密にいうと上だけど、下でいい場合もあるとのこと。
Schemeの仕様書のどこを見ても何も書いていませんが、たぶん下でいいということで話を進めます。
というか、どう考えても下で何にも問題ないです。

それでは、なぜ直積を取ってまで膨大な量の集合を作ったのでしょうか？
これは「全部の可能性を考えるとこんなになるんですよ」くらいの意味しかありません。
もうちょっと違う見方をしましょう。
${\rm L} \times {\rm L} \times {\rm T}$ というのは、「carのアドレスと、cdrのアドレスと、bool値の、3つの値を取る」くらいの理解で問題ありません。

それでは最後にbool値の意味を説明します。
ペアはcarとcdrの2つの値しか持たないため、bool値で直積を取る必要はないはずです。
理由は仕様書の最初の方に書いてあります。

「ペア、ベクタおよび文字列に紐づけられたブーリアンのフラグは、可変オブジェクトの場合は真、不変オブジェクトの場合は偽になります。」

だそうです。
readonlyかどうかの値なんですね。

${\rm E_v} = {\rm L^*} \times {\rm T}$ , vectors

$\rm E_v$ はベクトルです。
つまり一次元の配列です。

配列は要素がいっぱいあるから、引数の数だけ $\rm L$ があるのは分かります。
でも $\rm L^*$ ってどういうことなの？

ペアのときは要素が2つだけだったので、 ${\rm L} \times {\rm L}$ の直積を取っていました。
ということは、例えば5つの要素がある配列の場合は

$\rm L_1 \; L_2 \; L_3 \; L_4 \; L_5 \times {\rm T}$

ではなく、明らかに下記のようになりますね。

$\rm L_1 \times L_2 \times L_3 \times L_4 \times L_5 \times {\rm T}$

そういう時は $\Sigma$ みたいな書き方で、 $\Pi$ を使って表現してるのも見かけましたが、面倒ですし場合場合に応じて自分で予想していくしかないみたいです。
もしかしたら、自分が集合論とか形式意味論に慣れてないだけであって、こういうのは自明なのかもしれません。

${\rm E_s} = {\rm L^*} \times {\rm T}$ , strings

$\rm E_s$ は文字列です。
つまりは要素が「文字」だけの一次元配列（ベクトル）のことです。

${\rm M} = \{\rm false, true, null, undefined, unspecified\}$ , miscellaneous

その他いろいろです。

$\sigma \in {\rm S} = {\rm L} \to ({\rm E} \times {\rm T})$ , stores

ここからは説明する順番を変更します。

storesとは、メモリのことです。
まずは「 $\sigma \in {\rm S}$ 」であるということ。
$\rm S$ はメモリの全領域の集合をであり、 $\sigma$ が実際使えるメモリです。
次に定義ですが、

${\rm S} = {\rm L} \to ({\rm E} \times {\rm T})$

これの意味が分からない。
なんで「 $\to$ 」がここに出てきたの？
ずっと悩んでて、やっと意味が分かりましたが、

この書き方って、あんまり良いとは思えません。
まず「 $\to$ 」があるということは、関数を意味しています。
しかし集合である $\rm S$ が関数であるはずがないので、変数 $\sigma$ が関数であると言っています。
分けて考えると次の通り。

$\sigma \in {\rm S}$
$\sigma = {\rm L} \to ({\rm E} \times {\rm T})$

意味を日本語で書くと、

「変数 $\sigma$ は、 $\rm S$ の集合に含まれる。」
「変数 $\sigma$ は、引数 $\rm L$ 、返却値 $({\rm E} \times {\rm T})$ の関数。」

ということになります。
$\sigma$ が関数なんですね。
返却値 $({\rm E} \times {\rm T})$ とは、式 $\rm E$ とbool値 $\rm T$ の直積ですので、 $\rm E$ とboolの2つの値が返却されるという意味です。

ちなみに、 $\sigma$ はメモリを意味しており、具体的に値を格納しておく場所なので、とても出番があります。
例えば、位置情報 $\alpha$ があったとして、

$\sigma \: \alpha$

みたいに関数 $\sigma$ を呼び出すと、

$\langle {\rm E_1}, {\rm true} \rangle$

のような列が返却されます。
この場合、第一要素である $\rm E_1$ が値そのもので、第二要素のtrueは、そのメモリ領域に値が書き込まれたかどうかの値になります。
もし領域を確保したばかりならfalseであり、何かしらの値が設定されたらtrueになります。
値だけを取得したい場合は次のようになります。

$(\sigma \: \alpha) \downarrow 1$

$\rho \in {\rm U} = {\rm Ide} \to {\rm L}$ , environments

environmentsは、識別子からアドレスを求める関数です。
識別子とは変数のことです。

storesのときと同じように考えると、次のようになります。

$\rho \in {\rm U}$
$\rho = {\rm Ide} \to {\rm L}$

日本語で書くと、 $\rho$ は $\rm U$ 型の変数であり、また $\rho$ は ${\rm Ide} \to {\rm L}$ の関数です。
$\rho$ は引数に $\rm Ide$ を受け取り、その結果アドレスである $\rm L$ を返却します。

例えば、変数から $\rho$ でアドレスを取得し、アドレスから $\sigma$ でメモリ内容を取得するような使い方をします。

$\theta \in {\rm C} = {\rm S} \to {\rm A}$ , command conts

contsとは継続です。
$\theta$ はコマンドの継続と呼ばれています。

これがなぜ継続と呼ばれているのかは分かりません。
$\theta$ は継続の返却値です。
次の $\kappa \in {\rm K}$ の説明も継続なので、そこで詳しく説明します。

$\theta$ は引数に $\rm S$ を受け取り、 $\rm A$ を返却する関数です。
しかしこの辺りは全然出てこないので無視します。
単純に、 $\theta$ は継続の戻り値だと覚えておいてください。

$\kappa \in {\rm K} = {\rm E^*} \to {\rm C}$ , expression conts

$\kappa$ は式の継続です。
みなさんがよく知ってる継続のことです。

型で表されているとおり、継続 $\kappa$ は関数です。
継続とは、式の返却値を引数に受け取る関数です。
引数 $\rm E^*$ で返却値を受け取りますが、これはつまりvaluesのことです。
継続 $\kappa$ は関数なので、返却値を受け取り、コマンドの継続 $\theta$ を返却します。

$\theta$ は $\kappa$ 関数の返却値です。
注意して欲しいのは、引数に受け取る返却値 $\rm E^*$ と、継続の返却値 $\theta$ が別だということです。
$\rm E_0$ は、SchemeというLisp上の式の返却値です。
一方 $\theta$ は、形式意味論で扱われる返却値です。