…リーに向けて // スノーグローブ現象／マイクロコスモ原理」「マイクロコスモ原理と逆帰納ステップ」参照）による標的環境の高次元化を防いでいます。前々節で2-グラフは定義しているのですが、等式的2-グラフ（3-グラフの特殊なモノ）を定義するには、2-パスの集合 $`G_2^*`$ が必要になります。2-パスの集合は、次の公式で与えられます。$`\quad G_2^* := |\mathbb{Path}_2(G_2)|_2 = |\mathbb{U}_2( \mathbb{Fre…

…に圏を前提します！ スノーグローブ現象／マイクロコスモ原理（「依存アクテゴリーに向けて // スノーグローブ現象／マイクロコスモ原理」参照）は避けようがないことがあるので、そこは開き直ります*2。集合圏 $`{\bf Set}`$ をターゲットとする小さい圏〈small category〉の指標は次のようになります。幾つかの注意事項をすぐ後に書きます。$`\T{signature }\NN{SmallCategory}\T{ within } ({\bf Set} \T{ a…

…スード アナロジー スノーグローブ現象／マイクロコスモ原理 一貫性地獄 型理論からの事例 そしてそれから 弱、厳密、スード「依存アクテゴリーが面白い」で、「弱二重圏〈スード二重圏〉」という言葉に次のような注釈を付けました。 「弱」「スード」は、プロ方向の結合の法則が厳密に〈等式として〉成立するとは限らないことを意味します。単に「二重圏」と言った場合、厳密二重圏か弱二重圏かは人により場合により違います。 このブログ内で単に「二重圏」と言ったら、それは弱二重圏〈weak doub…

…圏の外部化・内部化とスノーグローブ現象」では、引き戻し付きデカルト閉圏を導入しました。有限完備デカルト閉圏〈finitely complete cartesian closed category〉と言っても同じだし、こっちのほうが一般的呼び名でした。有限完備デカルト閉圏には良い性質があります。それはエーレスマン夫妻〈Charles and Andrée Ehresmann〉の定理で述べられます（nLab項目 internal category // In a cartesia…

…圏の外部化・内部化とスノーグローブ現象 外部的意味領域は、$`{\bf Set}`$ や $`{\bf SET}`$ のようなコア銀河（「最近の型理論： 宇宙と世界、そして銀河」参照）を環境とする概念的事物達から構成されます。一方の内部的意味領域は単一のデカルト閉圏〈銀河〉のなかにある対象・射だけから構成されます。概念的意味領域にある諸々の概念的事物を、内部的意味領域であるデカルト閉圏に押し込めてしまう操作が内部化（あるいはレイフィケーション）です。逆に、デカルト閉圏内の対象…

…は、このような状況をスノーグローブに例えています。*3雪が降る景色のなかにある模型の家は、模型そっくりなホントの家の机に上に置いてあるのです。このスノーグローブを眺めることは、本物の家を“家の外から”眺めることと同じです。あるいは、「そっくりハウス」（谷山浩子）のジャケットの絵が同じ状況を描写しています。*4女の子が見ている家は、この子が居る家です。「自分のなかに自分が埋め込まれている」ことを素朴集合論の概念・記法で書けば $`x \in x`$ です。これは矛盾を導くから排…

…圏の外部化・内部化とスノーグローブ現象 最近の型理論： 宇宙より銀河 最近の型理論： 具体的・構文的なコンテキスト 最近の型理論： 拡張包括構造を持ったインデックス付き圏 関連記事： 射ファミリーと圏論的コンビネータ 圏の束構造と包含的圏 一般化されたファミリーの圏 自然言語混じり形式証明の意味論と最近の型理論 宇宙と世界語感としては、世界より宇宙のほうが広い感じがしますが、ここでは、世界は宇宙（と後述の銀河）の集まりだとします。$`\mathscr{W}`$ がひとつの世界…

