形式言語理論にも使える導出系 - 檜山正幸のキマイラ飼育記 (はてなBlog)

演繹、推論、導出、証明などと呼ばれる行為を形式的に遂行する概念的システムは色々な場面で色々な呼び名で出てきます。ここでは、それらのシステムを総称して導出系〈derivation system | 導出システム〉と呼ぶことにします。

論理や型理論だけではなく、形式言語理論の構文的生成系もある程度は包摂する形で導出系を定義したいと思います。形式言語理論で使うためには、構文的対象物の種類を表す記号が必要です。そういった構文的種類の概念を含む導出系がこの記事の話題です。

ついでにこの機会に、“構文”に関して曖昧で気持ち悪いな－、と思っていた事柄を出来るだけクリアにするように試みました -- という事情で長い記事です。

[追記]
続きの記事「導出系：反省と課題」があります。続きの記事に訂正と補足を書いています。しかし、この記事は変更しないで、そのままです。
[/追記]$`\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{\thrto}{\Rrightarrow }
\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{\Models}{ \mathrel{|\!\!\models} }
`$

内容：

はじめに
概要と注意
構文ソートとソート付き導出系
構文コンストラクタとソート無し導出系
ソート無し導出系の項集合
ソート無し導出系の記述の簡略化
ソート無し導出系達の圏
ソート付き導出系
注意事項：項と項集合
ソート付き集合達の圏
ソート付き導出系の項集合
ソート付き導出系達の圏
導出可能性
圏類似代数系-導出系の相対随伴
そしてそれから

続きの記事：

導出系：反省と課題

※色付きテキストは次の約束で使います。

青い文字：重要な概念・用語だがこの記事内では定義・説明してないもの。
赤い文字：この記事内で導入・定義した概念・用語。過去の定義の再掲・繰り返しのときもある。
マゼンタの文字：この記事内の後方で定義されるか参照〈リンク〉される概念・用語。

はじめに

論理や型理論に出てくる形式体系には幾つもの呼び名があります。正規表現パターンで書けば：

{演繹 | 推論 | 導出 | 証明}{系 | システム}

他に、形式言語理論でも形式言語を生成〈produce | generate〉するシステムが出てきます。また項書き換え系〈term rewriting system〉なんてのもあります。似たり寄ったりの概念装置に対して、呼び名や記法が矢鱈に増殖して実に鬱陶しい。なるべくまとめて議論したいと思います。

過去に、{演繹 | 導出}{系 | システム} という呼び名でこの話題を扱ったことがあります。

また、演繹系と帰納構造との関係は最近の記事で扱っています。

帰納構造と帰納原理 // 演繹系から作る帰納構造

上記記事の最後「「考え直したほうがいい点」」に次のように書きました。

帰納構造の台集合は大きな集合も許すべきだろう。なんなら台集合を宇宙にとってもいい。

帰納構造を、集合論または型理論の宇宙ともっと密接に関係付けるべきだろう。

帰納構造のベース集合 $`X_0`$ を、構文的コンストラクタの集合として定義してはどうか？

帰納構造の定義をもっと代数的にスッキリさせたい。

これらのことを考慮して考え直してみると、帰納構造を持つ導出系とは、具体的な表示〈presentation〉により定義される関手と考えるのが良さそうだ、と思い至りました。具体的な表示となる構造を導出系、導出系により定義される関手を項集合関手と呼ぶことにします。

概要と注意

導出系にとって何が大事かというと、導出系により生成される構文的対象物達の集合です。構文的対象物の呼び名は色々あります； 語〈word〉、記号〈symbol〉、文〈sentence〉、項〈term〉、式〈expression〉など。分野によっても呼び名が変わります。論理なら論理式〈formula〉、型理論なら判断〈judgement〉など。ここでは、諸々の構文的対象物を総称して項〈term〉と呼びます。一般論における「項」は、各分野・各場合の具体例ごとに違う呼び名で呼ばれるでしょう。

導出系 $`A`$ によって定義される項達の集合を $`\mrm{Term}(A)`$ と書きます（すぐ後でもっと精密に定義します）。項の集合は、帰納的に構成されます。帰納的構成は順序数に沿って実行されます。よって、順序数達の圏 $`\mbf{Odnl}`$ が重要です。$`\mbf{Odnl}`$ については、「再帰的構成のために：順序数の圏」「順序数と集合圏」を参照してください。

導出系 $`A`$ の項達の集合 $`\mrm{Term}(A)`$ は、実際は、順序数に沿った集合の増大列です。

$`\quad \mrm{Term}^0(A)\subseteq \mrm{Term}^1(A) \subseteq \mrm{Term}^2(A)\subseteq \cdots`$

$`\alpha \le \beta`$ である2つの順序数に対して、集合のあいだの包含写像（恒等写像もあり）を次のように書きます。

$`\quad \mrm{Term}^{\alpha\le\beta}(A) : \mrm{Term}^{\alpha}(A)\hookrightarrow \mrm{Term}^{\beta}(A) \In \mbf{Set}`$

右肩の順序数引数に注目すると、$`\mrm{Term}^\hyp(A)`$ は次のような関手になります。

$`\quad \mrm{Term}^\hyp(A) : \mbf{Odnl} \to \mbf{Set} \In \mbf{CAT}`$

関手とみなした $`\mrm{Term}(A)`$ が、導出系 $`A`$ が定義する項集合関手です。導出系は、項集合関手を定義するための装置〈defining device〉という位置付けです。

関手 $`\mrm{Term}(A)`$ は、大きい圏 $`\mbf{Odnl}`$ から大きい圏 $`\mbf{Set}`$ への関手ですが、小さい集合として余極限〈帰納極限〉が決まることがあります。関手 $`\mrm{Term}(A)`$ の余極限を $`\mrm{Term}^\infty(A)`$ と書くことにします。ここでの $`\infty`$ は、特定の順序数ではなくて、余極限を表す単なる符丁です。

ここから先、次のように約束します。

$`\mrm{Term}(A)`$ または $`\mrm{Term}^\hyp(A)`$ は、集合ではなくて、関手を表す。
$`\mrm{Term}^\alpha(A)`$ は、集合を表す。関手の値。
$`\mrm{Term}^\infty(A)`$ は、関手 $`\mrm{Term}(A)`$ の余極限である集合を表す。$`\infty`$ は特定の順序数ではない。

構文ソートとソート付き導出系

