宣言、束縛子

名前〈ラベル〉と型項のペアを型宣言、あるいは単に宣言と呼ぶ。型項は判断のパック形式〈packed form〉のことがある。したがった、判断も宣言にエンコード〈パッキング〉できる。

宣言=型宣言を束縛子ということもある。名前を型に束縛するから。しかし、名前を値に束縛する割り当て〈assignment〉も束縛子とも呼ぶ。

  • 型束縛子〈型バインダー〉: 名前〈ラベル〉と型項のペア
  • 値束縛子〈値バインダー〉: 名前〈ラベル〉と値項=計算項のペア

型束縛子と値束縛子の依存タプル/依存レコードがコンテキストだが、コンテキストは引数リストやライブラリ/パッケージ形式にも使える。指標もコンテキストと思える。また、テレスコープとコンテキストは同義だと思ってもよい。

公平〈unbaiased〉なテレスコープ=コンテキストをカリー化することができる。プログラミング言語の実装は、テレスコープを直接扱うことは出来なくて、カリー化のパック形式が使われる。

  • アンカリー化したテレスコープ/判断は概念的
  • カリー化したパック形式は実装
  • 表層構文上は、テレスコープを空白区切りリストで表現できる。
  • コンテキスト内の宣言と、ステージ上の判断の相互変換(パックとアンパック)が重要だが、暗黙化される。

宣言だけからなるテレスコープと指標は同義。テレスコープは通常、判断のコンテキスト側に使うが、ターゲットにテレスコープを許す。ターゲットにもテレスコープを許した質問の答〈アンサー | ソリューション〉は手続き項

手続き項は手続きのボディにある。手続き自体は、ターゲットにテレスコープを許したフル判断〈項を入れた判断〉になる。

テレスコープ=指標を多少とした圏ができるが、複圏/多圏でないと定式化できない。意味論はグロタンディーク・ファイブレーション。

なお、テレスコープは $`\vec{x} \hat{:} \vec{T}`$ と書く。$`\vec{x}, \vec{T}`$ は、同じインデックスセット $`I`$ を持つラベルベクトルと型項ベクトル。次の形に展開される。

  • $`(x_i : T_i)_{i\in I} = (x_1 : T_1, \cdots, x_n : T_n)`$

テレスコープを含む判断は:

  • $`\Gamma, \vec{x} \hat{:} \vec{T} \vdash!\; \vec{y} \hat{:}\vec{S}`$
  • $`\Gamma, \vec{x} \hat{:} \vec{T} \vdash \vec{y} \;\widehat{:=}\; \vec{t} \hat{:}\vec{S}`$

コンストラクタ

  • 帰納的型の値コンストラクタ記号
  • 帰納的型の型名は、パラメータを持つと型コンストラクタ
  • 構造体型は、単一の値コンストラクタを持つ帰納的型だが、フィールド名をコンストラクタとも言う。
  • オブジェクト指向のコンストラクタは、単元集合またはパラメータ集合から状態空間への写像。
  • 型を値とする関数はコンストラクタ

構造体型のフィールド・ラベルはコンストラクタと呼ばないほうがいいだろう。が、構成素〈コンスティチューエント〉ラベルとは呼ぶ。

アロー型と依存アロー型とパイ型

依存アロー型とパイ型は同じもの。アロー型=指数型は依存アロー型の特別なもの。

Lean 4 で依存アロー型の書き方が (x:α) → β (βは型項)となったが、Agdaでは以前からこの形だったようだ。

  • Π(x:α), β ≡ ∀(x:α), β ≡ (x:α)→β

カリー化/アンカリー化は同じようにできる。

  • Γ |-! (x:α)→β ⇔ Γ, (x:α) |-! β
  • Γ |-? (x:α)→β ⇔ Γ, (x:α) |-? β
  • Γ |- t^:(x:α)→β ⇔ Γ, (x:α) |-! t: β

導入と除去の規則

型の導入規則とは、型の生成規則で、型だけではなくて要素の構成規則も含む。

  • 型を型構成子で生成する。
  • 要素を要素〈値〉構成子で生成する。要素生成子は関数である。

