檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2018-10-15 (月)

論理/メタ論理の記法をどうするか

| 16:05 | 論理/メタ論理の記法をどうするかを含むブックマーク

最近割と、論理/メタ論理の話をする機会があるのですが、そのとき、どんな書き方をすればいいか悩みます。

内容:

  1. キーワード方式とターンスタイル方式
  2. 正しさを分類する
  3. 書き方の変種や修飾
  4. 意味的帰結の書き方

キーワード方式とターンスタイル方式

正確な記述と演繹のための非日本語記法」で次のような書き方をしました。

For x∈R, y∈R.
For x ≧0, y ≧0.
  IsCorrect x + y ≧ 0

少し前までは、次のような書き方をしてました。これ(↓)は、誰か(誰だか忘れた)の真似をしたものです。

Given x∈R, y∈R.
Given x ≧0, y ≧0.
  Holds x + y ≧ 0

キーワードの差(ForとGiven、IsCorrectとHolds)以外何の違いもありません。IsCorrectとHoldsは、ターンスタイル記号'|-'と同じ意味です。論理/メタ論理における標準的記法はターンスタイル記号です。

ターンスタイル記号より、上に紹介した書き方がいい点は:

  1. 英単語由来のキーワードのほうが、見慣れない記号'|-'より幾分か親しみやすい。
  2. 文脈(前提)を、何行かに分けてグルーピングして書ける。

「幾分か親しみやすい」は気分的なもので、たいした理由ではないです。「何行かに分けて書ける」もターンスタイル記法でもやれば出来ます。文脈をグルーピングしたいなら、区切り記号(例えばスラッシュ)を導入すればいいでしょう。

x∈R, y∈R / x ≧0, y ≧0 |- x + y ≧ 0

どう書こうが同じだろ、ってのが僕の感想ですが、“気分的な差”とか“視覚的な(見た目の)差”とかが実にバカにできなくて、「どう書くべきか」の判断は難しくなります。

正しさを分類する

前節のキーワード 'IsCorrect', 'Holds' は、「正しい」「成立する」という意味です。それ以上の説明は要らないように思えますが、そうではありません。メタ論理(モデル論や証明論)のモットーは、正しさや成立することを厳密に分析することです。

少なくとも、'|-'(ターンスタイル記号)と'|='(ダブルターンスタイル記号)はシッカリと区別する必要があります。ターンスタイル記号は“構文的に正しい”、ダブルターンスタイル記号は“意味的に正しい”という主張(に使う記号)です。今日は、内容的説明をする気はなくて、記法の話ですから、“構文的に正しい”と“意味的に正しい”がどう違うかは説明しません。

'|-' と '|=' をキーワードにするなら何がいいのだろう? 'IsProvable'と'IsValid'かな。

  • IsProvable x + y ≧ 0
  • IsValid x + y ≧ 0

'|-' と '|=' は、形は似てますが、使い方がだいぶ違います。'|-'の左側には証明の前提を書きます。

  • x ≧0, y ≧0 |- x + y ≧ 0

キーワードで書くなら(ピリオド打つのはやめた)、

For x ≧0, y ≧0
IsProvable  x + y ≧ 0

あるいは、

Given x ≧0, y ≧0
IsProvable  x + y ≧ 0

なんかGivenのほうがいいような気がしてきた。まったくの気分だが。

'|='の左側には、右側の命題を成立させるモデルを書きます。モデルとは、命題を解釈するための構造です。例えば、自然数の変数・定数・演算・関係を使うモデルをN-model、実数の変数・定数・演算・関係を使うモデルをR-modelとしたとき:

  • N-model |= ∀x, y.(x + y ≧ 0)
  • R-model |=/ ∀x, y.(x + y ≧ 0)

'|=/'は「正しくない」の意味です。全称限量子を付けないで、自由変数が残っていると妥当性〈validity〉の判断はできません。

  • R-model |= x + y ≧ 0 (なんともいえない)

変数への具体的な値の割り当てを、変数の状態〈state〉、束縛〈binding〉、付値〈valuation〉などと呼びます。状態まで付ければ妥当性が判断できます。

  • (R-model, {x←1, y←1}) |= x + y ≧ 0
  • (R-model, {x←0, y←(-1)}) |=/ x + y ≧ 0

状態の記述に'←'を使ったのは臨時の記法です(特に正式な記法はないと思います)*1

書き方の変種や修飾

'|-'で示す証明可能性は、証明を行う仕掛けである演繹系〈deduction system | 証明系〉が決まらないと定義できません。演繹系をSとして、「Sにより証明可能」は '|-S' を使えばいいでしょう。

  • x ≧0, y ≧0 |-S x + y ≧ 0

キーワード方式だと:

Given x ≧0, y ≧0
IsProvableBy S  x + y ≧ 0

By S はお尻のほうがいいか。

Given x ≧0, y ≧0
IsProvable x + y ≧ 0 By S

キーワードを使うと、“気分”と“見た目”が気になりだす。やはり、自然言語には言霊が宿るせいか?

'|='では、基本的には左側にモデルを書くのですが、何も書かないときがあります。

  • |= ∀x, y.(x + y ≧ 0)

実は、左が空白のときの解釈が場合により違うんですよ。ヤダナー。

  1. モデルをひとつに固定しているので、あえてモデルは書かない。
  2. 複数のモデルを想定するが、左側空白は、どのモデルに対しても成立することを意味する。

モデルがひとつであってもチャンと書くことにして、複数のモデルのどれでも成立するならワイルドカードの'*'を付けるとかすれば混乱は少ないでしょう。

  • N-model |= ∀x, y.(x + y ≧ 0)
  • * |= ∀x, y.(x + y ≧ 0)

モデルの集まりをMとして、左側にはモデルの集まりを書く約束なら:

  • {N-model} |= ∀x, y.(x + y ≧ 0)
  • M |= ∀x, y.(x + y ≧ 0)

左側にモデルの集まりを書く習慣はたぶんないと思うけど、「何も書かないで省略する」はたいていトラブルを招くんだよなー。

意味的帰結の書き方

ダブルターンスタイル'|='の左側にはモデルを書くので、論理式を書くことはできません。しかし、意味的判断で左側に論理式を書きたいことがあります。標準的記号がないので、僕は'|⇒'を使っています。

  • x ≧0, y ≧0 |⇒ x + y ≧ 0

これは、次の意味です。

  • いま考えているどんなモデルMと状態ρに対しても、 (M, ρ) |= x ≧0 かつ (M, ρ) |= y ≧0 ならば、(M, ρ) |= x + y ≧ 0 である。

論理式 A1, ..., An, B のあいだの関係 A1, ..., An |⇒ B は、通常は論理的帰結〈logical consequence〉と呼びます。しかし、これは意味的判断なので、意味的帰結〈semantic consequence〉と呼んだほうが適切でしょう。意味的帰結を伴意〈entailment〉ともいいます。次の記事を参照してください。

意味的帰結〈伴意〉を'|⇒'で表すと、左側に論理式を書けるようになりますが、今度は判断の根拠であるモデルの集まりが書けなくなります。右下添字かな。

  • x ≧0, y ≧0 |⇒M x + y ≧ 0

Mは、モデル(と状態)の集まりで、この意味的帰結を主張するときの根拠となったものです。こう約束すると、次の2つの書き方は同じ意味になります。

  1. M |= x + y ≧ 0
  2. |⇒M x + y ≧ 0

'|-' と '|=' は似てませんが、'|-' と '|⇒' は似た使い方ができます。左側に前提となる命題の並び、右下添字に判断の根拠となる仕掛けや集まりを書くことになります。'|=' は、'|⇒' を定義するための補助的なものと捉えたほうがいいような気がします。


関係しそうな過去記事:

*1:「型推論に関わる論理の概念と用語 その6:substitutionの記法」で色々な記法があることを書きました。状態〈束縛 | 付値〉と置換〈substitution | 代入〉は似てますが違う概念です。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20181015

2018-10-11 (木)

simulate

| 12:41 | simulateを含むブックマーク

"simulate"を「シュミレート」と言ってしまう、ときに「シュミレート」と書いてしまう。知っていても言ってしまう/書いてしまう。ウーム。

なんでだろう? 「シミュ」が発音しにくいことが原因のひとつだと思う。「シミュ・レート」とちゃんと発音しようとすると、「ミュ」で口をとんがらかす必要があり、負担がかかる。「シュミ」は言いやすい -- 「趣味」という日本語と同じ。

ジジ臭い感じにはなるが「シミ・レート」を心がけることにしようかな。「シミュ・レート」よりは楽に発音できる。「趣味・レート」から「染み・レート」へ。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20181011

2018-10-10 (水)

クリーネ代数 再論

| 10:07 | クリーネ代数 再論を含むブックマーク

クリーネ代数の圏化: ちょびっと」で、クリーネ代数を幾つかの方法で圏化/無限タワー化したら面白いかもなー、と書きました。で、圏化のもとになるクリーネ代数ですが、何度も取り上げている割には定義はしたことないですね。定義は「探せばあるだろう」という前提ですが、圏化を見越した定義を改めてしておいたほうがいいかな、と思いました。

内容:

  1. 何に使えるのか/何に使いたいのか
  2. クリーネ代数とは何か
  3. 順序構造と最小不動点
  4. クリーネ代数の定義
  5. 可換性とベキ等性
  6. コンウェイ半環

何に使えるのか/何に使いたいのか

「クリーネ代数〈Kleene algebra〉とは何か」の前に、クリーネ代数は何に使えるのか? 僕が何に使いたいと思っていた/いるのかを説明します。僕が想定している用途は主に2つで、

  1. プログラム意味論
  2. 形式言語理論