…参照してください。 スノーグローブ現象 再び マイクロコスモ原理の恐怖 証明の“お膳立て”のやり方 5： 証明可能性判断と推論規則 *1:随伴性は、双対対象ペア、随伴関手ペアを含む一般的な概念ですが、ここでは随伴関手ペアの意味です。 *2:もちろん、特定の文脈では定義され、識別もされます。 *3:世間一般に、不正確さや混乱のリスクがあっても、簡略な用語法・記号法を採用する傾向があります。面倒なのは嫌なんですが、こういう簡略さが、理解をおおいに阻害しているのも事実です。ほんとに…

…事で述べています。 スノーグローブ現象 再び マイクロコスモ原理の恐怖 推論規則と証明可能性判断「証明の“お膳立て”のやり方 4： 随伴による集合差の定義」の「前提の命題を推論規則として使う」では、推論規則と証明可能性判断を同じ形で書きました。同じ形で書いて差し支えないですが、厳密には、推論規則と証明可能性判断は別物です。推論規則とは、その名のとおり、どのような推論が可能かを書き下したものです。例えば、命題Pが証明済み、命題Qも証明済みのとき、連言命題P∧Qを導いてかまいませ…

怖い話。内容： スノーグローブ現象 マイクロコスモ原理 僕が出会った例：モノイド圏 どうやって無限後退を避けるか マイクロコスモ原理とスノーグローブ現象 過去記事 スノーグローブ現象スノーグローブ現象（snowglobe phenomenon）とは、世界（あるいは環境）の構造が、世界のなかのモノに写し込まれる現象です。特定のモノが持つ構造が世界の構造を反映することになります。スノーグローブ現象については、次の記事とそこから参照されている記事群を見てください。 スノーグローブ現…