構文的対象物の種類（例えば単語の品詞）を、言語学では構文範疇〈syntactic category | grammatical category〉と呼びます。日本語（翻訳語）「範疇」と「圏」は別ですが、もとはどちらも category です。このコンフリクトは嫌*1なので、構文範疇の代わりに構文ソート〈syntactic sort〉を使います。「ソート〈sort〉」も色々なところで色々な意味で使われていて、オーバーロード／コンフリクトしまくり*2ですが、「カテゴリー」よりはマシかと。

前節で述べた項の集合 $`\mrm{Term}^\alpha(A)`$ や $`\mrm{Term}^\infty(A)`$ は単なる集合で、構文ソートによる分類はされていません。構文ソート集合〈set of syntactic sorts〉を $`S`$ として、項集合〈termset〉が $`S`$ の要素（構文ソート）で分類されている状況を考えましょう。そのとき、項集合 $`\mrm{Term}^\alpha(A)`$ は、各 $`\sigma\in S`$ に対する部分集合 $`\mrm{Term}^\alpha_\sigma(A)`$ に分けられます。次の点には注意してください。

とある $`\sigma \in S`$ に対して $`\mrm{Term}^\alpha_\sigma(A) = \emptyset`$ かも知れない。
$`\sigma, \tau \in S, \; \sigma\ne \tau`$ であっても $`\mrm{Term}^\alpha_\sigma(A) \cap \mrm{Term}^\alpha_\tau(A) \ne \emptyset`$ かも知れない。
$`\bigcup_{\sigma \in S}\mrm{Term}^\alpha_\sigma(A) \ne \mrm{Term}^\alpha(A)`$ かも知れない。

上記1番は特に問題にはなりません。2番の状況は不便です。ある項 $`t\in \mrm{Term}^\alpha`$ に対して、構文ソート（項の構文的種類）が一意には決まらないのですから。とはいえ、自然言語（日本語とか英語とか）の文法では実際に2番の状況は起こります。単語だけ見て品詞を一意に決めるのは無理です。3番は、構文ソートを持たない項があるかも知れないということです。これも嬉しくありません。

項集合 $`\mrm{Term}^\alpha(A)`$ に構文ソートを割り当てる対応を $`\mrm{sort}^\alpha`$ とすると、一般には、$`\mrm{sort}^\alpha`$ は非決定性関数です。

$`\quad \mrm{sort}^\alpha : \mrm{Term}^\alpha(A) \to \mrm{Pow}(S) \In \mbf{Set}`$

非決定性関数 $`\mrm{sort}^\alpha`$ が部分関数になるとき、ソート付けは一意だ〈unique sorting〉といいます。非決定性関数 $`\mrm{sort}^\alpha`$ の値が空集合にならないとき ソート付けは全域だ〈total sorting〉といいます。ソート付けが一意かつ全域なら、$`\mrm{sort}^\alpha`$ は通常の関数になります。

話を簡単にするためには、ソート付けが一意かつ全域の場合を考えます。ですが、導出系の作り方によりソート付けが関数にならないときもあります。ソート付けが関数になる条件を吟味する必要があります。

ここで考える導出系はソート付けのメカニズムを持ちますが、構文ソート達の集合が単元集合のとき、ソート無し導出系〈unsorted derivation system〉と呼びます。ソート無し導出系は、特別なソート付き導出系〈sorted derivation system〉です*3。

構文コンストラクタとソート無し導出系

導出系の台集合〈underlying set〉を小さい集合に特定しないで、現在のワーキング宇宙を台集合にします。現在の（デフォルトの）グロタンディーク宇宙 を $`\mbf{U}`$ とします。グロタンディーク宇宙については以下の過去記事達を参照してください。

構文コンストラクタ〈syntactic constructor〉 $`C`$ は、現在のグロタンディーク宇宙の直積上で定義された部分関数です。

$`\quad C : \mbf{U}^n \parto \mbf{U} \In \mbf{SET}`$

ここで、$`\mbf{SET}`$ は現在の（デフォルトの）集合圏より1レベル上の集合圏です。記号 '$`\parto`$' については「帰納構造と帰納原理 // 部分関数」を見てください。なお、「帰納構造と帰納原理」では「構文的コンストラクタ」と呼んでましたが、「的」は取りました。

構文コンストラクタには、定義域 $`\mrm{def}(C)`$ が空ではないという条件だけを付けます。これから、像 $`\mrm{img}(C)`$ も空でないことが出ます（一般の像集合は空になり得ます）。構文コンストラクタ $`C`$ のアリティ〈項数〉は、$`\mrm{arity}(C)`$ と書くことにします。次が成立します。

$`\quad \mrm{arity}(C) = n \Iff \mrm{def}(C) \subseteq \mbf{U}^n`$

アリティが 0 である構文コンストラクタは、単元集合からの部分関数になります。しかし、定義域が空は許されないので、結局、$`\mbf{U}`$ の要素を一個指し示すポインティング関数になります。$`a`$ を指すポインティング関数とは次の関数です。

$`\quad \mbf{1}\ni 0 \mapsto a \in \mbf{U}`$

構文コンストラクタは、グロタンディーク宇宙のなかで集合論的に構成できる部分関数なら何でもいいです。次のような全域関数も構文コンストラクタです。

$`\quad \mbf{U}\ni x \mapsto x\cup \{x\} \in \mbf{U}`$
$`\quad \mbf{U}\times \mbf{U}\ni (x, y) \mapsto x \times y \in \mbf{U}`$
$`\quad \mbf{U}\ni x \mapsto \{\emptyset\}\times x \in \mbf{U}`$

「構文〈syntactic〉」という形容詞に特に意味はありません。単にそう呼ぶというだけです。「構文を議論している文脈で使いたい」というお気持ちは含まれます。

[追記]
ここからソート無し導出系の説明です。後で気付いたことですが、ソート無し導出系をソート付き導出系より前に導入するのは良くない選択でした。論理的に間違っているわけではないですが、説明が冗長になります。「導出系：反省と課題 // 導出系はすべてソート付き」参照。
[/追記]

適当なインデキシング集合でインデックス付けられた構文コンストラクタの族をソート無し導出系〈unsorted derivation system〉と呼ぶことにします。ソート無し導出系はソート付き導出系（後述）の下部構造になります。ソート無し導出系も特別なソート付き導出系なのですが、ここでは構文ソートのことは考えません（考える必要がありません）。

ソート無し導出系は次のように書けます。

$`\quad (I, n, (C_i)_{i\in I})`$

ここで：

$`I`$ はインデキシング集合、$`I = \emptyset`$ も許す。
$`n : I \to \mbf{N}`$ はアリティ関数
$`(C_i)_{i\in I}`$ は構文コンストラクタの族、$`\mrm{arity}(C_i) = n(i)`$

