…. Spivak〉の関手データモデル〈functorial data model〉に“衝撃”を受けていました。 デイヴィッド・スピヴァックはデータベース界の革命児か -- 関手的データモデル（2013-01-28） 衝撃的なデータベース理論・関手的データモデル 入門（2013-02-11） ほぼ同じ時期にアブラムスキーも、データベースに関するナカナカに衝撃的な理論を発表していたのです。僕は今まで13年間まったく知りませんでした。データベース・コミュニティで話題になったなんてこ…

…調べるには、可換環論や代数幾何っぽい道具が必要そうなので、このへんでやめておきます。前回も同じことを言ったけど、構文付き変換手インスティチューションの事例は、まだ色々あります。ローヴェアの代数セオリーやスピヴァックの関手データモデルも構文付き変換手インスティチューションの枠組みで記述できます。たぶん、まだ実例の紹介を続けるでしょう。 *1:「圏」をn-圏（n = 0, 1, 2, …）と解釈するなら「モデル圏」でもいいのですが、一般に、「圏」は1-圏と解釈するのが普通なので。

…データモデル 入門 関手データモデル／圏論データベース： その後の発展と現状 (2016) ローヴェア流セオリー論と統計モデル モナド・アプローチとリントンの定理モナド・アプローチにおける代数〈algebra〉とは、モナドのアイレンベルク／ムーア代数のことです。代数を（記号の乱用で） $`A = (A, \alpha)`$ とすると、それは次のように書けます。$`\quad \alpha : F(A) \to A \In \cat{D}`$ここで、$`\cat{D}`$ は圏…

…です。スピヴァックの関手データモデル（「衝撃的なデータベース理論・関手的データモデル 入門」参照）もローヴェア流セオリー論の応用例で、そこでは、指標またはセオリーはスキーマと呼ばれ、モデルはデータインスタンスと呼ばれています。（必ずしも圏論的ではない）論理では、論理式の集合をセオリーと呼ぶことがあります。これは、無関係ではありませんが、ローヴェア流セオリー論のセオリーとは少し違うので注意してください。統計セオリー論のアンビエント圏圏論的に確率統計の議論をするときの基本的なツー…

