「判断的セオリーと判断計算」で紹介したコラリア／ディ-リベールティの論文 "Context, Judgement, Deduction" は、「演繹〈deduction〉とは何なのか？」をテーマにしています。「メリス／ジルバーガーの圏論的判断計算」で紹介したメリス／ジルバーガーの論文 "Functors are Type Refinement Systems" も同じ問題意識を持っていたように思えます。
「演繹とは何なのか？」に対する現状の僕の答は、「計算可能な図式間関数」です。これについて説明します。「なぜ、計算可能な図式間関数を演繹とみなせるのか」についての説明は、次の機会にします。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\msc}[1]{\mathscr{#1}}
\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\In}{\text{ in }}
%\newcommand{\twoto}{\Rightarrow }
\newcommand{\op}{\mathrm{op} }
%\newcommand{\id}{\mathrm{id}}
%\newcommand{\u}[1]{\underline{#1}}
%\newcommand{\o}[1]{\overline{#1}}
%\newcommand{\hyp}{ \text{－} }
\newcommand{\Iff}{ \Leftrightarrow }
%\newcommand{\Imp}{ \Rightarrow }
%\newcommand{\incto}{\hookrightarrow }
%\newcommand{\fibto}{\twoheadrightarrow}
\newcommand{\T}[1]{\text{#1}}
\newcommand{\H}{\text{-}}
\newcommand{\SWArrow}{\style{display: inline-block; transform: rotate(-45deg)}{\Leftarrow} }
`$
内容：
図式
まず、「計算可能な図式間関数」における図式とは何か？ を説明します。図式を理解するためのキーワード〈重要語句〉は以下です。これらは名前〈名詞〉ですが、名前の種類（「名前の解釈： 正確なコミュニケーションのために // 名前の種類とスコット・ブラケット」参照）を括弧内に入れています。
- グラフ（一般名）
- 図式（一般名）
- 形状（構成素役割り名）
ここでの「形状」が一般名ではなくて構成素役割り名であることに注意してください。「図式の形状の形状〈the shape of the shape of a diagram〉」のような使い方ができます。
グラフについては、「属性付きn-グラフはいけてる // n-グラフ」で述べています。しかし、グラフを次元 n で分類しているだけなので、もう少し精密な分類をします。
$`R`$ をリーディ圏（「圏論で使う「図式」と「形状」 // リーディ圏」「組み合わせ的対象物の位相的実現 // リーディ圏」参照）だとします。リーディ圏 $`R`$ 上の前層を$`R`$-グラフ〈$`R`$-graph〉と呼ぶことにします。$`R`$-グラフは、形状が $`R`$ の形状付き集合（「指標の話： 形状の記述と形状付き集合 // 形状付き集合」「位相的形状付き集合 再論」参照）とまったく同義です。
$`\quad G \text{ が }R\H{グラフ}\\
\Iff G \text{ が }R\H{形状付き集合}\\
\Iff G \in |[R^\op, \mbf{Set}]|
`$
文脈によりますが、「関手の域」を「～の形状」と呼びます。ときに「域」と「形状」が同義語なのです。「域」は一般名ではないので、「形状」も一般名ではありません。グラフの形状〈the shape of a graph〉とは、関手（前層）としてのグラフの域のことです。ただし、反変関手 $`G`$ の域を $`R^\op`$ とするか $`R`$ とするかはゆらぎがあります（「イイカゲンとインチキを悔い改めるためのコスト」参照）。
$`\quad R \text{ は } G {の形状}\\
\Iff R = \mrm{dom}(G) \text{ or } R^\op= \mrm{dom}(G)\\
\Iff G \text{ が }R\H{グラフ}
`$
$`\cat{T}`$ を何らかの圏類似構造〈category-like structure〉だとします。この場合、$`\cat{T}`$ は、台構造〈underlying structure〉として$`R`$-グラフ〈$`R`$-形状付き集合〉を持ちます。$`\mbb{U}`$ を、圏類似構造に対してその台である$`R`$-グラフを対応させる忘却関手とします。
$`\quad \mbb{U}(\cat{T}) \in |[R^\op, \mbf{Set}]|`$
形状が $`G`$ で、ターゲットが $`\cat{T}`$ である図式〈diagram〉とは次のような関手 $`D`$ です。
$`\quad D: G \to \mbb{U}(\cat{T}) \In [R^\op, \mbf{Set}]`$
ここでの「形状」も関手の域のことです。ターゲット〈target〉は関手の余域のことです。
次の言い回しに混乱しないように注意してください。
- 図式 $`D`$ の形状はグラフ $`G`$ である。
- グラフ $`G`$ の形状はリーディ圏 $`R`$ （あるいは $`R^\op`$ ）である。
- 図式 $`D`$ の形状の形状はリーディ圏 $`R`$ （あるいは $`R^\op`$ ）である。
この節で定義した「$`R`$-グラフ、図式、図式の形状」は曖昧なところがないハッキリした概念です。
図式の形状ドクトリン
$`R`$-グラフ〈$`R`$-形状付き集合〉達の圏は関手圏 $`[R^\op, \mbf{Set}]`$ です。圏 $`[R^\op, \mbf{Set}]`$ の充満部分圏 $`\msc{D} \subseteq [R^\op, \mbf{Set}]`$ を選んで固定します。選んで固定した圏 $`\msc{D}`$ を形状ドクトリン〈shape doctrine | doctrine of shapes〉と呼びます。
形状ドクトリン $`\msc{D}`$ は、図式の形状（関手の域）として相応しいグラフ達の圏だと考えます。形状ドクトリンの対象である$`R`$-グラフ（$`R`$ はリーディ圏）を形状〈shape〉と呼ぶことがあります。今導入した「形状」は、「$`\msc{D}`$ の対象」を意味する一般名です。
- 構成素役割り名としての「形状」は、関手の域のこと。
- 一般名としての「形状」は、形状ドクトリンの対象のこと。
「図式の形状は、形状である」の意味は：
- 図式と呼ばれる関手の域は、形状ドクトリンの対象である。
図式空間
グラフの形状 $`R`$ （リーディ圏）と、図式の形状ドクトリン $`\msc{D}\subseteq [R^\op, \mbf{Set}]`$ 、そして、図式のターゲット（関手の余域）$`\cat{T}`$ も決まっているとします。このとき、次のホムセットを考えることができます。
$`\text{For }G\in |\msc{D}|\\
\quad [R^\op, \mbf{Set}](G, \mbb{U}(\cat{T}))`$
次の記法も使います。（$`\mrm{DS}`$ は Diagram Space から。）
$`\text{For }G\in |\msc{D}|\\
\quad \mrm{DS}^\msc{D}_\cat{T}[G] := [R^\op, \mbf{Set}](G, \mbb{U}(\cat{T}))`$
$`\mrm{DS}^\msc{D}_\cat{T}[G]`$ は、図式を要素とする集合です（圏にはなりません）。ターゲット $`\cat{T}`$ が了解されているときは下付き $`\cat{T}`$ は省略可能です。形状ドクトリン $`\msc{D}`$ が了解されているときは上付き $`\msc{D}`$ が省略可能です。考えられる省略形は：
- $`\mrm{DS}^\msc{D}_\cat{T}[G]`$ （省略なし）
- $`\mrm{DS}^\msc{D}[G]`$
- $`\mrm{DS}_\cat{T}[G]`$
- $`\mrm{DS}[G]`$
形状が $`G`$ である図式達の集合 $`\mrm{DS}[G]`$ を図式空間〈diagram space〉と呼びます。空間とは言っても位相を持つわけではありません。ここでの「空間」は集合と同義です。
形状ドクトリン $`\msc{D}`$ 上の（$`\cat{T}`$ をターゲットとする）すべての図式達の集合は次のように書けます。
$`\quad \sum_{G\in |\msc{D}|} \mrm{DS}[G]`$
つまり、形状 $`G\in |\msc{D}|`$ ごとの図式空間 $`\mrm{DS}[G]`$ を、すべての $`G`$ に渡って総和したものです。
図式間関数
図式空間 $`\mrm{DS}[G] = \mrm{DS}^\msc{D}_\cat{T}[G]`$ は、サイズが大きくなるかも知れませんが集合です。2つの（2つが一致してもよい）図式空間 $`\mrm{DS}[G]`$ と $`\mrm{DS}[H]`$ のあいだの関数〈写像〉を図式間関数〈function between diagrams〉と呼ぶことにします。図式間関数 $`\varphi`$ は次の形です。
$`\quad \varphi : \mrm{DS}[G] \to \mrm{DS}[H]\In \mbf{SET}`$
集合圏のサイズ（$`\mbf{Set}`$ か $`\mbf{SET}`$ か $`\mbb{SET}`$ か）は状況により変わります。
図式間関数は、「圏論的オペレーター／圏論的コンストラクタ／圏論的コンビネータ」などと呼んでいたモノ（の一部）の適切な定式化になっています。いずれリネームするかも知れませんが、今は暫定的名前として「図式間関数」にしておきます。
形状ドクトリン $`\msc{D}`$ は直和で閉じているとします。そのとき、次の同型が成立します。
$`\quad \mrm{DS}[G]\times\mrm{DS}[H] \cong \mrm{DS}[G + H]\In \mbf{SET}`$
空形状 $`\emptyset`$ が $`\msc{D}`$ に入っているとして：
$`\quad \mrm{DS}[\emptyset] \cong \mbf{1}\In \mbf{SET}`$
これにより、多変数の図式間関数や無変数の図式間関数は一変数の図式間関数として書けます。つまり、変数〈引数〉の個数に関わりなく、$`\mrm{DS}[G] \to \mrm{DS}[H]`$ の形に書けます。
計算可能性
図式間関数 $`\varphi : \mrm{DS}[G] \to \mrm{DS}[H]`$ は大きな集合のあいだの関数かも知れません。アルゴリズムで計算可能とは限りません。つうか、ほとんどの関数はアルゴリズムで計算可能ではありません。
今「計算可能」という言葉を使ったのですが、図式空間は自然数の集合などとはかけ離れたワケワカラン集合です。図式空間の上での関数の再帰的定義という概念も全然自明じゃないです。
となると、図式間関数が計算可能だという概念の定義も全然自明じゃなく、難儀するかも知れません。今のところ、ハッキリとは分かりません。
そしてそれから
図式間関数は、巨大で超越的ですが、いちおうチャンとした定義を持ちます。その計算可能性は課題です。が、直感的に明らかに計算可能な例はすぐに挙げられます。
$`R`$-グラフにも属性を付けて属性付き$`R`$-グラフを考えることができます（「属性付きn-グラフはいけてる」参照）。実際には、属性を使わないとうまくいかないことがあります。今回は属性を考えてませんが、実用上は属性が必須です。
図式間関数を考えた動機は「演繹とは何なのか？」に答えるためですが、どうして図式間関数が演繹なのかは書いてません。これはまた次の機会にします。