次の単射性は仮定しません。

$`\quad \forall i, j\in I.\, i\ne j \Imp C_i \ne C_j`$

異なるインデックスに同じ構文コンストラクタを割り当てると、曖昧性の記述に使えます。曖昧性は好ましいものではありませんけどね。

ソート無し導出系には記号の乱用は使わずに、ソート無し導出系 $`A`$ の構成素の右肩に $`A`$ を付けます。

$`\quad A = (I^A, n^A, (C^A_i)_{i\in I^A})`$

混乱の心配が無ければ右肩の $`A`$ は省略します。

ソート無し導出系の項集合

$`A = (I, n, (C_i)_{i\in I})`$ をソート無し導出系とします。ソート無し導出系に備わる構文コンストラクタ達を繰り返し適用して得られる要素を $`A`$ の項〈term〉と呼びます。以下に、項達の集合を帰納的に定義します。

まず、任意の集合を引数とする関数 $`F^A`$ を定義します。以下に出てくる記号は「帰納構造と帰納原理 // 部分関数」を見てください。

$`\text{For }X \in \mbf{U}\\
\quad F^A(X) :=
\bigcup_{i\in I}{C_i}_*(X^{n(i)})
`$

ここで、$`X^{n(i)}`$ は、集合 $`X`$ の $`n(i)`$ 個分の直積です。$`n(i) = 0`$ のとき $`X^{n(i)} = X^0`$ は単元集合 $`\mbf{1}`$ だと約束します。これは $`X = \emptyset`$ でも例外ではなく $`\emptyset^0 = \mbf{1}`$ です。

構文コンストラクタ $`C_i`$ は部分関数でも、$`F^A`$ は大きな全域関数*4になります。

$`\quad F^A : \mbf{U} \to \mbf{U} \In \mbf{SET}`$

順序数 $`\xi\in |\mbf{Odnl}|`$ に対して、集合 $`\mrm{Term}^\xi(A)`$ を次のように定義します。

$`\xi = 0`$ のとき： $`\mrm{Term}^\xi(A) = \mrm{Term}^0(A) := \emptyset`$
$`\xi = \chi + 1`$ のとき： $`\mrm{Term}^\xi(A) := \mrm{Term}^\chi(A) \cup F^A(\mrm{Term}^\chi(A) )`$
$`\xi`$ が極限順序数のとき： $`\mrm{Term}^\xi(A) := \bigcup_{\chi \in \xi} \mrm{Term}^\chi(A)`$

この作り方から次は言えます。

$`\text{For }\alpha, \beta\in |\mbf{Odnl}|\\
\quad \alpha \le \beta \Imp \mrm{Term}^\alpha(A) \subseteq \mrm{Term}^\beta(A)
`$

前述のように、写像 $`\mrm{Term}^{\alpha\le\beta}(A)`$ は包含写像だとします。$`\mrm{Term}^\hyp(A)`$ は次のような関手になります。

$`\quad \mrm{Term}^\hyp(A) : \mbf{Odnl} \to \mbf{Set} \In \mbf{CAT}`$

この関手が（$`A`$ の）項集合関手〈termset functor〉です。

項集合関手に余極限〈帰納極限〉が在れば、それを $`\mrm{Term}^\infty(A)`$ と書きます。

$`\quad \mrm{Term}^\infty(A) := \mrm{colim}\, \mrm{Term}^\hyp(A)`$

項集合関手 $`\mrm{Term}(A)`$ が（小さい集合としての）余極限を持つとき、ソート無し導出系 $`A`$ は収束する〈convergent〉といいます。実際に使う導出系は収束するものです。しかし、収束しない導出系も除外する必要はないでしょう。

ソート無し導出系の記述の簡略化

ソート無し導出系 $`A`$ を次の形に書くように変更します。

$`\quad A = (I^A, A)`$

これは、記号の乱用ではなくて、むしろ冗長な表現です。

ソート無し導出系は、インデキシング集合 $`I^A`$ 上で定義された、値が構文コンストラクタである関数です。現在のグロタンディーク宇宙におけるすべての構文コンストラクタ達の集合を $`\mbf{SynConstr}`$ とすると、ソート無し導出系 $`A`$ は次のように書けます。

$`\quad A : I^A \to \mbf{SynConstr} \In \mbf{SET}`$

$`I^A`$ は $`\mrm{dom}(A)`$ と同じです。よって、$`A = (\mrm{dom}(A), A)`$ は冗長な書き方になってます。アリティ関数 $`n^A`$ は次のように定義できます。

$`\quad \xymatrix{
I^A \ar[r]^-{A} \ar[dr]_{n^A}
& \mbf{SynConstr} \ar[d]^{\mrm{arity}}
\\
{}
& \mbf{N}
}\\
\quad \text{commutative }\In \mbf{SET}
`$

$`n^A`$ の定義をテキストで書けば：

$`\quad n^A := A;\mrm{arity}\; : I^A \to \mbf{N} \In \mbf{SET}`$

$`n^A`$ は $`\In \mbf{Set}`$ になりますが、$`\In \mbf{SET}`$ と書いてマズイわけではありません。

前節で、$`(C^A_i)_{i \in I^A}`$ と書いていた構文コンストラクタ達の族は $`A`$ そのものです。結局、ソート無し導出系とは、小さい集合 $`I^A = \mrm{dom}(A)`$ 上で定義された構文コンストラクタ達の集合 $`\mbf{SynConstr}`$ に値を持つ関数 $`A`$ です。$`n^A`$ は後から定義できます。

すべてのソート無し導出系達の集合は、大きな集合達のシグマ型構成を用いて次のように書けます。

$`\quad \sum_{X\in |\mbf{Set}|}\mrm{MAP}(X, \mbf{SynConstr})`$

ホムセット $`\mbf{SET}(\hyp, \hyp)`$ を $`\mrm{MAP}(\hyp, \hyp)`$ と書いています。（$`\mbf{Set}(\hyp, \hyp)`$ は $`\mrm{Map}(\hyp, \hyp)`$ です。）

ソート無し導出系達の圏

ソート無し導出系達の圏〈category of unsorted derivation systems〉を定義します。その圏を $`\mbf{UnsDerSys}`$ とします。対象はソート無し導出系なので、前節最後の式を使って次のように書けます。

$`\quad |\mbf{UnsDerSys}| := \sum_{X\in |\mbf{Set}|}\mrm{MAP}(X, \mbf{SynConstr})\In \mbf{SET}`$