…ます。スピヴァックの関手データモデル（「衝撃的なデータベース理論・関手的データモデル 入門」参照）によれば、データベーススキーマの圏は、小さい圏の圏Catと同一視可能です。特定のスキーマAのデータベース状態は関手 P:A → Set とみなすのでした。スキーマのあいだの射 F:A → B in Cat があると、B上のデータベース状態 Q:B → Set は、A上のデータベース状態 F＊Q に引き戻せます。この状態引き戻し操作がΔFです。 ΔF:[B, Set] → [A, …

… Spivak〉は、関手データモデル／応用圏論で有名なMITの先生です。スピヴァックに関連する記事を幾つか挙げると： 2013-01-28 デイヴィッド・スピヴァックはデータベース界の革命児か -- 関手的データモデル 2013-03-04 スピヴァックの圏論教科書 Category theory for scientists 2016-05-10 関手データモデル／圏論データベース： その後の発展と現状 (2016) そんなスピヴァックのオンラインコースは Applied …

…話は、スピヴァックの関手データモデルとの類似点があるので、以下の記事が参考になるかも知れません。 衝撃的なデータベース理論・関手的データモデル 入門 スキーマとインスタンス -- 一般関手モデル 一般関手モデル：「圏の表示」の圏 Quivを箙の圏とします（既に出てきました）。Quivには始対象・直和・余等値核〈余イコライザー〉を定義できます。終対象・直積も定義できるので、モノイド積として直積を選びます。これにより、Quivは有限余完備でモノイド積を持つ圏となります。このQui…

…圏論内部からの動機 関手データモデルとデータ移行関手 型クラスとモデル 相対モナド プログラム最適化 おわりに 圏論内部からの動機カン拡張というと、マックレーンの有名な言葉： All Concepts are Kan Extensions があります。圏論に出現するすべての概念はカン拡張で説明できる、ということです。ちょっと大げさな気がしなくもないですが、標準的・典型的な圏論の概念がカン拡張に包摂されるのは事実です。極限／余極限は、圏論の重要な道具ですが、それぞれ右カン拡張／…

…データベース理論は、関手データモデルに近いものです。Command-Query分離で名前を出したメイヤー先生は、契約による設計〈design by contract〉でも有名です。ソフトウェア仕様技術の根本を、権利と義務という比喩で極めて的確かつ鮮やかに描き出してくれました。指標はメイヤーの意味での契約書とみなせます。利用者の権利と実装者の義務を記述したものが指標＝契約書です。メイヤーの契約モデルは単なる比喩にとどまらず、理論的分析にも大変に有効です。僕は、普通の証明の話でも…

…としてスピヴァックの関手データモデルがあります。スピヴァックは、リレーショナルデータベースの言葉を使って説明しようと試みているので、「関手データモデルはリレーショナルモデルと相性がいい」と僕は思い込んでいました。しかし、改めてスピヴァック理論を眺めてみると、ER図の圏論的定式化の形になっています。そして、使っている言葉はSQLの用語（テーブル、カラム）です。となると、「ER図は嫌い、SQLはけしからん」と言っている純粋リレーション主義者は、関手データモデルをハナから相手にしな…

…1302.6946 関手データモデル／圏論データベースのスピヴァックによる圏論入門書です。「スピヴァックの圏論教科書」で紹介しています。PDFは紙の本より少し古い内容で、タイトルも微妙に異なっています。 Higher Topos Theory Higher Topos Theory (Annals of Mathematics Studies)作者: Jacob Lurie出版社/メーカー: Princeton Univ Pr発売日: 2009/07/06メディア: ペーパー…

「関手データモデル／圏論データベース： その後の発展と現状 (2016)」 にて： FQL IDEがサポートする4つの言語のなかで、位置付けがハッキリしないカワイソウなFQL++ですが、「圏論の学習にはとても有用」という特徴があります。これだけを切り出して圏論学習ツールにして欲しいくらいです。FQL++に関しては、いずれ別な記事で語りたいと思っています。 FQL++について語ります。2013年の記事「圏と関手をできるだけ簡単に書き下す方法」の内容を、FQL++で書いてみます。…

…ッド・スピヴァックの関手データモデル（functorial data model）について紹介しました。 デイヴィッド・スピヴァックはデータベース界の革命児か -- 関手的データモデル 衝撃的なデータベース理論・関手的データモデル 入門 あれから3年3ヶ月が経過して、今、関手データモデルや圏論データベース（categorical database）の状況はどうなっているでしょうか。一言でいえば、 派手に喧伝はされてないが、着実に発展している となるでしょう。その進展の様子を次…

…ます。スピヴァックの関手データモデルと同じ発想です。「表現、加群、前層、インデックス付き圏、導来子」あたりにチラッと書いたことがあります。色々なオートマトン小さい圏Cからの関手 φ:C→Set がオートマトンだと定義すると、オートマトンのバリエーションを考えるのは簡単です。集合圏Setを他の圏に取り替えるだけで色々なオートマトンが出てきます。PtSetを付点集合（pointed set）の圏、Relを関係圏とします。φ:C→PtSet ならφは部分的決定性オートマトンです。な…

…ます。スピヴァックの関手データモデルなら、Cはデータベーススキーマで、C-集合はデータベースインスタンスです。集合圏の代わりにベクトル空間の圏を採用すれば、圏Cの線形表現となります。特に、Cが順序集合や有向グラフのときは箙＜えびら＞（quiver）の表現として知られているようです。ホムセットに足し算が定義された圏（Ab-豊饒圏）Cを考えましょう。対象が1つだけなら、圏の結合を掛け算と考えて、Cは多元環となります。多元環の表現と多元環上の加群は同じことで、足し算を保存する関手 …

…番目の絵について、「関手データモデル入門 3：とても便利なスピヴァック流パス記法」で説明したパス記法を使うと： Employee.age = Employee.birth.calcAge 従業員の年齢は、従業員の生年月日から年齢を計算 Employee.officePhoneNum = Employee.office.phoneNum 従業員の勤務先電話番号は、従業員の勤務先営業所の電話番号 と定義しています。これにより、写像ageとofficePhoneNumは基本的な写像…

…スピヴァックは、彼の関手データモデルの枠組みとしてderivatorを意識しているのでしょう。ひょっとして（単なる憶測ですが）、データマイグレーション関手のアイディアの源泉は、derivatorの順像関手（direct image functor）かもしれません。「関手データモデル入門 4：ためらってしまう心を取り除く」で、 最近僕は、導来圏／導来関手、ホモトピー・カン拡張など、自分とは何の縁も接点もないと思っていた概念が、実務上も使えるんじゃなかろうか、という気分がしてます…

…なー、と関心します。関手データモデルにしろologにしろ、圏論を使っているとはいえ、どんな教科書にも載っている範囲の知識です。スピヴァックは、簡単な道具をうまく組み合わせて目覚ましい成果を挙げます。例え話で言うならば、ハイテク機器を駆使するわけじゃーないけど、誰もが困っていて半ば諦めている問題を、日曜大工道具で見事に解決してしまう、スピヴァックはそんな人でしょうか。おおよそ「olog = schema = 圏」と考えていいのですが、ologと関手データモデルのスキーマの違いは…

これは「関手データモデル入門」シリーズなんですが、なんだか道徳の訓話みたいなタイトル。なんだこりゃ？ まー、ちょっと訓話っぽいかもね、心の持ち方みたいな話だから。「関手データモデルからの教訓とノウハウ」と多少かぶってます。今年1月に、「デイヴィッド・スピヴァックはデータベース界の革命児か -- 関手的データモデル」というタイトルのエントリーを書いたわけですが、僕の評価では、スピヴァックは疑問の余地なく革命児です。データベースだけでなく、ITと計算科学に対して革命的な発見をした…

スピヴァックが関手データモデルでやったことは、データベースの諸概念を極端に単純化することにより、圏の基本概念（圏、関手、自然変換）だけで書き直すことです。これにより、圏論のあらゆる手法をデータベースに適用できる途が開けたわけです。徹底的に夾雑物を排除して単純化すればいいことあるよ -- これが関手データモデルから得られるひとつの教訓です。この教訓は、いつか役に立つとかではなくて、すぐさまに使えるノウハウでもあります。僕自身、身近な懸案に適用して効果があるのを確認しています。頂…

…ルは、スピヴァックの関手データモデルをデータベース以外にも適用する試みです。とはいえ実際のところ、特別に一般化する必要性は薄いですね、スピヴァック理論が既に十分に一般的に作られているので。今回の話も二番煎じで、関手データモデルがインスティチューションを定義することは既にスピヴァックが示しています。この事実を、観点と記述スタイルを若干変えて説明してみます。内容： 言葉と記号の約束 だいたいのところ（概要） 有向グラフに対する圏的演繹系とグラフ制約の圏 Pathモナドと有向グラフ…

スピヴァックの関手データモデルでは、圏の表示が重要な役割を果たします。なにもスピヴァック理論にかぎらず、圏一般において表示は重要です。特に有限表示（finite presentation）は、我々人間が手で圏を書き下す唯一の方法と言っていいでしょう。そこで、圏の有限表示について考えてみます。圏の有限表示とは、“ノードの個数”も“辺の本数”も有限な有向グラフと、有限個のパス同値関係（path equivalence relations）の組です。パス同値関係とはスピヴァックの用…

…/追記] プレーンな関手データモデルでは、スキーマ全体からなる圏Schは圏の圏Catの部分圏とみなせる圏です。Sch = Cat と考えてもいいでしょう。S∈|Sch| に対して、関手圏 [S, Set] がスキーマSのインスタンスの圏となります。Schの選び方を変えたり、集合圏Setを別な圏に取り替えたりして、様々なバリアントを構成できます。スキーマ全体からなる圏をドクトリン、インスタンスを構成するための圏をアンビエント圏と呼ぶと、プレーンな関手データモデルでは「ドクトリン…

