微分計算、ラムダ計算、型推論 - 檜山正幸のキマイラ飼育記 (はてなBlog)
微分の計算は色々な場面で必要です。が、微分の記号である や が入った式の解釈って難しいですね。式の型〈type〉が分かりにくいのです。実際、原理的に型が判断できない式が使われることがあります。にもかかわらず、「分かる人には分かる」のは、暗黙のお約束や習慣的手順が駆使されるからです。 僕は、暗黙のお約束や習慣的手順が嫌いなので、ハッキリした計算方法を示したいと思います。現状の記法の問題点と対処法を知りたい方は、前半をテキトーに読み飛ばして、後半の3つの節を読めばいいと思います。 事前にラムダ計算について少し知っているほうがいいでしょう。JavaScriptや絵を使って説明した記事は： JavaScriptで学ぶ・プログラマのためのラムダ計算 JavaScriptで学ぶ・プログラマのためのラムダ計算 問題集 絵を描いて学ぶ・プログラマのためのラムダ計算 ラムダ計算をJavaScript側に寄せ
ラムダ記法とイプシロン記法を組み合わせて関数を定義する - 檜山正幸のキマイラ飼育記 (はてなBlog)
イプシロン記号／イプシロン記法／イプシロン計算については何度か述べたことがあります。今回は、イプシロンを実用的に使うための補助構文について述べます。ここで述べるアイディアは、証明検証系Mizarから拝借しています。ただし、Mizarそのものには触れませんし、Mizarの知識も不要です。 内容： 関数の書き方 イプシロン記法 イプシロン項の基本性質 イプシロン項の不定性 イプシロン項による関数定義 関数の余域を制限する 関数の書き方 中学校で習う1次関数は、 y = 2x + 1 のような形で書かれます。このため、「関数とは、等式の書き方の一種だ」と思っている人もいます。 「y = 」の部分は、関数の定義としてはどうでもいい部分です。関数としてエッセンシャルな部分だけを書くにはラムダ記法が便利です。 λx.(2x + 1) しかし、ラムダ記法にも制限があります。既にある定数、関数、演算子など
ド・ラーム・コホモロジーとホッジ分解のオモチャ (2/2) - 檜山正幸のキマイラ飼育記 (はてなBlog)
「ド・ラーム・コホモロジーとホッジ分解のオモチャ (1/2)」の続き・後編です。今回の第2節から第6節（全8節）で、オモチャ＝有限離散モデルを作ります。この部分は、純粋に線形代数の話です。ここだけを取り出して（文脈を無視して）、線形代数の練習問題として読むこともできます。第7節で、前回の話との関係を述べます。「背景を知らずに代数的議論だけを追うのはイヤだ」という方は、第7節を先に読んでください。 内容： この記事の記述方法について 内積ベクトル空間と随伴線形写像 部分空間の直交性と直交補空間 ホッジの分解定理（ラプラシアンなしバージョン） ラプラシアンとホッジ分解 ド・ラーム・コホモロジー空間 多様体から線形代数へ おわりに 前回・前編の内容： 予備知識は線形代数だけ 背景のオハナシ（超・急ぎ足） 複体 複体上のパスとチェーン 実数係数チェーン空間 境界作用素 1 境界作用素 2 組み合わ
絵算からテキスト、そして可換図式化もやってみた（当然疲れた） - 檜山正幸のキマイラ飼育記 (はてなBlog)
「絵算のテキスト化を完全にやってみた（超・疲れた）」において、絵算の計算過程を、行列レイアウトの等式的推論としてテキストに写し取ってみました。これは、値を変えずに項を変形していく過程で、通常の等式変形（等式論理系における証明）そのものです。 ところで圏論では、可換図式が多用されます。可換図式が、圏論で一番ポピュラーな記述・計算デバイスなのです。この記事では、絵算やそのテキスト表現を可換図式にしてみます。また、この機会に可換図式に関する説明もします。 内容： 結合律の可換図式 この可換図式はどうやって作ったか 可換図式とは何なのか 可換図式と他の表現方法 おわりに 結合律の可換図式 以下の記事達で、強モナドから作られたモノイドの結合律を題材にしました。 新しい絵算手法：ストリング＋ストライプ図 絵算のテキスト表現（結論：疲れる） 絵算のテキスト化を完全にやってみた（超・疲れた） もとの定理（
絵算のテキスト表現（結論：疲れる） - 檜山正幸のキマイラ飼育記 (はてなBlog)
昨日、新しい絵算手法について述べたのですが、絵算の困るところは、適切な描画ツールがない、絵をテキストにシリアライズ／エンコードする方法とデータ交換形式〈data interchange format〉がないことです。“絵”と“絵の変形過程”をテキスト表現できれば、コミュニケーションのコストが劇的に下がります。 そうはいっても、テキスト・エンコード形式を提案したところで普及するような状況ではないので、既存の数式組版（＝TeX）でテキスト表現できないか試してみます。 内容： ほんとに困っている 例題：モナドから作るモノイド 図式順・反図式順混合記法と行列記法 計算してみる（が、疲れた） ほんとに困っている 絵算の絵を描く適当なツールはないと思います。Globularは、お絵描きに使えるほどの描画能力は持ってない*1し、ストライプ図をまったくサポートしていません。次のような絵（マースデンとマッカ
絵算ベースの証明支援系 Globular - 檜山正幸のキマイラ飼育記 (はてなBlog)
絵算ベースの証明支援系であるGlobularがWebサービスとして公開されています。 http://globular.science/ ブラウザー（Chrome推奨）上で動くJavaScriptプログラムが証明支援系の実体です。 証明支援系とは言っても、CoqやAgdaなどとはだいぶ趣が異なります。100%グラフィカルで、テキストによる表現や命令は一切使いません。パッと見ただけでは、何をするものか見当が付かないのではないでしょうか。 このソフトウェアを開発したのは、アブラムスキーとクック（この記事に二人の写真あり）が率いるオックスフォードのQuantum Groupで、開発の中心人物はジェイミー・ヴィカリー（Jamie Vicary）です。 Quantum Groupは、数年前から同種のソフトウェア（diagrammatic proof assistant）としてQuantomaticも提
データベースへの論理的アプローチ： NULLについてチャンと考えよう - 檜山正幸のキマイラ飼育記 (はてなBlog)
「奥野幹也『理論から学ぶデータベース実践入門』はどこがダメなのか」のなかで、ピンクで「（詳細は別途記述予定。）」と書いてあるところが6箇所あります。これらの“ピンクの宿題”を順不同で片付けていきます（全部、片付くかは不明）。 ピンクの宿題 その1 単なるベキ集合でも（ある意味）重ね合わせです。[...今回の話題に関係ないので省略...]この枠組内でNULLの意味も（ヨタ話じゃなくて）分析できます。（詳細は別途記述予定。） NULLに関する基本的な事項についてゼロから考察してみます*1。予備知識として、ラーメン屋さんに行った経験を仮定しますが、その経験がなくても読めるように心がけました。この記事を読めば、NULLの使用法とダメさ加減がハッキリと分かるでしょう。 内容： NULLはダメなの？ なんで？？ 型と型構成子 ベキ集合の型 ラーメン屋さんの食券販売機 繰り返し型と不明型 繰り返し型を禁
困った時の米田頼み、ご利益ツールズ - 檜山正幸のキマイラ飼育記 (はてなBlog)
米田埋め込みはやっぱり役に立ちますね。米田埋め込みを利用するときに便利なツールを幾つか紹介します。それらのツール達は： 関手に使うラムダ記法 米田の星 (-)米, (-)米 関手・自然変換のテンソル積 マルチ米田埋め込みのドット記法 内容： 過去の事例： CPSと確率変数 困った時の米田頼み、もうひとつの例 米田埋め込み ラムダ記法と米田の星 超巨大圏CATと直積 関手・自然変換のテンソル積 マルチ米田埋め込みとテンソル積 前層の圏とマルチ米田埋め込み おわりに 過去の事例： CPSと確率変数 プログラミングにおいて、継続（continuation）という不思議な概念が登場します。継続を用いたプログラミング技法として、継続渡し方式（CPS; Continuation Passing Style）という何だかヨクワカラナイやり方があります。 継続／継続渡し方式に関わる不可解さは、米田埋め込み
無料で入手できる本格的（紙なら高額）な理数系専門書15選 第2回（2017年春） - 檜山正幸のキマイラ飼育記 (はてなBlog)
去年・2016年の夏に、「無料で入手できる本格的（紙なら高額）な理数系専門書15選」という記事でインターネットから入手可能な専門書を15冊紹介しました。 出版されている書籍と同じ内容のPDFファイルやHTMLページがインターネットに公開されている例は意外と多いみたいで、一年たたずに新しい15冊のリストができました。前回（2016年夏）と同様に、著作権があやしいものは除外し、著者本人または著者の所属組織のWebサイト、あるいはarXiv.org, TAC (Theory and Applications of Categories)で公開されているものだけを紹介します。また、この記事の後半で、今回紹介する15冊と過去に紹介した20冊のタイトルとURLを再掲します。 内容： 幾何 Differential Algebraic Topology: From Stratifolds to Exot
上空にいる足し算の親玉を捕まえる - 檜山正幸のキマイラ飼育記 (はてなBlog)
足し算を持つような圏Cに対して、その圏Cの自己関手圏End(C)内に棲んでいる代数系が、Cの足し算構造を牛耳っている様子を観察します。実は蒸し返しだけど。 内容： 足し算を持つ圏 自己関手圏内の代数系 自己関手圏のモノイド構造 足し算の親玉 何が面白いの？ 足し算を持つ圏 足し算を持つ圏というと、半加法圏（semiadditive category）と加法圏（additive category）があります。その定義は、nLabやWikipediaを参照してください。 https://ncatlab.org/nlab/show/biproduct#SemiadditiveCategories https://ncatlab.org/nlab/show/additive+category https://en.wikipedia.org/wiki/Additive_category 半加法圏も
英語版無料PDFか、それとも日本語版商業出版物か：圏論と測度論 - 檜山正幸のキマイラ飼育記 (はてなBlog)
トム・レンスターの『ベーシック圏論』 「2017年 圏論に関する参考文献の案内（無料オンライン版含む）」で、書籍"Basic Category Theory"が無料PDFとして公開されたことを紹介しました。 ※ 書籍の表紙画像が表示されないときは、このページをリロードしてみてください。 Basic Category Theory (Cambridge Studies in Advanced Mathematics) 作者: Tom Leinster出版社/メーカー: Cambridge University Press発売日: 2014/07/24メディア: ハードカバーこの商品を含むブログを見る Title: Basic Category Theory Author: Tom Leinster AuthorHomePage: http://www.maths.ed.ac.uk/~tl/
オーバーロードは何故にかくも難しいのか：Haskellの成功と失敗 - 檜山正幸のキマイラ飼育記 (はてなBlog)
名前や記号の多義的使用をオーバーロードと呼びます。オーバーロードとは「曖昧な表現を使う」ことだ、と言ってもいいでしょう。曖昧さを嫌うコンピュータに、曖昧な表現を理解させるのは難しいことです。コンピュータに関する技術や理論以前に、「我々人間は、曖昧な表現をどう使い／どう解決しているのか？」と問う必要があります。 内容： Haskellの場合 -- The・構造の仮定 要素とコレクションの事例 型クラスの境界線は引けるのか 名前・記号の問題は難しい Haskellの場合 -- The・構造の仮定 「入門的ではない型クラスの話：Haskellの型クラスがぁ (´^｀;)」において： 後知恵で言えば、[注：Haskellのオーバーロード・メカニズムは]「悪いお薬」だったと思います。服用するとモノ凄く元気になるが、長期的には心身を蝕んでしまうお薬だったと。 Haskellが実装した記号の乱用はやはり
「関数型プログラミングはオブジェクト指向の正当な後継」なの？ - 檜山正幸のキマイラ飼育記 (はてなBlog)
オブジェクト指向を知っている人々に、「関数型もオブジェクト指向と大差ないよ、大丈夫だよ」とお誘いする記事は大いに存在意義があると思います。 関数型プログラミングはオブジェクト指向の正当な後継である 上記の記事は、そういう目的を持って書かれたのでしょう。その内容（目次）は次のようです（僕のこの記事の目次じゃないよ）。 対象読者 なぜこの記事を書こうと思ったのか？ なぜ関数型プログラミングはわかりにくいのか？ オブジェクト指向の負の遺産を捨てよう 関数型プログラミングの概要 「阿吽の呼吸」とも言うべき使いやすさの拡張 型にまつわる考察 まとめ 最初のほうを読むと、言ってることはまっとうで好感を持てます。が、「5. 関数型プログラミングの概要」の節あたりから雲行きが怪しくなって、ちょっと何言ってるかわかんない（(c)サンドウィッチマン）。 檜山のこの記事の内容： 真面目なポエム モナドっておいし
テンソル積の作り方 - 檜山正幸のキマイラ飼育記 (はてなBlog)
モノイド圏のモノイド積を“テンソル積”と呼ぶことがあります。この意味のテンソル積は最初から「在る」もので、「作る」ものではありません。では、最初はテンソル積がないのだけど、頑張って「作る」とき、どんな作り方をするのでしょうか？ 単に「作る」と言っても曖昧なので、ベクトル空間のテンソル積を事例に、その「作り方」を反省的に眺めてみようと思います。 内容： ベクトル空間のテンソル積の要件 テンソル積の構成には2つの圏が必要 「双」はやめる LとM2の定義 圏M2[A, B]と、AとBのテンソル積 射のテンソル積 インデックス付き圏のセクションとしてのテンソル積 モノイド圏の構成 ベクトル空間のテンソル積の要件 ベクトル空間と線形写像の圏をVectとします。スカラー体（係数体）は何でもいいので、特に明示しません。今、A, B∈|Vect| に対してABを定義したいわけです。ベクトル空間のテンソル積
無料で入手できる本格的（紙なら高額）な微分幾何の専門書4選 - 檜山正幸のキマイラ飼育記 (はてなBlog)
「コンピュータ科学や組み合わせ論を“微分幾何”とみなす：CADGの夢」に関連して微分幾何について調べていたとき、商業出版物（紙の書籍）と同等なPDFをみつけました。「無料で入手できる本格的（紙なら高額）な理数系専門書15選」への追加として、4点の書籍を紹介します。 内容： Functional Differential Geometry The Convenient Setting of Global Analysis Synthetic Differential Geometry Synthetic Geometry of Manifolds Functional Differential Geometry Functional Differential Geometry (The MIT Press) 作者: Gerald Jay Sussman,Jack Wisdom,Will Fa
コンピュータ科学や組み合わせ論を“微分幾何”とみなす：CADGの夢 - 檜山正幸のキマイラ飼育記 (はてなBlog)
『シン・ゴジラ』は僕のツボにはまったんですよね。コワ面白かった！ 最近、もうひとつ「これは面白い！」と思っていることがあります。微分幾何の応用の話です。多くの人が「応用」という言葉から連想する内容とはちょっと違います。微分幾何を換骨奪胎して、その枠組を、微分とも幾何ともまったく無関係と思える分野にも適用するのです。 「微分とも幾何ともまったく無関係と思える分野」には、コンピュータ科学や組み合わせ論が含まれます。これには驚きました。好奇心を刺激されて、しばらく猿になって調べまくってました。 調べても理解できないことがたくさんあるので、断片的で中途半端な知識を推測（妄想？）でつなぎ合わせるという手法（いつものやり口）で語ってみます。圏と多様体の定義くらいは仮定しますが、それ以外の知識は要求しないオハナシ調です。 内容： リソース計算が微分計算だってぇぇ?! 微分の計算が出来る圏 組み合せ論とデ
自然演繹はちっとも自然じゃない -- 圏論による再考 - 檜山正幸のキマイラ飼育記 (はてなBlog)
自然演繹は、その名の通りに「自然で分かりやすい」と言われたりします。僕は、そうは思いません。むしろ「不自然で分かりにくい」と感じます。導入規則と除去規則のあいだに綺麗な対称性がある、と言う人がいます。僕にはどこが綺麗か分かりません。無理クリに対称に見せてるだけで、むしろ歪んでいて汚ないじゃないか、と思います。 自然かどうか、綺麗かどうかは主観の問題ですから、議論しても不毛です。しかし、代替の定式化を示して、それを自然演繹と比較することにより、自然演繹を相対化することは出来ます。やってみます。 この記事の内容は、ここ10年くらい思っていたことです。口頭でしゃべったことはありますが（最後の節を参照）、まとまった記述はなかったので、割と丁寧に書きました。その結果、けっこう長大な記事となりました。 論理や圏論を学ぶには、まっとうな教科書を手元に置くのがよいでしょう。その教科書が主治医とするなら、僕
無料で入手できる本格的（紙なら高額）な理数系専門書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 理論： 等式論理と代数データベース ※ リンクと注釈がたくさんあるのは、この記事が、この話題に関する説明付きブックマ
読み方が分からない - 檜山正幸のキマイラ飼育記 (はてなBlog)
ウチの近所に八幡通りという通りがあります。おそらく、金王八幡宮へと向かう通りだからそう名付けられたのでしょう。 現在、東急東横線・中目黒駅から地下鉄副都心線を介して新宿三丁目まで乗り換え無しで行けます。新宿三丁目で都営新宿線に乗り換えて千葉県の本八幡駅まで行けるし、一方、新宿三丁目から京王線直通で八幡山駅まで行くことも出来ます。 上の文章内に「八幡」が何度も出てきますが、その読み方は： 八幡通り → はちまんどおり 金王八幡宮 → こんのうはちまんぐう 本八幡駅 → もとやわたえき 八幡山駅 → はちまんやまえき 社会科で八幡製鐵所ってのを習った覚えがありますが、これは： 八幡製鐵所 → やはたせいてつしょ 「はちまん」、「やわた」、「やはた」。フリガナが見当たらなくて、読み方を調べるのが手間だったりします。気になって調べたけど、それまでは漢字の形状は分かっていても発音できなかったですよ＞
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