ソート無し導出系のあいだの射は、ソート無し導出系そのものをゴニョゴニョしないで、対応する項集合関手を使って定義します。

$`\text{For }A, B\in |\mbf{UnsDerSys}|\\
\quad \mbf{UnsDerSys}(A, B) := [\mbf{Odnl}, \mbf{Set}](\mrm{Term}(A), \mrm{Term}(B))
`$

$`[\mbf{Odnl}, \mbf{Set}]`$ は大きい圏のあいだの関手圏です。ソート無し導出系のあいだの射〈morphism between unsorted derivation systems〉は、対応する項集合関手のあいだの自然変換です。次の3つの命題は同じことです。

$`\varphi : A \to B \In \mbf{UnsDerSys}`$
$`\varphi : \mrm{Term}(A) \to \mrm{Term}(B) \In [\mbf{Odnl}, \mbf{Set}]`$
$`\varphi :: \mrm{Term}(A) \twoto \mrm{Term}(B) : \mbf{Odnl} \to \mbf{Set} \In \mbf{CAT}`$

$`\varphi`$ は自然変換なので、次のような成分を持ちます。

$`\text{For }\alpha \in |\mbf{Odnl}|\\
\quad \quad \varphi_\alpha : \mrm{Term}^\alpha(A) \to \mrm{Term}^\alpha(B) \In \mbf{Set}
`$

自然変換の自然性図式は以下のようです。

$`\text{For }(\alpha\le \beta) \In \mbf{Odnl}\\
\quad \xymatrix{
{\mrm{Term}^\alpha(A)} \ar[r]^{\varphi_\alpha} \ar[d]_{\mrm{Term}^{\alpha\le\beta}(A)}
&{\mrm{Term}^\alpha(B)} \ar[d]^{\mrm{Term}^{\alpha\le\beta}(B)}
\\
{\mrm{Term}^\beta(A)} \ar[r]^{\varphi_\beta}
&{\mrm{Term}^\beta(B)}
}\\
\quad \text{commutative }\In \mbf{Set}
`$

ソート無し導出系のあいだの射は、まったく具体性がなく超越的に定義されます。なにか具体的に射を構成した場合は、それが項集合関手のあいだの自然変換になるかどうかをチェックします。

ソート付き導出系

集合 $`S`$ を固定して、$`S`$ を構文ソート達の集合とするソート付き導出系を定義します。$`S`$ を構文ソート集合〈set of syntactic sorts〉と呼びますが、$`S`$ には何の条件も付けません（任意の集合）。ソート付き導出系は、下部構造にソート無し導出系を持ち、それに加えて構文ルール達のインデックス付き族を持ちます。

$`S`$-ソート付き導出系〈$`S`$-sorted derivation system〉は次のように書けます。

$`\quad (I, (C_i)_{i\in I}, J, (R_j)_{j\in J})`$

ここで：

$`(I, (C_i)_{i\in I})`$ はソート無し導出系
$`J`$ は集合、特に条件はなく空集合でもよい。
$`(R_j)_{j\in J}`$ は、$`J`$ をインデキシング集合とする、構文ルールのインデキシング付き族

構文ルールの集合は、ソートの集合 $`S`$ と、ソート無し導出系 $`(I, (C_i)_{i\in I})`$ に対して決まります。構文ルール達の集合〈set of {all}? {syntax | syntactic} rules〉を $`\mrm{SynRule}_S(I, (C_i)_{i\in I})`$ とします。実際には、$`(C_i)_{i\in I}`$ の情報が必要なわけではなくて、アリティ関数 $`n : I\to \mbf{N}`$ があれば構文ルールの集合を定義できます*5。

$`\quad \mrm{SynRule}_S(I, (C_i)_{i\in I}) := \\
\qquad \{(\sigma_0, i, \vec{\sigma})\in S\times I\times \mrm{List}(S) \mid \mrm{length}(\vec{\sigma}) = n(i) \}
`$

$`\mrm{SynRule}_S(I, (C_i)_{i\in I})`$ の要素が構文ルール〈{syntax | syntactic} rule〉です。構文ルールは3つ組〈長さ 3 のリスト〉 $`(\sigma_0, i, \vec{\sigma})`$ ですが、内側のリスト $`\vec{\sigma}`$ を展開して次の形に書きます。

$`\quad (\sigma_0, i, \sigma_1, \cdots, \sigma_{n(i)})`$

形式言語理論では、構文ルールを生成ルール〈生成規則 | production rule〉とも呼びます。

構文ルールは色々な書き方・描き方をします。例えば、BNF〈Backus–Naur form〉風に書けば：

$`\quad \sigma_0 ::= i(\sigma_1, \cdots, \sigma_{n(i)})`$

左右を反転させた書き方は：

$`\quad (\sigma_1, \cdots, \sigma_{n(i)})i =:: \sigma_0`$

ノードを1つだけ持つツリー（開いたエッジがあるので正確には半ツリー〈semitree〉）で描けば：

$`\quad \xymatrix{
{} \ar@{-}[dr]|{\sigma_1}
&{\cdots} \ar@{}[d]|{\cdots}
&{} \ar@{-}[dl]|{\sigma_{n(i)}}
\\
{}
&*+[o][F]{i} \ar@{-}[d]|{\sigma_0}
&{}
\\
{}
&{}
&{}
}`$

上下を反転させた描き方は：

$`\quad \xymatrix{
{}
&{}\ar@{-}[d]|{\sigma_0}
&{}
\\
{}
&*+[o][F]{i} \ar@{}[d]|{\cdots}
\ar@{-}[dl]|{\sigma_1} \ar@{-}[dr]|{\sigma_{n(i)}}
&{}
\\
{}
&{\cdots}
&{}
}`$

論理の推論図風に書けば：

$`\quad \begin{array}{ccc}
\sigma_1 & \cdots & \sigma_{n(i)} \\
\hline
{} & \sigma_0 & {}
\end{array}i
`$

構文ルールをどのように書くか／描くかはどうでもいい話です。好きな書き方／描き方を使えばいいのです。

構文ルールのインデックス付き族 $`R`$ は、次のような関数です。

$`\quad R : J \to \mrm{SynRule}_S(I, (C_i)_{i\in I})`$

$`j\in J`$ に対する $`R`$ の値 $`R_j`$ は次のように書けます。

$`\quad R_j = (\sigma_{j, 0}, i_j, \sigma_{j, 1}, \cdots, \sigma_{j, n(i_j)})`$

推論図風に書けば：