型の除去規則とは、型の消費規則で、関数による要素の構成規則(「構成」で間違ってない)も含む。

  • 既に型構成子で生成した型と要素がある。
  • その型の要素に関数を後結合子て消費すると、中間の型を除去した(カットした)要素が得られる。

次のようにも言える。

  • 導入規則は、複合型を域とする関数の構成法を与える。当該複合型の新しい証拠を生成する。
  • 除去規則は、複合型を余域とする関数の構成法を与える。当該複合型の既存証拠を消費して、新しい証拠を作る。
  • 複合型には、アロー型、依存アロー型、直積型〈タプル型〉、直和型〈タグ付きユニオン型〉、一般的帰納的型がある。
  • 一般的帰納的型の導入規則と除去規則は難しくなる。簡単な例はタグ付きユニオン型の、値コンストラクタとパターンマッチ分岐処理。

規則はコンビネータであり、そのコンビネータを使うコマンドでもある。また、関数は後結合/前結合でコンビネータとみなすことができる。And.intro は関数だが、And.introを後結合するコンビネータ doPostComp And.intro でもあり、コンビネータを入力シーケントに適用するコマンドでもある。

テキスト-ピクチャー対応

テキスト ピクチャー
ラベル(名前) ワイヤー頂点
型(命題含む) 色付きワイヤー
ストリング図
宣言 入力端頂点とワイヤー
コンテキスト ワイヤーパレット
シーケント ノード
公理シーケント 展開不可能ノード
割り当て 展開可能ノード
ステージ パレット付きキャンバス
コマンド アクション/マニピュレーション
  • ムービー(動画): ステージ/キャンバスの時間的変化の様子を記録したデータ
  • リプレイ〈再生〉: ムービーの再生実演
  • スクリプト: ムービーと等価な情報を持ったテキスト表現
  • 散文化: ムービーの内容を自然言語テキストに書き下すこと。

関数型言語では関数を表せない

※ 2023-01-17に書いたけど投稿忘れ。

関数型言語で、デカルト閉圏の射としての関数を表すことはできない。表わされるのは、関数型〈指数型〉の要素。要素をポインター関数とみなしても、表わされるのはポインター関数に限る。2つのポインター関数に対して、eval二項演算を施して結果を得る。結果も要素=ポインター関数。

論理への応用上は、心のなかでポインター関数を反カリー化して関数とみなす。この解釈の切り替えも負担になる。

カリー化した関数を $`\hat{f}`$ 、反カリー化した関数を $`\check{f}`$ と書くといいかも知れない。

続・演算子の優先度

※ 2023-01-17に書いたけど投稿忘れ。演算子の優先度 - (新) 檜山正幸のキマイラ飼育記 メモ編 の続き

Leanの場合、まだ調整は必要かも知れない:

  1. PrefixSuffixPrecidence 1024 = max
  2. ArgumentPrecidence 1023 = arg
  3. CompositionPrecedence 90 ($`\circ`$)
  4. ExponentialPrecedence 80 (^)
  5. MultiplicationPrecedence 70 (*)
  6. AdditionPrecedence 65 (+)
  7. BindPrecedence 55 (>>=)
  8. ComparisonPrecedence 50 (=)
  9. LogicalNegationPrecedence 40 (¬)
  10. LogicalConjunctionPrecedence 35 (∧)
  11. LogicalDisjunctionPrecedence 30 (∨)
  12. TernaryPrecedence 25 ( ? : )
  13. AssignmentPrecedence 20 (:←)
  14. PipePrecedence 10 = min (|>)

ステージとコマンド

「状況」、「シーン」なども用語候補だが、「ステージ」を使う。コマンドは、ステージ上の判断/質問を操作する。またステージ自体もコマンドで操作する。

同じ名前に対して、フォワードコマンド doXxx とバックワードコマンド undoXxx がある。

