このブログの更新は X(旧Twitter)アカウント @m_hiyama で通知されます。
Follow @m_hiyama

ご連絡は上記 X アカウントに DM にてお願いします。

参照用 記事

万能対象 の検索結果:

ヴォエヴォドスキーの宇宙圏とパルムグレンの複前層

…の立場だと、計算的な万能対象〈universal object〉だと言えそうです。 「万能対象」のブログ内検索結果 しかし、ヴォエヴォドスキーが採用した宇宙の定義は計算的万能対象とはまったく違ったものでした。付点集合〈pointed set〉から特定された点〈要素〉を忘れる写像の機能・メカニズムに注目したのです。付点集合の圏を $`{\bf Set}_\bullet`$ とします。$`{\bf Set}_\bullet`$ の対象は、集合 $`X`$ とその要素 $`a`$ …

最近の型理論: デカルト閉圏の外部化・内部化とスノーグローブ現象

…にて、メタ巡回構造や万能対象*6の話をした後に幾分あきらめたような物言いをしています。 スノーグローブ現象が起きると、インスタンスレベルとメタレベルが混じり合うわけですが、エルブラン風のモデルの作り方をすると、さらに構文領域と意味領域も混じってきて、なんだか混沌としたスープ状の奇妙な構造物を相手にすることになります。奇妙と感じるのは我々に先入観があるからで、計算モデルの世界はそんなもんなのかも知れません。 スノーグローブ現象のメカニズムを明晰に理解することは難しいですね。「圏…

主キー/外部キーなんてドーデモイイ

…Aの符号化、UはCの万能対象(万能計算機のデータ領域)と考えることができます。興味がある人は確認してみてください。さて、Cの射 f:A→B が与えられたとき、f':A→K(B) が「fの代理」であるとは、次が成立することだとします。 f':A→K(B) と γB:B→K(B) で作られる余スパン A→K(B)←B のファイバー積P(プルバック図の頂点)が存在する。 ファイバー積の射影(プルバック図の辺)P→A は同型射(可逆射)である。 一番目の条件は、プルバック図がCをはみ…

スノーグローブ現象 再び

…これくらいにします。万能対象とスノーグローブ現象[D->D]⊆D となるようなDとしては、先に例に出した集合圏の単元集合のような小さなものもあります。Dがあまりに小さいと、世界全体(外の圏C)を映し出す(あるいは閉じ込める)ことはできません。圏Cの対象Uが万能(または普遍的)とは、Cの任意の対象Xに対して、X→U という埋め込みがあることです。埋め込みの定義は、先に言ったようにモノ射でいいときもあればEPペアにすべきときもあります。Cの部分圏として埋め込みの圏を指定することも…

大域計算モデルと局所計算モデル

…め込めるとき、それは万能対象(universal object)と呼びます。Uが万能(普遍的)なら、UU→U と埋め込めるので反射的になります。UはCのスノーグローブ対象だとも言えます。外の圏Cの構造を対象Uのなかでソックリ再現できます。つまり、外の圏Cと中の対象Uの関係はメタ巡回的となっています。「ラムダ計算、デカルト閉圏、ラムダ代数」の場合は、メタ巡回構造がハッキリとしているのですが、ここまでうまくいかないまでも、なんとなくメタ巡回的なことはあります。スノーグローブが外の…

関数で関手が表現できるって変でしょ、どういう仕掛けかな?

…もみなせます。つまり、おおざっぱに言えば: デカルト閉圏であるならば、型構成子Tと総称関数fにより自己関手Fを表現できるのです。 *1:一般的には、そのようなことが保証できない、ということです。 *2:最近書いた「デカルト閉圏を計算するスタックマシン、シーケント計算、カリー/ハワード対応」とは少し記法が違います。[A, B] は B←A と同じ意味です。 *3:普遍対象(万能対象)と呼ばれる特別な対象Uがあれば、C全体を(したがって|C|も当然)C(U, U)に埋め込めます。

セミナー補足:教科書・参考書

…報学入門』(朝倉書店 1982)がありましたが、今は絶版で入手困難でしょう。横内寛文・著『プログラム意味論』(共立出版 1994)なら手に入るのではないでしょうか([追記]絶版だそうです(泣く)、コメント欄参照[/追記])。領域理論も圏論も書いてあります。この本の最後のほうには、世界(圏)全体が忠実に埋め込める世界内のモノ(対象)として万能対象というのが定義してあります。万能対象内に実現されたマイクロコスモスは、外の世界とまったく区別が付かない完全なスノーグローブになります。