です。今ここではプログラム意味論のほうだけ述べます。クリーネ代数は、非決定性プログラムの記述と分析に使えます。だいぶ古いですが、次の3つの記事を読むと事情はわかるでしょう。

非決定性プログラムの意味論をやりたい場合は、単なるクリーネ代数ではなくて、論理条件〈logical condition〉に相当するテストも入れたほうが便利です。これはテスト付きクリーネ代数〈Kleene algebra with tests〉です。テスト付きクリーネ代数については、次の記事で書いています。

テスト付きクリーネ代数を使えば、if文やwhile文も代数的に定義できます。ホーア論理〈Hoare logic〉を組み立てることもできます。以下の記事はホーア論理に関するものですが、テストフレームワークを実際に作っていたときに書いた記事なので、現実的な考慮が色々入っていて、理論的な筋は若干見えにくいかも知れません。

クリーネ代数とはちょっと離れますが、ホーア論理の圏論的扱いについては:

というわけで、クリーネ代数/テスト付きクリーネ代数は、プログラムの振る舞いの分析、仕様記述の手法、テストフレームワークの作り方などに具体的な示唆を与えてくれます。これが、クリーネ代数/テスト付きクリーネ代数に興味を持つ(ひとつの、しかし大きな)動機です。

クリーネ代数とは何か

クリーネ代数を一言でいえば、アフィン線形不動点方程式を扱うための代数系です。となると、アフィン線形不動点方程式とは何か、から説明を始めるべきでしょう。

次は中学校で習った1次関数です。

  • f(x) = ax + b

aを比例定数〈proportionality constant | coefficient of proportionality | proportional coefficient〉、bを定数項〈constant term〉と呼びます。関数のグラフの形状から、aを傾き、bをy切片とも呼びますね。

アフィン線形関数〈affine linear {function | map | mapping}〉は1次関数の別名に過ぎません。fをアフィン線形関数として、次の形の方程式をアフィン線形不動点方程式〈affine linear fixed point equation〉と呼びます*1

  • f(x) = x

f(x)の定数項が特に1の場合は:

  • ax + 1 = x

この形のアフィン線形不動点方程式の解は、比例定数aだけから決まるので、それをa*と書きます。このa*のaのクリーネスター〈Kleene star〉と呼びます。つまり、次が成立することになります。

  • aa* + 1 = a*

両辺に右からbを掛けると:

  • a(a*b) + b = a*b

したがって、a*b は、一般的アフィン線形不動点方程式 ax + b = x の解です。

以上のような議論ができるためには、a, b, xが所属する代数系に何が要求され、何は要求されないでしょうか?

  • 足し算と掛け算がないと、1次式(アフィン線形式) ax + b が書けないので、足し算と掛け算は必要。
  • しかし、引き算と割り算はなくてもよい。
  • ax と xa を別に扱えば、掛け算の可換性も必要ない。

というわけで、アフィン線形不動点方程式を云々するには、足し算と(可換とは限らない)掛け算を持っている代数系が必要です。そのような代数系を半環〈semiring〉と呼びます。

クリーネ代数は、半環に、アフィン線形不動点方程式の解を与えるクリーネスターが付いたものです。が、もう少し構造が要求されます。それは実例を挙げた後で説明します。

順序構造と最小不動点

H = {x∈R | x ≧ 0}∪{∞} とします。∞はどの実数よりも大きいとします。足し算と掛け算は普通どおりですが、∞との足し算・掛け算は別途定義します。

x, yを非負実際として、

足す x
y x + y

x, yを正実数として、

掛ける 0 x
0 0 0 0
y 0 xy
0

この定義で、足し算・掛け算の計算法則はすべて成立します(引き算・割り算は考えない)。クリーネスターは次のように定義します。

  • 0 ≦ a < 1 のとき、a* := 1/(1 - a)
  • 1 ≦ a のとき、a* := ∞

ここで、1/(1 - a) に引き算と割り算を使ってますが、これはクリーネスターの定義のなかで実数の引き算/割り算を使っているだけで、H上の演算として引き算/割り算を認めているわけではありません。

記号の乱用で、H = (H, +, 0, ・, 1, (-)*) と定義します。・は掛け算です。Hは足し算/掛け算/クリーネスターを持った代数系です。

今定義したクリーネスター付き半環Hにおいて、アフィン線形不動点方程式 ax + b = x の具体例として、a = 1/2, b = 1 を考えると、

  • (1/2)x + 1 = x

x = 2 は不動点方程式の解ですが、x = ∞ も解です。一般に、アフィン線形不動点方程式の解はひとつとは限りません。クリーネスターa*は、ax + 1 = x の最小の解とします。最小が意味を持つためには、大小が比較可能、つまり順序構造を持つ必要があります。

クリーネ代数の要件として順序構造も追加すると:

  • クリーネ代数は、足し算、掛け算、順序を持つ順序半環である必要がある。
  • クリーネスターa*は、ax + 1 = x の最小の解を与える。

クリーネ代数の定義

クリーネ代数の公理を整備したのはデクスター・コゥゼン(Dexter Kozen)です。コゥゼンの定義では、足し算はベキ等、つまり a + a = a を仮定します。しかし、ベキ等性は要らない(強すぎる)でしょう。ベキ等性を要求すると、前節のHは除外されてしまいます。僕は、Hはクリーネ代数の仲間に入れてもいいと思うのです。

足し算のベキ等性は、半環上に順序を定義するために使われるのですが、足し算から誘導しなくても、順序が最初から在るとすればいいでしょう。クリーネ代数の下部構造を、ベキ等半環〈idemopotent semiring | ISR〉から順序半環〈ordered semiring | OSR〉に切り替えればいいのです。正確に言うと、0 ≦ a が成立する順序半環です。念の為、公理を書き出しておきます。以下の8番目までが半環の定義、その後は順序に関する定義です。全ての等式・不等式の前に全称限量子が付きますが、通常の習慣(悪習)にしたがって省略します。

  1. (a + b) + c = a + (b + c)
  2. 0 + a = a + 0 = a
  3. a + b = b + a
  4. (a・b)・c = a・(b・c)
  5. 1・a = a・1 = a
  6. 0・a = a・0 = 0
  7. a・(b + c) = a・b + a・c
  8. (a + b)・c = a・c + b・c
  9. ≦ は順序関係(全順序とは限らない)
  10. 0 ≦ a
  11. a ≦ b ⇒ a + c ≦ b + c
  12. a ≦ b ⇒ a・c ≦ b・c
  13. a ≦ b ⇒ c・a ≦ c・b

Hはこれらの公理を満たします。ZRでは ∀a.(0 ≦ a) が成立しないので、ZRは上記の公理は満たしません。

さて、Kは今提示した公理を満たす順序半環だとします。Kは半環なので、アフィン線形関数 f:K→K, f(x) = ax + b を考えることができます。t∈K がfの前不動点〈pre-fixed point | pre-fixpoint〉だとは、次が成立することです。

  • f(t) ≦ t

最小不動点〈least fixed point〉であることは、最小前不動点〈least pre-fixed point〉であることと同じな同様に扱えるので、次の2つの条件を満たすtは最小不動点となりみなせます。

  1. f(t) ≦ t (tは前不動点である)
  2. ∀x∈K.(f(x) ≦ x ⇒ t ≦ x) (前不動点のなかではtが最小)

[追記]等式で定義される不動点と不等式で定義される不動点は、似た扱いはできますが、完全に同じと言うのは不適切でした。ホントに同じなら区別する必要がなくなるので。最後の節に書いたように、不等式的不動点理論と等式的不動点理論の差と関連を僕は理解してないのですが、安直に同じってのはマズイですね。[/追記]

f(x) = ax + b と展開した形で書くと:

  1. at + b ≦ t
  2. ∀x∈K.(ax + b ≦ x ⇒ t ≦ x)

aのクリーネスターa*を使えば、t = a*b で与えられるはずなので、

  1. a(a*b) + b ≦ a*b
  2. ∀x∈K.(ax + b ≦ x ⇒ a*b ≦ x)

一番目の不等式を簡略化して:

  1. aa* + 1 ≦ a*
  2. ∀x∈K.(ax + b ≦ x ⇒ a*b ≦ x)

これがクリーネスターを規定する公理です。順序半環Kと、写像 (-)*:K→K の組 (K, (-)*) が上記の2つの公理を満たすとき、右クリーネ代数〈right Kleene algebra〉と呼ぶことにします。なぜ「右」が付くのかは次節で。

可換性とベキ等性

クリーネ代数の定義では、掛け算の可換性は仮定しません。例えば、Kが非決定性プログラムの代数だとすると、掛け算はプログラムの順次結合なので、まったく可換ではありません。非可換の場合は、一次式〈アフィン線形式〉は2種類になります。

  1. ax + b
  2. xa + b

比例定数を左から掛けるバージョンと右から掛けるバージョンです。比例定数ではなくて変数の位置のほうに注目すると、上が右アフィン線形式、下を左アフィン線形式と呼びましょう。毎度注意してますが、左右の決め方は恣意的なので、二種類を区別する以外の意味は何もありません。

前節では、右アフィン線形不動点方程式に基づきクリーネ代数を定義しました。なので、右クリーネ代数です。左アフィン線形不動点方程式に基づき定義すれば、左クリーネ代数〈left Kleene algebra〉になります。左クリーネ代数を定義する公理は:

  1. a*a + 1 ≦ a*
  2. ∀x∈K.(xa + b ≦ x ⇒ ba* ≦ x)

ひとつのクリーネスター(-)*が、同時に右クリーネ代数と左クリーネ代数の構造を与えるとき、(K, (-)*) をクリーネ代数〈Kleene algebra〉と呼びます。

