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

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

レイフィケーション の検索結果:

Σ-Δ-Π随伴、もう一言

… J(B) (Jは反レイフィケーション埋め込み関手)と置けば得られます。つまり、 さらに、f = !A, B = 1 と置けば が得られます。 「依存型と総称型の圏論的解釈」と「依存型とΣ-Δ-Π随伴、そしてカン拡張」で述べたのは、このような状況でした。ガロア接続のΣ-Δ-Π随伴ガロア接続とは、順序集合(またはプレ順序集合)に対して定義した随伴概念です。ガロア接続に馴染みがないなら、次の記事とそこからのリンクをたどってみてください。 ガロア接続(順序随伴系)の簡単な例 以前に…

依存型とΣ-Δ-Π随伴、そしてカン拡張

… C があるとき、反レイフィケーション関手Jにより、関手 J(f):J(A) → J(B) in CAT が誘導されます。J(f) をプレ結合〈pre-compose〉することは、[J(B), C] → [J(A), C] という関手(関手圏のあいだの関手)を定義します。その関手を Δf とします*2。 引数〈argument〉が下付きだったり丸括弧だったりは、習慣や気まぐれで意味はありません。プログラミング言語だと、引数渡し構文が一種類だけのものがありますが、それはそれで見…

依存型と総称型の圏論的解釈

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

文書処理:ソフトウェアAliceの設計方針

…く使っていた言葉は「レイフィケーション」です。 ブログ内 「レイフィケーション」の検索結果 余談ですが、レイフィケーションに関係するよく読まれた記事は: いまさらながらだけど、オブジェクトとクラスの関係を究めてみようよ 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):自己適用からゲーデル化へ」の「メタレベルも取り込むこと:レイフィケーション」という節に次のような絵を入れています。この絵は、「記述される対象物…

Catyの特徴と機能をイメージできるようなオハナシ

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

スノーグローブのなかの小人さん達

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

入れ子の世界が大好きだけど怖い

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

2010年末に再び考える、Catyスキーマとユーザーインターフェース

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

目の付けどころがいいねー、そして、間違ってもいいと思うぞ

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

Catyのインタプリタ=評価関数の表示的意味論

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

オブジェクトとクラス、とりあえずご質問に答えます

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

いまさらながらだけど、オブジェクトとクラスの関係を究めてみようよ

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

プログラマのための「ゲーデルの不完全性定理」(3):自己適用からゲーデル化へ

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