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

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

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

指標と仕様

「指標〈signature〉」とほぼ同じ意味の言葉(同義語・類義語)が山のようにあってウンザリするなー、って話は何度かしたことがあります。僕としては、同義語・類義語を使い分けるのは面倒で嫌なので、「指標」だけで済ませたいです。が、「指標」と「仕様」を使い分けるかどうかは、ちょっと悩みます。

内容:

指標の例

最初に具体例を挙げましょう。毎度お馴染みのモノイドの指標です。この指標は集合圏Setで解釈されるとします。集合圏Setは、直積'×'をモノイド積とするモノイド圏とみなし、'I'はそのモノイド単位(同時に終対象)である単元集合です。

signature Monoid {
 sort A
 operation m: A×A→A
 operation i: I→A
 equation assoc:: (m×id_A);m ⇒ (id_A×m);m :A×A×A→A
 equation lunit:: (i×id_A);m ⇒ id_A :A→A
 equation runit:: (id_A)×i;m ⇒ id_A :A→A
}

等式的法則(equationの部分)に出てくる'⇒'は、'='に置き換えてしまってもかまいません。ただし、上の記述は多少不正確で、モノイド圏の結合律子/左単位律子/右単位律子をちゃんと書いてはいません。ここらへんのところは、次の記事とそこから参照されている他の記事を参照してください。

僕は、法則(結合法則、左単位法則、右単位法則)も含めて「モノイドの指標」と呼んでいます。しかし、法則を除いたものを指標と呼び、法則を入れると仕様〈specification〉と呼ぶ人もいます。

インスティチューションの理論などでは、法則が入ってない指標と、法則を入れた仕様を区別したほうが確かに分かりやすいです。なんでもかんでも指標で済ませると、区別したいときに困るような気がします。

多パート指標

トム・レンスター〈Tom Leinster〉は(例えば https://arxiv.org/abs/math/9810017 で)、指標をデータ・パートと公理パートに分けて書いています(書き方はインフォーマルですが*1)。モノイドの指標をパート分けして書き直すと:

signature Monoid {
 Data {
  sort A
  operation m: A×A→A
  operation i: I→A
 }
 Axioms {
  equation assoc:: (m×id_A);m ⇒ (id_A×m);m :A×A×A→A
  equation lunit:: (i×id_A);m ⇒ id_A :A→A
  equation runit:: (id_A)×i;m ⇒ id_A :A→A
 }
}

パートへの分け方やパートの名称などは色々あり得るでしょう。パートに分けないことは、パート分けの特別な場合といえます。

パート分けを持つような指標を多パート指標〈multipart signature〉と呼ぶことにすれば、“指標と仕様の区別”を多パート指標により再現できます。

方法 法則なし 法則あり
指標と仕様を区別する 指標 仕様
多パート指標を使う Axiomsパートを持たない指標 Axiomsパートを持つ指標

Axiomsパートを持たない指標とは、Axiomsパートが空な指標と言っても同じです。

signature Monoid {
 Data {
  sort A
  operation m: A×A→A
  operation i: I→A
 }
 Axioms {
 }
}

台集合と演算だけが定義されて、法則は記述されてません。

多パート指標は入れ子構造を持つ指標なので、もっと深い(二段以上の)入れ子を使ってもいいでしょう。あまり複雑にすると扱いにくくなりますが、指標のパート分け(入れ子構造)を使えば、記述のツールとしての柔軟性が増すでしょう。

[追記]「どのようにパート分けすべきか?」とか「それぞれのパートはどんな意味・意義があるのか?」とか考え出すと、なかなかに難しい問題ですね。指標類似物が山のようにあるのは、それだけ重要な概念だからでしょう。指標のパート分けの問題もたぶん重要なんだと思います。[/追記]

*1:[追記]書き方の構文定義を事前にしてないだけで、厳密な書き方だから、インフォーマルというのは違うな。文法を明示しないけどフォーマルな書き方? とかかな。[/追記]