$`\quad R_j = \begin{array}{ccc}
\sigma_{j,1} & \cdots & \sigma_{j, n(i_j)} \\
\hline
{} & \sigma_{j, 0} & {}
\end{array}i_j
`$

より現実に近い*6レイアウトは：

$`\quad \begin{array}{ccc}
\sigma_{j,1} & \cdots & \sigma_{j, n(i_j)} \\
\hline
{} & i_j\:\sigma_{j, 0} & {}
\end{array}j
`$

$`j`$ は構文ルールのインデックス〈ラベル | 名前 | ID〉で、$`i_j`$ は構文コンストラクタのインデックス〈ラベル | 名前 | ID | 記号〉です。構文ソート、構文コンストラクタのインデックス、構文ルールのインデックスは混同されがちで、意図的に混同（同一視）していることもママあります。一旦は完全に区別してから適宜同一視するのが吉です。

関数（インデックス付き族）$`R`$ を文法〈grammar〉と呼びます。$`S`$-ソート付き導出系は、$`S`$ を構文ソート集合とする文法を備えた導出系です。文法が存在すると、項集合関手の構成法が変わります。

注意事項：項と項集合

ここで注意事項を挟みます。

ZFC集合論に基づくグロタンディーク宇宙 $`\mbf{U}`$ は、構文的観点からはノッペラボーな集合です。グロタンディーク宇宙 $`\mbf{U}`$ の要素が項か項集合（項達の集合）か？という議論はまったく無意味です。単に、$`\mbf{U}`$ の要素だという以外の特性は持ちませんから。しかし、構文コンストラクタ $`C`$ を利用する場面においては項と項集合の区別が出来ます。

順序数 $`\alpha`$ に対する集合 $`\mrm{Term}^\alpha(A)`$ を作るときに使う構文コンストラクタ $`C`$ への入力は項、または項のタプルです。構文コンストラクタの出力も項です。一方で、構文コンストラクタ $`C`$ の像写像 $`C_*(\hyp) = \mrm{img}(C, \hyp)`$ への入力は項集合、または項のタプルの集合です。像写像の出力は項集合です。

構文コンストラクタそれ自体の定義には、入力が項か項集合かの区別はありません（無意味）ですが、構文コンストラクタの利用場面では常に長さ $`n`$ （$`n = 0, 1`$ もあり）の項のタプルを入力として、ひとつの項を返します。

構文コンストラクタの像写像のように、利用する場面において項集合を入出力とする関数は、（使い方において）項集合コンストラクタ〈termset constructor〉と呼ぶことにします。構文コンストラクタ（項コンストラクタ）と項集合コンストラクタの区別はあくまで利用場面においてです。関数だけ見ての区別は出来ません。

ソート付き集合達の圏

ソート無し導出系は、順序数の圏から集合圏への関手（項集合関手）の生成系として定義しました。同様にソート付き導出系も、順序数の圏から“とある圏”への関手の生成系として定義します。となると、“とある圏”の定義が必要です。“とある圏”とは、ソート付き集合達の圏です。

ソート集合〈構文ソート達の集合 | set of {syntactic}? sorts〉 $`S`$ に対する$`S`$-ソート付き集合〈$`S`$-sorted set〉は以下のように書けます。

$`\quad X = (\u{X}, \mrm{sort}_X)`$

ここで：

$`\u{X}`$ は、$`X`$ の台集合〈underlying set〉
$`\mrm{sort}_{X}`$ は、$`X`$ のソート付け〈sorting〉

ソート付けは非決定性関数ですが、非決定性関数と関係は同じことなので、ときに関係とみなしてソート付け関係〈sorting relation〉とも呼びます。

$`S`$-ソート付き集合達の圏を定義するには、2-圏としての関係圏 $`\mbf{Rel}`$ を使うと話が早いです。2-圏 $`\mbf{Rel}`$ とは：

対象は、集合
射は、集合のあいだの（二項）関係
2-射は、関係のあいだの包含関係

ホム圏 $`\mbf{Rel}(A, B)`$ は順序集合なので、やせた圏になります。通常の記法により、関係（1-射）と包含（2-射）は次のように書きます。

$`\quad R:A\to B \In \mbf{Rel}\\
\quad \alpha :: R\twoto R' : A \to B \In \mbf{Rel}
`$

$`S`$-ソート付き集合は、$`\mbf{Rel}`$ のなかで次のような射です。

$`\quad \mrm{sort}_X : \u{X} \to S \In \mbf{Rel}`$

$`S`$-ソート付き集合達の圏〈category of $`S`$-sorted sets〉を $`S\H\mbf{SortSet}`$ とすると次は同値です。

$`(\u{X}, \mrm{sort}_X) \in |S\H\mbf{SortSet}|`$
$`\mrm{sort}_X : \u{X} \to S \In \mbf{Rel}`$

2つの$`S`$-ソート付き集合 $`(\u{X}, \mrm{sort}_X),(\u{Y}, \mrm{sort}_Y)`$ のあいだの射〈morphism | homomorphism〉は、2-圏 $`\mbf{Rel}`$ 内の以下の図式で定義されます（すぐ下に説明あり）。

$`\quad \xymatrix@C+2pc@R+2pc{
S \ar@{=}[r]
&S
\\
\u{X} \ar[r]_{{\u{f}}_*} \ar[u]^{\mrm{sort}_X} \ar[ur]|{g}
\ar@{.}@/^1.5pc/[ur]|{\SEArrow f^\#}
\ar@{.}@/_1.5pc/[ur]|{=}
&\u{Y} \ar[u]_{\mrm{sort}_Y}
}\\
\quad \In \mbf{Rel}
`$

点線は2-射の域側と余域側を分ける仕切り線です。詳しくは「n角形の対角線とペースティング図」参照。
射は $`\u{f}:\u{X}\to \u{Y}\In \mbf{Set}`$ と上図の $`f^\#`$ のペア $`(\u{f}, f^\#)`$ 。
$`{\u{f}}_*`$ は、関数〈写像〉 $`\u{f}`$ を関係とみなしたもの。
右下三角形内の $`=`$ は、三角形が厳密に可換であること。
左上三角形内の $`f^\#`$ は、$`\mbf{Rel}`$ の2-射。

右下三角形と左上三角形をテキストで書けば：

$`\quad {\u{f}}_* ; \mrm{sort}_Y = g \In \mbf{Rel}`$
$`\quad f^\# :: \mrm{sort}_X \twoto g : \u{X} \to S \In \mbf{Rel}`$

二番目は（一番目を使って）次の包含関係です。