…の記事「ラムダ計算とスノーグローブ現象：oto-oto-otoさんの疑問に答えるに次のように書いています。 バエズによると（間接伝聞）、2002年フィールズ賞受賞者のウラジーミル・ヴォエヴォドスキー(Vladimir Voevodsky）が、ホモトピー・ラムダ計算（the homotopy lambda calculus）なるものを作り始めているそうです。 その後、アウディ（Steve Awodey）やシュルマン（Michael (Mike) Shulman）ら多くの人が参加…

…ったのです。その事情は、上の例でだいたい察しが付くかと思います。自分で自分をテストする都合上、自分の実行環境のなかに自分のモデルを作る事が、さまざまな形で要求されます。“テストする自分”と“テストされる自分”がスノーグローブ現象として登場するのです。スノーグローブ現象は、テスト以外での利用価値もあります。テストはやらなくちゃいけないけど、メンドクサくてイヤなものです。テストを書くことを（ひとつの）目的としたスクリプト言語があれば、状況は改善するんじゃないかな、と思っています。

…できます。世界全体がスノーグローブ（和風の表現なら、箱庭の小世界）と同型になるわけです。 ここで使っている言葉「スノーグローブ」は僕のお気に入りで、このブログには何度も出てきます。今年（2012年）の記事でも「スノーグローブ」概念を振り返ったりしてます。 スノーグローブ現象 再び 現代のコンピュータの原理は、自分自身をも含む外部の世界を操作可能なデータに符号化してしまうことです。符号化された世界がスノーグローブです。符号化＝レイフィケーションですから、レイフィケーションされた…

…対象に写り込むので、スノーグローブ現象が起きている状況だとも言えます。ラムダ計算の大域計算モデル、つまり圏論的なモデルというとデカルト閉圏でほぼ決まりなのですが、局所計算モデルはなんだかイッパイ種類があるようです。ラムダ代数（lambda algebra）、ラムダ構造（lambda structure）、組み合わせ代数（combinatory algebra）、適用構造（applicative structure）、型フレーム（type frame）とか。大域と局所の区別以外…

…なかに“かなり正確なスノーグローブ”を作ろうとしているのです。少し前に「スノーグローブ現象 再び」という記事を書いたのも、そんな背景です。「かなり正確なスノーグローブ」とは、Catyシステムに関する情報を、Catyのデータ領域に埋め込む機能です。Catyのデータ領域はXJSON(JSONをわずかに拡張したフォーマット）データの集合なので、スノーグローブの実現は「メタ情報 → XJSONデータ」という写像を作ることになります。このような写像をレイフィケーションと呼びます。レイフ…

僕は「スノーグローブ」という言葉を気に入ってましてよく使ってますが、もともとはジョン・バエズ（John Baez）が説明のために持ちだした比喩です。次の絵もバエズから拝借。見ればわかるように、ガラス玉のなかに箱庭の世界が閉じ込められています。圏論の言葉ではデカルト閉構造（より一般にはモノイド閉構造）のことで、世界全体がある対象の内部に反映される現象です。このブログで「スノーグローブ」という言葉を最初に出したのは2007年夏ですね。 圏論的指数の周辺：ラムダ計算、デカルト閉圏、…

…になります。UはCのスノーグローブ対象だとも言えます。外の圏Cの構造を対象Uのなかでソックリ再現できます。つまり、外の圏Cと中の対象Uの関係はメタ巡回的となっています。「ラムダ計算、デカルト閉圏、ラムダ代数」の場合は、メタ巡回構造がハッキリとしているのですが、ここまでうまくいかないまでも、なんとなくメタ巡回的なことはあります。スノーグローブが外の世界と少しズレている、歪んでいる、くもっている、という感じです。最近僕がよく使っているモデルはデカルト半環圏です。デカルト半環圏は、…

…ですが「ラムダ計算とスノーグローブ現象：oto-oto-otoさんの疑問に答える」において、ヴォエヴォドスキーのホモトピーラムダ計算に触れたことがあります。ジョン・バエズなども注目していたようですが、当時目にした（できた）資料は次だけ。 Title: A very short note on homotopy lambda calculus (October 2, 2006) Author: Vladimir Voevodsky URL: http://www.math.ia…

…「再帰」でしょうが、スノーグローブ（もともとはバエズが使っていた言葉）、メタ循環／メタ巡回、レイフィケーションなんて話題でしょっちゅう言及しています。 「スノーグローブ」を含む記事のリスト 「メタ巡回」を含む記事のリスト 「レイフィケーション」を含む記事のリスト 「日常」タグを付けた記事でも： ムシバイキンと再帰 再帰現象の体験 職業がら、なのかな？ ある種の再帰的あるいは多層的構造について 手塚治虫の『火の鳥』でも、入れ子になった世界が出てきます（仏教的な世界観なのでしょう…

…ではしばしば出てくるスノーグローブ現象（バエズの用語； 檜山のお気に入り）です。レイフィケーションとかメタ巡回構造などの言葉も同様な現象・機構を指しています。そういう状況では、圏と圏の対象の意図的な混同もある意味では合理化できます。一方、対象が圏である圏は全然珍しくないですよね。Catはもちろんそうですが、モノイドの圏とか順序集合の圏だって、圏の圏と考えていいでしょう*1。「圏の圏の圏」とかいくらでも考えることができます。高次圏（higher category, n-cate…

…巡回構造 Catyのスノーグローブ現象と山猫スクリプト Evalを定義する パラメータとプロファイルCatyのコマンド（ネイティブコマンド）やスクリプトはパラメータを受け取れます。「パラメータ」は「引数」と同義ですが、オプションでない引数（プレーン引数、位置引数、名前なし引数などとも呼ばれます）を単に「引数」と呼ぶことが多いので、「オプション（名前付き引数） + 位置引数」の意味で「パラメータ」を使います。パラメータのデータ構造paramは次のスキーマで定義できます。 typ…

…呼ばれる構造ですね。スノーグローブ構造と言ってもいいかもしれません。Catyの内部を流れるデータは、表層部から中核部まですべてJSONデータです*5。JSONベースのデータ型は、帰納的定義を持つので、スカラーからはじめる帰納ステップにより列挙可能です。つまり、ブルートフォーステスト用データは容易に自動生成できます*6。こういうデータを三日三晩、自分自身に向けて打ち込み続ける、と。そんな苦行に耐え切れたなら、「俺って丈夫」って言ってもいいのじゃないかと思います*7。マゾっぽいけ…

…askellの世界（スノーグローブ）内でカリー化のミニチュア版を構成したいなら、タプルを引数とする g :: (a, b) -> c から g^ = (curry g) :: a -> (b -> c) を作り出すようなオペレータ curry :: ((a, b) -> c) -> (a -> (b -> c)) を定義することになるでしょうね。rst76さん曰く： 別の言い方をすると、g :: Int -> Int -> Int -> Int を Int -> Int ->…

トラックバックをたどって、「スノーグローブとゲーデルとマトリックス」： とりあえず俺はペンローズ派だ。小さく主張しとこう。 アハハハハ。だいぶ笑った。なんでおかしいか、というと： ジョニー（a.k.a. hiroki_f）は、ハードボイルドな物理研究者を目指しているようだ だが、彼はなんか変なところがある 「俺はペンローズ派」 -- あーーーー、ヤッパリ 意外性で大笑いすることもあるが、納得感も笑いを引き起こすらしい。あと、「小さく」もおかしい。

…NN という対応は、スノーグローブ現象によるミニチュア化の一例です*2。関数の自己適用／自己言及ここで現実のコンピュータを眺めてみれば、関数コード（型がNNであるデータ*3）は、そのままただちにビット列データとみなせるので、NNからNへの埋め込みが存在します。それならいっそ NN⊆N とみなしてしまいましょう。すると実行エンジン（apply, eval, exec, engine、お好きに呼んでください） E:NN, N→N は、E:N, N→N とみなしてもいいことになりま…

…o日記 ラムダ計算とスノーグローブ現象：oto-oto-otoさんの疑問に答える superstring04さん -- 檜山セミナーに行ってきたよ - 公的内省Δ まだスノーグローブ：superstring04さんへのフォロー 問題点アンケートによると： やはり、机が足りない／椅子が硬いというご指摘が圧倒的に多かったです。次回はなんとかしたいと思ってます。 時間が短い、計算やお絵描きが少ない、というご意見も多いです。 「これからと思ったら終わってしまった」という感じを抱いた方…

…のミニチュアが手元のスノーグローブに入っているとすれば、その中にあるスノーグローブには、もっと小さな世界が広がっているだろう、と。逆に考えて、私たちの世界もまたスノーグローブの中で、一段上の世界があるのかもしれない、と想像できる。 このような構図に僕はすごく魅力を感じるのです。手塚治虫の影響が入っているのかも知れません。これは個人的な趣味や傾向性の問題ですが、スノーグローブ的な状況がSFや映画によく出てくるということは、けっこう多くの人にアピールするんだろうな、とも思います。…

…の道具に使えます。 スノーグローブ現象は計算機をからめて語られていたけど、純粋数学的にもでも起こるようなことなのか。 今回は、計算機と計算現象を素材にしました。が、数学でも論理でも物理でも至るところに出現します。圏論的には、モノイド積とその随伴関手（指数）を扱っているので、論理の演繹定理、（古典的であれ現代的であれ）テンソル計算、結び目理論のライデマイスター移動やその拡張、量子テレポーテーションなども同様な現象として括れます。 論理とはなにか？ (4:完) -- 論理から圏へ…

…語やシステムのなかにスノーグローブ現象を発見することはできるだろうし、それこそが最良の練習問題だと思ったからです。KuwataさんはPythonで実例を書いてくれているので、まさに僕が望んだ宿題を即座に遂行してくれたことになっています。 後日セミナーの資料はちゃんと公開されるはずだし、 ウーン、確かにスライドは公開するけど、絵は入ってないのよね。どうせその場で手で描くつもりだから、なんかめんどくさくて。スライドは、価値ある資料とはとうてい言えませんね。参加された方が俺流まとめ…

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