Caty-Jcentric 型理論／型推論／意味論

形式系の微妙なところ

http://d.hatena.ne.jp/m-hiyama-memo/20090828/1251438577 より（竹内本を参考）

意味じゃなくて、もっぱら記号の話。

1. 定数とarity 0の関数
2. 関数と演算子
3. fooとfoo()の区別
4. 関数の引数渡しのバリエーション：可変引数、省略とデフォルト値、名前付き引数
5. 関数記号と関係記号の区別
6. ソートを入れるか、特に真偽値のソート
7. 真偽値のソートがあれば、関係記号も論理記号も関数記号じゃ

追記：

• 構文と意味の区別は実際にはエエカゲン、ちゃんとやる人は滅多にいない。
• ちゃんとやればめんどくさい、エエカゲンだと混乱する。いつものジレンマ！
• やるなら、オーバーバーよりは太いブラケットが便利。
• 意味に対するコード（1つに定まる標準の表現／名前）はゲーデル記法。

setoid with restriction predicate

1. なんでsetoidか？ 「1 と 1.0 問題」 -- なんでもsetoid
2. setoid射 「1 と 1.0」のとき
3. setoid射 バッグ配列のとき
4. setoid射 dateを入れたとき -- 変わり続けるsetoid構造
5. なんで with restriction predicate か？ 「integer, number 問題」
6. type integer = number(isInteger = true);
7. enum [1, 2] ≡ number(enum = [1, 2]) 構文糖衣
8. integer, enum, スキーマ属性はすべて restriction predicateの例。

原子論理式

論理式	意味	記号の乱用
x is T	val[T](x)∈Val(T)	x ∈ T
S included T	Val(S) ⊆ Val(T)	S ⊆ T
S disjoint T	Val(S)∩Val(T) = 0	S ◇ T

「S ◇ T」は単なる略記で問題ないが、「x ∈ T」は相当にヤバイ。「S ⊆ T」も極めて不正確だが許して。

tag関数とtags関数

1. まったくの別物
2. 名前はtagだが、ほんとはタグとは限らない（暗黙タグも）
3. tagはインスタンス領域の全域関数
4. tagsは型表現に対して定義される（JSONインスタンスも型表現とみなせるが、でも）
5. x is T ならば、 tag(x)∈tags(T)

tags(T) が非空有限集合である型表現はプロパー（特殊でない）。

接頭辞

接頭辞記法 α=>T は説明のためだけに使う。

1. 予約語接頭辞：number, string, boolean, null, array, object, bag
2. 使用不可能：integer, tuple, list, enum, multi, その他の予約語
3. 特別扱い：any, never
4. 予約語ではないすべてのタグ名は接頭辞

tags(T) = {α} のときに限り、 α=>T と書いてよい。

型推論の演繹系

いずれは実装する。

1. 変数のない項（閉じた項）と変数のない論理式（文）だけを考える。
2. 仮定のない、絶対的な証明だけを考える。
3. 論理式は、原子論理式またはそれの連言に限る。
4. ホントの組み込み基本型は、number, string, boolean, null の4つだけとする。
5. 組み込み型と事前定義型（predefined type）は別。integerは事前定義型扱い。
6. 特別な型として、never, undefined, anyを使う。意味論では必須。
7. 関数形式型構成子は、array, object, bagの3つとする。
8. 演算子形式型構成子は、?, &, @name, | とする。
9. その他、制限述語。

変数のある項／論理式、仮定のある証明（この2者は相関している）もいずれは扱う。

外の圏と中の演算

http://d.hatena.ne.jp/m-hiyama-memo/20090828/1251436086 より：

JSON領域が含まれる外の圏に次の演算が入る。

1. (X, p)|(Y, q) := (X + Y, [p, q]) （[q, q]は余デカルトペア）
2. (X, p)*(Y, q) := (X×Y, p(*)q) （p(*)qは∧によるテンソル積）
3. (X, p)&(Y, q) := (X∩Y, p∧q)

JSON領域内では：

1. 制限された演算 |
2. キーを適当に決めてobject構成
3. 演算 &、ただし、結果的に X = Y となる。

曇ったスノーグローブ。

型推論のための定理

http://d.hatena.ne.jp/m-hiyama-memo/20090826/1251259922 より：

たいした内容ではないけど、名前を付けておこう。

1. タグ排他性の原理：α≠β ⇒ (@α A)∩(@β B) = 0
2. 単調性の原理：S ⊆T ⇒ tags(S)⊆tags(T)
3. ハテナ定理：正規形の式なら、一番外側の'?'で確定型か不確定型か判断できる。
4. ν（nu）定理：Tがプロパーなとき、ν(T) ≧ 1、ν(T) = n なら、Tはn成分のユニオンとして書ける。
5. 排他的包含の原理：(α=>A) ⊆ (β1=>B1 | ... |βn=>Bn) ⇔ α = βi で (α=>A) ⊆ (βi=>Bi)

タグ排他性の原理は、もっともベーシックな事実。単調性の原理と排他的包含の原理は、そうなるように作りましょう、という指導原理。ν定理も指導原理に近い。が、ハテナ定理は定理だ。

型表現のハテナ正規化

