2016年9月に次の記事を書きました。 関数型プログラミングとオブジェクト指向について、何か書く、かも タイトルからして引き続く記事を予告しているのですが、その予告を実行することができませんでした。タイトル中の「何か」とは「型クラス」のことです。上記の記事の最後の部分は： 関数型プログラミングにもオブジェクト指向にも関係があって、今後重要度を増すであろう「型クラス」ですが、今述べた（愚痴った）ような事情で（あと、C++のコンセプトは宙ぶらりんだし）、説明の方針も題材も定まりません。でも、いつか、何か書く、かも。 今回この記事で、予備知識をあまり仮定しないで型クラスの説明をします。言いたいことの1/3くらいは書きました。1/3でも長い記事なので、ぼちぼちと読んでもらえれば、と。書き残したことは最後に触れます。いつか、1年はたたないうちに(苦笑)、続きを書くつもりです。 内容： Haskell

確率変数（random variable, stochastic variable）という言葉の意味が分からない！ と何度か書いています。 2015-05-26 「確率変数」と言うのはやめよう 2015-05-27 「分布、測度、密度」は同じか違うか 2015-06-17 まだ「確率変数」が分からない 結局分からないままでした。「慣れ」の問題かも？ と思ったこともあります。 2015-05-28 「慣れれば分かる」問題 慣れることも出来ませんでした。 最近、「これなら納得できるかな」という解釈に出会いました。 [追記 date="翌日"]最後に分かりやすいマトメを付けました。[/追記] 内容： 「確率変数」はなぜ分からないのか アレックス・シンプソンのアイディア 「確率変数」の2つの用法 確率空間と圏Prob 測度論的確率変数 曖昧な確率変数 前層と米田埋め込み 米田埋め込みとしての確率変

昨日の記事「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」では、Isabelleのユーザーインターフェースが備えている特徴的な機能である「継続的チェッキング」だけを取り上げました。ここで改めて、証明支援系としてのIsabelleシステムを紹介しましょう。客観的な紹介ではなくて、僕の雑駁な印象記です。 内容： Isabelleの独自な世界 Isabelleの未来 Isabelleの独自な世界 「Isabelle/jEditの野心的な試み「継続的チェッキング」に「ウォ」っとなった」より： PIDE構想は、Isabelleプロジェクト／コミュニティを世の趨勢とは離れた孤立化へと導くのか、それとも、時代がPIDEの先進性にいずれ追いつき、PIDEがスタンダードな証明支援系UIとなるのか？ なかなかに興味深いですな。 Isabelleが世の趨勢と離れるのか？

2013年の初頭に、デイヴィッド・スピヴァックの関手データモデル（functorial data model）について紹介しました。 デイヴィッド・スピヴァックはデータベース界の革命児か -- 関手的データモデル 衝撃的なデータベース理論・関手的データモデル 入門 あれから3年3ヶ月が経過して、今、関手データモデルや圏論データベース（categorical database）の状況はどうなっているでしょうか。 一言でいえば、 派手に喧伝はされてないが、着実に発展している となるでしょう。その進展の様子を次の3つの側面から概観してみます。 ビジネス ソフトウェア 理論 内容： ビジネス： Categorical Informatics, Inc ソフトウェア： FQL IDE 理論： 等式論理と代数データベース ※ リンクと注釈がたくさんあるのは、この記事が、この話題に関する説明付きブックマ

「モノイド圏上の加群圏の実例」にて： 僕が加群圏にちょっと興味をいだいたのは、変則的なラムダ計算のモデルとして加群圏が使えないかな？ と思ったからです。思っただけで、よく分かってません。 これ、分かりました。 何が分かったのか？ を大雑把に記します。どうしてそうなるのか？ を説明する余裕が今日はないので、それは時間と気力があるときに書くつもりです。 内容： 積分の計算がモナドみたいだった理由 積分計算 コンパクト測度空間 割とうまく出来てる 積分の計算がモナドみたいだった理由 ことの発端は、次の記事に書いてあります。 ラムダ計算と積分計算 積分を入れたラムダ計算 状況編 ラムダ計算に積分を入れてみた、あるいは積分計算にラムダ抽象を入れてみたわけです。ちょっと計算してみると、状況がなんかモナドやモナド変換と似ているんですよ。モナドの香りがするぞ！ けど、モナドそのものではないのです。モナド／

