現場の集合論としての有界素朴集合論 - 檜山正幸のキマイラ飼育記 (はてなBlog)
「奥野幹也『理論から学ぶデータベース実践入門』はどこがダメなのか」のなかで、ピンクで「（詳細は別途記述予定。）」と書いてあるところが6箇所あります。これらの“ピンクの宿題”を順不同で片付けていくシリーズ第二弾です。 データベース理論などを展開するのにお手頃な集合論・述語論理について云々します。 ピンクの宿題 その1 [奥野さんが言う集合論・述語論理とは、]あくまでリレーショナルモデル界隈を説明・分析する道具・枠組みのことであって、一般的集合論と一般的述語論理の話ではありません。（詳細は別途記述予定。） ピンクの宿題 その3 [奥野さんは、]述語論理のある特定の体系に対して、ある種の集合論（ZFCってことではない）の宇宙が健全な（ひょっとすると完全な）モデルになっている、ってことを言いたいのだと思います。（詳細は別途記述予定。） これらの宿題の完全解決とは言い難いですが、思うところを述べます
存在記号の除去規則について考える - 檜山正幸のキマイラ飼育記 (はてなBlog)
「全称記号の導入規則について考える」の続編として、存在記号の除去規則について考えます。 存在記号の除去規則の背景は比較的に簡単な事実です。にも関わらず、記号を換えたり書き方を縦にしたり横にしたりのどうでもいいワチャワチャが事情を見えにくくしています。この記事によって、ワチャワチャな作業（記法のあいだの翻訳）に慣れて、その“どうでもよさ”（記法が変わっても内実は変わらないこと）を感じていただければ幸いです。 内容： 存在記号の除去規則 限量随伴性 引き戻しと存在限量子の随伴性 随伴性を証明に利用する 随伴性からサイド証明へ メタ循環構造 存在記号の除去規則 標準的な自然演繹における「存在記号の除去規則」は次の形に書かれます。 P(a) : : ∃x.P Q -------------[∃除去] Q僕は、自然演繹に愚痴を言い、悪態をついてます（「自然演繹はちっとも自然じゃない -- 圏論による
奥野幹也『理論から学ぶデータベース実践入門』はどこがダメなのか - 檜山正幸のキマイラ飼育記 (はてなBlog)
言い訳から始めます。この記事を（途中まででも）読んだ人は、次のように言いたくなるでしょう。 『理論から学ぶデータベース実践入門』は良い本なのか悪い本なのか、いったいどっちなんだよ?! この本は間違いや説明不足があり、誤読されやすい表現も多く、その点では残念な本です。しかし、面白いアイディア、するどい観察も含まれていて、行間を補い深読みすれば、多くの示唆を得られる本でもあります。 よって、「良い／悪い」の二択では答えられません。良い点と悪い点の両方を、できるだけ客観的に記述するしかないのです。それをした結果、長い記事となりました。 内容： ことの発端： zhanponさんの批判 奥野本擁護と奥野本批判 僕の擁護・批判の方針 zhanponさんの指摘の再検討 1. 論理的な矛盾とデータの不整合を混同している 2. 命題論理の限界についての説明がおかしい 3. 古典論理の定義を間違えている 4.
食券販売機のユーザーインターフェースについて： ひとつのアンチパターン - 檜山正幸のキマイラ飼育記 (はてなBlog)
しばらく記事の更新が滞っておりました。そのあいだにあったことを書きます。松屋が期間限定で「ごろごろ煮込みチキンカレー」を発売しました。2017年6月6日からのことです。 【朗報】松屋史上屈指のウマさ「ごろごろ煮込みチキンカレー」が本日から大復活！ 凄まじく絶賛しているブログ記事があったりします。 松屋の「ごろごろ煮込みチキンカレー」は絶対に食べるべき“日本カレー”の到達点 この柔らかチキンとスパイス感が590円で提供される世の中に感謝しかない 6月21日（水曜）には終了のようだったので、6月19日（月曜）食べに行きました。このカレーについて言えば、確かに評判通り「凄い気合の入れよう」でした。（[追記 date="2017-07-07"]今日、松屋の前を通ったら、まだ「ごろごろ煮込みチキンカレー」やっているみたい。6月21日で終了はガセネタだったのか？[/追記]） でも話題はカレーじゃなくて
「確率変数」の正体は米田埋め込み - 檜山正幸のキマイラ飼育記 (はてなBlog)
確率変数（random variable, stochastic variable）という言葉の意味が分からない！ と何度か書いています。 2015-05-26 「確率変数」と言うのはやめよう 2015-05-27 「分布、測度、密度」は同じか違うか 2015-06-17 まだ「確率変数」が分からない 結局分からないままでした。「慣れ」の問題かも？ と思ったこともあります。 2015-05-28 「慣れれば分かる」問題 慣れることも出来ませんでした。 最近、「これなら納得できるかな」という解釈に出会いました。 [追記 date="翌日"]最後に分かりやすいマトメを付けました。[/追記] 内容： 「確率変数」はなぜ分からないのか アレックス・シンプソンのアイディア 「確率変数」の2つの用法 確率空間と圏Prob 測度論的確率変数 曖昧な確率変数 前層と米田埋め込み 米田埋め込みとしての確率変
「関数型プログラミングはオブジェクト指向の正当な後継」なの？ - 檜山正幸のキマイラ飼育記 (はてなBlog)
オブジェクト指向を知っている人々に、「関数型もオブジェクト指向と大差ないよ、大丈夫だよ」とお誘いする記事は大いに存在意義があると思います。 関数型プログラミングはオブジェクト指向の正当な後継である 上記の記事は、そういう目的を持って書かれたのでしょう。その内容（目次）は次のようです（僕のこの記事の目次じゃないよ）。 対象読者 なぜこの記事を書こうと思ったのか？ なぜ関数型プログラミングはわかりにくいのか？ オブジェクト指向の負の遺産を捨てよう 関数型プログラミングの概要 「阿吽の呼吸」とも言うべき使いやすさの拡張 型にまつわる考察 まとめ 最初のほうを読むと、言ってることはまっとうで好感を持てます。が、「5. 関数型プログラミングの概要」の節あたりから雲行きが怪しくなって、ちょっと何言ってるかわかんない（(c)サンドウィッチマン）。 檜山のこの記事の内容： 真面目なポエム モナドっておいし
コンピュータ科学や組み合わせ論を“微分幾何”とみなす：CADGの夢 - 檜山正幸のキマイラ飼育記 (はてなBlog)
『シン・ゴジラ』は僕のツボにはまったんですよね。コワ面白かった！ 最近、もうひとつ「これは面白い！」と思っていることがあります。微分幾何の応用の話です。多くの人が「応用」という言葉から連想する内容とはちょっと違います。微分幾何を換骨奪胎して、その枠組を、微分とも幾何ともまったく無関係と思える分野にも適用するのです。 「微分とも幾何ともまったく無関係と思える分野」には、コンピュータ科学や組み合わせ論が含まれます。これには驚きました。好奇心を刺激されて、しばらく猿になって調べまくってました。 調べても理解できないことがたくさんあるので、断片的で中途半端な知識を推測（妄想？）でつなぎ合わせるという手法（いつものやり口）で語ってみます。圏と多様体の定義くらいは仮定しますが、それ以外の知識は要求しないオハナシ調です。 内容： リソース計算が微分計算だってぇぇ?! 微分の計算が出来る圏 組み合せ論とデ
無料で入手できる本格的（紙なら高額）な理数系専門書15選 - 檜山正幸のキマイラ飼育記 (はてなBlog)
インターネットで資料探しをしていると、出版されている書籍と同じ内容のPDFがゴロンと置いてあってビックリすることがあります。以下に挙げるのは、そのような、“出版物と同等な内容”が無料公開されている理数系専門書のリストです。 紙の本とまったく同じものもありますし、ドラフト原稿が公開されているものもあります。紙の本の出版後もメンテナンスされていて、インターネット版のほうがより新しくより充実していることもあります。 例えば"Monoidal Functors, Species and Hopf Algebras"は、ハードカバー本は735ページで、現時点で24,650円もする大部な書籍です。公開されているPDFは書籍より増量して836ページあり、誰でも無料ダウンロード可能です。 著作権があやしいものは除外し、著者本人または著者の所属組織のWebサイト、あるいはarXiv.orgで公開されているも
関手データモデル／圏論データベース： その後の発展と現状 (2016) - 檜山正幸のキマイラ飼育記 (はてなBlog)
2013年の初頭に、デイヴィッド・スピヴァックの関手データモデル（functorial data model）について紹介しました。 デイヴィッド・スピヴァックはデータベース界の革命児か -- 関手的データモデル 衝撃的なデータベース理論・関手的データモデル 入門 あれから3年3ヶ月が経過して、今、関手データモデルや圏論データベース（categorical database）の状況はどうなっているでしょうか。 一言でいえば、 派手に喧伝はされてないが、着実に発展している となるでしょう。その進展の様子を次の3つの側面から概観してみます。 ビジネス ソフトウェア 理論 内容： ビジネス： Categorical Informatics, Inc ソフトウェア： FQL IDE 理論： 等式論理と代数データベース ※ リンクと注釈がたくさんあるのは、この記事が、この話題に関する説明付きブックマ
絵算ベースの証明支援系 Globular - 檜山正幸のキマイラ飼育記 (はてなBlog)
絵算ベースの証明支援系であるGlobularがWebサービスとして公開されています。 http://globular.science/ ブラウザー（Chrome推奨）上で動くJavaScriptプログラムが証明支援系の実体です。 証明支援系とは言っても、CoqやAgdaなどとはだいぶ趣が異なります。100%グラフィカルで、テキストによる表現や命令は一切使いません。パッと見ただけでは、何をするものか見当が付かないのではないでしょうか。 このソフトウェアを開発したのは、アブラムスキーとクック（この記事に二人の写真あり）が率いるオックスフォードのQuantum Groupで、開発の中心人物はジェイミー・ヴィカリー（Jamie Vicary）です。 Quantum Groupは、数年前から同種のソフトウェア（diagrammatic proof assistant）としてQuantomaticも提
もうGitは怖くない： 自信を持って使いたいあなたへ - 檜山正幸のキマイラ飼育記 (はてなBlog)
2014初頭に書いた「WindowsにおけるGit利用環境は整った： Git for Windows と SourceTree for Windows」の最後の文： ブランチは、Gitのなかで最も重要でありながら最も分かりにくい概念でしょう。表面的な言葉に騙されず、先入観を持たず、SourceTreeの視覚的表示（樹形図）の力を借りながら学習するのが、理解への一番の近道です。 そんへんの詳しいことはまたの機会に述べるかも知れません。 1年半以上たってしまいましたが、「またの機会」がやって来ましたよ。ええ、Gitの説明をします、ブランチを中心に詳しく。 「基礎編」と「ブランチ編」で2回に分けようかと思ったけど、長大な記事として一挙公開。これからGitを使う人が対象ではありません。Gitが何をやっているのか、自分が何をやっているのかイマイチ自信が持てない方向けです。 ブランチやマージって、なん
最近のビルドツールって何なの？ - 檜山正幸のキマイラ飼育記 (はてなBlog)
TypeScriptでは、コンパイルが必要です。プログラムをブラウザーとNode.jsの両方で使おうとすると、さらに加工が必要です。ミニファイだの文書も作るだのすると、ちょっとしたビルドプロセスとなるので手作業では辛くなります。 今更Makeでもないよなー、と思い、最近のビルドツールを試してみました。 内容： 流行りすたりが激しすぎる gulpを使ってみる：こんなサンプル gulpのビルドスクリプト タスクランナーってのはビルドツールとは違うのか？ ビルドツールは進化したのか 参考資料： 例題のファイルとコマンドの一覧 ソースファイル 追加の話： gulp問題ひきずり：ウォッチがまたおバカ過ぎる 流行りすたりが激しすぎる 「確かGruntってツールがあったよな」と、インストールと使い方を調べていると、やたらにgulpって単語が目立つんですよね。Gruntのライバルの新興勢力らしいです。 「
gulp問題ひきずり：ウォッチがまたおバカ過ぎる - 檜山正幸のキマイラ飼育記 (はてなBlog)
「最近のビルドツールって何なの？」において、gulpは「腕力はあるが知性を持たない」、ゴレライ的というかゴライアス的というか…、そんなツールだと述べました。二、三、後から思ったことがあるので追加します。 内容： プロジェクトは肥大しちゃうことがある ウォッチをいちいち手で書くのかよー OMakeと比較してみる ウォッチはこうでなきゃ じゃ、OMakeがいいのか？ プロジェクトは肥大しちゃうことがある 「そもそも大した事はしないのでシンプルなツールgulpでも十分」ということなら、「そうですよね」と同意して話はオシマイです。でもね、gulpを使うプロジェクトが、ほんとに小さくて簡単なものなんでしょうか。 目の前に、10種のプログラミング言語が混じった2000ファイルのソースコード群がいきなり与えられたとき、「よしっ、gulpを使おう」とはならないと思うのですが、小さなプロジェクトが（良くも悪
業務ソフトまたはゲームソフトとしてのCoq （誰も書かないCoq入門以前 2） - 檜山正幸のキマイラ飼育記 (はてなBlog)
うーむ、ムズカシイ。Coq、難しいなぁ。 Coqのプロモーションのために、「大丈夫、あなたも出来ます」みたいなこと言っちゃダメですよ。予備知識も心構えもなく安易に入門しても挫折するもの。「女子高校生でもやってます」って、ものすごく特殊な女子高校生でしょ。マララさんを例に出して「女子高校生でもノーベル賞とれます」って言っても、ノーベル賞とれないでしょ、ふつう。 まー、ノーベル賞に比べれば「大丈夫、あなたも出来る可能性が高いです」とは言えます。Coqがどんなものであり、どのへんに難所が潜んでいるかを知っておけば、Coqが出来るようになる可能性はより高まると思います（たぶん）。 僕自身、早々と挫折しかかっていたのですが、見方を変えると少しだけ見通しが立ちました。なので、これはCoqを触って困惑した人の助けにチョットはなるかも。 内容： Coqで使われる言語を分類しておく そもそもCoqはプログラ
誰も書かないCoq入門以前の話 - 檜山正幸のキマイラ飼育記 (はてなBlog)
「WindowsへのCoqのインストール」： 事情があって、AgdaかCoqを触ってみようか、と。 事情というのは、個々の命題の証明（確認）は割と簡単そうだが、命題がイッパイあるのでウンザリな状況のことです。家計簿の計算が筆算だと面倒だから電卓を使いたい、という状況と同様です。 それでCoqのインストールは済んだのですが、処理系の使い方が分からない。個々の操作は覚えていけばいいのでしょうが、そもそもCoq処理系が何をするものなのか？ が理解できないのです。Web上にCoqの解説は幾つもあるのですが、「いやいや、そうじゃなくて、それ以前のことがサッパリわからんのですけど」という感じ。スタートラインに立てない。 それで、「Coqの解説」じゃなくて「Coqの仕様」を読んだほうがいいのかも、と https://coq.inria.fr/distrib/current/refman/ （リファレンス
WindowsにおけるGit利用環境は整った： Git for Windows と SourceTree for Windows - 檜山正幸のキマイラ飼育記 (はてなBlog)
分散バージョン管理システムの利用は拡大しています。そのなかでも最も人気のあるツールはGitでしょう。しかし、GitをWindowsで使うのはなかなか困難でした。 Windows向けのGitであるmsysGitは、bashのコンソールを出して、最小限のUnix風コマンドライン環境を提供するものです。これは使いやすくありません。もう一つの選択肢であるTortoise Gitは、Windowsのエクスプローラー（ファイルマネージャ）に統合されたGUIツールですが、僕は「なんか違うな」と感じてました -- これは個人の感性の問題ですが、ファイルマネージャに横付けすることが、分散バージョン管理システムへの良いUIを提供するようには思えないのです。 ところが、最近は事情が大きく変わっています。使いやすいGUIツールとして、2013年6月に正式公開されたSourceTree for Windowsが存在
これは便利、tarを使ってファイルをコピーする - 檜山正幸のキマイラ飼育記 (はてなBlog)
バタリアンのタールマンが出てきてしまったわけですが*1、tarのmanページで何を調べていたかっていうと、ファイル抽出（extract）時に新ファイルを上書きしないオプションとか、なにやら。 ファイルのコピーというと、cp, copy, xcopyなどのコマンドを多く使うでしょうが、tarコマンドもファイルコピーに使えます。なかなか便利ですよ。Unix/Linux/Cygwin/MSYS などで GNU tar を使う場合の話です。 一番基本的なのは、カレントディレクトリにあるファイルをすべて再帰的にたどって宛先（destination）ディレクトリにコピーする方法です。 $ tar cf - . | (cd ../dest/; tar xvf -) ハイフン1文字「-」は標準入出力を表します。出力のときは「f - 」の代わりに -O（または --to-stdout）オプションが使えます。
関手的データモデルが変える世界 - 檜山正幸のキマイラ飼育記 (はてなBlog)
「キマイラ飼育記」は「関手的データモデル・ブログ」に変わりました -- みたいな状態。 どうして僕が関手的データモデルに興奮してイレ込んでいるのか？ まずは「面白いから」と答えるでしょうが、それだけではありません。長年に渡り、そして今でも僕を悩ませている問題に対して、関手的データモデルが解決、少なくとも解決のヒントを与えてくれるからです。 ソフトウェアシステムを変更すると、それまで使えていたデータが使えなくなる、あるいは、そのシステムに依存している他のプログラムが動かなくなることがあります。これは好ましくないので、ソフトウェアの世界では互換性が重視されます。 しかし、システムが発展していく途上では、互換性の維持が困難だったり、互換性を捨てる判断が妥当になることもあります。そんなときでも、「古いデータを守ってくれ」「今のプログラムをそのままで動くようにしてくれ」という圧力はかかります。設計者
衝撃的なデータベース理論・関手的データモデル 入門 - 檜山正幸のキマイラ飼育記 (はてなBlog)
デイヴィッド・スピヴァックによる衝撃的なデータベース理論である関手的データモデル。どうしたらうまく説明できるか？ と色々と悩んでしまいますが、まー、書けるところから書き始めてしまいましょう。 さー、いらっしゃい、いらっしゃい。関手的データモデルの世界へようこそ。圏論の言葉は出てきますが、圏論の予備知識はほぼゼロでOKですよ。 [追記 date="翌日"]取り急ぎ勢いで書きましたので、不注意と早とちりが混じっていました。追記と取り消し線の形で訂正と注記を足しました。字句レベルの表現の変更は直接編集しています。 あとそれと、圏論の基本用語を知りたいときはコチラ、… って、……、ゴメン！[/追記] 内容： はじめに 本の購入のサンプル スキーマのグラフ表現 キーとか計算カラムとか 圏としてのスキーマ 関手としてのデータベース状態 テーブルの変化 自然変換としてのデータ操作 データベースに圏論が使
関手的データモデルをどう説明するか？ 考えてます - 檜山正幸のキマイラ飼育記 (はてなBlog)
http://d.hatena.ne.jp/m-hiyama/20130128#c1359767497 : データベース技術者が「これを知らないのは不幸」と思えるので、（可能な範囲で）紹介はしようかな、と。 「これ」とはもちろんスピヴァックの関手的データモデルです。「データベース技術者」つうより、データベースに多少とも関わるすべての人にとって関手的データモデルは福音となる可能性があると思っています。RDBに限らず、現存するほとんどすべてのデータベース的システムに対して、極めて単純で統一的な記述を与えてくれます。データマイグレーションのように、これまでは途方に暮れていたような現実的な問題を鮮やかに解いてくれます。 「これ」を紹介する／説明する価値は十分にあります。僕自身が、すぐにでも実務的に使いたいと思っています。しかし、スピヴァックの論文群を要約したら関手的データモデルの説明になるかという
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
