僕は次のような構文で指標〈signature〉を書いています。
signature Semigroup {
sort U
operation m: U×U → U
equation assoc :: (m × id_U);m ⇒ α_(U,U,U);(id_U × m);m
: (U×U)×U → U
}これは擬似コードで、明示的な構文定義や構文解析系〈パーザー〉があるわけではありません。が、ちゃんと構文を定義して、パーザーも作ろうかな、と思いました。
内容：
めんどくさいところ
指標の構文は単純なので、パーザーはすぐ作れそうに思えますが、ちょっとめんどうな事があります。指標全体の構文と、指標の一部に出現する式の構文が別なのです。指標全体（枠組み）の構文をホスト構文、一部に出現する式の構文をゲスト構文を呼ぶことにします。
冒頭の例で言うと、以下の◯◯の部分はゲスト構文で記述される場所です。
signature Semigroup {
sort ◯◯
operation m: ◯◯ → ◯◯
equation assoc :: ◯◯ ⇒ ◯◯
: ◯◯ → ◯◯
}ゲスト構文で書かれた式を列挙すると次のようです。
- U
- U×U
- (m × id_U);m
- α_(U,U,U);(id_U × m);m
- (U×U)×U
ホスト構文では、これらの式の構文は未定義です。
ゲスト構文が何であるかの情報は、次のように指定します。
habitat _ under CarCat
とりあえず、CarCat にだけ注目してもらって、これは「デカルト圏〈Cartesian category〉」を意味します。この指定から、ゲスト構文はデカルト圏の構文だと分かります。この情報をもとに、ホスト構文のバーザーは、ゲスト構文 CarCat のパーザーを呼び出して当該部分のパージング処理を委譲します。
しかし、ゲスト構文が何であるかはホスト構文のパージングが終わらないと分かりません。ホスト構文のパージングの前にレキシング〈字句解析 | トークン化〉が必要ですが、必要ならゲスト構文のレクサー〈字句解析系〉を呼び出す必要があります。そのレクサーはゲスト構文が何であるかを知らないと判断できません。
「箱を開ける鍵は箱の中」状態が生じます。
別な例
前節の“ホスト構文／ゲスト構文の問題”を解決しないといけないのですが、それは棚上げにして、別な指標記述の例を見てみます。
0-habitat V under RealLinComb
0-signature LinEquation within V {
sort x
sort y
equation eq : 2*x + y → 0
}これは1次方程式 2x + y = 0 を書いているだけです。
通常、指標と言えば1次元の圏のなかの対象、射、等式〈2-射〉を記述しますが、0次元の圏（つまり集合）のなかの要素、等式〈1-射〉を記述してもかまいません。上記の指標において：
- 0-signature は、0次元の指標であることを示す。
- 0-habitat V は、Vが0次元の圏〈集合〉であることを示す。
- RealLinComb は、実数係数の線形結合〈linear combination〉の構文が使えることを示す。
2*x + y や 0 という式は実数係数の線形結合であり、ゲスト構文である RealLinComb によって定義されています。もちろん、ホストパーザーは実数係数の線形結合のパージングは出来ないので、RealLinComb のパーザーを呼び出します。
事情
構文定義とパーザーをちゃんとしようと思った理由は二つあります。
一つ目の理由は、自分以外の人に指標記述を書いてもらうかも知れないからです。そのとき、明示的な構文がないとマズいだろう、と。また構文エラーのチェックが出来ないのもマズいだろう、と。
二つ目の理由は、指標の見た目をきれいにするにはTeXで書くのがいいのですが、これがめんどくさい。プレーンテキストで書いてTeXに変換できたら楽です。そのためには、いったんパーズツリー〈構文解析木〉を作って、そこから変換するのが定石です。つまり、パーザーが必要です。
と、思い立ったのですが、まとめて時間を取る気はないので、ボチボチとやります。