全般的な管理コマンド:

  1. New ステージ名 : 現在のステージの子ステージを作る。ステージは入れ子にできる。
  2. [α]> Remove i >[] : ステージ上の項目(判断または質問)αを、その名前または番号 i を指定して削除する。
  3. []> Put f >[α] : ステージ上に項目 α を新規に置く。f は項目それ自体、項目のパック形式、ライブラリやコンテキスト内の名前または番号。
  4. [Γ |-! A]> Enlarge >[Γ’ |-! A] : 判断のコンテキストを増やす。
  5. [Γ |-? A]> Shrink >[Γ’ |-? A] : 質問のコンテキストを減らす。

フォワード・コマンド:

  1. []> doObvious >[A |-! A] : 明白な判断を無から生成する。
  2. []> doWitness t >[Γ |-! A] : 証拠 t を持つ判断を無から生成する。
  3. [α]> doCurry >[α'] : カリー化する。
  4. [α]> doUncurry a >[α'] : 反カリー化する。aは使用する名前。
  5. [α1, ..., αn]> doPostComp f >[β] : 関数 f を後結合する。
  6. [αi]_{i∈)}> doTupple >[β] : タプルを作る。
  7. [αi]_{i∈)}> doCotupple >[β] : コタプルを作る。

バックワード・コマンド:

  1. [A |-? A]> undoObvious >[] : 明白な質問を消す(無に帰す)。
  2. [Γ |-? A]> undoWitness t >[] : 証拠 t を持つ判断を消す(無に帰す)。
  3. [α']> udoCurry a >[α] : 反カリー化する。aは使用する名前。
  4. [α']> undoUncurry >[α] : カリー化する。
  5. [β]> undoPostComp f >[α1, ..., αn] : 関数 f を後結合する前の状態に戻す。
  6. [β]> udoTupple >[αi]_{i∈)} : タプルを分解する。
  7. [β]> undoCotupple >[αi]_{i∈)} : コタプルを分解する。

リーズニングまでの4レベル

  1. 型 ←→ 命題 ←→ 対象
  2. 関数(要素含む) ←→ 定理(証拠含む) ←→ 射
  3. 関数コンビネータ ←→ 定理コネクティブ?(言及も命名もされない) ←→ オペレーター/コンビネータ
  4. リーズニング・コマンド 対応物がないゲーム・コマンド

圏論的に整理するなら

もの〈シング〉 操作
0-射=対象 対象コンビネータ
1-射=射 射コンビネータ

データの計算

もの〈シング〉 操作
データ型 型コンビネータ
関数 関数コンビネータ

論理の証明

もの〈シング〉 操作
命題 命題コンビネータ
定理 定理コンビネータ

必要な背景は次に書いてある。

型コンビネータ〈型構成子 | 型関数〉は、論理コネクティブと対応するから比較的に分かりやすい。関数コンビネータ〈オペレーター〉には:

  1. 結合〈フル結合〉
  2. 部分結合
  3. 直積
  4. ペアリング/タプリング
  5. コペアリング/コタプリング
  6. カリー化/アンカリー化

コマンドは関数コンビネータを使うが、どのシーケントのどの部分に関数コンビネータを適用するかまで指示〈インスラクション〉が必要。コマンドはゲームの状態遷移を引き起こすのであって、単純なオペレーターではない。

推論規則が曖昧なのは:

  • 定理=関数を推論規則と呼ぶことがある。
  • 定理コンビネータ=関数コンビネータを推論規則と呼ぶことがある。
  • リーズニング・コマンドを推論規則と呼ぶことがある。

関数コンビネータは高階関数で表現できるので、定理と定理コンビネータの混同は致し方ないかも知れない。コマンドは完全に状態機械の状態遷移の話で別!

コマンドプログラミングは、状態指向の手続き的プログラミングになる。

grep で前後の行も表示する

  • B -A が before, after のオプション。-B 3 -A 3 は単に -3 でも同じ。-C は -2 つまり -B 2 -A 2 と同じ。
 mathlib > git branch
* master

 mathlib > git rev-parse master