$`\quad \mrm{sort}_X \subseteq \u{f}_* ; \mrm{sort}_Y \In \mrm{Pow}(\u{X} \times S)`$

対象の定義と射の定義から、圏 $`S\H\mbf{SortSet}`$ を構成するにはまだ作業が残っていますが、それは練習問題とします。

ソート付き集合 $`X \in |S\H\mbf{SortSet}|`$ と構文ソート $`\sigma \in S`$ に対して、集合 $`X_\sigma`$ を次のように定義します。

$`\quad X_\sigma := \{
x \in \u{X} \mid (x, \sigma) \in \mrm{sort}_X
\}
`$

上の定義では、$`\mrm{sort}_X`$ を関係とみなしています。

関係としての $`\mrm{sort}_X`$ の要素であるペア $`(x, \sigma)`$ を $`x \AS \sigma`$ とも書きます。$`x \AS\sigma`$ は、「構文ソートが $`\sigma`$ である項 $`x`$」という意味です。

集合（ソート付き集合ではない）$`U`$ と構文ソート $`\sigma \in S`$ に対して、$`U\AS \sigma`$ を次のように定義します。

$`\quad U\AS \sigma := U \times \{\sigma\} \subseteq U\times S`$

$`U\AS \sigma`$ は、台集合が $`U`$ である$`S`$-ソート付き集合になります。すべての要素の構文ソートが $`\sigma`$ になります。この形のソート付き集合を自明ソート付き集合〈trivial sorted set〉と呼ぶことにします。自明ソート付き集合はつまらないものではなくて重要です。

$`S`$-ソート付き集合 $`X`$ のソート付け関係 $`\mrm{sort}_X`$ が（関係あるいは非決定性関数として）一意／全域のとき、$`X`$ は一意〈unique〉／全域〈total〉といいます。

圏 $`S\H\mbf{SortSet}`$ のなかで、一意／全域な対象達から生成される充満部分圏を以下のように書きます。

$`\quad S\H\mbf{SortSet}_{\mrm{uniq}}`$
$`\quad S\H\mbf{SortSet}_{\mrm{tot}}`$

一意かつ全域な対象達から生成される充満部分圏は：

$`\quad S\H\mbf{SortSet}_{\mrm{uniq, tot}}`$

この節の最後に、2つの$`S`$-ソート付き集合 $`X, Y`$ の合併〈union〉を定義します。$`S`$-ソート付き集合も、集合の合併の記号をオーバーロードして $`X\cup Y`$ と書きます。合併は、$`S\H\mbf{SortSet}_{\mrm{uniq}}`$ のなかではうまく定義できません。$`S\H\mbf{SortSet}, S\H\mbf{SortSet}_{\mrm{tot}}`$ のなかなら定義できます。

台集合に関しては：

$`\quad \u{X \cup Y}:= \u{X}\cup \u{Y}`$

ここで、右辺の $`\cup`$ は集合の合併です。

$`\mrm{sort}_X \subseteq \u{X}\times S`$ を、$`(\u{X}\cup\u{Y})\times S`$ の部分集合だとみなしたものを $`\widetilde{\mrm{sort}_X}`$ と書きます。$`\widetilde{\mrm{sort}_Y}`$ も同様です。

合併のソート付け $`\mrm{sort}_{X\cup Y}`$ の定義は以下のとおりです。

$`\quad \mrm{sort}_{X\cup Y}:= \widetilde{\mrm{sort}_X}\cup \widetilde{\mrm{sort}_Y}\; \subseteq (\u{X}\cup\u{Y})\times S`$

$`:=`$ の右に現れる $`\cup`$ は集合の合併です。

ソート付き導出系の項集合

$`A`$ を$`S`$-ソート付き導出系だとします。

$`\quad A = (I^A, (C^A_i)_{i\in I^A}, J^A, (R^A_j)_{j\in J^A})`$

混乱の心配がなければ、上付きの $`A`$ は省略します。

順序数 $`\alpha \in |\mbf{Odnl}|`$ に対する $`A`$ の$`S`$-ソート付き項集合〈$`S`$-sorted termset〉を次のように書きます。

$`\quad S\H\mrm{Term}^\alpha(A)`$

$`S\H\mrm{Term}^\alpha(A)`$ は$`S`$-ソート付き集合であり、順序数 $`\alpha`$ を動かすと次のような関手になります。

$`\quad S\H\mrm{Term}^\hyp(A) : \mbf{Odnl} \to S\H\mbf{SortSet} \In \mbf{CAT}`$

以下に、$`S\H\mrm{Term}^\alpha(A)`$ の作り方を説明します。

まず、$`(I, (C_i)_{i\in I})`$ 上に定義されている構文ルール $`r = (\sigma_0, i, \sigma_1, \cdots, \sigma_n)`$ に対して、項集合コンストラクタ $`G_r`$ を作ります。

$`\text{For }X \in |S\H\mbf{SortSet}|\\
\quad G_r(X) := ({C_i}_*(X_{\sigma_1}, \cdots, X_{\sigma_n}))\AS \sigma_0
`$

構文ルールが $`r = (\sigma_0, i)`$ （$`C_i`$ のアリティが 0）のときは次のようです。

$`\quad G_r(X) := \{C_i(0)\} \AS \sigma_0 = \{ (C_i(0), \sigma_0) \}
`$

構文ルールが $`r = (\sigma_0, i, \sigma_1)`$ （$`C_i`$ のアリティが 1）のときは次のようです。

$`\quad G_r(X) := {C_i}_*(X_{\sigma_1}) \AS \sigma_0
`$

$`G_r`$ は、任意の$`S`$-ソート付き集合を引数に受け取って、自明ソート付き集合を返します。つまり、次のような関数です。

$`\quad G_r : |S\H\mbf{SortSet}| \to |S\H\mbf{SortSet}| \In \mbf{SET}`$

$`G_r`$ は、任意の $`r\in \mbf{SynRule}_S(I, (C_i)_{i\in I})`$ に対して定義できますが、文法 $`R`$ における構文ルール $`r = R_j`$ に対しては次のようになります。

$`\quad G_{R_j}(X) := {C_{i_j}}_*(X_{\sigma_{j, 1}}\cdots X_{\sigma_{j, n(i_j)}} ) \AS \sigma_{j,0}
`$

記法を簡素化するために、$`G_{R_j}`$ と単に $`G_j \text{ for }j\in J`$ とします。$`G_j`$ は文法 $`R`$ に依存し、文法はソート付き導出系 $`A`$ の一部なので、$`G_j`$ は $`A`$ に依存して決まります。

