はじめに

Schemeの仕様書を見ていました。
ものはここにあります。

さらに日本語訳もいくつかあるようです。
私はここを利用させていただきました。

R7RS 日本語訳　（milkpot様）
http://milkpot.sakura.ne.jp/scheme/r7rs.html

内容は難しいわけでもなく、まあ無難に読み進めていくことができるのですが、 7章の「7.2. Formal semantics」だけは一体なんなんだ。
本当になんなのこれ。
意味が分からない。
ということで長い間どうしたらいいものかと悩んでいました。

「形式意味論」だそうです。
この形式意味論なるものは、Schemeの仕様書を見るまで知りませんでした。
しかしながら知らなかったのは単純に私が無知だったためであり、 40年前から研究されてきたものだとしてびっくり。

情報っぽい大学に行った人なら知ってるみたいですね。
自分はそんなんじゃないので本当に全然知らず、こんなのやる必要があるのかずっと悩んでました。
でもやります。

本投稿は、素人なりにR7RSの形式意味論を理解するというものです。

形式意味論とは何なのか

「Denotational Semantics」というものらしいです。
日本語訳では表示的意味論、形式意味論、などいっぱい呼び方があります。
～的と～論ってどっから来たんでしょうか。
個人的には「表示意味」が簡潔でいいと思いました。
まあそれはいいとして、日本語訳では「形式意味論」と書かれていたのでそれでいこうと思います。

形式意味論とは、かなりプログラムに近い設計書のことです。
Schemeの仕様書だけ見てると、何の説明も無くいきなり出てくるためびっくりします。
特に自分のような何も知らない人が見るとやる気をなくします。
ずっと「本当にこれを理解しなきゃダメなの？」と思ってました。

それでちゃんと読んでいこうと決心したわけですが、苦労しますよ。
多分どんな人でも苦労すると思います。
形式意味論には、その名の通り「Denotational Semantics」なる本があるので、もしかしたらそれを読むと簡単に理解できるのかもしれません。
今回は何も知らない自分が覚悟を決めて読んでみたという内容になります。

何も知らないというのがポイントです。
この手の解説は、みんなベテランがベテランに向けて解説しているものばかりなのではないでしょうか。
私は完全な素人なので、素人が素人に教える視点で話を進めることができると思います。
とはいっても、Lispの経験はまあまああるので、そのあたりは不親切になるかもしれません。

便利なページの紹介

先にとても分かりやすい所を紹介します。

集合論　（数理大好き・tepika_math様）
http://proofcafe.org/k27c8/math/math/set_theory/
R7RSの形式的意味論を読む　（takl様）
https://qiita.com/takl/items/bed48daf47dc071fa828

なんでいきなり集合論なんだというと、どうも形式意味論って集合論の考え方をベースにしているようなのです。
最初に読んでおくと理解しやすいと思います。

ここでは自分でSchemeを実装できるようになることを優先して理解を進めます。
自分は学者でも何でもないので、やっぱり作ることが目的となります。
形式意味論を正確に理解することを目的としていないのでご注意ください。
とはいっても、そのうちちゃんと勉強したいですね。

それでは順番に見て行きます。

7.2. Formal semantics

仕様書のPDFやらなにやらを同時に見つつ話を進めます。
まずは「7.2 形式意味論」から。
ここでは記法について説明しています。

$\langle\,\ldots\,\rangle$ , sequence formation

単なる列です。
英語ではよくsequenceと言います。

Lispだと(10 20 30)みたいに書かれるやつです。
集合ではなく列なので順番があります。

こんな感じ $\langle a, b, c \rangle$ で表現されます。
空の列 $\langle \rangle$ なんかもありますので注意。

$s \downarrow k$ , $k$ th member of the sequence $s$ (1-based)

列の要素を取り出します。
Schemeのlist-refや、Common Lispのnth, eltみたいなもんです。
ただし位置 $k$ は、0開始ではなく1から始まるとのこと。

例えば、 $\langle a, b, c \rangle \downarrow 2$ は、列の2つ目ということなので $b$ です。
ちなみに、Schemeの $\TeX$ ファイルでは、この記号 $\downarrow$ の事をそのまんま「elt」定義してました。
Common Lispだ！

$\#s$ , length of sequence $s$

列の長さです。
Schemeでいうlength関数です。

例えば、 $\# \langle a, b, c \rangle$ は、要素数の3になります。

$s \:\S\: t$ , concatenation of sequences $s$ and $t$

