http://return0.info/note/2011-01-30.e : ライブラリを分離してリリースとなると、やっぱ一番ホットに感じてるところから離れた気がするのがなあ。 この気分は僕も同じ。説明しやすくて皆んなに役に立ちそうな部分ってのがあって、それの意義は認識している…

圏の指数の書き方は、含意記号「⊃」を使うことにします。デカルト閉圏は、型付きラムダ計算や連言含意論理のモデルなので、いくらでも例を作れます。非自明で最も簡単な例は、二値の真偽値を圏とみなしたモノでしょう。この例はやたらに簡単なので、手作業で…

僕の場合、育児をがんばったというよりは幼い子供達に依存した生活をしていた、と言うべきでしょう。だから、子供達がおおきくなるのが寂しい、なんか喪失感があります。 休日 声変わりも近いかもな そんな状況なので、ひげぽんさんのこの記事とか読むと、妬…

ソフトウェアの形式手法では、なにかしら論理の力の借ります。論理には、ウンザリするほどの種類がありますが、コンピューティングに利用するなら、ホーア論理が一番基本的で一番役に立つものだと思います。ホーア論理の圏論的な定式化というと、アブラムス…

サッカーの録画を見ながら：次男：「左サイドあいてるー」父親：「…」次男：「うーん、もっとプレッシャーかけないと」父親：「…」次男：「そうそう、コンパクトに」父親：「…」次男：「おっとフェイント、ロコモティブだ」父親：「君さ、随分と難しいこと知…

圏Cがデカルト圏だとして、Cの対象Aを掛け算する関手 (-×A) に随伴の相方Gがあれば、C(X×A, Y) = C(X, G(Y)) （イコールは集合の同型）が成立します。この G(Y) を、普通は YA と書いて「指数」とか「ベキ」と呼びます。YA という書き方は、普通の指数との類…

データの（あるいはデータ型の）大事な性質に次のものがあります。 変更可能性（ミュータビリティ） 複製可能性（コピーアビリティ） 破棄可能性（ディスカーダビリティ） 状態を表すデータは変更可能でないと使い物になりませんが、一方で、変更してはいけ…

シーケント計算は論理の計算手法ですが、圏論との関係が深いことがわかっています。であるなら、圏論から出発してシーケント計算を構成してはどうでしょうか。やってみます。内容： 記号の使い方 背景となる圏の種類 単なる圏のシーケント計算 モノイド圏の…

コンピュータに何かをさせるとき、現実の世界や概念の世界をコンピュータのなかに写像しようとします。そうすると、当のコンピュータ自身もコンピュータの世界のなかに写像されることがあります。ハードウェアエミュレータなんて典型的で、「ハードウェア → …

少し前まで、行きつけのセブンイレブンでは三色ボールペンを売っていました。が、最近3色ペンがないのですよ。なぜか代わりに4色ペンです。黒、赤、青に緑が追加されています。今まで緑なんて使ったことなかったので、なんか無駄なモノ買わされている気分。…

「論理的であるかのごとくに装って、根拠のないイチャモンをつける 13+2 の方法」は、当初の企画としては、割と真面目に論理（ロジック）の話をするつもりだったのですが、面倒になって論理的背景はほとんど入れませんでした。最後に次のような言い訳を書い…

長男とガラポンの抽選会に行く途中、またもワケわからん会話：長男：「今日は当てるぞー」父親：「おー、当ててくれ」長男：「俺ね、くじ運が悪いんだよね」父親：「あんなもんはそうそう当たらないからな」長男：「だけど今日は当てるぞー、五等のポケット…

デカルト閉圏は計算（computations）のモデルとして大変に使いやすいものです。しかし、どうもデカルト閉圏が矮小化されて理解され、応用範囲を狭めているような印象も持ちます。デカルト閉圏が型付きラムダ計算のモデルであるのは事実ですが、このことが強…

「サブオブジェクト・クラシファイアーの素朴な説明」とかで、「モノ射の引き戻しはモノ射である」ことを使ってるんですが、念のため確認しようとしたら手間取った。で、その経過を貼っておきます。とりあえず絵だけ。後で説明を足します、たぶん。（[追記 d…

計算（computations）が圏Cでモデル化できるとします。圏Cの対象は型で、圏Cの射は強く型付けされた関数（計算処理）だとしましょう。このモデルのなかで関手 F:C→C を関数（＝Cの射）で表現できるでしょうか？ できないですよ。だって、関手はCの外にあるも…

今日外を歩いていたら、たまたま長男を見かけたので声をかけた。何年か前までは、外で会うと「おとーさーーん」と大声を上げて走ってきた。ところが最近は、緊張したような気まずいような回りをうかがうようなギゴチナイ感じで、「あ、おっ、おとうさん」と…

デカルト閉圏（Cartesian Closed Category; 略称CCC)は、型付きラムダ計算のモデルです。でも、僕らが普通にデカルト閉圏で計算するとき、ほんとうに型付きラムダ計算を使っているかと言うと、そうでもなくて、多変数の関数とかも使います。タプルの一変数じ…

デカルト作用圏やフレイド圏は随分と役に立つなー、と実感。リアルな（現実をうまく写す）計算モデルを簡単に作れるようになりました。 デカルト作用圏によるプログラムの意味論 （たぶん、その1） デカルト作用圏が面白い デカルト半環圏の定義を確認してみ…

「ハイパースキーマまでの道」に書いた予定に従って、JSON向けのシンプルセレクターの次はパートという概念を定義します。内容： プロパティ／項目からパートへ パートの例 パートのドメイン型とコドメイン型 パートの利用例 BNFによるパート定義の構文 パー…

次男：「ウーン、思い出せない」父親：「なんか忘れたの？」次男：「うん、忘れて思い出そうとしているんだけど」父親：「なにを？」次男：「何を思い出そうとしていたんだか忘れちゃったんだよ」父親：「えっ」次男：「何かを忘れて、それを思い出そうとし…

まっとうなハイパースキーマがないことはシリアスな問題なんだよなー。わしゃ困るわ、フントに。ハイパースキーマに向けて； まずはセレクター。JSONデータが与えられたとき、その部分構造の集合を取り出す（セレクトする）式があると便利です（つうか、必要…

次男が、（去年だけど）遊戯王カードゲームの大会に参加したとか。予選は10人中1位だったらしいが、本戦ではあえなく1回戦敗退。話を聞いてみたら：父親：「最初の相手が優勝者だったんだって」次男：「そう、運が悪かったー」父親：「そうだなー。で、その…

http://twitter.com/#!/oto_oto_oto/status/21809570707931136 ： subobject classifier で定式化される部分対象とMonoだったかSubで定式化される部分対象は同じものなんだろうか。 http://d.hatena.ne.jp/m-hiyama/20101230/1293682058 ： クリスマスにトポ…

2010年12月30日に（http://twitter.com/#!/m_hiyama/status/20322641730600960）： とりあえず今年の目標： 今年中に、作用圏とフレイド圏を使えるようになる。 と書いたが、それは達成できず。正月にやろう、っと。しかし、「クリスマスは終わってしまった…

正月などは別にドーデモイイと思いつつも、明けましておめでとうございます。「ハイパースキーマについて再び考えよう、っと」という次第で、年末年始も、ナントハナシにJSONハイパースキーマについて考えていました。ハイパースキーマが必要なのは、Webサー…