$`S`$-ソート付き導出系 $`A`$ から決まる項集合コンストラクタ $`F^A`$ を次のように定義します。

$`\text{For }X \in |S\H\mbf{SortSet}|\\
\quad F^A(X) := \bigcup_{j\in J}G_j(X)
`$

ここでの $`\bigcup`$ は、$`S`$-ソート付き集合達の合併です。各 $`G_j(X)`$ は自明ソート付き集合であり、それらの合併はソート付き集合です。「ソート付き集合達の圏」では2つのソート付き集合の合併しか述べてませんが、任意個数のソート付き集合達の合併も同様に定義できます。項集合コンストラクタ $`F^A`$ は次のような関数です。

$`\quad F^A: |S\H\mbf{SortSet}| \to |S\H\mbf{SortSet}| \In \mbf{SET}`$

さて、準備が出来たので、順序数に沿った帰納的構成により$`S`$-ソート付き項集合関手〈$`S`$-sorted termset functor〉を定義しましょう。定義の仕方はソート無しのときと同様です。

順序数 $`\xi\in |\mbf{Odnl}|`$ に対して、$`S`$-ソート付き集合 $`S\H\mrm{Term}^\xi(A)`$ を次のように定義します。

$`\xi = 0`$ のとき： $`S\H\mrm{Term}^\xi(A) = S\H\mrm{Term}^0(A) := \emptyset`$
$`\xi = \chi + 1`$ のとき： $`S\H\mrm{Term}^\xi(A) := S\H\mrm{Term}^\chi(A) \cup F^A(S\H\mrm{Term}^\chi(A) )`$
$`\xi`$ が極限順序数のとき： $`S\H\mrm{Term}^\xi(A) := \bigcup_{\chi \in \xi} S\H\mrm{Term}^\chi(A)`$

$`\cup, \bigcup`$ はソート付き集合の合併です。

関手の射パート〈morphism part〉と余極限の定義はソート無しのときと同じです。次の関手が定義できます。

$`\quad S\H\mrm{Term}(A) : \mbf{Odnl}\to S\H\mbf{SortSet}_\mrm{tot} \In \mbf{CAT}`$

$`S\H\mrm{Term}(A)`$ の値が全域ソート付き集合であることは、その作り方から分かります。

順序数 $`\alpha \in |\mbf{Odnl}|`$ に対して $`S\H\mrm{Term}(A)`$ は$`S`$-ソート付き集合ですが、その台集合とソート付け〈sorting〉は次のように略記（記号の乱用）します。

$`\quad S\H\mrm{Term}^\alpha(A) := \u{S\H\mrm{Term}^\alpha(A)}`$
$`\quad \mrm{sort}^\alpha := \mrm{sort}_{S\H\mrm{Term}^\alpha(A)}`$

つまり、次の書き方を許します。

$`\quad \mrm{sort}^\alpha : S\H\mrm{Term}^\alpha(A) \to S \In \mbf{Rel}`$

関手に余極限が存在する場合は次のように書きます。

$`\quad \mrm{sort}^\infty : S\H\mrm{Term}^\infty(A) \to S \In \mbf{Rel}`$

ソート付き導出系達の圏

目次に見出しがあったほうがよいだろうと節を設けましたが、述べることはほぼありません。前節で、ソート付き導出系からソート付き項集合関手を定義したので、ソート無しの場合と同様にして圏を定義できます。

$`S`$-ソート付き導出系達の圏を $`S\H\mbf{DerSys}`$ とすると、ホムセットは次のように与えられます。

$`\quad S\H\mbf{DerSys}(A, B) := [\mbf{Odnl}, S\H\mbf{SortSet}](S\H\mrm{Term}(A), S\H\mrm{Term}(B))`$

ソート付き導出系のあいだの射は自然変換なので、関手 $`S\H\mrm{Term}(\hyp)`$ が問題であり、ソート付き導出系の構造に直接的には言及していません。

導出可能性

論理において、証明可能性〈provability〉を表すメタレベルの記号に '$`\vdash`$' が使われます。しかし、導出系の項のなかに記号 '$`\vdash`$' が現れてしまうことがあります -- 例えば、型理論の判断形式〈judgement form〉がその例です。混乱を避けたいので、導出系について語るメタレベルの記号は '$`\Vdash`$' とします。

$`A`$ が$`S`$-ソート付き導出系のとき、$`x\in S\H\mrm{Term}^\alpha_\sigma(A)`$ であることを次のように書きます。

$`\quad \Vdash_A x \text{ as }\sigma \text{ at }\alpha`$

これはソート付き導出系 $`A`$ に関する命題です。この命題が記述している性質を、$`A`$ における項 $`x`$ の導出可能性〈derivability〉といいます。

項の導出ツリー〈derivation tree〉については述べてませんが、具体例における導出ツリーは「球体集合達の圏の構文表示 2/2」にあります。とりあえず、項 $`x`$ にはその導出ツリーというモノが存在すると思ってください。

項 $`x`$ の導出ツリーを $`t`$ として、導出ツリーも添えた導出可能性の記述は次です。

$`\quad \Vdash_A x \text{ as }\sigma \text{ at }\alpha \text{ by }t`$

導出ツリー $`t`$ により導出される項の集合（単元集合になる）を $`S\H\mrm{Term}^\alpha_\sigma(A)_t`$ とすると、上の導出可能性命題は次の意味です。

$`\quad x \in S\H\mrm{Term}^\alpha_\sigma(A)_t`$

$`\sigma, \alpha, t`$ のどれかを省略すると、$`x`$ を導出可能とする $`\sigma, \alpha, t`$ が存在する、という意味になります。幾つか例を挙げると：

$`\quad \Vdash_A x \text{ as }\sigma \text{ at }\alpha \\
\Iff \exists t\in \mrm{DerTree}(A).\, x \in S\H\mrm{Term}^\alpha_\sigma(A)_t
`$

$`\quad \Vdash_A x \text{ as }\sigma \\
\Iff \exists \alpha \in |\mbf{Odnl}|.\exists t\in \mrm{DerTree}(A).\, x \in S\H\mrm{Term}^\alpha_\sigma(A)_t
`$

$`\quad \Vdash_A x \text{ by }t\\
\Iff \exists \sigma\in S.\exists \alpha \in |\mbf{Odnl}|.\, x \in S\H\mrm{Term}^\alpha_\sigma(A)_t
`$

