…落として捉えること（レイフィケーション）ができます。これは、プログラミングにおいて、プログラムコードもデータだとみなせるのと似た状況です。半グラフ・プロ射／半グラフ変形一般に、二重圏の縦1-射を単に射ともいい、横1-射はプロ射〈promorphism | proarrow〉ともいいます。この用語法の習慣により、半グラフ二重圏の横1-射は半グラフ・プロ射〈semi-graph promorphism | promorphism between semi-graphs〉とも呼びま…

…作が内部化（あるいはレイフィケーション）です。逆に、デカルト閉圏内の対象・射をデカルト閉圏の外に取り出すことが外部化（あるいは反レイフィケーション）です。自然言語混じり形式言語の意味論を構成するときは、自由度が高い外部的意味領域を使い、ソフトウェア実装（に近いモノ）の純形式言語の意味論は内部的意味領域を使います。自然言語混じり形式言語の議論（構文論も含める）では伝統的な自然演繹やシーケント計算を使い、純形式言語の議論では依存型付きラムダ計算を中心に考えます。大枠は以上に述べた…

…、$`\J`$ を反レイフィケーション〈dereification〉と呼んでましたが、ちょっと分かりにくい言葉なので、型圏化に置き換えました。型圏化を前提にすれば次のように言えます。 型は圏〈銀河〉の対象だが、それ自体が圏である。 相対的完備性「依存型と総称型の圏論的解釈」で、自己完備〈self complete〉な圏という概念を導入しています。ここでは、自分自身だけではなく、他の圏に対して相対的に完備という概念を導入します。$`\cat{C}`$ は前節と同じとして、$`\…

…トへの作用を内部化〈レイフィケーション〉できるとすると、コンビネータであるデカルト・ペアリングも次のように内部化できます。 $`\langle\hyp, \hyp\rangle : [X, A]\times [X, B] \to [X, A\times B] \In \cat{C}`$ $`\langle\hyp, \hyp\rangle^\wedge : {\bf 1} \to [ [X, A], [ [X, B] , [X, A\times B] ] ]\In \cat{…

… は $`J`$ のレイフィケーション〈reification〉*1とかコード化〈encoding〉と呼びます。集合部分圏であるデカルト圏 $`\cat{K}`$ が作用しているデカルト圏 $`\cat{C}`$ では、$`\cat{K}`$ に属する集合／写像を $`\cat{C}`$ 内にレイファイ／コード化〈エンコード〉することができます。テンソリング〈コパワーリング〉テンソリングとモノイド作用は独立な概念です。テンソリングのためにモノイド作用が必要なわけではありません…

… J(B) （Jは反レイフィケーション埋め込み関手）と置けば得られます。つまり、 $` \Delta_f := \Delta_{J(f)}`$ さらに、f = !A, B = 1 と置けば $`\Sigma_A \dashv \Delta_A \dashv \Pi_A`$ が得られます。 $` \Delta_A := \Delta_{!_A} := \Delta_{J(!_A)}`$ 「依存型と総称型の圏論的解釈」と「依存型とΣ-Δ-Π随伴、そしてカン拡張」で述べたのは、この…

… C があるとき、反レイフィケーション関手Jにより、関手 J(f):J(A) → J(B) in CAT が誘導されます。J(f) をプレ結合〈pre-compose〉することは、[J(B), C] → [J(A), C] という関手（関手圏のあいだの関手）を定義します。その関手を Δf とします*2。 $` \Delta_f(\mbox{-}) := J(f)\ast \mbox{-} `$ $` \Delta_f:[J(B), \mathcal{C}] \to [J(A)…

…ミリーとカインド 反レイフィケーションとパイ型 シグマ型 依存型理論の記法 依存型と総称型 「依存積型」「依存和型」について：1. 記憶に頼った用語法で記事を書いた。2. 別な用語法の論文を読み、ゲゲッとなった。3. 訂正と謝罪。4. コメント欄のご指摘で「どちらも許容」と分かった。5. 訂正と謝罪を訂正 ← 今ここhttps://t.co/6U3KgXGtKu— 檜山, キマイラの爺さん (@m_hiyama) 2021年1月14日 要旨と注意デカルト閉圏Cを舞台として型理…

…く使っていた言葉は「レイフィケーション」です。 ブログ内 「レイフィケーション」の検索結果 余談ですが、レイフィケーションに関係するよく読まれた記事は： いまさらながらだけど、オブジェクトとクラスの関係を究めてみようよ Aliceは存在したんだぜ「レイフィケーション」のような、よくわからない言葉を使って能書きをたれることが、いわば僕の仕事だったわけですが、能書きでソフトウェアができるわけはありません。ミッションとして課せられた二項目の要求も、やや趣味的な三項目の方針も、それを…

…つの宇宙 U∈V とレイフィケーションで無限系列をシミュレートする手があるかも知れません。いずれにしても僕には、適切な強さを持つ宇宙の系列を実際に作ってみせる技量はないので、楽観的に「たぶん大丈夫」と考えて、ご都合主義的マルチバースを想定することにします。けっこう多くの人がこういうパラダイスを期待している、あるいは（潜在的には）使っているんじゃないかと思います。“宇宙”関係： 集合の宇宙論 ファンタジー： (-1)次元の圏と論理 圏論的宇宙と反転原理と次元付きの記法 有界な圏…

…pe1 : Type2 : Type3 ... のような人為的な無限チェーンを想定したりします。このような細工も、銀河を認めない態度からだと思われます。ある一定の階数以上の高階なモノが不要なら、階層を打ち切って銀河（＝最上階）にしてしまえばいいと思います。自己言及が必要なら、レイフィケーション機構を導入して、Type : Type を合理化すればいいでしょう。 *1:Nの空部分集合も定義上はアトムですが、空集合はアトムから除外してもいいでしょう。気にする程の問題ではないです。

…。）つまり、gというレイフィケーション機能を付けた一階述語論理内で自己言及が可能です。しかしgは、構文領域の存在物Pred(D)と意味領域の存在物Dをまたぐ写像なので、当該の一階述語論理体系内で表現されていません。ニ階述語論理体系を使えば、体系内でgを記述できるでしょうか？ たぶんできます。そのうちやってみます。（詳細は別途記述予定。）とはいえ、奥野本の趣旨と構成からいえば、自己言及への“言及”はそもそもアラズモガナなので、一段落（p.49からp.50）削除すべきです。消極的…

…8年） メタクラス・レイフィケーション 入門 → いまさらながらだけど、オブジェクトとクラスの関係を究めてみようよ （2008年） ラムダ計算 入門 → JavaScriptで学ぶ・プログラマのためのラムダ計算 （2007年） ゲーデルの不完全性定理 入門 → プログラマのための「ゲーデルの不完全性定理」(1) （2006年） 公開年を見るとわかるように、いずれも10年近く前です。一度書いてしまうと、同じことを繰り返し書く気にはなれないので、このテの入門記事を書くことはなくな…

内容 レイフィケーション 形式化された証明と算術プログラミング メタプログラミングと妖精さん達 レイフィケーション2006年の正月に、「ゲーデルの不完全性定理」に関する記事を何本か続けて書きました。 最初の記事： プログラマのための「ゲーデルの不完全性定理」(1) 3本目の記事である「プログラマのための「ゲーデルの不完全性定理」(3)：自己適用からゲーデル化へ」の「メタレベルも取り込むこと：レイフィケーション」という節に次のような絵を入れています。この絵は、「記述される対象物…

…す。この機能を我々はレイフィケーション（reification）と呼んでますが、リフレクション（reflection）とかイントロスペクション（introspection）と呼ぶほうがお馴染みでしょう。設計時／プログラミング時に概念として意味を持つ情報が、実行時にもデータとして存在していて、かつ“概念を表現するデータ”（メタオブジェクト）をプログラムで操作可能なのです。Webシステムの設計時に意味を持つ、クライアント状態（画面）、リクエスト処理、ハイパーリンクなどが、実行時の…

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

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

…ーションを含む型」のレイフィケーション（reification）、あるいはメタ循環（メタ巡回）構造です*2。Catyのメタ循環構造はまだ不完全なのですが、少しずつ整備しています。そのうち、副産物としてランチ注文フォームが作れるようになるでしょう。ついでに、僕がなんでメタ循環構造に拘るかをチョット： コンピュータが扱えない対象物に対する操作は、人間がやることになります。その作業が十分に知的で、コンピュータでは出来そうにない事ならやる意義も価値もあるでしょう。しかし、さして知的で…

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

…。リフレクションとかレイフィケーションと呼ばれる操作が可能となり、スノーグローブ現象が引き起こされます。Catyのスノーグローブ現象と山猫スクリプト巡回的包含関係 String ⊆ Json ⊆ Expr ⊆ String は、厳密に言えばインチキです。Exprを、例えば構文解析後のツリー（AST; Abstract syntax Tree）の集合だと思えば、Expr ⊆ String がウソなのは明らかでしょう。しかし、Exprはテキストへとマーシャリングできるので、Mar…

…hebenさんの： レイフィケーションとパワータイプって同じような概念ととらえてよいのかな? 檜山さんのエントリで、is-created-by とレイフィケーションは、他の関係と矢印の向きが逆な気がするんですけど、何か意図があるのでしょうか? id:higeponさんの質問は、当該エントリーとは別な文脈でのものですが、一連の流れとしては関連するので。もし、「いまさらながらだけど、オブジェクトとクラスの関係を究めてみようよ」の続編を書くとしたら（書かないけどね）、MetaObj…

…わけで、メタクラスやレイフィケーション（reification）なんて少し珍しい概念も含めて、オブジェクトとクラスの関係を整理してみましょう。今回の目標は、「Classクラスオブジェクト」（書き間違ってないぞ！）という概念を、実感を伴って明確に理解することです。内容： まずは、クラスの継承関係を絵に描く オブジェクトの生成とインスタンス概念 オブジェクト・プレーンとクラス・プレーン クラスオブジェクトとレイフィケーション クラスオブジェクトが所属するクラス すべてを一階に押し…

…ベルも取り込むこと：レイフィケーション ゲーデル符号化、ゲーデル化 また自己批判 前の記事 速攻速習編 全体目次＋総論 ●著述スタイルを変更します、たぶん前回（第2回）は、実は当初の予定から外れたエントリーでした。なぜに予定外だったかを説明するエントリーはなおさらに予定外となります。そんな展開では、当初の予定なんか守れっこないなー、… まー、そもそも予定を守る必然性もないし。そこで、説明としての筋書きはあまり気にせず、日記風(?)のスタイル（思い付きと勢い重視）で書き続けよう…