2014初頭に書いた「WindowsにおけるGit利用環境は整った： Git for Windows と SourceTree for Windows」の最後の文： ブランチは、Gitのなかで最も重要でありながら最も分かりにくい概念でしょう。表面的な言葉に騙されず、先入観を持たず、SourceTreeの視覚的表示（樹形図）の力を借りながら学習するのが、理解への一番の近道です。 そんへんの詳しいことはまたの機会に述べるかも知れません。 1年半以上たってしまいましたが、「またの機会」がやって来ましたよ。ええ、Gitの説明をします、ブランチを中心に詳しく。 「基礎編」と「ブランチ編」で2回に分けようかと思ったけど、長大な記事として一挙公開。これからGitを使う人が対象ではありません。Gitが何をやっているのか、自分が何をやっているのかイマイチ自信が持てない方向けです。 ブランチやマージって、なん

TypeScriptでは、コンパイルが必要です。プログラムをブラウザーとNode.jsの両方で使おうとすると、さらに加工が必要です。ミニファイだの文書も作るだのすると、ちょっとしたビルドプロセスとなるので手作業では辛くなります。 今更Makeでもないよなー、と思い、最近のビルドツールを試してみました。 内容： 流行りすたりが激しすぎる gulpを使ってみる：こんなサンプル gulpのビルドスクリプト タスクランナーってのはビルドツールとは違うのか？ ビルドツールは進化したのか 参考資料： 例題のファイルとコマンドの一覧 ソースファイル 追加の話： gulp問題ひきずり：ウォッチがまたおバカ過ぎる 流行りすたりが激しすぎる 「確かGruntってツールがあったよな」と、インストールと使い方を調べていると、やたらにgulpって単語が目立つんですよね。Gruntのライバルの新興勢力らしいです。 「

他人の過去ネタを蒸し返し、自分用のメモにするエントリー。 [追記]トラックバック／コメント蘭で、色々なやりとりがありましたが、（この部分以外の）本文への修正や追加はしません。その代わり、「閉圏、弱いラムダ計算、弱い論理」で、似た話題を扱っています。[/追記] たけをさんが、だいぶ前の彼のエントリーで次のようなことを述べています； 圏Cがデカルト閉（cartesian closed）なとき、“Yを（デカルト積の意味で）掛ける作用 (-)×Y” と “Yで累乗（べき、指数）する作用 (-)Y” が互いに随伴なC上の自己関手になるわけですが、HomC(A×Y, B) と HomC(A, BY) の同型は集合圏での話であり、もとの圏Cの内部で同型が与えられるわけではない、と。 だがしかし、随伴による同型は、実はCの内部でもちゃんと定式化できるのです。Cのデカルト閉性（cartesian close

二値真偽値 {true, false} のブール代数は、論理ORを足し算、論理ANDを掛け算として半環となります。集合Aのベキ集合Pow(A)は、合併を足し算、共通部分を掛け算として半環です。アルファベットΣの言語の代数 Lang(Σ) = Pow(Σ*) も（たいていは非可換の）半環です。 これらの半環の足し算部分は可換モノイドであり、ベキ等でありω-総和可能です。論理、形式言語理論、プログラム意味論などに登場する半環／可換モノイドは、ベキ等性やω-総和可能性を持つ場合が多いのです。 モノイドや半環の理論は、できるだけ群や環の理論に似せて作りたい、という希望があります。しかし、ベキ等性やω-総和可能性を要求すると、群や環から離れてしまい、ある意味で対極的な構造になってしまいます。群や環の常識は通用しないことを覚悟しなくてはなりません。この記事では、その覚悟を促すいくつかの状況証拠を示しま