列の連結です。
例えば、 $\langle a, b, c \rangle \:\S\: \langle d, e, f \rangle$ は、 $\langle a, b, c, d, e, f \rangle$ です。

Common Lispだとconcatenate関数になるかと思います。

$s \dagger k$ , drop the first $k$ members of sequence $s$

列 $s$ の、最初から $k$ 個の要素を削除します。
例えば、 $\langle a, b, c, d, e, f \rangle \dagger 2$ だと、 $a$ と $b$ の2つ削除されるため、 $\langle c, d, e, f \rangle$ です。

Common Lispだとsubseq関数がそのまま当てはまりますね。

* (subseq '(a b c d e f) 2)
(C D E F)

余談というか、よく使われるLispっぽい操作を下記に示します。

(car s)は、 $s \downarrow 1$
(cdr s)は、 $s \dagger 1$
(cons x y)は、 $\langle x \rangle \: \S \: y$

となります。
再帰呼出なんかで出てきますので、覚えておくといいと思います。

$t \to a, b$ , McCarthy conditional "if $t$ then $a$ else $b$ "

if文です。
マッカーシーの条件と言います。
直接書かれている通り、そのまんまifです。

${\tt false} \to a, b$ みたいな感じだと、結果は $b$ になります。
どんな使われ方をするかというと、 $\#s = 1 \to s \downarrow 1, {\tt error}$ みたいな感じになります。

$\rho[x/i]$ , substitution " $\rho$ with $x$ for $i$ "

$\rho$ に値を格納する際に使います。
$\rho$ はハッシュテーブルのようなものであり、 $x$ が値で $i$ がキーです。

格納すると言っても $\rho$ そのものを書き換えるのではありません。
新たに $x$ と $i$ が結びついている新しい $\rho$ が返却されます。

$x$ in ${\tt D}$ , injection of $x$ into domain ${\tt D}$

$x$ を $\tt D$ の型として扱うという意味です。

正直、この辺はよくわかりません。
ただ使い方を見ていると、 $x$ という値ができたから、それを無理矢理D型として扱って下さいと言ってるように見えます。
無理矢理とはどういうことかというと、「どうせあなたは処理系を作ってるんだろうから、メモリの書き換えでも何でもいいから無理矢理キャストして下さい」という意味に感じます。

あと、 $\tt D$ は型と書いてますが、実際は集合です。
あとでふわっと説明します。

$x\,\vert\,{\tt D}$ , projection of $x$ to domain $\tt D$

$x$ を $\tt D$ の型として扱うという意味です。

$x$ in $\tt D$ と同じじゃんということですが、正直何が違うのかよくわかりませんでした。
こっちの方は、新規で割り当てられたメモリに対して明示的に型を指定したりだとか、あと変数に対して「この要素を取り出してね」みたいな操作を行う際に使われていました。

絶対ダメなんだろうけど、何となく雰囲気で使って行きたいと思います。

この章後それ以降

ゴチャゴチャ書いてますが省略します。
話しを進めて行って、必要になったらその都度説明します。

7.2.1. Abstract syntax

抽象構文です。
どういう意味か分かりませんが、型の説明などがされています。

まずは集合について説明します。
集合というのは要素の集まりであり、例えば

${\rm A} = \{x, y, z\}$

のようにした場合、「集合 $\rm A$ は、要素 $x, y, z$ で構成される」という意味になります。
よく使われるのは「 $\in$ 」という記号であり、これは「含まれる」ということを意味します。

例えば要素 $z$ は、集合 $\rm A$ に含まれるため、

$z \in {\rm A}$

が成り立つということになります。

形式意味論では、集合を「型」とみなすことができます。
具体的にどういうことなのか、説明を見て行きましょう。

${\rm K} \in {\rm Con}$ , constants, including quotations

定数についての説明です。
ここで言う定数とは、100とか"Hello"のことです。
また、(quote xxx)とか'xxxも定数に含まれます。

${\rm K} \in {\rm Con}$ とは、 $\rm K$ が $\rm Con$ に含まれるということを意味します。
よって、 $\rm K$ は要素であり、 $\rm Con$ は集合です。
とはいっても、 $\rm K$ というアルファベットが要素ではありません。

$\rm Con$ とは、この世にあるすべての定数の集合だと考えてください。
$\rm K$ は要素というよりも変数です。
$\rm Con$ は集合というよりもなら「型」とみなします。
つまり変数 $\rm K$ は、 $\rm Con$ 型であると言っています。

式の中に $\rm K$ が出てきたら、それは $\rm Con$ 型の変数であるという意味です。
「型」というのは、プログラミングでよく出てくる「タイプ」のことです。
例えば「100はinteger型」とかの型です。

この考え方はずっと出てきます。
繰り返しになりますが、 ${\rm K} \in {\rm Con}$ ということは、「変数 $\rm K$ は、 $\rm Con$ 型である」という意味になります。

注意点を一つ。
仕様書では、 $\rm K$ を定数以外にも、継続を表す集合という意味で使っています。
なんで同じ記号なのか知りませんが、どっちのことなのかは文脈で判断するしかありません。
たぶん、K（アルファベット）とΚ（Kappa）の違いなんだと思います。
そんなの分かんないよ。

継続の集合については、あとでちゃんと説明します。

${\rm I} \in {\rm Ide}$ , identifiers (variables)

$\rm Ide$ は識別子の型です。
プログラミングだと識別子より「変数」と読んだ方が自然だと思います。

定数 $\rm Con$ の時と同じように「変数 $\rm I$ が集合 $\rm Ide$ に含まれる」ということです。
$\rm Ide$ が変数全体の集合で、 $\rm I$ が変数そのものです。
Schemeでは、変数とはシンボルのことです。

「変数 $\rm I$ は、 $\rm Ide$ 型である」という意味です。

${\rm E} \in {\rm Exp}$ , expressions

$\rm Exp$ とは式のことです。
$\rm E$ は具体的な式を表しており、今後めちゃくちゃ出てきます。
$\rm E^*$ とか $\rm E_0$ みたいに、 $\rm E$ に関する表記が出てきたら、 $\rm Exp$ 型の変数なんだなと思って下さい。
式とは、10とか、(+ 10 20 30)のようなものです。
この式というものの定義が形式意味論の中核であったりします。

${\rm \Gamma} \in {\rm Com} = {\rm Exp}$ , commands

ここは混乱しました。
「 $\in$ 」と「 $=$ 」の演算子の優先順位ってどうなってるの？

最初に ${\rm \Gamma} \in {\rm Com}$ であり、続けて ${\rm Com} = {\rm Exp}$ です。
自分はこの辺の表記を本当に全く知らないため、 $\rm \Gamma$ が ${\rm Com} = {\rm Exp}$ という等号の結果に含まれるってどういうことなんだと真剣に悩んでいました。
だって $\rm Com$ と $\rm Exp$ が一緒ならなんで分けるの？って事になりません？

では、なぜ分けるのかというと、 $\rm Exp$ は返却値込みの式を表しているようで、 $\rm \Gamma$ と $\rm Com$ は、返却値を無視した式ということで分けて考えるようです。

ということで、 $\rm Com$ と $\rm Exp$ は、今のところ同じです。
どういう時に使うかというと、例えばlambdaのbody部を見てみます。

(lambda ()
  100            ;; Γ1, ここはCom型、値は捨てるから
  (+ 10 20 30)   ;; Γ2, ここはCom型、値は捨てるから
  'hello)        ;; E1, ここはExp型、なぜなら戻り値に意味があるから

こんな感じの分類になります。

$\rm Exp$ の定義

$\rm Exp$ の説明になります。

${\rm Exp} \to {\rm K} \: | \: {\rm I} \: | \: ({\rm E_0} \: {\rm E^*})$
$\qquad \qquad | \: ({\tt lambda} \; ({\rm I^*}) \; {\rm \Gamma^*} \: {\rm E_0})$
$\qquad \qquad | \: ({\tt lambda} \; ({\rm I^*}) \; {\rm \Gamma^*} \: {\rm E_0})$
$\qquad \qquad | \: ({\tt lambda} \; ({\rm I^*} \; . \;\; {\rm I}) \; {\rm \Gamma^*} \: {\rm E_0})$
$\qquad \qquad | \: ({\tt lambda} \;\; {\rm I} \;\; {\rm \Gamma^*} \: {\rm E_0})$
$\qquad \qquad | \: (\tt if \rm \; E_0 \; E_1 \; E_2)$
$\qquad \qquad | \: (\tt if \rm \; E_0 \; E_1)$
$\qquad \qquad | \: (\tt set! \rm \;\; I \;\; E)$

まず次のような形になっています。

${\rm Exp} \to \cdots$

これは導出です。
マッカーシーの条件（if文のこと）ではないので注意。
$\rm Exp$ とは、右のようなことを意味します。
右辺に現れる縦棒の $\; | \;$ はorのことで、区切られたどれかに当てはまりますよと言っています。
つまり「 $\rm Exp$ は、 $\rm K$ か、 $\rm I$ か、 $\cdots$ のどれかになります。」ということです。
それでは右辺の内容を、ひとつずつ見て行きましょう。

${\rm Exp} \to {\rm K}$

${\rm K} \in {\rm Con}$ なので、 $\rm K$ というのは定数のことです。
$\rm Exp$ は、定数も含んでいますよということになります。

100とか'helloみたいな定数が評価されると、 $\rm Exp$ 型の $\rm E$ として扱われるようになります。

$\rm Exp \to \rm I$

$\rm I$ は変数です。
変数には値が束縛されていますので、その値が $\rm Exp$ として扱われます。

${\rm Exp} \to ({\rm E_0} \: {\rm E^*})$

関数の呼び出しです。
具体的に言うと

(+ 10 20 30)

みたいなやつですね。

表記についていろいろ説明が必要です。
$\rm E_0$ は、 ${\rm E_0} \in {\rm Exp}$ なので、式になります。
上の例で言うと、+の部分に該当します。

続いて $\rm E^*$ というのは、「 $\rm E$ の0個以上の繰り返し」を意味しています。
つまり、

$({\rm E_0})$
$({\rm E_0} \: {\rm E_1})$
$({\rm E_0} \: {\rm E_1} \cdots {\rm E_n})$

みたいな感じになります。 $\rm E^*$ も当然 ${\rm E^*} \in {\rm Exp}$ です。
上の例にあてはめると、 10が $\rm E_1$ 、 20が $\rm E_2$ 、 30が $\rm E_3$ になります。

かなり面倒なことに、今回のようにアスタリスクである「*」が付いた場合、 0個以上の繰り返しではなく、「 $\rm E^*$ 」という一つの変数を表すケースもあります。
大抵の場合は、その変数には、複数の値が格納されている列が格納されています。
では、繰り返しなのか、変数そのものなのかというのは、見ただけでは分かりませんので、その時の文脈で自分で判断するしかありません。

${\rm Exp} \to ({\tt lambda} \; ({\rm I^}) \; {\rm \Gamma^} \: {\rm E_0})$

lambda式です。
$\rm I^*$ は変数がずらずら並ぶので、

(lambda () ...)
(lambda (x) ...)
(lambda (x y z) ...)

みたいな感じになります。

$\rm \Gamma^*$ とは、 $\rm \Gamma$ が0個以上連なるという意味ですが、最後以外の式は戻り値が無視できるので、 $\rm E$ ではなく $\rm \Gamma$ で表されています。
戻り値は $\rm E_0$ が返却します。

ふと思ったのですが、 $\rm E_0$ は必須なんですね。
Common Lispではbody部が空だった場合はnilが返却されるのですが、 Schemeでは必ず $\rm E_0$ が必要なようです。
つまり(lambda ())はダメで、 (lambda () 100)のように、最後に何か書きましょう。

${\rm Exp} \to ({\tt lambda} \; ({\rm I^} \; . \;\; {\rm I}) \; {\rm \Gamma^} \: {\rm E_0})$

lambda式のdotted listの場合です。
例えばこんな感じ。

(lambda (x y . z) ...)

ちなみに定義ではこんなのも許されてしまうようです。

(lambda (. z) ...)

なんだよこれ。
ダメに決まってんだろ。

${\rm Exp} \to ({\tt lambda} \;\; {\rm I} \;\; {\rm \Gamma^*} \: {\rm E_0})$

lambda式の引数全体を表す表現です。
つまりこんな感じ。

(lambda x ...)

${\rm Exp} \to (\tt if \rm \; E_0 \; E_1 \; E_2)$

if文の場合です。
$\rm E_0$ の返却時に応じて実行する式が変わります。
もしfalseではなかった場合（真の場合）は $\rm E_1$ を実行し値を返却します。
もしfalseだった場合は $\rm E_2$ を実行し値を返却します。

普通の関数であれば、 $\rm E_0$ の値に関係なく、 $\rm E_1$ と $\rm E_2$ は両方とも実行されてしまいますが、if文は実行を制御できるので特別扱いされているのです。

${\rm Exp} \to (\tt if \rm \; E_0 \; E_1)$

if文のelse項が省略された場合です。
もし $\rm E_0$ がfalseではなかった場合（真の場合）にのみ、 $\rm E_1$ を実行して返却します。
もしfalseだった場合は $\rm E_1$ は実行されませんが、if文全体の戻り値は規定されていないとのこと。
これはCommon Lispとは違っていますね。
Common Lispだと、(if e0 e1)は(if e0 e1 nil)と同じです。

${\rm Exp} \to (\tt set! \rm \;\; I \;\; E)$

この文は、変数 $\rm I$ に値 $\rm E$ を代入する命令です。
set!式の戻り値は規定されていないとのこと。

余談ですが、Common Lispのsetqとはいろいろ違っています。
setqの場合は、

(setq v1 e1 v2 e2 ... vn en)

という書式であり、左から右へ変数viに値eiを代入していくというもの。
setqの戻り値は最後の値であるenです。
しかしもし(setq)と呼ばれた場合はnilが返却されます。
さらにviはシンボルですが、もしdefine-symbol-macroかsymbol-macroletが代入の対象になった場合は、そこだけ抜き出されてsetf式に展開されます。
もう何が何だかわかりませんね。

続きます

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

nptclのブログ

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

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

はじめに

形式意味論とは何なのか

便利なページの紹介

7.2. Formal semantics

$\langle\,\ldots\,\rangle$ , sequence formation

$s \downarrow k$ , $k$ th member of the sequence $s$ (1-based)

$\#s$ , length of sequence $s$

$s \:\S\: t$ , concatenation of sequences $s$ and $t$

$s \dagger k$ , drop the first $k$ members of sequence $s$

$t \to a, b$ , McCarthy conditional "if $t$ then $a$ else $b$ "

$\rho[x/i]$ , substitution " $\rho$ with $x$ for $i$ "

$x$ in ${\tt D}$ , injection of $x$ into domain ${\tt D}$

$x\,\vert\,{\tt D}$ , projection of $x$ to domain $\tt D$

この章後それ以降

7.2.1. Abstract syntax

${\rm K} \in {\rm Con}$ , constants, including quotations

${\rm I} \in {\rm Ide}$ , identifiers (variables)

${\rm E} \in {\rm Exp}$ , expressions

${\rm \Gamma} \in {\rm Com} = {\rm Exp}$ , commands

$\rm Exp$ の定義

${\rm Exp} \to {\rm K}$

$\rm Exp \to \rm I$

${\rm Exp} \to ({\rm E_0} \: {\rm E^*})$

${\rm Exp} \to ({\tt lambda} \; ({\rm I^}) \; {\rm \Gamma^} \: {\rm E_0})$

${\rm Exp} \to ({\tt lambda} \; ({\rm I^} \; . \;\; {\rm I}) \; {\rm \Gamma^} \: {\rm E_0})$

${\rm Exp} \to ({\tt lambda} \;\; {\rm I} \;\; {\rm \Gamma^*} \: {\rm E_0})$

${\rm Exp} \to (\tt if \rm \; E_0 \; E_1 \; E_2)$

${\rm Exp} \to (\tt if \rm \; E_0 \; E_1)$

${\rm Exp} \to (\tt set! \rm \;\; I \;\; E)$

続きます

はじめに

形式意味論とは何なのか

便利なページの紹介

7.2. Formal semantics

, sequence formation

, th member of the sequence (1-based)

, length of sequence

, concatenation of sequences and

, drop the first members of sequence

, McCarthy conditional "if then else "

, substitution " with for "

in , injection of into domain

, projection of to domain

この章後それ以降

7.2.1. Abstract syntax

, constants, including quotations

, identifiers (variables)

, expressions

, commands

の定義

続きます

$\langle\,\ldots\,\rangle$ , sequence formation

$s \downarrow k$ , $k$ th member of the sequence $s$ (1-based)

$\#s$ , length of sequence $s$

$s \:\S\: t$ , concatenation of sequences $s$ and $t$

$s \dagger k$ , drop the first $k$ members of sequence $s$

$t \to a, b$ , McCarthy conditional "if $t$ then $a$ else $b$ "

$\rho[x/i]$ , substitution " $\rho$ with $x$ for $i$ "

$x$ in ${\tt D}$ , injection of $x$ into domain ${\tt D}$

$x\,\vert\,{\tt D}$ , projection of $x$ to domain $\tt D$

${\rm K} \in {\rm Con}$ , constants, including quotations

${\rm I} \in {\rm Ide}$ , identifiers (variables)

${\rm E} \in {\rm Exp}$ , expressions

${\rm \Gamma} \in {\rm Com} = {\rm Exp}$ , commands

$\rm Exp$ の定義