3-signature {
 sort LoicalCat

 2-signature {
  /* Cは論理的圏の構造を持った圏
     Cでは、対象定数_Bや指数ベキが意味を持つ。
  */
  sort C in LogicalCat

  signature proposition, 命題, 真偽 {
   p:_1→_B
  }
  signature predicate, 述語, "propositional function", 命題関数 {
   sort X in C
   operation p:X→_B in C
  }

  signature "logical connective", 論理結合子, "truth function", 真理関数 (value n:_1→_N){
   opertion p: _B^n→_B in C
  }
 }
}

法則とは何かを示唆する指標と構成。インデントなしで書いている。

3-signature {
 sort CartCat
2-signature {
 /* Cはデカルト圏 */
 sort C in CartCat

signature PointedMagma {
 sort X in C
 operation m:X×X→X in C
 operation a:_1→X in C
}

constructin LeftUnitLaw from PoitedMagma to predicate {
 X := X
 p := λx∈X.(eq(m(i, x), x))
}

constructin LeftUnitLaw2 from PoitedMagma to proposition {
 p := ∀x∈X.(eq(m(i, x), x))
}

}
}

親子関係で入れ子になった指標や構成の書き方としてダブルギュメも使ってみる。

《3-sort CartCat |
  《2-sort C in CartCat |
    《1-sort X in C, 1-operation m:X×X→X in C, 1-operation a:_1→X in C |
        1-sort X := X in C
        1-operation p:X→_B := λx∈X.(eq(m(i, x), x)) in C
     》
   》
》

大きなラムダ式を含めて、ダブルギュメは何らかの構成の記述で、コンテキスト部がソース指標、ターゲット指標は暗黙に指定される。

2019-08-26

キーワード無し構文

セオリー論メモ

備忘録。

kは0以上の整数とする。使う記号。

記号	意味
in	~~アンビエント~~アビタを示す
from	構成のソース指標
to	構成のターゲット指標
k-σ	k-指標
k-γ	k-構成
k	k-射の宣言
:k	k重のコロン
→k	k重の矢印
:=	割り当て記号
( )	パラメトライズ
( )	気休め語〈consolation word〉
{ }	ブロック構造

気休め語〈consolation word〉は次の形で使える。

k-σ(fooBar)
k-γ(fooBar)
k(fooBar)
X(fooBar){ } パートのブロック、Xはラテン大文字

2019-08-26

項の使い方、ジニアロジー

セオリー論メモ

備忘録。

指標内で項を使ってよい。項は、プロファイルのなかで使える。ただし、当該の宣言文が出現する前に登場した（提供された）基本記号と、メタ指標（指標の指標＝親指標）のメタ記号を使って構成される項に限る。

一方で、構成〈construction〉でも項は使える。構成は（原則として）、割り当て文〈assignment statement | 代入文〉しかない。割り当て文の左辺は記号だけなので、項は割り当て文の右辺になる。右辺を割り当て文のボディとも呼ぶ。よって、割り当て文の項はボディ項〈body term〉という。

構成のボディ項は、構成のソース指標が提供する記号と構成のメタ指標の記号の組み合わせになる。

さて、なんらかのモノ（圏論的な実体／スタッフ）、またはモノを表す記号があるとき、その型つけ〈typeing〉は容易ではない。完全な型つけで得られる情報全体を、そのモノ（や記号）のジニアロジー〈系譜 | genealogy〉と呼ぶ。

ジニアロジーは、モノのクラス／指標／アンビエントを、無限の上方まですべて辿ったもの。ジニアロジーは、特定のモノを下端とする代数的ラダーで、代数的セオリーそのものだと言ってもよい。ジニアロジーは、モノに対する構文論・意味論の情報をすべて持っている。

2019-08-26

3つの等号

セオリー論本編ネタ

超越的等号：実質的に集合論の等号
(n+1)-射：n-圏の(n+1)-射としての等号
述語：トポスにおいて、対角射 Δ_A:A→A×A の特性射 eq:A×A→Ω。

2019-08-26

アドホック選択

セオリー論型理論プログラム意味論具体例本編ネタ

後で追加修正するかも。

指標の一覧：