…カケはスピヴァックの関手データモデルです。「デイヴィッド・スピヴァックはデータベース界の革命児か -- 関手的データモデル」のコメント欄でid:bonotakeさんとのやり取り（http://d.hatena.ne.jp/m-hiyama/20130128#c1359936671 ）で、 AlloyモデルとRDBが似てる、とかじゃなくて、まったく同じ概念を具現化しているとなれば、Alloyでデータベース設計やプロトタイピングがすごく実際的になる気がします。 関手データモデルと…

…、スピヴァックによる関手データモデルのセッティングを復習します。ただし、出てくる言葉に「データベース」という形容詞は付けません。データベース以外でも使うつもりがあるからです。以下の2つの記事に書いた内容の要約です。 スキーマとインスタンス -- 一般関手モデル 一般関手モデル：インスタンスのモノイド積とテンソル積 Schを“圏の圏”として、ドクトリンと呼びます。ドクトリンの対象 S, T などがスキーマであり、個々のスキーマは圏です。スキーマのあいだの関手 σ:S→T はドク…

…ょう。スピヴァックの関手データモデルはごく最近の話題ですが、使っている圏論は初等的なものです。というわけで、21世紀のモダンな圏論を知る／使うような機会はないですね。ジェイコブ・ルーリー（Jacob Lurie）が何やらやっているらしい事は知ってますが、僕の手が届くようなシロモノじゃないし。スピヴァックを通じて、間接的にルーリー的な発想をチョビっとはうかがい知ることが可能かなぁー？？ という程度。昨日、渋谷のMARUZEN&ジュンク堂書店に寄ったら、雑誌バックナンバーのコーナ…

