このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

指標記述のための構文

僕は次のような構文で指標〈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 :: ◯◯ ⇒ ◯◯
                  : ◯◯ → ◯◯
}

ゲスト構文で書かれた式を列挙すると次のようです。

  1. U
  2. U×U
  3. (m × id_U);m
  4. α_(U,U,U);(id_U × m);m
  5. (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に変換できたら楽です。そのためには、いったんパーズツリー〈構文解析木〉を作って、そこから変換するのが定石です。つまり、パーザーが必要です。

と、思い立ったのですが、まとめて時間を取る気はないので、ボチボチとやります。