名前	提供記号	ひとこと
Magma	*	乗法記号使ったマグマ
UnitalMagma	*, 1	単位的マグマ
MonoidAste	*, 1	モノイド
MonoidPlus	+, 0	モノイド
Group	*, 1, ~	群
AbGroupPlus	+, 0, -	アーベル群
Ring	+, 0, -, *, 1	可換とは限らない環
SemiRing	+, 0, *, 1	可換とは限らない半環
CommRing	+, 0, -, *, 1	可換環

指標の忘却関係

UnitalMagma →Magma
MonoidAste → UnitalMagma
Group → MonoidAste
AbGroupPlus → MonoidPlus
SemiRing → Ring
CommRing → Ring

集合の一覧：

名前	ひとこと
Real	実数
String	文字列
Vect3	3次元数ベクトル
SqMat[n]	n次元数正方行列

※ SqMat = square matrix

二項演算子のアドホック選択テーブル、指標を選ぶ：

	+	*
Real	CommRing	CommRing
String	MonoidPlus	UnitalMagma
Vect3	AbGroupPlus	Magma
SqMat[n]	Ring	Ring

※選択テーブル＝ルックアップ・テーブル

単項演算子のアドホック選択テーブル、指標を選ぶ：

	~	-
Real	なし	CommRing
String	なし	なし
Vect3	なし	AbGroup
SqMat[n]	なし	Ring

定数のアドホック選択テーブル、指標を選ぶ：

	0	1
Real	CommRing	CommRing
String	MonoidPlus	UnitalMagma
Vect3	AbGroupPlus	なし
SqMat[n]	Ring	Ring

実装の選択テーブル、指標の実装を選ぶ：

	Real	String	Vect3	SqMat[n]
Magma	なし	継承	Vect3Cross	なし
UnitalMagma	なし	StringMult	なし	なし
MonoidAste	なし	なし	なし	なし
MonoidPlus	なし	StringAdd	なし	なし
Group	なし	なし	なし	なし
AbGroupPlus	なし	なし	Vect3Add	なし
Ring	継承	なし	なし	AqMatRing[n]
SemiRing	継承	なし	なし	継承
CommRing	RealRing	なし	なし	なし

2019-08-23

言葉の整理

セオリー論型理論用語法

あまりにも車輪の再発明が凄まじ過ぎて、用法や雰囲気（だけ）が違う同義語が山のようだ。少し整理しておく。

基本レベルとは圏の次元を基準としたレイヤー番号のこと。基本レベルが1の存在物〈スタッフ〉はレイヤー1にいて、存在物の圏論的次元は1。

基本レベル k	k-クラス	k-インスタンス	圏論的には
0	集合, 型	要素,値, データ	要素 in 0-圏
1	2-型,種,型クラス	型,代数系,クラス実装	対象 in 1-圏
2	3-型,メタ種	種	1-圏 in 圏の2-圏

注意：

0-クラスは0-圏なので集合。プレーンな集合とは限らず、直積集合とか指数集合とかかも知れない。
0-インスタンスは0-クラスの対象なので、集合の要素。値、データだが、タプルデータや関数データもあり得る。
1-クラスは1-圏なので圏。プレーンな圏とは限らず、直積圏とか関手圏とかかも知れない。
1-インスタンスは1-クラスの対象なので、圏の対象。集合、構造付き集合、代数系だが、公理を満たす必要があるかも知れない。
2-クラスは2-圏。プレーンな2-圏とは限らず、直積2-圏とか関手2-圏とかかも知れない。
2-インスタンスは2-クラスの対象なので、2-圏の対象。圏、構造付き圏、代数圏だが、公理を満たす必要があるかも知れない。

0-インスタンスには、制約を満たす直積集合の要素が許されるから。データベース・レコードは0-インスタンスとなる。

0-インスタンスであるレコードを要素とする集合は0-クラスになる。したがって、データベース・テーブルは1-クラスになる。1-クラスは演算を持ってもいいので、オブジェクト指向クラスは1-クラスになる。オブジェクト指向クラスの1-インスタンスは、オブジェクト・インスタンスとしてのレコード・データである。

代数系、実装／（言語処理）エンジンは同義語だけど、言葉の運用が違う。A:Σ --◇ A' がAのプロファイルだとして：