下部構造の順序半環が可換のとき、左右の区別はなくなるので、右クリーネ代数は左クリーネ代数にもなり、常にクリーネ代数になります。

半環の足し算がベキ等で、順序と整合している(a + b = b ⇔ a ≦ b)とき、クリーネ代数はベキ等クリーネ代数〈idempotent Kleene algebra〉です。コォゼンのオリジナルの定義によるクリーネ代数は、ベキ等クリーネ代数のことです。ベキ等性を外すとうまくいかないことも当然にあるでしょう。そのときはベキ等性を追加します*2

コンウェイ半環

前節まででクリーネ代数の話はオシマイ。この節はオマケです。

不動点を扱うための代数系というと、コンウェイ半環〈Conway semiring〉もあります。ちなみに、コンウェイ代数〈Conway algebra〉は別な代数系を意味するので、コンウェイ半環と呼びます。

コンウェイ半環は、スターオペレータを持つ半環 L = (L, (-)*) で、次の等式を満たすものです。

  1. (a + b)* = (a*b)*a* --(和スター等式)
  2. (ab)* = 1 + a(ba)*b --(積スター等式)

和スター等式(公式)については、次の記事で説明しています。

クリーネ代数は不等号(順序)に基づく法則で規定されますが、コンウェイ半環は、完全に等式的な代数系です。この2つは別物なんですが、圏化するとクリーネ代数とコンウェイ半環の違いはハッキリしなくなります。不動点を扱う圏は、クリーネ代数の圏化とも言えるし、コンウェイ代数の圏化とも言えるような圏になります(たぶん、だいたい)。

クリーネ代数とコンウェイ半環は別だが似てるのは知ってました。が、相互関係を僕は理解してません。圏化すると、ほんとに違いが消えるのか、やっぱり別な圏になるのか? 正確には知らないなー。気力が湧いたら考えます。

*1:不動点は、"fixed point", "fix point, "fixpoint", "fixed-point", "fix-point"などの表記の揺れがあるので、検索しにくいですね。

*2[追記]ベキ等性をいったん外したのは、ベキ等性の役割をハッキリさせたかったからです。もし、大部分の結果がベキ等性に依存していることが分かれば、ベキ等性は最初から入れたほうがいいでしょう。[/追記]

トラックバック - http://d.hatena.ne.jp/m-hiyama/20181010

2018-10-09 (火)

クリーネ代数の圏化: ちょびっと

| 13:44 | クリーネ代数の圏化: ちょびっとを含むブックマーク

マイクロコスモ原理とクリーネ構造」の続きの話。ほんのちょびっと分かったこと。

内容:

  1. 圏化の多様性
  2. 狭義の圏化と亜化〈oidification〉
  3. クリーネ代数の場合は

圏化の多様性

前の記事に書いたように、僕は、クリーネ代数に関して「なんか違う」「なんか足りない」という感じをいだいてました。

今思えば、それは「クリーネ代数を圏化〈categorify〉せねば」という感覚だったのかも知れません。トレース付きデカルト圏は、クリーネ代数の圏化と捉えることができます。クリーネ代数より強力で使いやすいです。で、それで「めでたし、めでたし」なのかと言うと、そうでもないのです。

クリーネ代数の圏化がトレース付きデカルト圏だけでよいのか? どうもそうじゃない。クリーネ代数の特徴的機能であるクリーネスターに関しては、大規模な一般化ができそうな気配があります。

トレース付きデカルト圏は、クリーネ代数の圏化の one of them に過ぎないのではないか? 他にもっと別な圏化があるのではないか? -- こういう問に答えが出てないので、スッキリしない。「マイクロコスモ原理とクリーネ構造」でも、次のように書いています。

マイクロコスモ原理を信じるなら、1-クリーネ構造=クリーネ代数、2-クリーネ構造=クリーネ圏、3-クリーネ構造=メタ・クリーネ圏、… というクリーネ構造の無限タワーがあるはずです。構造の無基底性・多様性から、無限タワーが一意ではなくてたくさんのバリアントがあるかも知れません。

「たくさんのバリアント」がどんなものなのか、もっと具体的に分からないと、スッキリはしないですよね。「マイクロコスモ原理とクリーネ構造」の記述では(修正はしませんけど)、複数の圏化がゴッチャになって書かれているようです。状況が整理されてないですね。

狭義の圏化と亜化〈oidification〉

確かバエズ〈John C. Baez〉が言っていたと思うんだけど、圏化には少なくとも二種類があると(もっとあるかも知れないが)。何らかの概念Xに対して、X categoryと名付けるタイプの圏化と、X-oidと名付けるタイプの圏化です。

名付けの際に、語尾を形容詞にするとか綴り・発音を整えるとかしないことにして、「X → X category」タイプの典型例は「monoid → monoid category」(= monoidal category)です。「X → X-oid」の典型例は「group → group-oid」(= groupoid)です。日本語訳が難しいけど、前者を狭義の圏化、後者を亜化としておきます(苦しい訳だ)。「X圏化」と「亜X化」のほうが落ち着くかな。

X圏化は、集合を台〈underlying thing〉とする構造を、圏を台とする構造に拡張することです。集合を台とする構造Xとそのあいだの準同型写像からなる圏を太字のXとします。X圏化した構造とそのあいだの関手からなる圏をXCatとします(自然変換は考えないことにします)。そのとき、次の図式が可換になります。

 X - D → XCat
 |     |
 U     U
 |     |
 v     v
Set- D → Cat

ここで、Uは台集合/台圏を対応させる忘却関手、Dは集合を離散圏として埋め込む関手です。X = Monoidの場合なら:

Monoid-D→ MonoidCat
 |     |
 U     U
 |     |
 v     v
Set - D → Cat

この可換図式からX圏化の特徴はつかめるでしょう。

亜X化は、対象が1つだけの亜XとしてXが再現するような拡張です。亜X化した構造とそのあいだの関手からなる圏をX-oidとします。そのとき、次の圏同値が成立します。

  • X ¥stackrel{¥sim}{=} X-oid1ob

ここで、X-oid1ob は、単対象X-oidからなる部分圏です。X = Group の場合なら:

  • Group ¥stackrel{¥sim}{=} Group-oid1ob

Group-oidのエンドセットGroup-oid(A, A)は、すべて群の構造を持つので、一般的X-oidの圏X-oidにおいても、エンドセットX-oid(A, A)がXの対象という状況を考えるのもアリです。

クリーネ代数の場合は

クリーネ代数の圏化の場合も、X圏化と亜X化を考えることができます。トレース付きデカルト圏、半加法圏〈双積圏〉などは、亜X化の意味でのクリーネ代数の圏化です。つまり、KleeneAlgebra-oidを求める方向ですね。それとは別に、KleeneAlgebraCategoryを求める方向もあるわけです。

どうも僕は、KleeneAlgebra-oidとKleeneAlgebraCategoryをゴッチャにしてきたようです。関連はあるでしょう*1が、KleeneAlgebra-oidとKleeneAlgebraCategoryは区別しないと混乱します。圏化の多様性に目が眩んでしまう、というか…

KleeneAlgebra-oidは、ある程度は分かっているし、形式言語理論/プログラム意味論との関係も分かります。が、KleeneAlgebraCategoryはそれほどハッキリしません。半環のX圏化であるSemiringCategoryに、クリーネスター自己関手が付いたものだろうとは思います。関数に対する再帰の定式化がKleeneAlgebra-oidで、領域に対する再帰の定式化がKleeneAlgebraCategoryという感じかな。

KleeneAlgebraCategoryの実例がまったくないのか? というと、そんなことはありません。集合圏Setは、リストモナドをクリーネスターと考えておそらくKleeneAlgebraCategoryになるだろうと思います。今のところ、KleeneAlgebraCategoryのチャンとした定義がないので、実例だと言い切ることは出来ませんが。

前節で述べたように、圏化にはバリエーションがあり、もとの構造(圏化する前の構造)が、台が離散圏の場合に再現したり、台が単対象圏の場合に再現したり、あるいはエンドセットとして再現したりします。さらに、マイクロコスモ原理との関連では、圏化した圏がもとの構造をホストできるか? も問題になります。

クリーネ代数(あと、テスト付きクリーネ代数も)の圏化/無限タワー化は、モノイド構造やデカルト構造に比べると、事情が複雑になるでしょう。が、部分的にでも出来れば、もともとの動機である形式言語理論/プログラム意味論にもフィードバックがあると期待できます。


2005, 2006年くらいに考えていたことがメモ編には残っているので、読み直してみようかな。色々な種類の圏化を比較したり組み合わせたりが重要なんじゃないかと思います。

*1:2-圏のレベルでは、KleeneAlgebra-oidとKleeneAlgebraCategoryを統合できるだろう、と思っています。

2018-10-05 (金)

マイクロコスモ原理とクリーネ構造

| 16:41 | マイクロコスモ原理とクリーネ構造を含むブックマーク

昨日の記事は妄想に近い話でしたね。とりとめのない雑感/思いつき/妄想のたぐいは、積極的に書こうとは思わないのだけど、後でなんかのヒントになる可能性がある事は書き留めておこうかな、と。

十数年前から、クリーネ代数にある種の“違和感”をいだいているんですよ。マイクロコスモ原理により、その違和感の正体がわかるかも知れない。(分からないかも知れない。)

内容:

  1. クリーネ代数
  2. クリーネ行列とクリーネ圏
  3. クリーネ圏とクリーネ構造のタワー

クリーネ代数

このブログは2005年初頭から始めました。始めた当時から最近まで、散発的にクリーネ代数〈Kleene algebra〉の話題を取り上げています。クリーネ代数は、形式言語やプログラムの意味論に使えます。よく出来た代数系だと思うのですが、一方で、「なんか違う」感がつきまとってました。その“違和感”に言及した記事を3つ挙げれば:

クリーネ代数に対する僕の印象は、「クリーネ代数という代数系は、現象の一部をうまくモデル化しているが、現実的には不十分なことが多い」というものです。不十分な感じに対しては、「より強力なトレース付きデカルト圏に乗り換えればいい」と思っていました。このような印象や対処は、間違っているとは思いませんが、別な見方がありそうです。

別な見方とは、マイクロコスモ原理の観点からの解釈です。マイクロコスモ原理は、次のように主張します。(例えば「マイクロコスモ原理の恐怖」参照)

  • 特定の代数構造は、その代数構造を圏化した構造を備える圏のなかで定義可能である。

クリーネ代数も代数構造なので、次のように言えます。

  • クリーネ代数は、クリーネ代数を圏化した構造を備える圏のなかで定義可能である。

「クリーネ圏」〈Kleene category〉という言葉は、既に定義して使っている人がいますが、ここでは、マイクロコスモ原理で言うところの「クリーネ代数を圏化した構造を備える圏」という(若干曖昧な)意味で使います。

クリーネ代数に関するマイクロコスモ原理を信じるなら、クリーネ代数という構造は、必然的にクリーネ圏という圏論的構造を要求することになります。

クリーネ行列とクリーネ圏

クリーネ代数は、ベキ等な足し算と可換とは限らない掛け算、それとクリーネスターを備えた代数構造(代数系)です。ベキ等な足し算から順序が入り、クリーネ代数は順序半環になります。クリーネ代数を K = (K, +, 0, ・, 1, (-)*, ≦) のように書きましょう。≦ は、足し算 + から導かれた順序です(x ≦ y ⇔ x + y = y)。

クリーネスターを仮定する代わりに、次のように言っても同じです。

  • a, b∈K に対するアフィン線形不動点方程式 x = ax + b は、常に唯一の最小解を持つ。

b = 1 の場合の不動点方程式 x = ax + 1 の解を a* と定義することによりクリーネスターは後から導入できます。

アフィン線形不動点方程式は1次方程式(の特殊形)なので、多次元化したくなります。連立の不動点方程式は次の形になります。

x1 = a1,1x1 + ... + a1,nxn + b1

...

xn = an,1x1 + ... + an,nxn + bn

クリーネ代数Kを係数域とするn×nの正方行列 [aj,i] が出てきます。正方行列に対してもクリーネスターが定義できて、有限オートマトン理論とうまく繋がります。

行列計算をするなら、正方行列に限定する必然性はありません。任意の n, m に対するn×m行列を考えることができます。クリーネ代数K上の行列線形代数が構成できます。行列線形代数は、K上の有限次元自由加群を議論していることになります。単なる線形代数というわけではなくて、アフィン線形不動点方程式/クリーネスターの話も入ります。

クリーネ代数Kを調べるには、K上の行列線形代数は必須です。よって、クリーネ代数を定義して調べることができる環境は、少なくとも行列線形代数を展開できるような環境ということになります。そんな環境は半加法圏〈semiadditive category〉だと言っていいでしょう。次の記事で書いています。

クリーネ圏が在るとすれば、それは半加法圏の構造を備えているはずです。

クリーネ圏とクリーネ構造のタワー

クリーネ代数Kを、K = (K, +, 0, ・, 1, (-)*, ≦) と書きました。これは、足し算(中立元は0)/掛け算(中立元は1)/クリーネスター/順序を持つ構造であることを表しています。クリーネ代数の圏化〈categorification〉を仮にクリーネ圏と呼ぶことにしたのですが、クリーネ圏の構成素〈constituents | stuff〉はまだハッキリしません。クリーネ代数との対応を考えるなら:

代数系
足し算 双積(半加法構造)
掛け算
クリーネスター
順序

足し算に対応する双積以外は不明です。が、以前に半加法圏を考えたとき、テンソル積〈モノイド積〉も一緒に考えてました。掛け算の対応物は、双積と協調するテンソル積でしょう。

クリーネスターは不動点方程式の解なので、圏論的対応物は(圏論的)不動点オペレーターでしょう。もし、圏がデカルト圏なら、カザネスク/ステファネスク/ハイランド/長谷川の定理より、不動点オペレーターはトレースと同じことになります。ここいらのことは:

半加法構造(双積)とデカルト構造はうまく両立しない(たぶん)ので、カザネスク/ステファネスク/ハイランド/長谷川の定理が使えるのか? は現状よく分かりません。よく分からないながらも、先の対応表を(暫定的に)埋めてみると:

代数系
足し算 双積(半加法構造)
掛け算 テンソル積
クリーネスター 不動点オペレーター
順序 EPペア

EPペアについては、次を参照してください。

今までは「クリーネ代数は不十分だ、代わりにもっと強力な圏を考えよう」というだけの発想でした。クリーネ代数が不十分なのは、その環境を一緒に考えてなかったからかも知れません。「クリーネ代数を圏化する」、あるいは「クリーネ代数達に、適切な棲息環境を見つけてあげる」と考えると、別な景色が見えるかも知れません。

クリーネ代数が定義される環境であるクリーネ圏が定義できたとして、マイクロコスモ原理の無限階層性から、クリーネ圏が定義される環境であるメタ・クリーネ圏が必要になります。実は、半加法圏に関してはメタ圏を考えたことがあります。

マイクロコスモ原理を信じるなら、1-クリーネ構造=クリーネ代数、2-クリーネ構造=クリーネ圏、3-クリーネ構造=メタ・クリーネ圏、… というクリーネ構造の無限タワーがあるはずです。構造の無基底性・多様性から、無限タワーが一意ではなくてたくさんのバリアントがあるかも知れません。

マイクロコスモ原理を信じてみようかと宗旨変えしたのは割と最近(2018年9月13日あたりから)で、その有効性を確信はしてないのですが、クリーネ構造タワーが見つかれば面白いし、マイクロコスモ原理への確信が生まれるかも。

2018-10-04 (木)

チャーチ/チューリングの提唱とバーウィック/ショマー=プリの定理

| 12:54 | チャーチ/チューリングの提唱とバーウィック/ショマー=プリの定理を含むブックマーク

妄想かも知れない、トンチンカンかも知れない、雑感。

内容:

  1. チャーチ/チューリングの提唱
  2. 高次圏論
  3. バーウィック/ショマー=プリの唯一性定理
  4. もう一度チャーチ/チューリングの提唱

チャーチ/チューリングの提唱

チャーチ/チューリングの提唱〈Church-Turing thesis〉とは、およそ次のような主張です。

  • 計算可能性の概念は、どのような方法で定義しても同値になる。

これは、チャーチ/チューリングの定理でもチャーチ/チューリングの公理でもなく、提唱〈テーゼ〉です。主張を正確に述べることもできないし、もちろん証明もできません。経験則を指導原理として位置付けたものでしょう。

計算可能関数の定義は色々とあります。

これらの方法で定義される関数のクラスが同じであることは証明できる(証明された)定理です。まったく異なる定義が同じ関数のクラスを定義するのです。この事実から、直感的な「計算可能」という概念は、定義によらない普遍的な概念であるように思えます。

その「思い」を言葉にしたのがチャーチ/チューリングの提唱なんでしょうが、それを言ったからってなんなんだ? というスッキリしない感じが残ります。

高次圏論

高次圏論でも同じような事情があります。誰かが提唱したわけではないので、名前は付いてませんが、多くの人が次のような「思い」を抱いているでしょう。

  • 高次圏の概念は、どのような方法で定義しても同値になる。

高次圏の定義も色々とあります。2004年に書かれたチェン/ラウダの高次圏の教科書がありますが:

その目次を見てみましょう。

  • 2. Penon
  • 3. Batanin and Leinster
  • 3.3 Leinster
  • 3.4 Batanin
  • 4. Opetopic
  • 5. Tamsamani and Simpson
  • 5.3 Simpson's definition .
  • 5.4 Tamsamani's definition
  • 6. Street
  • 7. Joyal
  • 8. Trimble and May
  • 8.1 Trimble
  • 8.2 May

4章のOpetopic以外はすべて人名です。OpetopicもBaez-Dolanとすれば、11人の人名が並びます。それぞれの人がそれぞれの定義を提案しています。

計算可能性の場合とは違って、異なる定義が同値であることの証明は難しく、同値性が証明された例は少数です。「どのような方法で定義しても同値になる」は、経験則と呼ぶには弱く、希望的観測や努力目標といったところでしょう。

n-圏は、次元n以外のもうひとつの整数mを使ってより細かい分類がされます。(n, m)-圏とは、m次を超える射がすべて可逆であるn-圏です。チェン/ラウダの教科書で扱っているのは(n, n)-圏(nが無限でもよい)で、その後で多用されるようになった高次圏に(∞, n)-圏があります。

バーウィック/ショマー=プリの唯一性定理

高次圏の場合は、定義がたくさんあり、それらの定義を書き出すのも難しく、定義の同値性を示すのも難しく、「いったいどうすりゃいいんだ?」な状況です。一見、混沌とした状況に対して、別なアプローチをする人もいます。「高次圏とは何か?」に答えるのではなくて、「高次圏“論”とは何か?」に焦点を移すのです。

「高次圏とは何か?」にはたくさんの人がそれぞれの定義を持ち、それぞれに高次圏論を展開しています。それらの高次圏論(高次圏ではない)に共通する特徴を探して、高次圏論を公理化しよう、というわけです。

卑近な例で言えば; 「ベクトルとは何か?」は今は問題にされないでしょう。単に「ベクトル空間の要素」です。公理化されて興味の対象となっているのは「ベクトル空間」のほうです。同様に、高次圏とは単に「高次圏論で扱う対象」で済ませるのです。

