演繹系とお絵描き圏論 - 檜山正幸のキマイラ飼育記 (はてなBlog)
次の2つの事情からこのエントリーを書きます。 oskimuraさんのコメントに対して、あまりにそっけない対応でちと申し訳ない。 「ラムダ計算、論理、圏」セミナーで、圏の話はほとんど出なかったんじゃないの？ というご指摘に少しだけ応えたい。 「ラムダ計算、論理、圏」セミナーの楽屋裏を紹介するような意図もあります。論理と圏論の知識が若干必要なので、この記事は自己完結的とは言えません。が、流し読みしても大意は伝わると思います。「命題論理とデカルト閉圏」のセクションにある対応表がメダマのつもり。 内容 十人十色な演繹系 自然演繹とシーケント計算 論理の圏論的意味論 演繹系の健全性 命題論理とデカルト閉圏 構造規則とお絵描き 十人十色な演繹系 図書館に行って論理学の教科書を端から眺めてみると、採用している論理記号、公理系、推論規則などが著者ごとにバラバラなのがわかると思います。有名どころの演繹系（演
お尻・ハナクソ問題：統計的に有意になる程度の母集団が欲しい - 檜山正幸のキマイラ飼育記 (はてなBlog)
いいかげん昔のことだが、若い女性を含むある集団（20人くらい）に対して、トイレで紙を使うとき、右手を使うか左手を使うかをアンケートしたことがある。当然にひんしゅくを買うだろうと思っていたのだが、驚くほど真面目に答えてくれたのが印象に残っている。右利き左利きとの相関関係が知りたい、と前置きしたので、僕がアカデミックで崇高な目的を持っていると納得してくれたのだろう（ホントかよ）。 結果の数値は忘れてしまったが、右利きなのに左手でお尻を拭く僕が少数派だったことは憶えている。 なんで、こんなことを思い出したかというと、長男が「ハナクソをほじるとき、おとうさんは右手を使うか、左手を使うか」というバカな質問をしたからだ。ほんとにコイツはくだらんことを聞くなー、とあきれたんだけど、あーそういえば昔の僕も同じような質問を複数の人々にしていたわ、と。やっぱり親子か。 さて、ここで誰もが感じるであろう疑問は、
カリー／ハワード（Curry-Howard）の対応を知らない子ども達および大人達へ - 檜山正幸のキマイラ飼育記 (はてなBlog)
3月19日(木)にやったセミナーに関して、さっそくにKuwataさんによるまとめが公開されています。 http://return0.dyndns.org/log/2009/03/20#s_2（20日の記事までスクロール） これがまた、とんでもない力作で驚きました。とてもよく仕上がったレポートで、僕の話なんかより、これを読んだほうが分かりやすいくらい。ホントにお疲れさま。どうもありがとう。 Kuwataさん曰く： 今回は内容的に俺がまとめを書けるレベルじゃねえと思っていたら、他の参加者から「また徹夜してまとめ書くんでしょ」と言われてもう後に引けない状況。 僕も含めて皆さん期待していたのは確か。「まとめるんだよね、帰ったら書くんだよね、朝まで書くんだよねー」と、何人かがKuwataさんに声をかけていたけど、彼を殺してしまいかねないから、もうあまり言わないように。 Kuwataさん曰く： さすが
こんなRuby言語 - 檜山正幸のキマイラ飼育記 (はてなBlog)
Ruby言語ってご存知ですか？ インタプリタを開始すると、次のようなバナーが出るようです（動かしたことないけど）。 + `The Ruby Interpreter' Copyright 1993 Graham Hutton graham@cs.chalmers.se + ソースコードは、こんな宣言で始まるようです。 type prog = PRIM prim + SWAP + FORK + SEQ prog prog + PAR prog prog + INV prog type prim = AND + NOT type network == (List node # wire # wire) type node == (wire # prim # wire) type wire = NAME Int + TUPLE (List wire) んで、なんかトランスレーションの定義が並んだり
セミナー非参加者にもわかるリアルワールド向けラムダ計算 - 檜山正幸のキマイラ飼育記 (はてなBlog)
セミナーをやって良い点でもあり辛い点でもあるのは、終わった後で 「こういう説明ならもっと分かりやすかったのでは」 「あーいう順序で話すほうが合理的だった」 「あそこは省略すべきだった」 「駄洒落がスベッた」 「せっかく考えていたギャグを言い忘れた」 などなど、反省つうか後悔が、夏場（今、冬だけど）の入道雲のように湧き湧きしてくることです。 本人（檜山）はかなり強調しているつもりでも、それでもハッキリとは伝わらない事項がいくつかあったようです -- 別な機会（セミナー第1回も含め）で、檜山が何にこだわっているかを承知していれば話は別かもしれませんが。まーともかく、可能な限りアフターフォローします。 本エントリーは、「技術者／プログラマのためのラムダ計算、論理、圏」セミナーとなるべく独立に読めるようにしたつもりですが、次の資料をザッと眺めたほうがいいとは思います。 http://www.chi
時計とポールで学ぶファイバーバンドル - 檜山正幸のキマイラ飼育記 (はてなBlog)
hiroki_fさんがゲージ理論との関連でファイバーバンドル（fiber bundle, fibre bundle、ファイバー束）の説明をしています。 一般相対性理論のゲージ理論的見方(1) 一般相対性理論のゲージ理論的見方(2) 勝手に説明のお手伝いをします。とはいえ、僕が書きかけた話と関係あるので、そっちの話題とつなげようとの下心があります。 内容： 髪の毛とかマルとかがビッシリ生えている ポール付き時計もどきが生えている土地 針を真上にあわせる話 道ごとにポールの傾きの差が与えられる あなたを混乱させる情報 これは整合的じゃない コサイクル条件 コサイクル条件の破れ おまけ：ファイバーバンドルと圏 髪の毛とかマルとかがビッシリ生えている hiroki_fさんがファイバーバンドルの説明に使っている絵は、次のものです。 頭に生えている髪の毛です。 これは確かにファイバーバンドルのイメージ
まだスノーグローブ：superstring04さんへのフォロー - 檜山正幸のキマイラ飼育記 (はてなBlog)
なんか、セミナーへのフォローばっかりやってる感じですが、質問も批判もウェルカムと公言してるから、全部対応します。 http://d.hatena.ne.jp/superstring04/20090201/1233489026 ： もし私たちの世界のミニチュアが手元のスノーグローブに入っているとすれば、 その中にあるスノーグローブには、もっと小さな世界が広がっているだろう、と。 逆に考えて、私たちの世界もまたスノーグローブの中で、一段上の世界があるのかもしれない、と想像できる。 このような構図に僕はすごく魅力を感じるのです。手塚治虫の影響が入っているのかも知れません。これは個人的な趣味や傾向性の問題ですが、スノーグローブ的な状況がSFや映画によく出てくるということは、けっこう多くの人にアピールするんだろうな、とも思います。 さて、以下の部分、若干の混乱があるかもしれません。 数学者流のbマシ
セミナー補足：関数コードの実行エンジン - 檜山正幸のキマイラ飼育記 (はてなBlog)
セミナー終わって、みんなでご飯食べて、太田君の補習をしていたら、（僕にしては）だいぶ遅くなってしまったのですが、なにしろ事前にテンションあげていたので、すぐに眠れない。んでまー、本日の「Eの、いろいろな定式化」について補足します。（ほぼ参加者にしか通用しない話で申し訳ないのですが。） fが2引数関数で、f^ は、fの関数コード、ただしパラメータは残ってないとする。 E(f^, a, b) = f(a, b) -- Eは3引数 E(f^, [a, b]) = f(a, b) -- Eは2引数、第2引数はタプル E([f^, a, b]) = f(a, b) -- Eはタプル1引数、タプルは3項 E([f^, [a, b]]) = f(a, b) -- Eはタプル1引数、タプルは2項だが入れ子 関数コードf^とは、関数の計算手順を刷り込んだデータです。Eは、Exec, Eval, Engine
閉圏、弱いラムダ計算、弱い論理 - 檜山正幸のキマイラ飼育記 (はてなBlog)
「モノイド圏、豊饒圏、閉圏と内部ホム」は自分用メモと思って書いたら、トラックバック／コメント欄で色々とやりとりがあって面白かったです。お相手してくださった皆様、ありがとうございます。 でまー、またゴニュゴニョ続けるのですけど、このての話（って、まだ話してないが）は、ランベック（J. Lambek）とかケリー（G. M. Kelly）あたりが大昔にやっていそうで気が引けますが、まー、練習問題ということで。 “そとの人”と“なかの人” 例え話で、閉圏（閉じた対称モノイド圏のこと）のなかに棲む生物を出したのですが、比喩だからピンとこない人もいるでしょう。でも、この比喩に共感できる人は、強烈で具体的なイメージを持てると思います。「そと」とか「なか」が何を意味するか、もう少し説明しましょう。 まず、“そとの人”は、神様のつもりになった我々人間。圏に対して何でもできます（つうか、そういう幻想を抱いてい
セミナー補足：教科書・参考書 - 檜山正幸のキマイラ飼育記 (はてなBlog)
ラムダ関連の教科書・参考書を聞かれてもよく知らない、というのがホントのところです。が、知ってるものだけ挙げると、まず、正統的なラムダ計算の定番教科書は、 Barendrect, H. "The Lambda Calculus -- its Syntax and Semantics" (North Holland 1981) HINDLEY & SELDIN "Introduction to Combinators and λ-Calculus" (Cambridge, 1986) とかでしょう。しかし、これらは随分古いので今はもっと読みやすいものがあるのかも知れません。 Barendrect はよく引用されているようですが、僕は見たことがありません。HINDLEY & SELDIN は持ってますが、付録3の CARE OF YOUR PET COMBINATOR 以外はちゃんと読んでません
セミナー補足：報告記事とか後悔とか独り言とか - 檜山正幸のキマイラ飼育記 (はてなBlog)
return0のKuwataさんがまとめを書いてくださいました。→ http://return0.dyndns.org/log/2009/01/24 勘違いしてる部分がないとは言えないので、あんまり鵜呑みにしないように。 いえいえ、極めて正確な報告です。ここまでチャンと理解してくれる人が一人でも（もっとイッパイいるならなおさら）僕としては満足。成功だった、と判断してもいいかも*1。 僕は、LispとJavaScript（ほんのチョビット）のコード例しか出さなかったのですけど、それには理由が2つあって（面倒だというのを入れると3つか）； ひとつは特定のプログラミング言語の話だと受け取られるのがイヤだ、という事情。セミナー冒頭で引用した中島先生の言葉にも： 特定のプログラム言語、慣用の計算機システム、ルーティン化したプログラム作成の手順などによって規定される閉じた世界から解き放ち、 とあります
横滑りする興味 -- 閉圏／豊饒圏 - 檜山正幸のキマイラ飼育記 (はてなBlog)
「雑談しながら思ったこと」： type of types とかラムダキューブについて教えてもらった。これは面白いネタなので、別エントリ（来年？）にして書くかも。 ラムダキューブについては、稲葉（k.inaba）さんが説明してくださったのですが、その一部 -- 型パラメータを取る型は、デカルト閉圏と豊饒圏（enriched category）を使うとうまく定式化できそうな感じを抱きました。それで、年末年始業務の合間に、「ボブ・クックの『物理系実務者のための圏論入門』」の冒頭で紹介したことがある、Francis BorceuxとIsar Stubbeによる"SHORT INTRODUCTION TO ENRICHED CATEGORIES"（http://www.win.ua.ac.be/~istubbe/PDF/EnrichedCatsKLUWER.pdf）という論説を読み返していました。
竹内外史・著『層・圏・トポス』 - 檜山正幸のキマイラ飼育記 (はてなBlog)
「トラックバック／コメントは日付を気にせずにどうぞ。蒸し返し歓迎!」で、2007年1月のエントリー（http://d.hatena.ne.jp/m-hiyama/20070109）でのやり取りなので、誰も眺めてないでしょうから、ここに転記しておきます。 http://d.hatena.ne.jp/m-hiyama/20070109#c1229535963 内海さんによると： 昨日のお昼に近所のジュンク堂に行って、何気なく数学書のコーナーを見ていたら、竹内外史さんの「層・圏・トポス」が復刊されて棚に並んでたので、音速の速さでレジに持っていって買ってさっそく読みました(^_^) 説明がシンプルで丁寧なので、もの凄く読みやすいですね。 檜山さんが読まれていたというのも頷けます。 とりあえず一足飛びに第二章の「圏」に行かずに、第一章の「層」から読んでますが、この本だったら層の理論の基礎が解りそうな
人は、できるだけ安く買うことと、自分の評価を伝えることのどちらを選ぶだろう - 檜山正幸のキマイラ飼育記 (はてなBlog)
引き続き、個人デジタル出版のことを考えてます。必ずしも個人じゃなくてもいいのですけど、デジタルでダウンロード可能にはこだわることにします。 僕は紙の本も嫌いじゃないし、紙のメリットもわかるんだけど、なにしろ重いしかさばるし、検索や引用にも不便だしと、そこらへんはデジタルデータにしたい理由になります。それと、紙の商業出版ではニッチな分野をカバーできないですしね。 以前に挙げた「書籍風デジタルコンテンツに要求する条件」のなかで、次のことは紙では難しいから、デジタルコンテンツの優位な点になると思います。 レビュー、フィードバックができる、それを誰でも見られる バージョンアップ／メンテナンスのサポートが付く レビュー／フィードバックなのですが、価格とリンクするようにしたらどうでしょうか？ 例えば、読者が5段階で評価するとします。 評価 意味 定価への乗数 ☆ 買うべきじゃなかった 80% ☆☆ 少
子供と大人、あるいは技術的成熟度 - 檜山正幸のキマイラ飼育記 (はてなBlog)
子供の行動（文字通りの幼稚な行動）や、ある分野の初心者が犯す間違いパターンをみていると、人間の能力や傾向性に対し何らかの示唆を得られたりします。稚拙な行動というのは、たいてい「自然さ」を持っていて、自然だからこそ多くの人が同じパターンに陥るのでしょう。そのパターンが具合が悪いものなら矯正したほうがいいでしょうが、矯正には人為的／意図的（あるいは意志的）トレーニングが必要です。 ウチの子供達の話 長男が小さいときオバアチャンと電話で話していて、目の前のテレビにロボットが出てくると「ほらっ、いまロボットがでてきたでしょ、あのロボットはね…」とか説明を始めてオバアチャンを困惑させていました。次男が今より小さいとき、夢のなかにおにいちゃん（長男）が出てきたらしく、朝起きると「おにいちゃん、夢のなかであんときさー …」とオシャベリをはじめました -- 自分とおにいちゃんは同じ夢を共有していると思って
コミックが現実になった日 - 檜山正幸のキマイラ飼育記 (はてなBlog)
吉田えり投手がプロ野球選手になったというニュースで、水原勇気を思い起こす人は多いでしょうね。吉田さんと水原のキャラクターはだいぶ違いますが。（柔道の谷選手とコミックのヤワラ（YAWARA）ちゃんもギャップがありました。）
この間違いは、なぜ自然なんだろう？ - 檜山正幸のキマイラ飼育記 (はてなBlog)
二十年とかもっと前のことですが、僕は次のような発言（つっても単なるオシャベリ）をしたことがあります。 九州の人って髭が濃いよね。 なんでそんなことを今でも憶えているかというと、言った直後に「あー、自分は間違ったことを言ってるな」と意識し、その瞬間の印象が強く残ったのです。間違った推論について考えるとき、最初に思い起こす実例なのです。 僕が「九州の人って髭が濃いよね」と言った根拠は： 知り合いのAは、福岡県出身で髭が濃い。 知り合いのBは、大分県出身で髭が濃い。 この2つの事実です。 少数事例から一般法則を導く -- こういうタイプの認識とか推論は、僕だけじゃなくて多くの人が行います。古典論理の立場からいうと「間違い」なんですが、多くの人が使っているし、それが通用する場面もあるということは、人間にとってなにかしらの「自然さ」があるように思えます。 「自然だ」とは、このテの認識／推論による言明
Seven Trees：最後のヒント＋もっと面白い話 - 檜山正幸のキマイラ飼育記 (はてなBlog)
そろそろネタ元をばらしましょう。次の論文です。これを[Fiore/Leinster]として引用します。 Marcelo Fiore, Tom Leinster "Objects of Categories as Complex Numbers" http://arxiv.org/abs/math/0212377 [Fiore/Leinster]から参照されている以下の論文がSeven Treesを詳しく扱ったもののようです（僕はまだ読んでません）。 A. Blass "Seven trees in one" Journal of Pure and Applied Algebra, 103:1.21, 1995. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.8517 Seven trees と A tree が同じにな
Seven Trees：これは難しいパズルだ、取り急ぎ紹介 - 檜山正幸のキマイラ飼育記 (はてなBlog)
いずれ、もっと詳しく書くつもりだけど、まーともかく、ざっと紹介しますね。説明が不十分かもしんないけど（ごめんなさい）。[追記]詳しく説明しました。[/追記] 二分木を考えます。空な木は認めない。けど、ルートノードだけの木は認めます。ノードにも辺にもラベルは付いてません。形状だけが問題。ノード数が1から７までの例を描けば次のようですね。 いま、なんでもいいから7本の二分木があったとして、例えば次のような“テンプレート”（番号が付いた白丸のところがプレースホルダ）に当てはめると、1本の二分木ができます。 テンプレートは何種類でも用意してよくて、テンプレート内のプレースホルダを埋めるのに与えられた7本の木全部を使う必要もないとします。例えば、テンプレート内のプレースホルダが1個だけでも0個（単なる二分木）でもいいわけ。 7本の二分木（二分木からなる長さ7のタプル [t1, t2, t3, t4,
Erlang実験室：分かりにくいと評判のErlangエラーのまとめ - 檜山正幸のキマイラ飼育記 (はてなBlog)
Erlangのエラーメッセージは暗号のようだ（Cryptic error messages）とか言われたりします。確かに分かりにくいです。http://bluebones.net/2006/12/erlang-error-messages/ に良いまとめがあった*1ので、これを敷衍＜ふえん＞する形で説明します。 内容： 例外の一般論 ランタイムエラーとスタックトレース reasonタームの一覧 ●例外の一般論 Erlangの例外（exceptions）は次の3種に分類されます。 throw例外 ： ユーザー（プログラマ）が任意の時点で生成する例外 exit例外 ： プロセス*2の終了に伴って生成される例外 error例外 ：主にシステムが生成するランタイムエラー それぞれの例外を、次の関数で引き起こす（raiseする）ことができます。 throw(Term) exit(Term) erla
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