$`\quad \Vdash_A x\\
\Iff \exists \sigma\in S.\exists \alpha \in |\mbf{Odnl}|.\exists t\in \mrm{DerTree}(A).\, x \in S\H\mrm{Term}^\alpha_\sigma(A)_t
`$

圏類似代数系-導出系の相対随伴

現時点では、おぼろげに見えている景色（幻影かも知れない）なのですが、次のような相対随伴系（相対スード随伴系）が在りそうな気がします。

$`\quad \xymatrix{
{}
&{x\mbf{Alg}} \ar[dr]^{x\mrm{AlgSyn}}
\ar@{}[d]|{\dashv}
&{}
\\
{x\mbf{FinDerSys}} \ar[rr]_J \ar[ur]^{x\mrm{SynAlg}}
&{}
&{x\mbf{DerSys}}
}\\
\quad \In \mbf{CAT}
`$

ここで、$`x`$ は圏類似代数系〈category-like algebraic {system | structure}〉の種別を表す記号だとします。圏 $`x\mbf{Alg}`$ は、種別が $`x`$ である圏類似代数系達の圏（ドクトリン）です。$`x\mbf{DerSys}`$ は、種別が $`x`$ である圏類似代数系を記述するための導出系達の圏です。$`x\mbf{FinDerSys}`$ は、何らかの意味で“有限的”な導出系達の圏で、人間が具体的に構成可能な導出系は $`x\mbf{FinDerSys}`$ の対象に限られます。$`J`$ は包含関手です。

この状況のもとで、関手 $`x\mrm{SynAlg}`$ は、導出系に対して、その導出系が“自由に”生成する圏類似代数系を対応させる関手です。一方、関手 $`x\mrm{AlgSyn}`$ は、圏類似代数系に対して、それを記述する（支える）のに“適切な”導出系を対応させる関手です。

これらが相対随伴系を形成するとは、次のホムセット同型が系統的に在ることです。

$`\text{For }A \in |x\mbf{FinDerSys}|\\
\text{For }\cat{D} \in |x\mbf{Alg}|\\
\quad x\mbf{Alg}(\mrm{SynAlg}(A), \cat{D}) \cong x\mbf{DerSys}(J(A), \cat{D})
`$

外側の世界が $`\mbf{CAT}`$ ではなくて $`2\mathbb{CAT}`$ のときは、ホムセット同型ではなくてホム圏同値となり、相対随伴系は相対スード随伴系となり、より複雑になります。

具体例は、「論理や型理論の圏論的意味論」で述べた、カリー／ハワード／ランベック対応の例です。$`x`$ として $`\mrm{cc}`$（Cartesian Closed から）を取ると、相対随伴系は次のようになります。

$`\quad \xymatrix{
{}
&{\mrm{cc}\mbf{Alg}} \ar[dr]^{\mrm{ccAlgSyn}}
\ar@{}[d]|{\dashv}
&{}
\\
{\mrm{cc}\mbf{FinDerSys}} \ar[rr]_J \ar[ur]^{\mrm{ccSynAlg}}
&{}
&{\mrm{cc}\mbf{DerSys}}
}\\
\quad \In \mbf{CAT}
`$

$`\mrm{cc}\mbf{Alg}`$ はデカルト閉圏達の圏で、$`\mrm{cc}\mbf{FinDerSys}`$ は、連言と含意を持つ自然演繹系〈natural deduction system〉達の圏です。連言含意の自然演繹系 $`A`$ に対して、$`\mrm{ccSynAlg}(A)`$ は、演繹系〈導出系〉から生成される最小のデカルト閉圏で、$`A`$ のモデル達の圏の始対象となるはずです。

圏類似代数系の種別 $`x`$ が具体的に与えられ、比較的単純なときは、相対随伴系を完全に記述できそうですが、一般論となると茫漠としていて霧の彼方です。

そしてそれから

長い記事でしたが、それでも書き残したことはイッパイあります。ほんとにイッパイあります。

残った話題・課題を列挙すると：

構文解析器
様々なツリー／半ツリーの利用
1. 項導出ツリー
2. 項集合導出ツリー
3. ルール半ツリー
導出系が退化する場合
1. アリティ0の構文コンストラクタのインデックス付けが単射の場合
2. 構文コンストラクタのインデキシング集合をルールのインデキシング集合に流用する場合
3. 構文ソート集合が単元集合の場合
ルールの副条件〈サイドコンディション〉
導出系のあいだの演算
導出系の具体例
1. 論理の自然演繹
2. 論理のシーケント計算
3. 型理論の判断の導出系
4. 正規文法による言語生成系
5. 文脈自由文法による言語生成系
6. 形状付き集合達の圏の構文表示（「球体集合達の圏の構文表示 1/2」参照）
構文ルールの分類
1. 導入ルール、形成ルール〈{formation | forming} rule〉
2. 消去ルール
3. 変換ルール〈conversion rule〉、計算ルール〈computation rule〉
項書き換え系
導出系と閉包系の関係（「演繹系と閉包系」参照）
構文ソート／構文ソート達の集合に構造を持たせる
動的文法
1. ソート集合を固定しない
2. 導出系内に、新しいソートを定義するルールを持つ
3. 帰納的定義において、ソート集合も増えていく
導出系のオペラッドによる定式化（「演繹系とオペラッド」参照）

うん、イッパイあるなー。

続きの記事：

導出系：反省と課題

*1:嫌な理由（のひとつ）は「論理や型理論の圏論的意味論 // 導出システムの構文圏と随伴系」参照。

*2:「タイプ」や「クラス」を使えば、オーバーロード／コンフリクトはもっと酷いでしょう。「球体集合達の圏の構文表示 2/2」では「構文的役割り〈syntactic role〉」を使ってました

*3:ソート無し導出系は、ソート概念と一切無関係に定義して、後から単一ソートのソート付き導出系とも“みなせる”と考えるのが分かりやすそうです。

*4:大きな〈必ずしも小さくはない〉集合のあいだの通常の関数のことです。

*5:$`S`$ 以外に、$`I`$ と $`n:I\to \mbf{N}`$ だけあれば構文ルールの集合を定義可能です。

*6:教科書に載っている図式に近い、ということです。

はじめに

概要と注意

構文ソートとソート付き導出系

構文コンストラクタとソート無し導出系

ソート無し導出系の項集合

ソート無し導出系の記述の簡略化

ソート無し導出系達の圏

ソート付き導出系

注意事項： 項と項集合

ソート付き集合達の圏

ソート付き導出系の項集合

ソート付き導出系達の圏

導出可能性

圏類似代数系-導出系の相対随伴

そしてそれから

注意事項：項と項集合