バーウィックとショマー=プリは、(∞, n)-圏論を公理化して、その公理を満たす(∞, n)-圏論は、本質的には(ある種のupto-isoで)1つしかないことを示しています。

  • Title: On the Unicity of the Homotopy Theory of Higher Categories
  • Autohrs: Clark Barwick, Christopher Schommer-Pries
  • Pages: 45p
  • URL: https://arxiv.org/abs/1112.0040

上記論文の最初の投稿は2011年末(30 Nov 2011)ですが、今年(7 Aug 2018)になって大幅にリライトされてます(Completely rewritten)。改善が続けられて、読みやすくなったのでしょうが、僕にはハードル高すぎ。

テクニカルな内容は追えないまでも、バーウィック/ショマー=プリの戦略は見当が付きます。

  1. 対象物そのものではなくて、対象物を扱っている理論に注目する。
  2. その理論を公理化する。
  3. 公理化された理論は、本質的には唯一であることを示す。
  4. 現在知られている理論が公理を満たすことを確認する。
  5. 複数の理論が同値であることが分かる。
  6. どの理論を使っても、(ある抽象レベルでは)同じ結果が出ることが保証される。

もう一度チャーチ/チューリングの提唱

さて、冒頭のチャーチ/チューリングの提唱ですが、バーウィック/ショマー=プリと同様な戦略で、定理にできないものでしょうか? 「計算可能性とは何か?」ではなくて「計算可能性の理論とは何か?」に注目して、計算可能性理論を公理化するというアプローチです。計算可能性の場合は、直接的・個別的に同値性が証明できたので、理論の公理化の必要性はなかったのでしょうが、計算可能性が「定義によらない普遍的な概念」だとすれば、定義・定式化をどうしようが本質的に唯一の概念的実体を記述する、という形の定理があってもよさそう、と思うんですが。

2018-10-02 (火)

ゲーデル化をどうするか? その2

| 12:17 | ゲーデル化をどうするか? その2を含むブックマーク

昨日の「ゲーデル化をどうするか?」の続きです。

内容:

  1. 「コード」という言葉
  2. ゲーデル符号が自然数であることのメリット
  3. ゲーデル化を具体的に定義したいわけ
  4. ツリー構造が良さそうなわけ
  5. そんなわけで

「コード」という言葉

昨日の記事の途中「ゲーデル化をどうするか? // プログラミング言語の利用」で、「コード」という言葉の多義性で“ウワーってなって”います。

ゲーデル化=ゲーデル符号化の写像 G:S→D に対して、Sの要素を「コード」と呼ぶときもあれば、Dの要素を「コード」と呼ぶときもあるのです。「コード」という言葉は、ものすごくよく使うし、とても便利な言葉なんですが、混乱を避けるには使わないのが無難かな。

写像Gの余域である集合Dの要素は、漢字で「符号」と書き、encode/encodingは「符号化」、decode/decodingは「脱符号化」。D自体は「データ領域」「符号集合」「符号空間」とか呼びましょう。

では、写像Gの域である集合Sの要素は何と呼ぶ? … … ウーン。Sはのっぺらぼうな集合じゃなくて、「原子記号、定数記号、項、論理式、証明」のような階層があるんですよね。みんなひっくるめて呼ぶときは … 「式」〈expression〉かな。データの種類としては文字列とみなすので、「テキスト」でもいいかな。論理ってさ*1、いうほど概念・用語が整理・整備されてないんだよね。

ゲーデル符号が自然数であることのメリット

ゲーデル化をどうするか?」で、ゲーデル化=ゲーデル符号化の値が自然数であるのは辛い、と書きました。しかしもちろん、符号が自然数であることによるメリットがあります。

扱うデータは自然数だけなので、集合(基本データ型)は、Nだけでこと足ります。関数は、f:NnN という形のものだけ考えれば十分です。データ領域を含む意味論的システムが単純であり、それに伴い構文論的システムもまた単純なもので済みます。単純さはメリットです。

ゲーデル化をどうするか?」より:

構文的対象Aに対するG(A)は巨大な数になってしまい、...[snip]... ゲーデル数G(A)を見て、Aを想像するのもほぼ不可能です。

ゲーデル符号G(A)を見ても、もとの構文的対象Aがサッパリ分からないのはメリットと捉えることもできます。ゲーデル符号化は、構文的対象の無意味化/脱意味化という側面も持ちます。もともとは意味を持っていた構文的対象から意味を剥ぎ取って単なるデータにする働きがあります。G(A)を見ても意味が分からないことは、十分に無意味化/脱意味化されていることになります。

コード[構文的対象]とデータ[符号]があまりにもソックリだと、コード[構文的対象]とデータ[符号]の違いを意識できなかったり混乱したりするかも知れません。

ホモアイコニック言語を使ったゲーデル符号化(クォーティング)の難点は、無意味化/脱意味化の効果が薄いことです。意味が容易に想像できるデータに対して「意味を考えるな!」と言われても難しいんですよ。人間の意味的連想力って、ほんとに強烈で制御困難なんです*2

ゲーデル化を具体的に定義したいわけ

ゲーデル自身が使ったゲーデル化(符号化)を「オリジナルのゲーデル化」と呼ぶことにします。オリジナルのゲーデル化は、 G:S→N という写像で、Nの演算や性質(算術〈arithmetic〉と呼ぶ)で組み立てられます。Gは、原理的には明確で簡単な関数です。が、現実的にはほぼ計算できません。

現実的(理論的じゃないよ!)に計算できるかどうかは、ゲーデルの不完全性定理にとってはどうでもいいことです。なんなら、「G:S→N という写像があったとしましょう」からスタートしてもいいかも知れません。Gの存在を信用できない人のために、具体的な定義を一応は出すだけで、値をホントに計算したいわけじゃないのです。

でも僕は、値をホントに計算したいのです。しかも手で。Gに対して、「定理の証明のための概念上の道具」とは若干別な用途を想定しています。Nとは限らない(つうか、Nじゃない)データ領域Dに対して、G:S→D を具体的に定義することは、Sの構造をハッキリと理解する助けになります。そして、具体的な式(項/論理式/証明)Aに対して、G(A)をホントに手で計算することは、システムに対する実感を得るのに効果があるからです。

以上の動機からは、写像Gは、明示的/具体的に定義される必要があるし、現実的に手で計算できる写像であることも要件です。オリジナルのゲーデル化ではうまくないですね。手で計算できないもん。

ツリー構造が良さそうなわけ

ゲーデル化をどうするか?」で、テキストとしての式(構文的対象)をパーズしたツリーをデータにする案を述べました。まだ、決定ではなく案ですが。

ノードにラベル(文字列だと思ってください)をくっつけたツリー構造というのは、かなり馴染み深いデータ構造だと思います。実際によく利用されます。その操作や性質もよく知られています。小学生でも知っている自然数には負けますが、ポピュラーなデータ/データ領域と言っていいでしょう。

オリジナルのゲーデル化では、項や論理式は(下位の)記号の列とみなします。それはまーいいのですが、証明も論理式の列とみまします -- これはどうなの? 「定理の証明のための概念上の道具」としてはそれでもいいでしょう。しかし、手で符号化/脱符号化を実際に計算する場合は嬉しくないです。

命題の列が証明であるのは、列内の命題が、それより前に出現する命題(複数でもよい)から、なんらかの推論規則で導出できる場合です。この基準で、命題列が最後の命題の証明になっているか/なってないかを判断できます。実際の(形式化してない)証明も、おおむね命題の列だと言えるでしょう。

でもね、命題の列としての証明というのは分かりにくい。自然演繹でもシーケント計算でも、(形式化された)証明は、ツリー構造に編成されています。証明をデータとして扱う場合、リストよりはツリーのほうがずっと扱いやすいです。この理由もあって、証明も含めた構文的対象の符号化データはツリーがいいと思うのです。

データ領域Dを、ラベル付きツリーの集合と決めると、自然数の加減乗除に対応するものは、ツリーに対する様々な操作です。ツリーの操作(演算)は、大雑把な合意はあるでしょうが、算術のように強い標準はないので、あらためてハッキリと決める必要があります。ツリーの算術を設定するわけです。

そんなわけで

自然数の算術の代わりにツリーの算術を確定して、ツリー算術の意味での計算可能性/定義可能性/表現可能性/構成可能性(どれも似たりよったり)を考えようかな*3、と思っています。ツリーの算術は自然数の算術ほどにポピュラーじゃないにしろ、学習負担はさほどではなく、表現力は相当に強力です。

先に述べた「符号が自然数であることによるメリット」は失われるけど、それはトレードオフだからしょうがない。あと、ちょっと懸念があるのは、「ゲーデル化をどうするか?」で触れた心理的インパクトかな。心理的な問題だから、優先度は高くないですけど。

*1:他の分野もたいてい事情は同じです。

*2:誤解・曲解・混乱などの原因の多くは、自動的に働いてしまう連想じゃないかと思います。

*3:データ領域を自然数の集合からツリーの集合に切り替えると、計算可能関数(帰納的関数)の定義をやり直さないといけなので、そこは手間が増えます。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20181002

2018-10-01 (月)

ゲーデル化をどうするか?

| 14:25 | ゲーデル化をどうするか?を含むブックマーク

9月29日に「不完全性定理ゼミ」第0回=ガイダンス回を行い、10月からは本編ゼミ(第1回から第6回)が始まります。

1回の時間も長く(3時間)全6回なので、トータルの時間はけっこうあります。「ゆっくりジックリやれるな」という気もしますが、予備知識ゼロを標榜しているので、「余裕がある」と安心はできません。今から、先のストーリーを細部まで考えておいたほうがいいよね。