http://d.hatena.ne.jp/m-hiyama-memo/20090826/1251259924 より：

1. A?? → A?
2. (A?|B) → (A|B)? など
3. A? & B → A & B など
4. A? & B? → (A & B)?
5. bag [A?] → bag [A] (ハテナ定理には不要)
6. @name A? → @name A (ハテナ定理には不要)

ハテナ定理に必要なのは、演算子?, |, & に関する正規化だけ。

項の計算

1. ハテナ正規化は計算
2. 分配法則による展開は計算
3. & を下に押し込めて消してしまう計算

& の計算

1. array [Ai] & array [Bi] ⇒ array [Ai & Bi]
2. object {pi: Ai} & object {pi:Bi} ⇒ object {pi: Ai & Bi}
3. (bag [A]) & (bag [B]) ⇒ bag [A & B]
4. (@α A) & (@α B) ⇒ @α (A & B)

neverの計算

1. array [... never ...] ⇒ never
2. object {... never ...} ⇒ never
3. bug [never] ⇒ never
4. @α never ⇒ never
5. never & X ⇒ never
6. never | X = X

anyの計算

1. any & X ⇒ X
2. any | X 制約違反

分解還元法による演繹系

http://d.hatena.ne.jp/m-hiyama-memo/20090827/1251338342 より：

Catyの型推論のために、分解還元法というのを考えた。シーケント計算とタブローの中間のような感じのもの。推論は逆向きに（結論から仮定へと）行われるので、次の用語を導入する。

• 分解図 -- 推論図（1ステップ）の逆
• 還元図 -- 証明図（nステップ）の逆

シーケントに対応するのは、有限個(n≧0)の原子論理式をカンマで区切った列。列式、または単に式と呼ぶ。列式のなかの原子論理式は次のいずれか：

1. 真であるとすぐに判断できる。
2. 偽であるとすぐに判断できる。
3. 分解できる。

「真であるとすぐに判断できる」原子論理式は、aを基本型記号（basic type symbol）だとして、a⊆a か a⊆any のどちらかの形。あきらかに偽の論理式は色々ある。

分解とは、列式のなかの1個の原子論理式に注目して、それを1個以上の別な原子論理式の集合（構文的にはカンマ区切り列）に置き換えること。分解が p→q1, ..., qk のとき、次の性質が成立している。

1. |= p ⇔ |= (q1∧...∧qk)
2. rank(p) ＞ rank({q1, ..., qk})

上の主張が確認できるためには、原子論理式に対する意味論が定義されていることと、rankが定義されていることが必要。

意味論は意味領域がないとしょうがないが、rank関数は構文的に定義される。

1. 基本型記号のrankは0
2. 型項（型表現）のrankは、含まれる型関数記号、型演算子記号の総数。
3. 原子論理式のrankは、左右のrankの和
4. 列式のrankは、原子論理式rankの最大値

分解図では、上の式と下の式が意味論的には等価で、下の式のほうが確実にランクが下がっていることになる。常に分解可能性が保証できれば、ランクはゼロに落ちるから、列式の決定可能性が（メタ）証明できる。

意味論を適切に構成すれば、完全性（complete = sound and adequate）が成立する。完全になるように意味論を組み立てる、ってのがホントウのところだけど。

以上の話は、述語pに対する λx:A.p というラムダ式の定義域Aの議論。領域計算と呼びたいが、領域が多用されているから、台領域（キャリア；carrier）計算とでもするか。台の計算をもとにして、その上のラムダ式の計算が可能となる。ラムダ式の計算のほうが制限（restriction）計算となる。制限の実体はスキーマ属性だから属性計算と呼んでもいいかもしれない。

分解還元法の分解図

http://d.hatena.ne.jp/m-hiyama-memo/20090827/1251349683 より：

u = undefined として、記号の乱用で u = {u}。ブラケット内の数値はランクが減少する量。

●opt-right
          A ⊆ B+u

[u!∈A] -----------[-1]

          A ⊆ B
●opt-both

                A+u ⊆ B+u

[u!∈A, u!∈B] -----------[-2]

                 A ⊆ B
●object
  object {pi: Ai} ⊆ object {pi: Bi}

 ------------------------------------[-2]

       Ai ⊆ Bi  (i=1, ..., n)
●array
  array [Ai] ⊆ array [Bi]

 ------------------------------------[-2]

       Ai ⊆ Bi  (i=1, ..., n)
●union-left
  A|B ⊆ C

 ----------------[-1]

  A ⊆ C, B ⊆ C
●union-right
  α=>A ⊆ (α=>B | C)

 ----------------------[-1]

  A ⊆ B
●bag
   bag [A] ⊆ bag [B]

 --------------------[-2]

      A ⊆ B
●tagging
  @α A ⊆ @α B

 ----------------[-2]

   A ⊆ B
●intersection-right
  A ⊆ B & C

 ------------------[-1]

  A ⊆ B, A ⊆ C
●intersection-left
  α=>A & α=>B ⊆ α=>C

 ------------------------------[-1]

      α=>X ⊆ α=>C 

最後の「α=>X」のところをちゃんとやる必要がある。

それと次は「すぐに偽だとわかる」ケース。

                 A+u ⊆ B

[u!∈A, u!∈B] -----------

                  false