自分が過去に言ったことを引き合いに出して、「あー、やっぱりね、だから言ったでしょ」みたいな物言いはお下品だから、下劣な奴と思われるでしょう。でも、言いたい衝動に勝てない。 あー、やっぱりね

「Parse.comとMailGunを普通のWebサイトのバックエンドとして使ってみる」で紹介したParse.comが、サービスを停止するようです。次のようなメールが来てました。 We have a difficult announcement to make. Beginning today we're winding down the Parse s…

先週の記事でGlobularを紹介しました。日本語を食わせるとお腹を壊して死んだりします。でも、けっこう使えるし十分に面白い。僕がなぜ絵算やGlobularに興味を持つのか、と言うと； これが計算や証明、そしてコミュニケーションに革命を起こすものだと感じる…

Globularのサンプルを追加しました。 http://globular.science/1601.006 このワークスペースの内容：次の素材があって、 圏 C 圏 D 関手 F:C→D 関手 G:D→C 自然変換 η::IdC⇒F*G:C→C 自然変換 ε::G*F⇒IdD:D→D ニョロニョロ関係式（snake relations）を満たす…

Globularはとっつきにくいソフトウェアなので、使い方を伝えるには、最初から順番に説明する必要があるでしょう。しかし、タクサンの画面キャプチャを撮ってマウス操作の説明を付けていく気力は湧きません（大変過ぎる！）。とりあえず、Globularのデモンス…

[追記]事情が分かりました。最後に書き足してます。[/追記]一昨日紹介したGlobularの使い方を説明するために、簡単な例題とかを作ってます。Globularにはソースコードとかデータという概念がなく、ソフトウェアの状態（ワークスペース）のセーブとリストアが…

絵算ベースの証明支援系であるGlobularがWebサービスとして公開されています。 http://globular.science/ ブラウザー（Chrome推奨）上で動くJavaScriptプログラムが証明支援系の実体です。証明支援系とは言っても、CoqやAgdaなどとはだいぶ趣が異なります。1…

はいだしょうこおねえさんのアノ絵が今でもYouTubeで見られるのね。あの時、スタッフはどういう気分でこの映像を撮ったのだろう。「これはこれで面白いんじゃないか」という判断だったのだろうか、それとも、ヤケクソで制作したのだろうか。いずれにしても、…

ジョン・バエズ（John C. Baez）がどこかで、「豊饒圏はピノキオのようなものだ」と言ってました。ピノキオは人間ではないがまるで人間のように振る舞う -- 豊饒圏は圏ではないがまるで圏のように振る舞う。ピノキオは物語の最後にほんとうの人間になれる --…

「随伴のニョロニョロ関係をTypeScriptで確認する」で話題にした2つのニョロニョロ関係式： εP(X) P(ηX) = idP(X) E(εX) ηE(X) = idE(X) 一番目だけをTypeScriptで書いてみました。TypeScriptプログラムで出来ることは、幾つかの個別事例を確認することだけ…

遅ればせながら、明けましておめでとうございます。年は変われど、僕の興味はあいも変わらず。Cがデカルト閉圏のとき、直積による掛け算関手と関数空間を作る指数関手*1は随伴ペアとなります。この事実が型付きラムダ計算のモデル作成のベースとなります。つ…