んっ、この記事がネタバレになるんじゃないか? その心配はないでしょ。内容の話ではなくてメタ内容の話だから。

内容:

  1. ゲーデル化とデータ領域
  2. プログラミング言語の利用
  3. コンパイラとゲーデル化
  4. 心理的なインパクト
  5. じゃ、どうする

ゲーデル化とデータ領域

ゲーデルの不完全性定理の証明を律儀に追うのは、語るのも辛いし聞くのも辛いポイントが幾つかあります。なので、技術的な細部をカットして、“その意義”がドータラの“人間知性”がカンタラの、みたいな話に流れがちなんでしょう。ドータラカンタラは楽しいからね。

辛くなるポイントのひとつ*1は、ゲーデル化をちゃんと追いかけるところです。ゲーデル化は、項/論理式/証明などの構文的対象に対して、自然数を対応させる写像です。構文的対象の集合をSとして、G:S→N という写像がゲーデル化〈ゲーデル符号化 | ゲーデル数化〉です。

写像Gの構成には、自然数の加減乗除、つまり小学生でも出来る計算しか使わないので、特に予備知識が要らないのは事実です。しかし、構文的対象Aに対するG(A)は巨大な数になってしまい、具体的に計算するのはまず不可能です。また、ゲーデル数G(A)を見て、Aを想像するのもほぼ不可能です。「具体的なAに対する具体的な数G(A)が必要なわけじゃない」はおっしゃる通りなんですが、そうは言ってもゲーデル数は扱いにくい。

そこで、なんらかのデータの集合(データ領域)Dを準備して、G:S→D とできないかな、という話になります。DがN(自然数全体の集合)じゃなきゃいけない理由はありません。Dは、我々にとってお馴染みで、確実な操作ができる集合ならいいのです。NをDに埋め込めて、自然数の演算はD内で再現(模倣)できる必要はあります。Dは、算数ができる程度にはリッチなデータ領域です。

プログラミング言語の利用

ゲーデル化を分かりやすくするために、プログラミング言語を使う方法があります。項/論理式/証明なども、プログラミング言語のコード(ソースコード)として記述して、データ領域Dも、そのプログラミング言語が持つデータ領域を利用します。

こういった用途に向いているプログラミング言語Lispがあります。項、論理式、証明などをLispコード(S式ともいう)として書きます。ゲーデル化はとても簡単でクォートするだけです。(foo bar baz) というS式は、「barとbazを引数にしてfooする」という意味ですが、'(foo bar baz) なら単なるリストデータになります。

プログラミング言語のコード構文とデータ構文が同じ(または、とても似ている)という性質をホモアイコニシティ〈homoiconicity〉といいます。Lispはホモアイコニックなプログラミング言語のひとつです。ホモアイコニックなプログラミング言語を使えば、項/論理式/証明などをコード構文で書き、ゲーデル化(による符号)はコードに対応するデータで与えることができます。(←この文や次段落の文の意味が分かりにく理由は、この節最後の段落参照。)

この方法は、自然数にコード化する方法(オリジナルのゲーデル化)の問題点を解消しますが、コードとデータがあまりにもソックリだと、コードとデータの違いを意識できなかったり混乱したりするかも知れません。それと、プログラミング言語を知らない人にプログラミング言語の学習を強いることになるのも、「ウーン、ドウカナ?」と思う点です。

と、ここまで書いて気付いたけど; プログラミング言語の「コード」は、項/論理式/証明などを記述するテキストのことで、ゲーデル化の「コード」のほうは、ゲーデル化された符号データのほうですね。同じ言葉で意味が逆だわ、トホホ。このテの用語法の混乱って、けっこうシリアスな障害になるんだよなー(愚痴る)。

コンパイラとゲーデル化

技術者・プログラマにとって、ゲーデル化(に相当する操作)は実はお馴染みのものです。コンパイラはゲーデル化を実行しているとみなせます。プログラミングの意味でのコード(ソースコード)は、構文的対象です。それをコンパイルした結果はバイナリデータ(バイト列/ビット列)です。コンパイラは、構文的対象の集合Sからデータの集合Dへの写像 G:S→D です。

今述べたように、ゲーデル化をプログラミングシステムに埋め込んで説明すれば、技術者・プログラマにとっての日常的経験・直感により、比較的に分かりやすい説明になります。実際僕は、この説明方法をよく使います。

バイナリデータの領域は、2進数表記*2を通じて自然数の領域と1:1対応します。この単純な対応があるので、オリジナルのゲーデル化のデータ領域=Nと繋げるのも容易です。バイナリデータと自然数を同一視すると、コンパイラは、プログラミング言語ソースコードの領域SからNへの写像となるので、そのまんまゲーデル化です。

この説明方法は、特定の職業・趣味の人々のツールへの慣れ・親しみに依拠しているので一般性はないですね。技術者・プログラマにしろ、コンパイラの中身をよく知ってる人はそうはいないわけで、ゲーデル化の定義を明示的には与えず、ブラックボックスのまま扱う説明方法です。

心理的なインパクト

ゲーデルの不完全性定理が人々を驚かせる理由として、データ領域に自然数の全体Nを使っていることが大きいと思います。自然数は、ほんとに初等的なデータで、知らない人はいません。自然数の計算は、みんな慣れ親しんだ操作です。

そんな自然数に関する命題のなかに、証明も反証(否定の証明)もできない命題があるなんて、ビックリですよね。自然数は分かりきっているモノと感じているからです。これが、複雑怪奇・謎なデータ領域Dに関する命題のなかに、証明も反証もできない命題があるよ、って話だと、そこまでのインパクトはないでしょう。

となると、十分に慣れ親しんでいて、分かりきっていると感じられるデータ領域を選ばないと、不完全性定理の心理的インパクトは損なわれることになります。この観点から、S式の集合やバイナリデータの集合はどうなんでしょうかね?

Lispの説明では、S式〈S-expression〉のこと、あるいはS式全体からなる集合をSexと書きます(書くことがあります)。データ領域としてSexを使った場合の不完全性定理のステートメントは:

  • Sexに関する命題のなかに、証明も反証もできない命題がある。

これは心理的インパクトあるのかな?

じゃ、どうする

全面的にプログラミング言語/プログラミング・システムを使う案は却下です。先に述べたように「特定の職業・趣味の人々のツールへの慣れ・親しみに依拠している」のがヨロシクナイと思うからです。

項/論理式/証明の書き方は、通常の(比較的標準的な)数学・論理の記法を採用します。これらの項/論理式/証明は、ゲーデル化の写像Gに渡す引数になるので、その意味ではデータとみなす必要があります -- 文字列データとみなすのが妥当でしょう。すると、写像Gの域〈domain〉は、文字列全体の集合Stringの部分集合となります。

では、Gの行き先はどこ? ゲーデルのオリジナルである G:S→N だと具体的な計算ができないし、G:S→String は混乱しそうだし。ウーム。テキスト(文字列)として書かれた項/論理式/証明をパーズした結果であるツリーはどうかな?

例えば、算術式 5 + 12 に対して G("5 + 12") の値は:

   +
 / \
5   12

+, 5, 12 などの原子記号(トークン)は、ツリーに付いた文字列ラベル "+", "5", "12" だと解釈すれば、文字列データ、または文字列データをもとにした複合構造データの世界で話が済みます。S式と同じっちゃ同じだけど、構文領域側にS式構文を採用しないので、構文側とデータ側の混乱は起きないでしょう。


まだ考える余地はあるし、変更の可能性もあるけど、現状ではこんな方針かな。

*1:最初「辛くなる最大のポイント」と書いてたのですが、「辛さ」は主観的だから、文言は修正しました。僕は、ゲーデル数が自然数であることが辛かったです。

*2:8進数でも16進数でも256進数でも何でもいいけど。

2018-09-26 (水)

圏論的な相互依存主義から見たペアリング

| 10:57 | 圏論的な相互依存主義から見たペアリングを含むブックマーク

デカルト構造の無限タワー: 怖がらずに登れ」にて:

順序対(ペア) (a, b) はどっから来るのでしょう? その起源、故郷はどこにあるのでしょうか?

「どうしてそんなことを疑問に思うのか? それが疑問だ」と思う方が多いでしょう。一連の話のなかで、大乗仏教中観〈ちゅうがん〉派とか手塚治虫とかを引き合いに出してはいますが、僕が仏教思想をマトモに分かるはずもなく、そこは“マジ”ではなく“ネタ”です。疑問や興味の動機は、圏論的な発想から出てくるものです。座禅を組んでいたら舞い降りた考えではありません。

「ペアはどっから来るのか?」という問題意識が納得できるように、出来るだけ丁寧な説明を試みます。参照をあまり辿らずに読めるように、以前の内容をある程度は再掲します。

内容:

  1. 圏論的な相互依存主義とは
  2. 恐縮だが、またモノイドの例
  3. Setを外から眺める
  4. ペアを作る操作
  5. ペアリングとデカルト構造
  6. 階層横断的な記述
  7. おわりに

圏論的な相互依存主義とは

大乗仏教中観派と一般モデル理論」で、谷村先生の「物理学者のための圏論入門」から引用をしました。現在、谷村講義録は次のURLから入手できます。

以前とまったく同じ引用を再度します。

対象たちが無関係にばらばらにあるのではなく, 射の有機的なネットワークでつながっている, というのが圏の大事な性質です.


[対象である] a や b は集合のように内部を持っているかどうかすらわかりません. いまのところ a, b の内部には立ち入らず, さしあたって対象と呼んでいるだけです. 圏論では, 元や集合の存在に先立って, 射の存在を認めるのです.


