前回（昨日）、長い記事「形式言語理論にも使える導出系」を書きました。いつものことで、熟考したわけではなくて勢いで書いています。読み返すと気になる点がすぐに見つかります（でも、もとの記事は修正しません）。この記事で、前回記事に対する反省と課題を述べます。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\twoto}{\Rightarrow }
\newcommand{\parto}{ \supset\!\to }
\newcommand{\In}{\text{ in }}
%\newcommand{\op}{\mathrm{op}}
%\newcommand{\id}{\mathrm{id}}
\newcommand{\u}[1]{\underline{#1}}
%\newcommand{\o}[1]{\overline{#1}}
\newcommand{\hyp}{ \text{－} }
\newcommand{\H}{ \text{-} }
\newcommand{\Iff}{ \Leftrightarrow }
\newcommand{\Imp}{ \Rightarrow }
\newcommand{\AS}{ \circledast }
%\newcommand{\SEArrow}{\style{display: inline-block; transform: rotate(45deg)} {\Rightarrow} }
\newcommand{\NEArrow}{\style{display: inline-block; transform: rotate(-45deg)} {\Rightarrow} }
%\newcommand{\Models}{ \mathrel{|\!\!\models} }
`$
内容：
導出系はすべてソート付き
「形式言語理論にも使える導出系 // 構文ソートとソート付き導出系」で以下のように書きました。
構文ソート達の集合が単元集合のとき、ソート無し導出系〈unsorted derivation system〉と呼びます。ソート無し導出系は、特別なソート付き導出系〈sorted derivation system〉です。
しかし、本文の記述では、ソート無し導出系を別扱いしています。これにより、記述・定義・説明が冗長になっています。ソート無し導出系を先に定義して、その拡張としてソート付き導出系という流れはダメですね。最初にソート付き導出系を定義して、その特殊ケースとしてソート無し導出系を導入すべきでした。
ソート無し導出系が $`(C_i)_{i\in I}`$ （構文コンストラクタ達のインデックス付き族）の形で、それに文法（構文ルール達のインデックス付き族） $`(R_j)_{j\in J}`$ を追加したので、インデキシング集合が $`I`$ と $`J`$ の2つになっています。$`i\in I`$ が構文コンストラクタのインデックス〈ラベル | 名前 | ID〉で、$`j\in J`$ が構文ルールのインデックス〈ラベル | 名前 | ID〉です。
インデキシング集合はひとつにまとめましょう。構文ルールのインデキシング集合 $`J`$ だけにします。文法（構文ルール達のインデックス付き族）$`R`$ に含まれる構文ルール $`R_j`$ は次のように書けます。
$`\quad R_j = (\sigma_{j, 0}, C_j, (\sigma_{j,1}, \cdots, \sigma_{j, n(j)}))`$
$`J\ni j\mapsto C_j`$ は、構文ルールのインデックス $`j`$ に構文コンストラクタを対応させます。$`n`$ はアリティ関数ですが、その定義は：
$`\text{For }j\in J\\
\quad n(j) := \mrm{arity}(C_j)
`$
特定の文法 $`R`$ には縛られない、すべての構文ルール達の集合（全体集合）は次のように書けます。
$`\quad S\times \mbf{SynConstr}\times \mrm{List}(S)`$
$`S`$ は構文ソート達の集合で、$`\mbf{SynConstr}`$ はすべての構文コンストラクタ達の集合です。構文コンストラクタについては「形式言語理論にも使える導出系 // 構文コンストラクタとソート無し導出系」を見てください。
文法 $`R`$ は関数〈写像〉で、$`J = \mrm{dom}(R)`$ として次の形になります。
$`\quad R : J \to S\times \mbf{SynConstr}\times \mrm{List}(S) \In \mbf{SET}`$
$`S`$ は小さい集合ですが、$`\mbf{SynConstr}`$ が大きい集合なので、外の集合圏は $`\mbf{SET}`$ になります。ただし、像集合 $`\mrm{img}(R)`$ は小さい集合です。
導出系といえば、それは常にソート無し導出系のことだとします。そうすれば、「ソート付き」という形容詞は不要になります。
導出系が特に「ソート無し」であるとは、構文ソート集合 $`S`$ が単元集合 $`\mbf{1} = \{0\}`$ （単元集合の唯一の要素 $`0`$ に特に意味はない）であり、構文ルールが次の形のときです。
$`\quad R_j = (0, C_j, (0, \cdots, 0) )`$
$`(0, \cdots, 0)`$ は、$`\mrm{arity}(C_j)`$ の個数（$`n(j)`$）だけ $`0`$ を並べたリストです。構文ルール $`R_j`$ は何の制限にもなりません。
構文ソート集合は固定しない
「形式言語理論にも使える導出系 // ソート付き導出系」では、ソート集合〈set of {syntactic}? sorts〉を固定して議論しています。これはダメです。導出系ごとのソート集合は異なってもかまわないし、異なるソート集合を持つ導出系達を同時に扱う必要があります。
したがって、導出系 $`A`$ の構成素としてソート集合を明示的に入れます。
$`\quad A = (S, R)\\
\text{where}\\
\quad S \in |\mbf{Set}|\\
\quad R: \mrm{dom}(R) \to S\times \mbf{SynConstr}\times \mrm{List}(S) \In \mbf{SET}
`$
$`A`$ の項集合関手〈termset functor〉は、「形式言語理論にも使える導出系」と同じ方法で定義できます。デフォルトが「ソート付き」なので、いちいち「ソート付き」は付けませんが、項集合はソート付きです。つまり、$`\mrm{Term}^\alpha(A)`$ はソート付き集合です。使うソート集合は $`A`$ に依存して変わります。
なお、「ソート集合〈set of {syntactic}? sorts〉」と「ソート付き集合〈sorted set〉」は似た語ですが、意味は全然違うので注意してください。ソート集合の実体は単なる集合ですが、ソート付き集合は関係（または非決定性関数）です。ソート付き集合の余域〈コドメイン〉の役割り名〈role name〉が「ソート集合」です。
語彙を文法から切り離す
形式言語理論では、「トークン」、「字句解析」、「語彙」などの言葉〈テクニカルターム〉が出てきます。例によって、用語法は人によりコミュニティにより違うので、広く合意された意味・用法はありません。翻訳語も、"token" が「字句」で、形容詞 "lexical" も「字句」だったりします。「語彙」は、"vocabulary" と "lexicon" があります。"lexicon" は「辞書」とも訳されます。
$`\quad \xymatrix{
\text{token} \ar@{-}[r]
&\text{字句}
\\
\text{lexical} \ar@{-}[ur]
&\text{語彙}
\\
\text{lexicon} \ar@{-}[r] \ar@{-}[ur]
&\text{辞書}
\\
\text{vocabulary} \ar@{-}[uur]
&\text{}
\\
\text{dictionary} \ar@{-}[uur]
&\text{}
}`$
ここでは、アリティが 0 の構文ルールを字句ルール〈lexical rule〉と呼びます。構文ルールのアリティ〈項数〉とは、構文ルールの構文コンストラクタのアリティのことです。
$`\text{For } r = (\sigma_0, C, \vec{\sigma}) \in S\times \mbf{SynConstr}\times \mrm{List}(S)\\
\quad \mrm{arity}(r) := \mrm{arity}(C)
`$
用語「アリティ〈項数〉」も関数名 '$`\mrm{arity}`$' もオーバーロードします。インデックスに対するアリティ関数 $`n`$ もあったので、異なる3つのモノに同じ呼び名をオーバーロードしています。
- $`\mrm{arity} : \mbf{SynConstr} \to \mbf{N}`$
- $`n : J \to \mbf{N}`$ （アリティ関数）
- $`\mrm{arity} : S\times \mbf{SynConstr}\times \mrm{List}(S) \to \mbf{N}`$
$`\quad \xymatrix{
J \ar[r]^-R \ar[d]_{n}
&{ S\times \mbf{SynConstr}\times \mrm{List}(S) } \ar[dl]|{\mrm{arity}}
\ar[d]^{\pi_2}
\\
\mbf{N}
&\mbf{SynConstr} \ar[l]^{\mrm{arity}}
}\\
\quad \text{commutative }\In \mbf{SET}
`$
構文ルールから、字句ルールだけを別に切り出して、$`(V_i)_{i\in I}`$ とします。それで、$`(R_j)_{j\in J}`$ は、字句ルールではないルール（アリティが 1 以上のルール）に対するインデックス付けだとします。
インデキシング集合（インデックス付き族の域）がまた2つになりますが、導出系は次のように書けます。
$`\quad A = (S, V, R) = (S, (V_i)_{i\in I}, (R_j)_{j\in J})`$
インデキシング集合の直和 $`I + J`$ 上に $`V, R`$ を載せれば、もとの単一の文法を再現できます。字句ルール（アリティ 0 のルール）をなんで切り離すのか？ と言うと、形式言語理論の扱いでは字句レベルと構文レベルを分けていることが多いからです。
字句ルール達のインデックス付き族 $`V`$ を（導出系 $`A`$ の）語彙〈vocabularuy〉と呼びます。$`R`$ のほうは引き続き文法〈grammar〉と呼びます。この呼び分けは、形式言語理論における「語彙と文法」の分類をだいたい反映していると思います。
ソート付き集合の圏は変わる
「形式言語理論にも使える導出系 // ソート付き集合達の圏」では、ソート集合〈set of sorts〉 $`S`$ を固定して、圏 $`S\H\mbf{SortSet}`$ を定義しました。ソート集合を固定しない方針にすると、これではダメです。
それと、"SortSet" という綴りは "set of sorts" か "sorted set" か分かりにくいので "SortedSet " とします。
ソート付き集合達の圏 $`\mbf{SortedSet}`$ を改めて定義します。定義の基盤には、「形式言語理論にも使える導出系 // ソート付き集合達の圏」同様に、関係達の2-圏 $`\mbf{Rel}\in |2\mbf{CAT}|`$ を使います。
ソート集合はソート付き集合の余域のことでしたが、余域を固定しないと、ソート付き集合とは任意の関係のことになります。しかし、全域ではない関係はどうやら出てこないので、ソート付き集合は全域に限ることにします。すると、ソート付き集合の定義は次のようになります。
- ソート付き集合〈sorted set〉とは、全域関係のことである。
- ソート付き集合の台集合〈underlying set〉とは、関係の域〈ドメイン〉のことである。
- ソート付き集合のソート集合〈set of sorts〉とは、関係の余域〈コドメイン〉のことである。
要するに、一般的概念に分野特有の呼び名を追加しているだけです。同じモノに新しいラベルを貼っているだけです。こういうラベルの追加・貼り直しをすることは矢鱈に多いですね。ラベルの追加・貼り直しをしても、内容は何の変化もないです。
「形式言語理論にも使える導出系 // ソート付き集合達の圏」の $`X = (\u{X}, \mrm{sort}_X)`$ という書き方は、ソート集合（関係の余域）を固定していたので、ソート集合も添えるなら $`X = (S, \u{X}, \mrm{sort}_X)`$ とかになります。この書き方は冗長です。
- $`S = \mrm{cod}(X)`$
- $`\u{X} = \mrm{dom}(X)`$
- $`\mrm{sort}_{X} = X`$
これまた、一般的概念に分野特有の書き方〈記法〉を追加しているだけです。書き方〈記法〉の追加・変更もまた矢鱈に多いのです。呼び名〈用語〉と書き方〈記法〉が、分野・コミュニティごとに分断されているのはもうしょうがないので諦めるしかないでしょう。無味無臭の一般論に還元すると虚しくなる、って事情もありますし。
さて、ソート集合〈set of sorts〉を固定しないソート付き集合〈sorted set〉のあいだの射ですが、これは2-圏 $`\mbf{Rel}`$ 内の図式で定義できます（「形式言語理論にも使える導出系 // ソート付き集合達の圏」と同様）。全域関係を表す矢印には $`\text{tot}`$ 、関数（全域かつ一意な関係）を表す矢印には $`\text{fun}`$ を付けることにします。
ソート付き集合 $`X`$ からソート付き集合 $`Y`$ への射 $`\varphi`$ は3つの構成素 $`\varphi_0, \varphi_1, \varphi_2`$ を持ちます。それは次の図式で表現できます。
$`\quad \xymatrix{
{\mrm{dom}(X)} \ar[d]|{\;\text{ tot}}_{X} \ar[r]|{\text{fun}}^{\varphi_0}
\ar@{.}[dr]|{\NEArrow \varphi_2}
&{\mrm{dom}(Y)} \ar[d]|{ \text{tot }\; }^{Y}
\\
{\mrm{cod}(X)} \ar[r]| {\text{tot} }_{\varphi_1}
&{\mrm{cod}(Y)}
}\\
\quad \In \mbf{Rel}
`$
$`\varphi_0`$ は台集合（関係の域）のあいだの関数（全域かつ一意な関係）、$`\varphi_1`$ はソート集合（関係の余域）のあいだの全域関係（関数である必要はない）、$`\varphi_2`$ は以下のような関係のあいだの包含関係です。
$`\quad \varphi_2 :: X;\varphi_2 \twoto \varphi_0;Y : \mrm{dom}(X) \to \mrm{cod}(Y)
\In \mbf{Rel}`$
ソート付き集合のあいだの射の結合は、2-圏の四角形〈クインテット〉の結合として定義できます。
$`\varphi_1`$ が単に全域関係だけでは扱いにくいかも知れません。$`\varphi_1`$ も関数にしたほうがいいような気もしますが、現時点ではハッキリ分かりません。
項集合関手の引数を増やす
導出系 $`A`$ の性質は、項集合関手 $`\mrm{Term}(A)`$ により調べることが基本的な手法です。しかし、導出系 $`A`$ の語彙が空（語彙のインデキシング集合が空集合）の場合、項集合関手 $`\mrm{Term}(A)`$ は何の情報も持ちません。項集合関手 $`\mrm{Term}(A)`$ により $`A`$ を調べることは出来ません。ダメですね。
語彙が空でないという条件を課しても良いことがありません。語彙（字句ルールのインデックス付き族）の定義を少し簡略化すると、語彙を単一のソート付き集合で表現できます。ソート付き集合としての語彙を、項集合関手の引数としてはどうでしょうか。項集合関手 $`\mrm{Term}(A)`$ は次のようになります。
$`\quad \mrm{Term}(A) : \mbf{SortedSet}\times \mbf{Odnl} \to \mbf{SortedSet}\In \mbf{CAT}`$
引数渡しの形式は単純に $`\mrm{Term}(A)(V, \alpha)`$ として、順序数変数 $`\alpha`$ に関して常に余極限を持つとすると、次の関手を定義できます。
$`\quad V\mapsto \mrm{colim}_\alpha \, \mrm{Term}(A)(V, \alpha) \in |\mbf{SortedSet}|`$
これは、帰納的定義のプロセスは考慮しないで結果だけ見ていることになります。ひょっとすると、帰納的定義のプロセスをブラックボックス化して、入力である初期集合（語彙相当）と出力である帰納極限だけに注目したほうが話が簡単になるかも知れません。
メタ導出系とは何なのか？
導出系の集まり（ドクトリン）を記述するためにメタレベルの導出系を使うことはよくあります。例えば、自然演繹の導出系達を形式的に扱うとき、シーケント計算風（あるいは型判断形式の）メタ導出系を使うでしょう。
よくやっていることだと思うのですが、どうもハッキリしません。メタ導出系の記述対象がオブジェクトレベルの導出系だとすると、導出系の意味論の話となり、完全に構文的な議論では無理かも知れません。いずれにしても、導出系達の振る舞いを導出系により記述する、とはどんなことか？ 何をやっているのか？ はハッキリさせたいですね。
他にも、「形式言語理論にも使える導出系 // そしてそれから」の箇条書きのなかに課題が含まれます。個別の導出系を見てるときは気付かなくても、導出系一般を相手にすると、全然ハッキリしてないことがイッパイあります。
