というか、ジェネリックに近いのかしら・・・
という話を、
■楽しい数学 第四夜 「同じ」を考えるー「型の理論入門」
で聞いてきたのでメモメモ（最後のほうに）
型の話
ヴオェボドスキー（Voevodsky）最近亡くなった：新しい型の考え方
はじめに
・同じとは
・今日は３部構成
１．同じ―哲学者の考え
２．同一性：概念の変化
→相対論では同時性が成り立たない
量子論→同じ素粒子
→不変性：変わらないものがないと、変わっていることが認識できない
→物理的同一性：情報
→エンタングルメント 量子テレポーテーション⇔量子はコピーできない
３．型の理論の成立
ラッセル
チャーチ：型つきラムダ計算
ホモトピー型理論 HOTT：Univalengt Axiom同じ価値
→コンピューターで証明
１．同じについて考える
・君が１０年前にイメージした「三角形」は、今僕はイメージした三角形と同じだろうか
→三角形の抽象概念としては同じ（比較不能）
・君の１０年と僕の１０年は、同じ１０年だろうか
→ちがう：同じ時の流れ（物理的な時間）は同じ
・１０年前の君と、今の君は同じか
→人は変わっても、アイデンティティは変わらない：同一性
人格：パーソナリティ
パーソナリティとアイデンティティの違い
→同一性？
性同一性障害は、パーソナリティの問題？アイデンティティの問題？
→今は性同一性障害という考えをとらない
・未来の人工知能は、人間と同じ何かを作り出すのだろうか
→その前に人間の能力の定義がいる
・哲学者たちが考えたこと
ユークリッド幾何学の公理：用語の関係
プラトンの「観念実在論」：イデア→観念が実在する
中世哲学「不変論争」：実在論、唯名論
ライプニッツ 不可識別者同一の原理
ヘーゲル 同一性と非同一性の同一性：同一性は、同一性と非同一性の同一性である？？
ヴィトゲンシュタイン：２つのものが同一だというのは無意味。
般若心経：色即是空
２．物理学と同一性
ミンコフスキー以前の時空像
歩行者のスピードによって、同時刻の空間は異なる
光円錐：外側に出ることはない（光より早く行けない）
→外側から因果関係を与えることはできない
→特殊相対論
アインシュタインは、時空の各点に時計を置いた
・量子論と同一性
原子論
ライプニッツの不可識別性の議論は、原子論・真空に反対するための議論だった
１９世紀でも原子の存在は、疑われていた
マッハ→ボルツマンいじめる→自殺する（カントールは発狂する）
・素粒子論は現代の原子論に他ならない
同じ状態にある量子は互いに区別できない
観測値が観測される確率が分かる→確率でしかわからない
・フェルミオンとボソン
半整数のスピンをもつ：フェルミオン
→クォーク、電子、ニュートリノ：物質を構成している
→同一の状態を占めることができない「パウリの排他律」
整数のスピンをもつ：ボソン
→光子・・・
・保存量の存在
エーミ
・ゲージ不変性
マックスウェルの電磁方程式
８つの方程式→ヘビーサイド ４つの方程式
アインシュタインの一般相対論と一般共変性
ネーターの定理：「対称性がじょぞんそくを導く」
ゲージ不変性
・エンタングルメント
EPRペア もつれあった２つのキュービット
→宇宙のかなたに行っても、結びつきは切れない
・量子力学と同一性
No Cloning定理：コピーできない
量子テレポーテーション：アリスのφがボブに移る→コピーでは？
アリスのφは失われる→観測するので
→誰も気が付かなかった。
アインシュタインはエンタングルメントは間違いだといった
３．数学と同一性
・ライプニッツ モナド
ライプニッツ
１．同一なものの不可識別性
２．等号の満たす性質「同値関係」
不可識別性から対称律は導かれる
カントールの集合理論
ラッセルの逆理：R∈Rとなってしまう：述語の適用
→ラッセルの型の理論に
チャーチのλ計算
１．αコンバージョン：変数は自由に変えられる
２．βリダクション：代入
３．ηコンバージョン：ｘで抽象化されたｆ（ｘ）がｆに等しい
λ計算への型の導入
カリーハワード対応と型つき
論理と型の理論の関係
PAT
型を持つλ式→と論理の→に対応がある
ハリーが１９６９年に気付き、１９８０年に論文
ディペンデントタイプセオリー
判断の概念は常に明大の概念に先立つ
証明
こるもろふ：命題を証明に変換する方法を構築すること
同一性の型
でぃぺんでんと たいぷ
パラメータによって、型が決まる→ポリふぉもにずむ
構造主義の原理→同型
カテゴリー論の同型：戻ってくる
同型を持っているときの不変性
カリーハワード：命題は、型である
オブジェクトの同一性
項の同一性、型の同一性
ゆにばらんす Axiom
２つのものの同一性は、２つのものの等価性と等価である
帰結として
構造主義の原理、
ライプニッツの原理をまとめる
HOTTでの同一性の解釈
という話を、
■楽しい数学 第四夜 「同じ」を考えるー「型の理論入門」
で聞いてきたのでメモメモ（最後のほうに）
型の話
ヴオェボドスキー（Voevodsky）最近亡くなった：新しい型の考え方
はじめに
・同じとは
・今日は３部構成
１．同じ―哲学者の考え
２．同一性：概念の変化
→相対論では同時性が成り立たない
量子論→同じ素粒子
→不変性：変わらないものがないと、変わっていることが認識できない
→物理的同一性：情報
→エンタングルメント 量子テレポーテーション⇔量子はコピーできない
３．型の理論の成立
ラッセル
チャーチ：型つきラムダ計算
ホモトピー型理論 HOTT：Univalengt Axiom同じ価値
→コンピューターで証明
１．同じについて考える
・君が１０年前にイメージした「三角形」は、今僕はイメージした三角形と同じだろうか
→三角形の抽象概念としては同じ（比較不能）
・君の１０年と僕の１０年は、同じ１０年だろうか
→ちがう：同じ時の流れ（物理的な時間）は同じ
・１０年前の君と、今の君は同じか
→人は変わっても、アイデンティティは変わらない：同一性
人格：パーソナリティ
パーソナリティとアイデンティティの違い
→同一性？
性同一性障害は、パーソナリティの問題？アイデンティティの問題？
→今は性同一性障害という考えをとらない
・未来の人工知能は、人間と同じ何かを作り出すのだろうか
→その前に人間の能力の定義がいる
・哲学者たちが考えたこと
ユークリッド幾何学の公理：用語の関係
プラトンの「観念実在論」：イデア→観念が実在する
中世哲学「不変論争」：実在論、唯名論
ライプニッツ 不可識別者同一の原理
ヘーゲル 同一性と非同一性の同一性：同一性は、同一性と非同一性の同一性である？？
ヴィトゲンシュタイン：２つのものが同一だというのは無意味。
般若心経：色即是空
２．物理学と同一性
ミンコフスキー以前の時空像
歩行者のスピードによって、同時刻の空間は異なる
光円錐：外側に出ることはない（光より早く行けない）
→外側から因果関係を与えることはできない
→特殊相対論
アインシュタインは、時空の各点に時計を置いた
・量子論と同一性
原子論
ライプニッツの不可識別性の議論は、原子論・真空に反対するための議論だった
１９世紀でも原子の存在は、疑われていた
マッハ→ボルツマンいじめる→自殺する（カントールは発狂する）
・素粒子論は現代の原子論に他ならない
同じ状態にある量子は互いに区別できない
観測値が観測される確率が分かる→確率でしかわからない
・フェルミオンとボソン
半整数のスピンをもつ：フェルミオン
→クォーク、電子、ニュートリノ：物質を構成している
→同一の状態を占めることができない「パウリの排他律」
整数のスピンをもつ：ボソン
→光子・・・
・保存量の存在
エーミ
・ゲージ不変性
マックスウェルの電磁方程式
８つの方程式→ヘビーサイド ４つの方程式
アインシュタインの一般相対論と一般共変性
ネーターの定理：「対称性がじょぞんそくを導く」
ゲージ不変性
・エンタングルメント
EPRペア もつれあった２つのキュービット
→宇宙のかなたに行っても、結びつきは切れない
・量子力学と同一性
No Cloning定理：コピーできない
量子テレポーテーション：アリスのφがボブに移る→コピーでは？
アリスのφは失われる→観測するので
→誰も気が付かなかった。
アインシュタインはエンタングルメントは間違いだといった
３．数学と同一性
・ライプニッツ モナド
ライプニッツ
１．同一なものの不可識別性
２．等号の満たす性質「同値関係」
不可識別性から対称律は導かれる
カントールの集合理論
ラッセルの逆理：R∈Rとなってしまう：述語の適用
→ラッセルの型の理論に
チャーチのλ計算
１．αコンバージョン：変数は自由に変えられる
２．βリダクション：代入
３．ηコンバージョン：ｘで抽象化されたｆ（ｘ）がｆに等しい
λ計算への型の導入
カリーハワード対応と型つき
論理と型の理論の関係
PAT
型を持つλ式→と論理の→に対応がある
ハリーが１９６９年に気付き、１９８０年に論文
ディペンデントタイプセオリー
判断の概念は常に明大の概念に先立つ
証明
こるもろふ：命題を証明に変換する方法を構築すること
同一性の型
でぃぺんでんと たいぷ
パラメータによって、型が決まる→ポリふぉもにずむ
構造主義の原理→同型
カテゴリー論の同型：戻ってくる
同型を持っているときの不変性
カリーハワード：命題は、型である
オブジェクトの同一性
項の同一性、型の同一性
ゆにばらんす Axiom
２つのものの同一性は、２つのものの等価性と等価である
帰結として
構造主義の原理、
ライプニッツの原理をまとめる
HOTTでの同一性の解釈
アクセス
トータル
ランキング