対象 a の性質を圏論的に知りたかったら, [a 自体ではなくて] 射の連動関係・絡み具合を調べることによって対象 a の特徴を探ろうとします. [...snip...] 物理学や化学では, 未知の物質に光や音や熱や他の粒子をぶつけるなどの刺激を与えて, そこから出て来る光や破片などを見て, その物質の性質や正体をつきとめようとします. このような方法は, 物理と化学に限った話ではなく, 生物学や心理学でも似たような方法が使われるでしょう.

この引用内に端的に記述されているのですが、圏論のマントラは:

  • 対象だけではなく射を考えよ。
  • 対象の内部構造(が仮にあったとしても、それ)を見るな。

です。n-圏論(高次圏論)だとさらに:

  • 1-射(通常の射)だけではなくk-射(k ≦ n)を考えよ。

も加わります。ケンロニストは毎日これを唱えています(嘘です)。

圏やn-圏の対象が、それ自身で集合である、圏である、2-圏であるといった状況は珍しくはありません。しかし、対象の内部構造には言及せずに、対象の外にある射やk-射により議論を進めたいのです。くどいですが、繰り返し言うと:

  • 対象が集合であっても、その内部の要素に言及するな。
  • 対象が圏であっても、その内部の対象と射に言及するな。
  • 対象が2-圏であっても、その内部の対象と1-射と2-射に言及するな。
  • …(以下同様)…

対象の内部構造を見ないので、すべての議論は対象の外にあるモノ、つまり対象をホストしている環境が備えているモノを使って行います。「環境が備えているモノ」とは、環境側にある(他の)対象、射、2-射、…… です。

今回の話における圏論的発想とは、今述べたような捉え方/考え方だと思ってください。モノの構造や特徴は、モノの内部に在るのではなく、他のモノ達との関係性、相互依存性のネットワークのなかに在る、のです。相互依存性のネットワークは、環境側が持っています

すごく雰囲気的な例え話をすれば、… … 囲み記事にしよう。

[補足]

集合や圏が、硬い殻を持った生き物だとしましょう。殻をかち割れば、内臓やら何やらが見えます。でも、殻を割られたら彼らは死にます。生物学的研究のために、殻を割って解剖をすることもあるでしょう。が、殺生は良くない(また仏教だ)。できるなら、殻を割らないで彼らの特徴や生態を調べるほうが望ましいでしょう。

無闇な殺生はつつしめという教えです。これ、例え話ね。

[/補足]

恐縮だが、またモノイドの例

前節で述べた圏論のマントラに忠実に従うのは容易ではありません。今日は頑張って従いますが、圏論の戒律は厳しくはないので、対象の内部構造を使ってしまうことも日常茶飯事です。そこはご安心下さい。

さて、毎度同じ例で恐縮ですが、モノイド M = (M, ・, 1) を考えます。"・"は二項演算、"1"は単位元です。今書いた "M = (M, ・, 1)" は記号の乱用をしていて、モノイド構造とその台集合〈underlying set〉を同じ"M"で表しています。ちゃんと区別すれば、

  • M = (U, ・, 1)

"・"は中置演算子記号のつもりですが、前置する関数記号として使いたいときは、Haskellのセクション風に"(・)"とします。念の為、y = (・) と別名も付けておきましょう。

以上の状況で、

  • U in Set
  • y:U×U→U in Set

です。"in"の使い方は:

  • X in C ⇔ X∈|C|
  • f:X→Y in C ⇔ f∈C(X, Y)

上で言ってることは、「Uは圏Setの対象」「yは圏Setの射」です。

では、単位元1はどうでしょうか?

  • 1は圏Setの対象ですか?
  • 1は圏Setの射ですか?

どちらの問に対しても答えはNOです。1は集合Uの要素です。

  • 1∈U

次のモットーを思い出してください。

  • 対象が集合であっても、その内部の要素に言及するな。

集合Uの要素1を表に出したら、圏論の戒律(厳しくはないですよ!)を破っています。じゃ、どうすればいいの? -- 要素1の代わりに、要素1をポインティングする写像

  • i:1→U

を使います。これならば、

  • 1は単元集合で、圏Setの対象です。
  • iは写像で、圏Setの射です。

したがって、Uの要素への言及はなくなっています。Uの環境であるSetに備わったモノだけになっています。

モノイドの法則である結合律、左単位律、右単位律も、U, y, i と、どんな圏でも持っている id(恒等射), ;(結合)、それとデカルト・モノイド構造である ×(直積), α(結合律子), λ(左単位律子), ρ(右単位律子)で記述します(律子に関しては「律子からカタストロフへ」を参照)。変数は用いません。idUをjと略記することにして:

  • [結合律] (y×j);y = αU,U,U;(j×y);y :(U×U)×U→U in Set
  • [左単位律] (i×j);y = λU : 1×U→U in Set
  • [右単位律] (j×i);y = ρU : U×1→U in Set

添字が付いた αU,U,U, λU, ρU は圏Setの射で、

  • αU,U,U:(U×U)×U→U×(U×U) in Set
  • λU:1×U→U in Set
  • ρU:U×1→U in Set

Setを外から眺める

前節で頻繁に、中置演算子記号"×"が出てきています。これは直積集合を作る演算を表します。"×"(が表すモノ)は何でしょうか?

  • ×は圏Setの対象ですか?
  • ×は圏Setの射ですか?

どちらの問に対しても答えはNOです。×は、次のような二項関手です。

  • (×):Set×SetSet

おっと、2つの"×"の区別が付くように片方を黒板文字にしておきます。

  • (×):Set𝕏SetSet

では、二項関手(×)の棲んでいる環境は何でしょうか? Setを対象として持つような環境ですね。これには、小さくない圏も許す“圏の圏”CATを持ち出す必要があります*1

  • Setは、2-圏CATの対象です。
  • 二項関手(×)は、2-圏CATの射です。

そして、

  • α, λ, ρ は、2-圏CATの2-射です。

出てくる記号(が表すモノ)が、いったいどこに棲んでいるのか、その次元はいくつか(対象か、射か、2-射か)を常に強く意識するようにしてください。"in"記法を徹底的に使うといいですよ。

次の記号を使うことにします。

  • I -- 単一対象と恒等射だけからなる自明圏 I in CAT
  • 𝕀 -- 単元集合を指すポインティング関手 𝕀:ISet in CAT
  • J -- IdSetの別名 J = IdSet : SetSet in CAT
  • Y -- (×)の別名 Y = (×) : Set𝕏SetSet in CAT
  • 𝕏 -- メタな直積演算子(二項関手) in (さらに上の環境)
  • α, λ, ρ -- メタな結合律子/左単位律子/右単位律子(自然変換) in (さらに上の環境)

"*"を関手の図式順結合記号として、α, λ, ρ のプロファイルを書いておきましょう。モノイドの法則との類似性に注意してください。

  • α::(Y𝕏J)*Y⇒αSet,Set,Set*(J𝕏Y)*Y : (Set𝕏Set)𝕏SetSet in CAT
  • λ::(𝕀𝕏J)*Y⇒λSet : I𝕏SetSet in CAT
  • ρ::(J𝕏𝕀)*Y⇒ρSet : Set𝕏ISet in CAT

環境Set内のモノイドと、環境CAT内のデカルト圏(の実例Set)は次のような類似性を持ちます。

環境Setにおいて 環境CATにおいて
台対象 U Set
単位対象 1 I
単位ポインティング i:1→U 𝕀:ISet
台の恒等射 j = idU:U→U J = IdSet:SetSet
乗法/積 y = (・):U×U→U Y = (×):Set𝕏SetSet
結合性 結合律(等式) 結合律子 α (自然変換)
左単位性 左単位律(等式) 左単位律子 λ (自然変換)
右単位性 右単位律(等式) 右単位律子 ρ (自然変換)

𝕏, α, λ, ρ は、CATのさらに外(上)にある環境の射と2-射です。

この類似性は、マイクロコスモ原理に由来するもので、無限に続きます。今日は深入りしませんが、Setをホストする環境であるCAT、さらにCATをホストする環境などを扱うためにグロタンディーク宇宙宇宙公理が必要になります。

太字だの黒板文字だのを使うのはシンドイ、勘弁してくれという人(それは僕だ!)のために、ダッシュ記法という書き方を考案しました(メモ編の「モノイドやモノイド圏の指標 補足解説」参照)。これを使うと太字だの黒板文字だのは避けられます。