8618f40d51539454fe06511d5c8504a77f30c598

 mathlib > grep -A 3 -B 3 8618 ..\..\lake-manifest.json
  {"git":
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "subDir?": null,
    "rev": "8618f40d51539454fe06511d5c8504a77f30c598",
    "name": "mathlib",
    "inputRev?": null}},
  {"git":

プレ順序集合とその実例

structure PreOrder where
 U : Type
 le : U → U → Prop
 le_refl : ∀(x : U), le x x
 le_trans : ∀(x y z: U), (le x y ∧ le y z) → le x z

inductive ab where 
  | a
  | b

def ab_le (x : ab) (y : ab) : Prop :=
  match (x, y) with
  | (.a, _) => True
  | (.b, .a) => False
  | (.b, .b) => True

{U := ab, le := ab_le, .. } が実例になるには、le_refl, le_trans の証明が必要。

証明関係、混乱の原因

次を区別しなくてはならない。

  1. 命題
  2. 証明〈証拠〉
  3. 判断〈主張〉シーケント
  4. 質問〈問題 | 問い合わせ〉シーケント
  5. フォワードリーズニング(推論ルール含む)
  6. バックワードリーズニング(バックワード推論ルール含む)

定理は、証拠〈証明〉を引数として証拠を返す関数で、その型プロファイルがステートメント。判断シーケントは、コンテキストとターゲット命題のペアだが、意味的には証明項の存在の主張〈メタ命題〉。質問シーケント=ゴールは、コンテキストとターゲット命題のペアではあるが、証明項が不明で未知ラベル〈未知数〉になっている。

次の混乱がある。

  1. 命題(型)と証拠(要素)の混同
  2. 命題へのオペレーター(論理コネクティブ | 型演算)と証明へのオペレーター(推論 | 基本リーズニング | ルール)の混同
  3. 定理と、その定理を使ったルール(ポスト結合リーズニング)の混同
  4. 推論の意味が、定理または証明の基本構成素(関数)と、リーズニングの基本構成素(高階関数)でオーバーロードされている。どちらも関数だが、命題の要素が引数か、シーケントの集合が引数かの違いがある。

言葉として次が欠けている。

  1. FR=フォワードリーズニング
  2. BR=バックワードリーズニング
  3. FRルール=FRの基本構成素
  4. BRルール=BRの基本構成素
  5. 証明機械と証明状態〈ステージ〉
  6. FRコマンド(状態遷移)
  7. BRコマンド=タクティク(状態遷移)

ステージには判断と質問がいくつかあり、ステージ自体にコンテキスト(ステージ・コンテキスト=暗黙のコンテキスト)が付いている。コンテキストの変更は重要な操作になる。ステージコンテキストの背後にライブラリコンテキストがある。

ライブラリ、コンテキスト、ステージ、判断、質問、リーズニングルール、リーズニングコンビネータなど、命題以外のメカニズムを理解するのが困難。

追記:まとめ

「混同するな、区別しよう」「同じだから区別するな」を標語にまとめれば:

  1. 命題とその証拠は違う
  2. 証拠〈witness〉と証明〈proof〉は同じ
  3. 証拠と要素〈element〉も(宇宙多相で)同じ
  4. 証明にプロファイル〈シーケント〉とオプショナルに名前を明示すると定理
  5. 定理の引数は命題ではなくて証拠。
  6. 定理の戻り値も命題ではなくて証拠。
  7. 証明とリーズニングはまったく違う
  8. 定理はリーズニングの基本構成素になる。
  9. リーズニングの基本構成素をルールと呼ぶ。
  10. 定理と推論規則〈ルール〉と基本リーズニングは同じ
  11. 証明/定理は、FRコマンドに埋め込める。apply 定理
  12. 証明/定理は、BRコマンドに埋め込める。deapply 定理 だが、タクティク名は apply 、最悪。
  13. リーズニング(FRとBR)は、リーズニングステージの時間的推移過程を表すリーズニング図〈リーズニンググラフ〉で表現できる。
  14. リーズニング図のトランジションがリーズニング・コマンドで引き起こされる。