Aは、A'におけるΣ-代数
Aは、ΣのA'{値}?エンジン
Aは、ΣのA'実装
Aは、(Σ, A')-クラスのインスタンス

次の記事を見て、言葉の運用も考えるとよい。

2019-08-23

放物線に制約された点のクラス

セオリー論型理論具体例課題

_R のような下線で始まる語は太字の代替で、固有名詞（特定インスタンスを指す名前）となる。

次元ごとに付けるキーワードは恣意的なので括弧に入れることにした。

1-sinature movable {
 0(sort) S in _Set
 1(mathod) moveBy:S×_R→S in _Set
 2(equation) assco:: for s in S. moveBy(moveBy(s, x), y) = moveBy(s, x+y) : S×_R×_R→S in _Set
 2(equation) unit:: for s in S. moveBy(s, 0) = s : S→S in _Set
}

0-signature parabola {
 0(slot) x in _R
 0(slot) y in _R
 1(constraint) con: x*x = y in _R
}

この2つの指標を組み合わせると、「放物線内に成約された点」のクラスが出来ると思うが、その構造を分析せよ。

一般に内部〈content〉を持つ台対象があり、内部の仕様も指標で書いたものがクラス定義になる。クラス定義を指標の立場から言えば、次元が異なる指標の組み合わせ。0次元指標のクラス（レコード集合）が、1次元指標の台対象（アンビエント圏の対象）を与える状況。

ここでも、対象とそのアロー化リフトである点射〈point morphism〉の関係を使っているような気がする。

アロー化リフトの解説：

n-圏Cを(n+1)圏D内で扱う方法のひとつ。n-圏Cは、内部に0-射からn-射を持つが、それを、外の(n+1)-圏Dの1-射から(n+1)-射に対応させて持ち上げる。キュリアの格上げと呼んでいたテクニック。

アロー化するには、外の(n+1)-圏Dに単位対象が必要。単位対象をIとして、a∈ ₀ C を、a~:I→C in D に対応させる。D(I, C) はDのホムシングなのでn-圏だが、ここにCをスッポリと埋め込むと C~⊆D(1, C) となる。

Cの内部構造は、D内にC~として展開されるので、Cの内部構造に言及する必要はなくなる。

2019-08-23

型の縦階層と横階層

セオリー論型理論本編ネタ

型階層を考える上で、型を分類する必要がある。

型と種
無構造型（集合）と構造付き型
単純型〈基本型 | 組み込み型〉と複合型〈構成型 | 複雑型〉
全域型と部分型〈制約型〉

型と種は縦階層。縦階層は、オブジェクトレベル、メタレベル、メタメタレベルのような階層で、タワー、ラダーなどと呼ぶ。異なるレベルをプレーンやレイヤーで識別する。階層グラフの辺はレイヤー間を必ずまたぐ。

横階層は、同一のプレーン／レイヤー内でのツリー構造やグラフ構造のこと。階層グラフは同一レイヤーにあるので、レイヤーをまたぐ辺はない。

グラフ形状が同じでも：

縦階層のグラフ（Nは自然数、Rは実数）

 モノイド圏の2圏
 ｜
 モノイドの圏
／＼
N　R

縦階層のグラフ

 モノイドの圏
 ｜
 N
／＼
1　3

横階層のグラフ（Cは複素数、2Zは偶数）

 C
 ｜
 R
／＼
N　2Z

横階層の場合でも、階層グラフの辺が何で与えられるか？が違う。

台集合の埋め込み写像で与えられる。部分型と全域型。
台集合の射影写像で与えられる。構造付き型の構造を忘れる。

これ以外の階層はうまくいかないことがあるし、この二種を混合するのはマズい。

階層の例：

図形クラスのクラス階層：点クラス、色付き点クラス、折れ線クラス、多辺形クラス
数系の包含階層：N⊆Z⊆Q⊆R
代数系の構造的階層：群、モノイド、半群、マグマ

階層グラフの辺の実体：

状態空間の射影写像
台集合の埋め込み写像〈包含写像〉
圏の忘却関手 ≒ 指標の埋め込み写像

階層構造を理解するとは、その階層グラフが世界のなかで、どのような形で配置されているかを正確に知ること。また、階層グラフの頂点と辺の実体が何であるかも正確に知ること。