Uにおいて Setにおいて CATにおいて さらに上の環境において
1 1' = 1 1'' = I 1'''
i:1'→U i' = 𝕀:1''→Set i'':1'''→CAT
j = idU:U→U J = IdSet:SetSet J' = IDCAT:CATCAT
y = (・):U×U→U Y = (×):Set×'SetSet Y' = (×') = (𝕏):CAT×''CATCAT
結合律 α α' = α
左単位律 λ λ' = λ
右単位律 ρ ρ' = ρ

ダッシュ〈プライム〉を使えば、文字種/文字装飾をだいぶ減らせます。扱う次元が増えれば、文字種/文字装飾で区別する方式は破綻します。なお、ダッシュの数は直接に次元を表すわけではなくて、基準となった記号(ダッシュなし)からいくつ次元を上げたかを示すだけなので注意してください。

ペアを作る操作

では、a∈A, b∈B に対するペア (a, b) について考えていきます。(a, b) は、「ハイフンをプレースホルダ(何かを入れる場所)として、(-, -) というオペレータ」があって、それに「引数 a, b」を渡したように見えます。となると、(-, -) は2引数(2項)のオペレータでしょうか?

とりあえず、 (-, -):A, B→A×B と書いてみます。矢印の左の A, B は2引数のつもりで書きましたが、2引数は1タプル引数ですから、(-, -):A×B→A×B ですね。この状況で (-, -) はいかなるオペレータか? と考えると:

  • (-, -) = idA×B

単なる恒等写像に過ぎません。なーんだ、ツマラン*2

以上のように考えるのは何も間違ってないし、まっとうで健全な態度です。当然ながら、「(a, b) を使ったらマズイ」なんてことは全くありません。ですが、我々は圏論の教義、もとい、考え方に従うので、そもそも集合Aの要素には言及しません。

  • 対象が集合であっても、その内部の要素に言及するな。

要素の代わりに、集合圏の単位対象 1' = 1 からの射を使えます。1'からの射をポインティング〈pointing morphism〉、あるいはポインター〈pointer〉と呼びましょう。a∈A, b∈B の代わりに、f:1'→A, g:1'→B in Set を考えます。

ペアリングは、2つの要素ではなく2つのポインターに対して構成されます。すぐに思いつくのは、×です。(×):Set×'SetSet は関手(二項関手)でしたから、関手の値である f×g は意味を持ちます。

  • (f×g):1'×1'→A×B in Set

このままだと dom(f×g) = 1'×1' でポインターとは言えません(ポインターの域は1')。対角自然変換δの1'成分は:

  • δ1':1'→1'×1' in Set

これを前結合〈pre-composition〉すると:

  • δ1';(f×g):1'→A×B in Set

ポインター f, g に対する δ1';(f×g) を <f, g> と略記することにします*3

  • <f, g>:1'→A×B in Set

いま定義されたペアリング <-, -> はプリミティブではありません*4。×, δ, 1', ; から構成されています。そして、構成の素材は、(1'を除けば)Setの外の世界に棲んでいます。つまり、<-, -> はメタレベルの素材から組み立てられているのです。

ペアリングとデカルト構造

集合論でペアをよりプリミティブな素材から構成する場合、通常はクラトフスキーペア (a, b) := {{a, b}, {a}} を使います。これが集合論的ペアの標準的定義です。

それに対して、圏論的ペアの定義として、前節で <f, g> := δ1';(f×g) : 1'→A×B in Set を提示しました。この定義は、集合の要素を使ってません。よりプリミティブな素材は、集合圏Setの外(上)の世界からやって来ます。

  • 集合圏内のペアリングを構成するには、素材を上位の階層から調達する必要がある。

上位の階層であるCAT内でペアリングを構成したいなら、さらに上位の階層から素材を調達する必要があります。こうして我々は、無限階層を無限に登り続けるはめになります。でも、「世界はそんなふうにできている」と淡々と受け入れましょう。「悟り」ですね。

まー、それはそうと、圏論的に定義した <-, -> が集合論的ペアの代替としてうまく機能するのでしょうか? Setのデカルト構造は、「デカルト構造の無限タワー: 怖がらずに登れ // デカルト構造」で述べたように、×, i' に関するモノイド構造に加えて、!, π1, π2, δ を使って定義します。これらが満たすべき公理(等式)は、環境CATのなかで記述されます。

デカルト構造の定義には、「デカルト圏、こんな定義もあります」で紹介したように、随伴性を利用します。随伴性〈随伴系〉の素材を列挙すると(紛らわしいけど、!, i, 1の違いに注意!):

  • !'Set:Set→1'' in CAT
  • i':1''→Set in CAT
  • δ'Set:SetSet×'Set in CAT
  • (×):Set×'SetSet in CAT

ここで、!'とδ'は、CATの外(上)の環境にある自然変換で、!'Set と δ'Set はその特定成分射です。×', !', δ' などは、CATのデカルト構造の素材なんですね。つまり、Setのデカルト構造のための素材調達の段階で、CATのデカルト構造の存在を前提してます。そのCATのデカルト構造は、その外の環境のデカルト構造なしには定義できません。そう、マイクロコスモ原理です。「世界はそんなふうにできている」のです。

デカルト構造を定義する随伴系は次のように書けます。

  • (η, ε): i' -| !'Set :Set→1'' in CAT
  • (δ, π): (×) -| δ'Set :SetSet×'Set in CAT

恒等は一律に"^"で表すとして、単位・余単位のプロファイルは:

  • η::Set^⇒!'Set*i':SetSet in CAT
  • ε::i'*!'Set⇒(1'')^:1''→1'' in CAT
  • δ::Set^⇒δ'Set*(×):SetSet in CAT
  • π::(×)*δ' Set⇒(Set×'Set)^:Set×'SetSet×'Set in CAT

ここで、η = ! 、εは自明な2-射、δは対角自然変換そのもの、π = <π1, π1>' = δ'Set*(π1×'π2) です。CATより上の世界の概念(×', !', δ' など)がバンバン使われているのが分かるでしょう。「世界はそんなふうにできている」のです。

随伴系はニョロニョロ等式〈snake {equation | identity}〉で統制されます。2つの随伴系があるので、合計4つのニョロニョロ等式があり、それがデカルト構造に対する天空の支配者〈Ruler in the Sky〉になっています。

天空のニョロニョロ等式から、それなりの作業を経ることにより、我々にお馴染みの等式/命題を得ることができます。f, h:1'→A, g, k:1'→B in Set に対して:

  • <f, g>;π1 = f
  • <f, g>;π2 = g
  • <f, g> = <h, k> ⇔ f = h かつ g = k

圏論的オペレータ/自然変換の添字をチャンと付けて、プロファイルも添えれば:

  • <f, g>A,B;(π1)A,B = f : 1'→A in Set
  • <f, g>A,B;(π2)A,B = g : 1'→B in Set
  • [(<f, g>A,B = <h, k>A,B : 1'→A×B) ⇔ (f = h :1'→A かつ g = k : 1'→B)] in Set

これらの事実は、圏論的ペアリング <-, -> を、集合論的ペアリング (-, -) と同じように取り扱ってもよいことを保証します。

階層横断的な記述

圏論のマントラによれば、我々が集合圏Set内で作業をするとき、Setの対象である集合の「内部構造を見るな」と訓戒されています。しかし、「見るな」と言われても見えてしまうかも知れません。

A in Set, a∈A と見えてしまったとします。見えてしまったものはしょうがないですが、aを直接使うのは憚られます。そんなとき、要素aの代理としてaをポインティングするポインティング写像 f:1'→A in Set, 1' = {0}, f(0) = a を使います。fはaから一意に決まるので、a~ と書きましょう。

a~ は、僕が格上げ〈bump up | promotion〉と呼んでいたものです。格上げについては、例えば次を参照。

集合論的な/あるいは内部的な (a, b) の代わりに、圏論的な/あるいは外部的な <a~, b~> を使っても何も不都合は起きません。次のような同値性がありますから。

  • (a~ = b~ :1'→A in Set) ⇔ (a = b in A)

<a~, b~> という表現は、集合圏Setにいながら、その下の階層である集合Aの内部も見ています。その意味で2つの階層にまたがった記述になっています。「内部構造を見るな」を破ってますが、階層的世界を垂直方向に見るときは、階層横断的な観察と記述も必要だと思います。

おわりに

ある階層における概念が、それより下の階層で定義された概念をもとに構成されるなら、安心感もあるし確実な感じがします。一方で、ある階層における概念が、それより上の階層における概念をバンバン使って構成されたら、不安をおぼえ、不確実な感じがします。

僕の比較的最近の経験で言えば、「上の階層を前提してしまう」のはもうしょうがないと思います。モノイド構造、デカルト構造、ペアリングなどは、構成の前提がドンドン上の階層に逃げてしまう典型例です。割と簡単で基本的な構造でこの現象が起きるので、避けるのは無理だろう、と(現状では)思っています。

*1CAT全体が必要なわけではなく、CATのごく小さな一部分でも十分です。が、その一部分を切り取るのがめんどうなので、超巨大な2-圏CATで議論することにします。

*2:別なアプローチとして、(-, -)を複圏のなかで考える方法があります。形式上は (-, -) と idA×B は区別されますが、事実上は同じものとして扱います。

*3:f, g がポインターでなくても <f, g> を考えることはできます。dom(f) = dom(g) ならOKです。

*4:<-, -> をプリミティブにする定式化もあります。今は、対角や射影をプリミティブにするアプローチを採用しています。

はいはい 2018/10/05 23:54 「このままだと」が「このまだまだと」になっています.

cohheecohhee 2018/10/06 13:34 「恐縮だが、またモノイドの例」の節で、

- λ_U:I×U→U in Set
- ρ_U:U×I→U in Set

となっているところ、ここはまだ Set での話なので、ドメインにある I (大文字 i の太字) は Set の対象の 1 (の太字) ではないですか?

m-hiyamam-hiyama 2018/10/06 17:10 はいさん、
ご指摘ありがとうございます。直します。

cohheeさん、
おっしゃる通りです。
1(イチ), i(小文字アイ), I(大文字アイ)とその太字ですから、我ながら紛らわしい。
[Ctrl]+[+]で拡大しないと判読できないレベル(老眼+近眼なので)。
ありがとうございます。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20180926

2018-09-25 (火)

告知:9月29日までなら一万円割引「ゲーデルの不完全性定理」

| 12:06 | 告知:9月29日までなら一万円割引「ゲーデルの不完全性定理」を含むブックマーク

先週の木曜(2018-09-20)に告知した「ゲーデルの不完全性定理」に関するセミナーなんですが、9月29日のガイダンス回、またはそれ以前に有料ゼミ(本編)へお申し込みをいただけると、一万円割引になります。

ガイダンス回(上のURL)でのお申し込みなら、もちろんOKですが、もし(そんな人がいるかどうか分からんが)ガイダンス回は出席できないが本編ゼミは申し込むつもりだ、という人がいたら、早めの申し込みのほうがお得です。僕(mail: hiyama{at}chimaira{dot}org)に連絡いただいても、かまいません。

トラックバック - http://d.hatena.ne.jp/m-hiyama/20180925