矢印の奪い合い問題
- 含意を表す
- 指数型〈関数型 | アロー型〉を表す
- 射のプロファイルの区切り記号
- シーケントの区切り記号（前提と結論）
暫定的解決
- 含意と指数はカリー／ハワード対応により同一視して → を使う。
- 射のプロファイルの区切り記号にターンスタイル $`\vdash`$（\vdash） を使う。
- 射はバンチ複圏〈bunched multicategory〉の複射でもよい。バンチとして依存レコード〈テレスコープ〉を考えることが多い。
- 射のプロファイルとシーケントは同義語として、シーケントの区切り記号もターンスタイル〈turnstile〉を使う。
定義による効果： コンテキストの拡張・増大
定義によって何が生成されるか？ これも曖昧。
define function x:A := t
に対して、次の6つのモノが混合コンテキストに追加される。
- declared name x : A
- confiermed typing t:A
- assigned body x := t
- registered equation x ≡ t
- registered conversion x ~~> t
これらの追加〈append〉のためには、validityが必要。
- 名前が構文的に正しい名前である。
- 型項が構文的に正しい型項である。
- 値項が構文的に正しい項である。
- 型付け〈タイピング〉が正しい。
これらの検証〈チェック〉作業が終わると、コンテキストに追加されて、結果的にコンテキストが膨らむ。次の作業は、膨らんだコンテキストに基づいてなされる。
等号の奪い合い問題
- 定義的等号〈definitional equality symbol〉
- 命題的等号〈propositional equality symbol〉
- 述語記号〈predicate symbol〉
- n-圏のn-射
次のようにする。
- 定義的等号： ≡
- 命題的等号： =
- 述語記号： eq
- n-圏のn-射： ⇒ などの次元付き矢印記号と id-アノテーション
他に、一般的同値関係は ～ で表す。
判断、問題、解の区别
区別してない。
- 型つけ判断： judgement Γ |- t:A
- 型つけ問題： problem Γ |- t:?A
- 項構成問題： problem Γ |- ?t:A
- 存在判断： existential judgement Γ |- A
- 問題の解： solution of problem Γ |- t:?A
- 問題の解： solution of problem Γ |- ?t:A
- 問題の解： solution t of problem Γ |- t:A
- 問題の解： solution A of problem Γ |- t:A
- 相対判断： providing Γ judgement Δ |- t:A
- 相対問題： providing Γ problem Δ |- ?t:A
- 相対問題の解： providing Γ solution of problem Δ |- ?t:A
項構成問題に対して、順行ソルバーと逆行ソルバーがあり、ソルバーをプログラムとして作ることをソルバー・プログラミングと呼ぶ。特に、項が証明項のときの逆行ソルバーのプログラミングはタクティク・プログラミング。
事実と予告
宣言文が環境としての事実の宣言と、今後やることの予告の宣言がある。
declare defined succ: Nat |- Nat declare defining add: Nat, Nat |- Nat
自然言語風に書くと：
it's already defined succ: Nat |- Nat we will define add: Nat, Nat |- Nat
引数渡しとカリー化後の適用演算
f: A |- B と f': |- (A → B) があるとき、a: |- A に対して、
- a;f = a▷f = f◁a = f' a （ベータ等式）
f |→ f' というカリー化はコアージョンとして組み込まれている。その結果、カリー化したモノの名前はオーバーロードされる。
コロンの奪い合い問題
- 圏論： f: プロファイル でプロファイル宣言
- 型理論： a: 型 で型つけ宣言〈タイピング宣言〉
- (型理論 a:型) ⇔ (圏論 a: 1 |- 型)
- 圏論のプロファイル宣言は、フルカリー化して型理論のタイピング宣言にする。ここで齟齬が生まれる。