スピヴァックの関手データモデルは、実に示唆に富んでいます。スピヴァックのアイディアは、データモデルに限らず、ソフトウェアシステムのさまざまな側面のモデル化に使えそうです。関手データモデルの要点を簡略にまとめるなら： （データベース）スキーマは圏である。 （データベース）スキーマの制約は可換図式である。 （データベース）スキーマの全体は“圏の圏”である。 （データベース）インスタンスは（データベース）スキーマからの関手である。 （データベース）インスタンスのあいだの準同型射は自…

関手データモデルのデイヴィッド・スピヴァックが、圏論の教科書を書いたようです。商業出版ではなくて、Web上にPDFが公開されています。スピヴァックの大学での講義のテキストとして書かれたようです。 Title: Category theory for scientists Author: David I. Spivak Submitted: 27 Feb 2013 URL: http://arxiv.org/abs/1302.6946 This book attempts to…

…ります。(その1) 関手データモデル： スピヴァックの関手データモデルには色々と刺激を受けました。スピヴァック理論を実際に使ってみたいですよね。関係データベースのほうがスピヴァック理論を適用しやすいでしょうが、僕はもともとXMLのような“文書っぽい”データが好きなので、入れ子と並びを持つデータを直接扱いたいのです。この点では、「ドキュメント指向」を標榜しているMongoDBのほうが向いているでしょう。(その2) 現実的な要求： データの操作がボトルネックになって困っている状況…

「関手データモデル入門 2.1：名称変更のお知らせ（それだけ）」（入門 2.1）でお知らせしたように、「関手的」の「的」を取って「関手データモデル」とします。「関手的データモデル入門 2：統一的に制約を書く方法」（入門 2）にて： それにしても、「入門 2」なんて番号付けていいんでしょうかね？ 「衝撃的なデータベース理論・関手的データモデル 入門」を「入門 1」とみなすつもりですが、「入門 3」「入門 4」があるかどうか不安。 不安(苦笑)。なので、小ネタも混じえようかと。ス…