「久しぶりに圏論勉強会」で触れた次のこと： 非対称なモノイド圏という概念 モナドの定義をモノイドとして再確認 これを、お絵描き計算（pictorial calculation）を使ってチャント（になるかな？）説明してみようか、と思いました。こういうことは一気にババッと書き切らないと、ヘタって後が続かないことが多いのですが、残念、本日は厳密モノイド圏の実例で息切れ。でもまー、お絵描きの準備はできたから、いいとしよう。 内容： モナドはモノイドだ -- 言ってるだけ 循環的な状況が恐いけど魅力的 準備：ボックス図からストリング図へ 準備：徹底的に左から右の記法 自己関手の圏End(C) 余談：圏論は、ほぼ計算だけ 厳密モノイド圏 実例：行列の圏 実例：非負の実数 実例：釘にラベルが付いたブレイド図の圏 ほんとに面白いのは モナドはモノイドだ -- 言ってるだけ 実は、「モナドはモノイドだ」とい

渋谷に行くのは億劫になったので、圏のファイブレーションでも調べようか、と。スピヴァックがグロタンディーク、グロタンディークと言っているのも理由があることで、グロタンディーク構成／グロタンディーク・ファイブレーションはやっぱり使うのですよ。 ファイブレーション界隈も用語がけっこう乱れているので、調べて整理しようと、Wikipedia項目 http://en.wikipedia.org/wiki/Fibred_category とnLabの http://ncatlab.org/nlab/show/Grothendieck+fibration を見比べたりました。 まず、英語の綴りがfibreとfiberがあるんですよね。とりあずfibre使うことにします。それで、fibre category と fibred category は全然意味が違います。なので、日本語で「ファイバー圏」は紛らわし

先日「代数と余代数、クラスと余クラス」というエントリーを書きました。これは、あまり正確さは気にしない「おはなし」です。「おはなし」であっても、雰囲気や感じをつかむにはそれなりの意味があると思っています。もう少し補足をする気はあるのですが、正確で体系的な記述は、能力・気力・体力の点で僕の手には余ります。代数と余代数に関する（余代数が中心の）良い教科書や資料はたくさんありますので、おすすめできる解説を挙げておきます。 Title: Exercises in Coalgebraic Specification Author: Bart Jacobs URL: http://www.cs.ru.nl/~bart/PAPERS/mathfit00.pdf 43ページ、Exercises と略称 Title: Universal coalgebra: a theory of systems Autho

デイヴィッド・スピヴァックによる衝撃的なデータベース理論である関手的データモデル。どうしたらうまく説明できるか？ と色々と悩んでしまいますが、まー、書けるところから書き始めてしまいましょう。 さー、いらっしゃい、いらっしゃい。関手的データモデルの世界へようこそ。圏論の言葉は出てきますが、圏論の予備知識はほぼゼロでOKですよ。 [追記 date="翌日"]取り急ぎ勢いで書きましたので、不注意と早とちりが混じっていました。追記と取り消し線の形で訂正と注記を足しました。字句レベルの表現の変更は直接編集しています。 あとそれと、圏論の基本用語を知りたいときはコチラ、… って、……、ゴメン！[/追記] 内容： はじめに 本の購入のサンプル スキーマのグラフ表現 キーとか計算カラムとか 圏としてのスキーマ 関手としてのデータベース状態 テーブルの変化 自然変換としてのデータ操作 データベースに圏論が使

最近、「おおおー、これは凄い、すんばらしい！」と思ったことがあるので、それについて書きます。 最初に言葉についてのお断り； "categorical"の訳語をどうしようか？ と。片仮名で「カテゴリカル」が無難ですが、漢字で書きたい。「圏論的」が落ち着きがいいようですが、必ずしも「論」の意味を含まないときもあります。そこで、以下、「圏的」を使います。 [追記 date="2013-02-12"]入門的解説を書きました。→「衝撃的なデータベース理論・関手的データモデル 入門」[/追記] スピヴァックと関手的データモデル デイヴィッド・スピヴァック（David I. Spivak, http://math.mit.edu/~dspivak/）は、MITの研究者です。 彼は圏的情報学（categorical informatics）を提唱しています*1。圏的情報学の中心的な概念が関手的データモデル