檜山トレラン4 B08 0-文法

--- tags: TrRun4 id: Theo-B08_0-grammar.md --- <style> div.def { border-left: 5px solid skyblue; padding-left: 1em } </style> # 檜山トレラン4 B08 0-文法 $\newcommand{\In}{\text{ in } } \newcommand{\id}{\mathrm{id} } \newcommand{\Id}{\mathrm{Id} } \newcommand{\ID}{\mathrm{ID} } \newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\u}[1]{\underline{#1} } \newcommand{\twoto}{\Rightarrow} \newcommand{\threeto}{\equiv\!\gt} \newcommand{\imp}{\mathop{=\!\!\triangleright} } \newcommand{\hyp}{\text{-}} \newcommand{\rew}{\leadsto} \newcommand{\reww}{ \mathrel{ \leadsto\!\!*} } % \require{color}% \newcommand{\Keyword}[1]{ \textcolor{green}{ \bf \text{#1} } }% %\newcommand{\For}{\Keyword{For }}% \newcommand{\Let}{\Keyword{Let }}% %\newcommand{\WeWillDefine}{\Keyword{WeWillDefine }}% %\newcommand{\WeDefine}{\Keyword{WeDefine }}% \newcommand{\Where}{\Keyword{Where }} % 使っている %\newcommand{\Justification}{\Keyword{Justification }}% %\newcommand{\Using}{\quad\Keyword{Using }} %\newcommand{\Family}{\Keyword{Family }} %\newcommand{\Index}{\Keyword{Index }} %\newcommand{\Variable}{\Keyword{Variable }} %\newcommand{\ChangeNotation}{\quad\Keyword{ChangeNotation }} %\newcommand{\Substitution}{\quad\Keyword{Substitution }} %\newcommand{\When}{\Keyword{When } } %\newcommand{\WeAssert}{\Keyword{WeAssert }} \newcommand{\WeIntroduce}{\Keyword{WeIntroduce }} %\newcommand{\WeInstantiate}{\Keyword{WeInstantiate }} %\newcommand{\WeConstruct}{\Keyword{WeConstruct }} %\newcommand{\From}{\Keyword{ From } } %\newcommand{\WeAddmit}{\Keyword{WeAddmit }} \newcommand{\Requires}{\Keyword{Requires }} \newcommand{\As}{\Keyword{ As } } \newcommand{\IsA}{\Keyword{ IsA } } \newcommand{\Of}{\Keyword{ Of } } %使っている %\newcommand{\ClassOf}{\Keyword{ClassOf } } %\newcommand{\Things}{\Keyword{ Things} } \newcommand{\Assuming}{\Keyword{Assuming } } %\newcommand{\Alias}{\Keyword{Alias } } %\newcommand{\To}{\Keyword{ To } } %$ - 必要な予備知識： [A07 文法と証明](https://hackmd.io/@m-hiyama/r1zsgiPk5)、[B07 セオリー](https://hackmd.io/@m-hiyama/HyfJByJlc) は読んでいるとする。 [B07 セオリー // セオリーと文法](https://hackmd.io/@m-hiyama/HyfJByJlc#%E3%82%BB%E3%82%AA%E3%83%AA%E3%83%BC%E3%81%A8%E6%96%87%E6%B3%95) より引用： > ==注意：== 文法のクリアな定義は、指標の圏を含む随伴系〈adjunction〉である。したがって、随伴系をお勉強しないとクリアな定義は導入できない。当面は直感的な（モヤモヤな）理解でもいいので、文法の存在はちゃんと認識しよう。文法を随伴系として理解するのはちょっと先（このクールでは無理）だろうが、直感的モヤモヤを少しはクリアにしておく。我々の主たる興味は“1-指標から1-セオリーを生成する1-文法”だが、時間と分量の関係で、この文書では“0-指標から0-セオリーを生成する0-文法”の事例しか述べてない（前半は一般論の準備だが）。続きは後日（かな？）。「コンピュータ利用者がCPUやメモリを理解する必要はない」と同じ事情で、セオリー論（の道具）の利用者がこの文書の内容を理解しなくてもいいかも知れない。が、道具のメカニズムを知っていればその道具を==より良く使える==。また、練習問題があるので、練習問題の設定を知るために解説を読むでもよい。 - [B08Ans B08の練習問題の解答例](https://hackmd.io/@m-hiyama/B1Oh0JIx9) 逆に、練習問題を全部飛ばして解説部分を流し読みしてもそれなりに参考になる情報はあるだろう。特に、[構文解析木と表層構文](#%E6%A7%8B%E6%96%87%E8%A7%A3%E6%9E%90%E6%9C%A8%E3%81%A8%E8%A1%A8%E5%B1%A4%E6%A7%8B%E6%96%87) で、檜山が何回も（何十回もかな？）強調していることを、文法との兼ね合いで語っている。これだけでも再確認よろしく。 ## 用語と語学的注意例によって例のごとく、色々な分野で同じ概念を独立に繰り返し繰り返し何度も何度も発見しているので、同義語・類義語・多義語・オーバーロード・コンフリクトが==ジャングル状態==。 ![jungle.jpg](https://www.chimaira.org/img-sem/jungle.jpg) 画像：出典不明ジャングルを整地するのは至難の業、ほぼ不可能。諦めて、ジャングルはジャングルとして受け入れるしかないだろう。 ![nonjungle.jpg](https://www.chimaira.org/img-sem/nonjungle.jpg) 画像： <https://readyfor.jp/projects/whitecorn> 形式言語理論では、文法を形式的に定義している。正規文法〈正則文法〉とか文脈自由文法とかの分類がある。ここで扱う文法は、形式言語理論の文法をすべて包摂してるわけではないが、正規文法などはカバーしている。プログラミング言語の代数的データ型の概念は、ここで述べる文法で完全に解釈できる。依存型理論の基本的部分も、ここで述べる文法で理解できる。論理やプログラミング意味論で使う、帰納的構成〈帰納的定義〉、帰納的データ型もここで述べる文法で理解できる。分野ごとに用語はバラバラだが、==だるい==ので列挙はしない。必要があれば、自分で用語対応表を作ってちょうだい。以下、幾つかの注意点だけ述べる。本セミナーで「コンビネーション」と呼んでいる概念の呼び名の多数派は「**項**〈term〉」、「多項式の項」とはコンフリクトしている（オーバーロードではない）。絵図〈グラフィカルなコンビネーション〉を項とは呼ばないので、ツリーを生成する**ツリー文法**、より一般のグラフを生成する**グラフ文法**などの分類がある。が、テキスト ←→ 絵図の相互変換を考えると、こういう分類にはあまり==意味がない==。形式言語理論でのコンビネーションは、統語範疇に応じて「**語**〈word〉」「**句**〈phrase〉」「**文**〈sentence〉」とか呼ばれる。そんな分類は==我々には不要==。構文解析ツリー（または構文解析グラフ）のノードをここでは記号{ノード}?〈symbol {node}?〉と呼ぶが、他の呼び名もイッパイあるだろう、==知らんがな==。記号に、**原子的**〈atomic〉、**基本**〈basic〉、**単純**〈simple〉、**基礎**〈ground〉、**組み込み**〈built-in〉などの形容詞が付くかも知れない。==ドーデモイイ==。コンビネーションを構成する記号{ノード}?の分類で重要な（ドーデモよくない）のは： 1. 指標から提供されるラベル。文法では規定してない記号。 2. 文法から提供される連結子〈コネクティブ〉〈connective〉。指標には含まれない記号。 3. ターゲット圏から提供されるリテラル〈literal〉。ターゲット圏のシングの固有名。「ラベル」の同義語は [D01 混乱しがちな言葉 // ローカル用語の同義語・類義語](https://hackmd.io/@m-hiyama/S19pMmljK#%E3%83%AD%E3%83%BC%E3%82%AB%E3%83%AB%E7%94%A8%E8%AA%9E%E3%81%AE%E5%90%8C%E7%BE%A9%E8%AA%9E%E3%83%BB%E9%A1%9E%E7%BE%A9%E8%AA%9E) に列挙している。 "connective" の翻訳語は「結合子」だが、「結合」を "composition" の意味で使うので「連結子」にする。めぼしい同義語は： 1. 演算{子}?{記号}? 2. オペレータ{ー}?{記号}? 3. オペレーション{記号}? 4. コンビネータ{ー}?{記号}? 5. {データ \| 項}?{構成子 \| コンストラクタ{ー}?}{記号}? 用語から受ける印象で意味を判断する“お花畑連想”（下図参照）をするくらいなら、同義語は「==一切知らない／まったく使わない==」ほうが吉〈安全 \| 災難防止〉。 ![ohanabatake-ibodekita.jpg](https://www.chimaira.org/img-sem/ohanabatake-ibodekita.jpg) 画像： <https://mobile.twitter.com/ibodekita> リテラルは「定数{記号}?」とも呼ぶが、定数はたいてい変数〈ラベル〉だし、ときに連結子〈コネクティブ〉を「定数」と呼ぶこともあるので要注意〈罠〉、リスキーな「定数」は==使わない==のが吉〈安全 \| 災難防止〉。 ## アンラーン／リラーン以下の主張は初見では意味不明、困惑するだろう。 - 文法は指標である。 - ラベルはコネクティブである。 - 1-ラベルは2-ラベルである。 - セオリーはモナドである。 - コンビネーションはラベルである。表現は雑だが、どれも正しい主張である。補足の文言を入れると： - 文法は［上位の］指標である。 - ［下位の］1-ラベルは［上位に格上げすると］2-ラベルである。 - ［上位の指標の］ラベルは［下位の文法の］コネクティブである。 - セオリーは［指標の圏の上の］モナドである。 - ［指標から作られる］コンビネーションは［モナドの値である指標の］ラベルである。これらの主張を理解するには、概念を形式的に定義して正確な分析をする必要がある。日常的によく使っている「変数、定数、式」などの言葉は、よく使っているが故に意味がモンヤリ（モヤッとボンヤリ）だったり、逆に特定具体的用法への強い連想が付着してしまっていたりする。つまり、==お花畑的理解==しかしてない言葉に成り下がっている。お花畑言葉の不正確な定義や印象をいったんアンラーンして、テクニカルタームとしてより形式的／より厳密にリラーンしよう。 | お花畑言葉 | テクニカルターム | |-----------|-----------------| | | 指標 | | 変数 | ラベル | | 定数 | リテラル | | 演算子 | 連結子〈コネクティブ〉 | | 項、式、図式 | コンビネーション | | | セオリー | | 文法 | セオリーモナド | [追記]「文法＝セオリーモナド」には至ってない。「文法 ≒ 指標」まではこの文書内で示唆している。[/追記] ## 部分指標と切り捨て指標 $\Sigma$ を宣言文の集合と考える。集合と考えて $\Sigma$ の部分集合 $\Gamma$ が指標であるとき、$\Gamma$ を $\Sigma$ の部分指標〈subsignature〉と呼び、$\Gamma \sqsubseteq \Sigma$ と書く（念の為、'$\subseteq$' と違う記号を使った）。例として次の指標を考える。 $\text{1-signature _ } \In {\bf Set}\;\{\\ \quad \text{0-mor } U\\ \quad \text{1-mor } e:{\bf 1} \to U\\ \quad \text{1-mor } m: U\times U \to U\\ \}$ 当該指標以外に次のような部分指標がある。 $\text{1-signature _ } \In {\bf Set}\;\{\\ \quad \text{0-mor } U\\ \quad \text{1-mor } e:{\bf 1} \to U\\ \}\\ \:\\ \text{1-signature _ } \In {\bf Set}\;\{\\ \quad \text{0-mor } U\\ \quad \text{1-mor } m: U\times U \to U\\ \}\\ \:\\ \text{1-signature _ } \In {\bf Set}\;\{\\ \quad \text{0-mor } U\\ \}\\ \:\\ \text{1-signature _ } \In {\bf Set}\;\{\\ \}$ 任意の指標 $\Sigma$ からk次元以下の宣言文だけを抜き出した部分指標を $\Sigma|_{\le k}$ と書きk-切り捨て〈k-truncation〉と呼ぶ。言い方を変えると、$\Sigma|_{\le k}$ は、kを超える次元の宣言文をすべて捨てたもの。上記指標を $\Sigma$ として $\Sigma|_{\le 0}$ は： $\text{1-signature _ } \In {\bf Set}\;\{\\ \quad \text{0-mor } U\\ \}$ $\Sigma|_{\le 0}$ が0-指標になるわけではない。切り捨ては指標の次元を変えない。 ==練習問題： 1== 集合圏におけるモノイドの指標を自分で書いて、その3-切り捨て、2-切り捨て、1-切り捨て、0-切り捨て、(-1)-切り捨てを求めよ。 ==練習問題： 2== 以下はモナドの指標である（これで、モナドの定義は完璧）。3-切り捨て、2-切り捨て、1-切り捨て、0-切り捨て、(-1)-切り捨てを求めよ。 $\text{2-signature Monad within }{\bf CAT}\;\{\\ \quad \text{0-mor }\cat{C}\\ \quad \text{1-mor }F : \cat{C} \to \cat{C}\\ \quad \text{2-mor }\mu :: F*F \twoto F : \cat{C} \to \cat{C}\\ \quad \text{2-mor }\eta :: \Id_{\cat{C}} \twoto F : \cat{C} \to \cat{C}\\ \quad \text{id 3-mor assoc }::: (\mu * \ID_F); \mu \threeto (\ID_F * \mu) ; \mu :: F*F*F \twoto F : \cat{C} \to \cat{C}\\ \quad \text{id 3-mor lunit}::: (\eta * \ID_F); \mu \threeto \ID_F :: F \twoto F : \cat{C} \to \cat{C}\\ \quad \text{id 3-mor runit}::: (\ID_F * \eta ); \mu \threeto \ID_F :: F \twoto F : \cat{C} \to \cat{C}\\ \}$ ==練習問題： 3== $\mrm{Seq}({\bf Set})$ における半環（掛け算は可換）の指標を書いて、代数的に意味のありそうな部分指標を5つ挙げよ。「意味がありそう」は主観でよい。 ==練習問題： 4== モノイドの指標を宣言文の集合とみての部分集合で、指標ではないものを挙げよ。 ## フィルター付き指標何か $X$ に対して、次のような部分対象の列を与えることをフィルター付け〈filtration〉という。 $\quad X_0 \subseteq X_1 \subseteq \cdots \subseteq X_l = X$ 番号は無限まで延ばしてもいい（ドーデモイイが）。 $\quad \cdots \subseteq X = X_l = X_{l + 1} = \cdots = X_{\infty}$ 参考：チラッと眺めれば、テクニカルタームとしての「フィルター」の用法が分かるだろう。 - <https://en.wikipedia.org/wiki/Filtration_(mathematics)> - <https://en.wikipedia.org/wiki/Filtered_algebra> - <https://ncatlab.org/nlab/show/filtered+topological+space> - <http://pantodon.jp/index.rb?body=stratified_topology> 次のようなフィルター付けを備えた指標をフィルター付き指標〈filtered signature〉と呼ぶ。 $\quad \Sigma_0 \sqsubseteq \Sigma_1 \sqsubseteq \cdots \sqsubseteq \Sigma_l = \Sigma$ $\Sigma$ がn-指標のときに一番よく使うフィルター付けは： $\quad \Sigma|_{\le 0} \sqsubseteq \Sigma|_{\le 1} \sqsubseteq \cdots \sqsubseteq \Sigma|_{\le n + 1} = \Sigma$ 特に1-指標では： $\quad \Sigma|_{\le 0} \sqsubseteq \Sigma|_{\le 1} \sqsubseteq \Sigma_{\le 2} = \Sigma$ 1-指標では、フィルター付け成分に無難な名前を付けられる。 1. $\Sigma|_{\le 0}$ を、$\Sigma$ の台指標〈underlying signature〉と呼ぶ。 1. $\Sigma|_{\le 1}$ を、$\Sigma$ の無法則指標〈lawless signature〉と呼ぶ。 2-指標になると、合意が取れそうなネーミングはない。どこまでが「台」か？「法則」とは何か？もうハッキリしない。番号で呼べばいいので、自然言語起源の呼び名に拘る必要はない。むしろ、頭悪そうな不毛な議論（「台とは何か？」「法則とは何か？」）を避けるために==拘るべきではない==。[X02 半形式的記述の説明と例題 // As の用法](https://hackmd.io/@m-hiyama/SkKQRn1aK#As-%E3%81%AE%E7%94%A8%E6%B3%95) のヒルベルトの言葉も参照 -- 「法則とは何か？」「ビールジョッキである」で議論終了。 ==練習問題： 5== モノイドの指標を書いて、その台指標と無法則指標を抜き出せ。 ==練習問題： 6== 半環（掛け算は可換）の指標を書いて、その台指標と無法則指標を抜き出せ。 ==練習問題： 7== モナドの2-指標を書いて、切り捨てフィルター付け〈filtration by truncation〉を書き下せ。 ==練習問題： 8== モノイドの指標を $\Sigma$ として、切り捨てフィルター付けではないフィルター付け $\Sigma_0 \sqsubseteq \Sigma_1 \sqsubseteq \Sigma_2$ の例を挙げよ。 ## 改めて0-指標とは 0-指標は例えば次の形で表記できる。 $\text{0-signature abc within }{\bf N}\;\{\\ \quad \text{0-mor }a\\ \quad \text{0-mor }b\\ \quad \text{0-mor }c\\ \quad \text{id 1-mor } bc: b \to c\\ \}$ 0-切り捨てすると： $\text{0-signature _ within }{\bf N}\;\{\\ \quad \text{0-mor }a\\ \quad \text{0-mor }b\\ \quad \text{0-mor }c\\ \}$ ここで、次を思い出して欲しい。 [E05 基本用語刷り込み回避バージョン // ラベル](https://hackmd.io/@m-hiyama/SJ4fzkhaK#%E3%83%A9%E3%83%99%E3%83%AB) より： > ラベル〈label〉は、記号〈シンボル〉、文字〈字 \| レター〉、識別子、不定元、プレースホルダーなどとも呼ばれる構文的対象物で、シングを名指す目的で準備された名前である。名前＝ラベルの実体は単に集合の要素、人が目で読める綴りを持つ必要などない。 0-指標の0-ラベルは何でもいいので、0-ラベル達は任意の集合 $A$ でよい。1-ラベルは、2つの0-ラベルを両端に持つので、1-ラベル達の集合を $B$ として、 $\quad \mrm{dom}:B \to A \In {\bf Set}\\ \quad \mrm{cod}:B \to A \In {\bf Set}$ という写像がある。上の例で言えば： $\quad A = \{a, b, c\}\\ \quad B = \{bc \}\\ \quad \mrm{dom}(bc) = b\\ \quad \mrm{cod}(bc) = c$ つまり、0-指標は有向グラフに他ならない。 0次元のはずの0-指標が有向グラフとは？辺は1次元図形ではないか？ ==そのとおり==、次も思い出そう。 [B07 セオリー // 圏の次元のドタバタ](https://hackmd.io/@m-hiyama/HyfJByJlc#%E5%9C%8F%E3%81%AE%E6%AC%A1%E5%85%83%E3%81%AE%E3%83%89%E3%82%BF%E3%83%90%E3%82%BF) より引用： > というわけで、現状の次元概念は==色々間違っている==。 > ...[snip]... > 次元に関して「変だな」と思ったとき、それは勘違いではなくて正しい認識かも知れない。 > ...[snip]... > 前節の「辻褄が合わないときにはアドホックに次元をズラす」方針として、慣例・伝統的次元を使い続ける（世間はそうしている）。 “0-指標”という概念を1-指標で書くなら： $\text{1-signature '0-signature' within }{\bf Set}\;\{\\ \quad \text{0-mor } A \\ \quad \text{0-mor } B \\ \quad \text{1-mor } \mrm{dom}: B \to A\\ \quad \text{1-mor } \mrm{cod}: B \to A\\ \}$ 同じことだが別形式で書くと： 【★定義】0-sign <div class=def> $\WeIntroduce (A, B, \mrm{dom}, \mrm{cod}) \As \text{0-signature}\\ \Where\\ \quad A \in |{\bf Set}| \As \text{set of 0-labels}\\ \quad B \in |{\bf Set}| \As \text{set of 1-labels}\\ \quad \mrm{dom}:B \to A \In {\bf Set} \As \text{domain map}\\ \quad \mrm{cod}:B \to A \In {\bf Set} \As \text{codomain map}$ </div> 0-指標のあいだの準同型写像〈homomorphism〉は次のように定義する。 【★定義】0-sign-hom <div class=def> $\Assuming S \IsA \text{0-signature}\\ \Assuming T \IsA \text{0-signature}\\ \Let A := (\text{set of 0-labels} \Of S)\\ \Let B := (\text{set of 1-labels} \Of S)\\ \Let \mrm{dom}_S := (\text{domain map} \Of S)\\ \Let \mrm{cod}_S := (\text{codomain map} \Of S)\\ \Let C := (\text{set of 0-labels} \Of T)\\ \Let D := (\text{set of 1-labels} \Of T)\\ \Let \mrm{dom}_T := (\text{domain map} \Of T)\\ \Let \mrm{cod}_T := (\text{codomain map} \Of T)\\ \WeIntroduce (S, T, f_0, f_1) \As \text{homomorphism between 0-signatures}\\ \Where\\ \quad f_0:A \to C \In {\bf Set} \As \text{0-underlying map}\\ \quad f_1:B \to D \In {\bf Set} \As \text{1-underlying map}\\ \Requires\\ \quad \forall x\in B.\, \mrm{dom}_T(f_1(x)) = f_0(\mrm{dom}_S(x)) \text{ on } C \As \text{preservation of domain}\\ \quad \forall x\in B.\, \mrm{cod}_T(f_1(x)) = f_0(\mrm{cod}_S(x)) \text{ on } C \As \text{preservation of codomain}$ </div> 0-指標とそのあいだの準同型写像は圏〈1-圏〉を形成する。この圏を $0\hyp{\bf Sign}$ または $0{\bf Sign}$ と書く（ハイフンはあってもなくてもいい）。 ==注意：== 習慣として使い続けているインチキくさい次元と、理論的により整合的な次元がある。この二重構造は鬱陶しいし紛らわしい。が、しょうがない。==諦める==。アドホックに（その場しのぎで）対処する。 0-指標のなかで、1-ラベルを持たない（1-宣言文が書いてない）ものを無法則0-指標〈lawless 0-signature〉と呼ぶことにする。言い方を変えると、$\Sigma|_{\le 0} = \Sigma$ である0-指標が無法則0-指標。無法則0-指標と準同型写像の圏を $0\hyp{\bf Sign}_\mrm{lawless}$ とする。 ==語学的注意：== 「0-指標の法則と何か？」の答は「1-ラベルの宣言のこと」。1-指標のときに、2-ラベルの宣言〈等式〉を「法則」と呼んでいたから流用しただけ。「[フィルター付き指標](#%E3%83%95%E3%82%A3%E3%83%AB%E3%82%BF%E3%83%BC%E4%BB%98%E3%81%8D%E6%8C%87%E6%A8%99)」でも注意したとおり、「法則」という言葉自体を詮索するのは不毛・有害・悪弊（頭悪くなるからヤメレ）。 0-指標は有向グラフとみなせる。辺は、1-ラベルと1-宣言文で与えられる。辺の別名〈同義語〉がある。0-指標に対する特定の解釈や特定利用場面に由来する。 1. ムーブ〈move〉 2. 遷移〈transition〉 3. 書き換え〈rewrite〉 4. 同値関係の生成元〈generator of equivalence relation〉 ==練習問題： 9== 「ムーブ」は次のような比喩に基づく； 0-ラベルを場所と考えて、1-ラベル〈グラフの有向辺〉があると移動可能とする。{拡張した}?移動可能性〈movability〉を次のように定義する。 1. ある場所からその場所自身へは移動可能〈movable〉とする。 2. ある場所から1-ラベル〈グラフの有向辺〉があれば、余域〈codomain \| target \| destination〉の場所に移動可能とする。 3. ある場所から別の（同じでもいいが）場所へ移動可能なら、逆向きにも移動可能とする。 4. 推移的〈transitive〉に移動可能とする。移動可能性は同値関係であることを示せ。（1-ラベル〈グラフの有向辺〉から同値関係が作れるので、「同値関係の生成元」という呼び名もあるわけ。） ==学習上の注意：== 移動／移動可能性の比喩がわかりやすく感じるなら、それをメンタルモデルに持つことはかまわない（むしろ推奨する）。が、何でも移動の比喩で考えようとするような態度はダメ。 ==練習問題： 10== 0-指標 $\Sigma$ を有向グラフと見て、2つの0-ラベル〈頂点〉のあいだにパス（長さ0のパスも許す）があるとき、パスが何本あろうとも1本の無向辺に置き換える。こうしてできた無向グラフを $\Sigma'$ とする。次が成立することを示せ。 - 2つの0-ラベル〈頂点〉が $\Sigma$ 内で移動可能 ⇔ 2つの0-ラベル〈頂点〉が $\Sigma'$ 内で無向辺で結ばれている〈隣接している〉 ==練習問題： 11== ［グラフの隣接行列を知っている人向け（調べりゃすぐ分かる）］前問と同じ設定で、$\Sigma$ の0-ラベル〈頂点〉の集合を $A$ とする。$\Sigma'$ の隣接行列をブール値係数で考えたものを $S$ とする。$S\in {\bf XMat}[{\bf B}](A, A)$ となる。次を示せ。 1. ブール値正方行列 $S$ の対角成分はすべて 1 。 2. ブール値正方行列 $S$ は対称行列、つまり転置しても変わらない、$S^t = S$ 。 3. ブール値正方行列 $S$ はベキ等行列〈idempotent matrix〉、つまり $S S = S$ 。 ==練習問題： 12== ${\bf Graph}$ は有向グラフの圏とする。次のような圏の同一性、同型、包含を納得せよ。 1. ${\bf Graph} = 0{\bf Sign}$ 1. ${\bf Set} \cong 0{\bf Sign}_{\mrm{lawless}}$ 圏の同型 1. $0{\bf Sign}_{\mrm{lawless}} \subseteq 0{\bf Sign}$ 圏の包含 ==練習問題： 13== ［発展的：随伴系〈adjunction〉を知っている人向け］ ${\bf Set}$ は $0{\bf Sign}$ に規準的〈canonical〉に埋め込める。その埋め込み関手〈embedding functor〉を $\quad F:{\bf Set} \to 0{\bf Sign} \In {\bf CAT}$ とする。 0-指標の0-ラベルの集合を取り出す（1-ラベルがあれば捨てる）関手を $\quad U:0{\bf Sign} \to {\bf Set} \In {\bf CAT}$ とする。 0-指標 $\Sigma$ をグラフと見て、パスで繋がる頂点〈0-ラベル〉を同値とする同値関係で割った商集合を $Q(\Sigma)$ とする。これは関手に拡張できるので、 $\quad Q:0{\bf Sign} \to {\bf Set} \In {\bf CAT}$ とする。次の随伴関係があることを示せ。 $\quad Q \dashv F \dashv U$ ## 構文解析木と表層構文文法があれば、コンビネーション（テキストや絵図）を構文解析できる。文法とは、**構文解析を可能にするための規則集**だと言える。例えば、「2 + 3」というテキストは次のような構文解析木を持つ。 ```graphviz digraph { two[label="2"] three[label="3"] add[label="+"] add -> two[arrowhead=none] add -> three[arrowhead=none] } ``` 文法は、構文解析木の情報をテキスト化する方法も指定する。「2 + 3」という標準的テキスト化以外に、==各種括弧、区切り記号、空白改行、上下左右の添字など==の使い方により、膨大な数のテキスト化方法がある。例えば： 1. $+\;2\;3$ （ポーランド記法） 1. $2\;3\;+$ （逆ポーランド記法） 1. $+(2, 3)$ （関数呼び出し記法） 1. $(2, 3)+$ （後置関数呼び出し記法） 1. $(2, 3).+$ （図式順ドット適用記法） 1. $2.\,3.+$ （図式順ドット適用記法のカリー化） 1. $+_{2,3}$ （引数をインデックスで渡す記法） 1. $+_2^3$ （引数を上下インデックスで渡す記法） 1. $+^2_3$ （上下インデックスが逆） 1. ${_2 +_3}$ （引数を左右の下付きインデックスで渡す記法）このような違いを「記法の違い」とか「表層構文〈surface syntax〉の違い」と言う。以下の記事の練習は、表層構文の違いを無視する練習である。 - [基本スキルの確認と練習 (G2 A6P3, C A7P3)](https://m-hiyama-second.hatenablog.com/entry/2019/11/17/134521) 解答例の一部は [タプルの書き方](https://hackmd.io/@m-hiyama/S1b6tmHbO) 次に、「2 → two、3 → three、+ → Add」と置換してみると： 1. $\mrm{Add}\;\mrm{two}\;\mrm{three}$ （ポーランド記法） 1. $\mrm{two}\;\mrm{three}\;\mrm{Add}$ （逆ポーランド記法） 1. $\mrm{Add}(\mrm{two}, \mrm{three})$ （関数呼び出し記法） 1. $(\mrm{two}, \mrm{three})\mrm{Add}$ （後置関数呼び出し記法） 1. $(\mrm{two}, \mrm{three}).\mrm{Add}$ （図式順ドット適用記法） 1. $\mrm{two}.\,\mrm{three}.\mrm{Add}$ （図式順ドット適用記法のカリー化） 1. $\mrm{Add}_{\mrm{two},\mrm{three}}$ （引数をインデックスで渡す記法） 1. $\mrm{Add}_\mrm{two}^\mrm{three}$ （引数を上下インデックスで渡す記法） 1. $\mrm{Add}^\mrm{two}_\mrm{three}$ （上下インデックスが逆） 1. ${_\mrm{two} \mrm{Add}_\mrm{three}}$ （引数を左右の下付きインデックスで渡す記法）これらも表層構文の違いであり、意味内容は同じ。学習・理解の一般的スキルとして、**表層構文の違いを無視する能力**（構文解析木を直接認識する能力）は最重要なものだと檜山は思う。徹底的なトレーニングが望まれる。（余談だったが。） ## 0-文法 AddArith 小学校一年の算数の目標は足し算を含む式の理解だろう。足し算〈addition〉だけの算数〈arithmetic〉で使う文法を AddArith とし、この文法を説明する。 ==語学的注意：== "arithmetic" は算数の意味もあるが、整数論や代数幾何の高度・難解な分野を指すこともある。"INTRODUCTION TO ARITHMETIC GEOMETRY" <https://math.mit.edu/~poonen/782/782notes.pdf> より引用： > **What is arithmetic geometry?** > > Algebraic geometry studies the set of solutions of a multivariable polynomial equation (or a system of such equations), usually over ${\bf R}$ or ${\bf C}$. ...[snip]... > > Arithmetic geometry is the same except that one is interested instead in the solutions where the coordinates lie in other fields that are usually far from being algebraically closed. Fields of special interest are ${\bf Q}$ (the field of rational numbers) and ${\bf F}_p$ (the finite field of $p$ elements), and their finite extensions. Also of interest are solutions with coordinates in ${\bf Z}$ (the ring of integers). 文法 AddArith で採用する記法は逆ポーランド記法。コネクティブ〈連結子〉（文法が提供する記号）は $\mrm{A}, \mrm{Z}$ の2つ。文法には、コンビネーション〈項〉の生成規則〈{production \| forming \| generation} rule〉とコンビネーション〈項〉の書き換え規則〈{rewrite \| reduction \| contraction \| simplification \| conversion \| transformation \| deformation \| mutation} rule〉がある。AddArith の規則を列挙する。生成規則： 1. $\mrm{Z}$ はコンビネーション〈項〉である。 2. $\alpha, \beta$ がコンビネーション〈項〉のとき、$(\alpha\;\beta\;\mrm{A})$ はコンビネーション〈項〉である。 3. 以上で生成されるものがコンビネーションのすべてである。書き換え規則：書き換えの記号に '$\rew$' を使う。 1. $((\alpha\; \beta\; \mrm{A})\; \gamma\; \mrm{A}) \rew (\alpha\; (\beta\; \gamma\; \mrm{A}) \; \mrm{A})$ と書き換えてよい。 2. $(\alpha\; \beta\; \mrm{A}) \rew (\beta\; \alpha\; \mrm{A})$ と書き換えてよい。 3. $(\alpha\; \mrm{Z}\; \mrm{A}) \rew \alpha$ と書き換えてよい。書き換え規則から同値関係を定義する方法は==幾つかある==が、ここではジグザグ同値〈zig-zag equivalence〉を使う。上記の基本書き換えと==その逆==を何度か（0回を含む有限回）適用した書き換えを、 $\quad \alpha \reww \beta$ と書く。 ==練習問題： 14== 文法 AddArith で生成されるコンビネーション〈項〉の例を5つ挙げよ。 ==練習問題： 15== $\alpha$ を、文法 AddArith で生成されるコンビネーション〈項〉だとして、$\alpha \reww \mrm{Z}$ と書き換え可能であることを示せ。上記練習問題の結果から、文法 AddArith だけだと面白くない。 ## AddArith に指標を付ける次の0-指標を考える（ターゲットはない）。 $\text{0-signature ABC }\;\{\\ \quad \text{0-mor }a\\ \quad \text{0-mor }b\\ \quad \text{0-mor }c\\ \}$ この指標を基にして拡張（後述）した文法 AddArith で生成したコンビネーションに、書き換え規則による同値関係で割った商集合を、 $\quad \mrm{Th}^{\mrm{AddArith}}(\text{ABC})$ と書く。この書き方は [B07 セオリー // セオリーと文法](https://hackmd.io/@m-hiyama/HyfJByJlc#%E3%82%BB%E3%82%AA%E3%83%AA%E3%83%BC%E3%81%A8%E6%96%87%E6%B3%95) 参照。 ==毎度困っている==ことだが、商集合にする前と商集合を区別する用語・記法がない。そのせいで線形結合の説明が混乱してしまった（例えば [3/ A08 過去の構文より現在の構文](https://hackmd.io/@m-hiyama/r1tKdWA1Y) 参照）。指標のフィルター付けを使うとちゃんと説明できるのだが、だいぶ面倒。とりあえず、商集合にする前の集合に生〈raw〉という形容詞を付けておく。 - $\mrm{RawTh}^{\mrm{AddArith}}(\text{ABC})$ ：生成規則で作った生のコンビネーション〈raw combination〉の集合、プレゼンテーション〈表示〉の集合ともいう - $\mrm{Th}^{\mrm{AddArith}}(\text{ABC})$ ：書き換え規則により移りあえる生のコンビネーションは同値とした同値関係で割った商集合、生のコンビネーションの同値類の集合商集合にする前と商集合にした後の==区別ができない／曖昧にする==ことが、教育過程全般に渡って悪影響を及ぼしていると思うのだが‥‥ 指標により拡張した生成規則は以下の通り。拡張した生成規則： 1. $\mrm{Z}$ はコンビネーション〈項〉である。 2. ［追加］$a, b, c$ はコンビネーション〈項〉である。 3. $\alpha, \beta$ がコンビネーション〈項〉のとき、$(\alpha\;\beta\;\mrm{A})$ はコンビネーション〈項〉である。 4. 以上で生成されるものがコンビネーションのすべてである。書き換え規則はそのまま使う。 ==練習問題： 16== $\mrm{RawTh}^{\mrm{AddArith}}(\text{ABC})$ の要素を5つ挙げよ。 ==練習問題： 17== $\mrm{Th}^{\mrm{AddArith}}(\text{ABC})$ が無限集合になることを示せ。 ==練習問題： 18== 指標 $\text{ABC}$ の場合と同様に生成規則を拡張するとして、$\mrm{Th}^{\mrm{AddArith}}(\text{0-signature }\{ \text{0-mor }a \} )$ をできるだけ具体的に記述せよ。 ==練習問題： 19== $\mrm{Th}^{\mrm{AddArith}}(\text{0-signature }\{ \})$ をできるだけ具体的に記述せよ。 ## AddArith に有法則指標を付ける次の0-指標を考える。 $\text{0-signature ABC2 }\;\{\\ \quad \text{0-mor }a\\ \quad \text{0-mor }b\\ \quad \text{0-mor }c\\ \quad \text{id 1-mor }bc: b \to c\\ \}$ この指標に対して文法 AddArith を適用するときは、次のように書き換え規則を追加する。拡張した書き換え規則： 1. ［追加］$b \rew c$ と書き換えてよい。 1. $((\alpha\; \beta\; \mrm{A})\; \gamma\; \mrm{A}) \rew (\alpha\; (\beta\; \gamma\; \mrm{A}) \; \mrm{A})$ と書き換えてよい。 2. $(\alpha\; \beta\; \mrm{A}) \rew (\beta\; \alpha\; \mrm{A})$ と書き換えてよい。 3. $(\alpha\; \mrm{Z}\; \mrm{A}) \rew \alpha$ と書き換えてよい。 ==練習問題： 20== $\mrm{Th}^{\mrm{AddArith}}(\text{ABC2})$ をできるだけ具体的に記述せよ。 ## AddArith にターゲット付き指標を付ける次の0-指標を考える。 $\text{0-signature ABCN within }{\bf N}\;\{\\ \quad \text{0-mor }a\\ \quad \text{0-mor }b\\ \quad \text{0-mor }c\\ \}$ ターゲット圏は ${\bf N}$ だが0-圏なのでターゲット集合である。ターゲット集合の要素を表す固有名をリテラル〈literal〉と呼ぶのだった。シングとリテラルは、3 と '3' のように区別すべきだが、ここでは（面倒なので）同じ書き方をする。文法 AddArith にリテラル 0, 1 を加えた文法を AddArith2 とする。AddArith2 と指標 ABCN の規則は次のようになる。拡張した生成規則： 1. $\mrm{Z}$ はコンビネーション〈項〉である。 2. ［追加］$0, 1$ はコンビネーション〈項〉である。 3. $\alpha, \beta$ がコンビネーション〈項〉のとき、$(\alpha\;\beta\;\mrm{A})$ はコンビネーション〈項〉である。 4. 以上で生成されるものがコンビネーションのすべてである。拡張した書き換え規則： 1. ［追加］$\mrm{Z} \rew 0$ と書き換えてよい。 1. $((\alpha\; \beta\; \mrm{A})\; \gamma\; \mrm{A}) \rew (\alpha\; (\beta\; \gamma\; \mrm{A}) \; \mrm{A})$ と書き換えてよい。 2. $(\alpha\; \beta\; \mrm{A}) \rew (\beta\; \alpha\; \mrm{A})$ と書き換えてよい。 3. $(\alpha\; \mrm{Z}\; \mrm{A}) \rew \alpha$ と書き換えてよい。 ==練習問題： 21== $\mrm{Th}^{\mrm{AddArith2}}(\text{ABCN})$ をできるだけ具体的に記述せよ。 ## 文法のドクトリン指標 0-指標から0-コンビネーション〈0-項〉を生成する0-文法である AddArith は、0-指標やターゲット集合により多少のカスタマイズをするが、「足し算の式」を生成することは間違いない。文法のメカニズムに、足し算の法則や足し算の計算法がエンコードされていることは分かるだろう。足し算を“支配”しているのは次の1-指標である。 $\text{1-signature CommMonoid within }\mrm{Seq}({\bf Set})\;\{\\ \quad \text{0-mor }U\\ \quad \text{1-mor } \mrm{A}:(U, U) \to (U)\\ \quad \text{1-mor } \mrm{Z}:() \to (U)\\ \quad \text{2-mor assoc } :: (\mrm{A}\times \id_{(U)});\mrm{A} \twoto (\id_{(U)} \times \mrm{A});\mrm{A} :(U, U, U) \to (U)\\ \quad \text{2-mor comm } :: \mrm{X}_{(U), (U)}; \mrm{A} \twoto \mrm{A} :(U, U) \to (U)\\ \quad \text{2-mor lunit } :: (\mrm{Z} \times \id_{(U)}); \mrm{A} \twoto \id_{(U)} : (U) \to (U)\\ \}$ この指標を、0-文法 AddArith のドクトリン指標〈doctrine signature〉と呼ぶ。 - 0-文法 AddArith のコネクティブ〈連結子〉は、ドクトリン1-指標 CommMonoid の1-ラベルである。 - 0-文法 AddArith の生成規則は、ドクトリン1-指標 CommMonoid の1-宣言文に対応する。 - 0-文法 AddArith の書き換え規則は、ドクトリン1-指標 CommMonoid の2-宣言文に対応する。文法はドクトリン指標で（細かいカスタマイズを除いて）決まってしまう。なので、文法とドクトリン指標を同一視することもある。その場合は： - 文法とは、1階層上位の（次元が1つ上がった）指標である。となる。