日々の流転

λ. 風邪ひいた

体調が悪いので泳ぎに行くのは諦める。 ……と思ったら、夜になって熱が上がってきた。 風邪ひいたっぽい。最近、疲れが溜まってたのかなぁ。 インフルエンザとかじゃないといいけど。

λ. 麻生太郎「ニコ割アンケートに答える」

観た。こういうのを観てると印象は良いのだけどねぇ……

• 【政策編】麻生太郎「ニコ割アンケートに答える!」Vol.1
• 【プライベート編】麻生太郎「ニコ割アンケートに答える!」Vol.2

λ. 風邪でダウン中

一晩寝たら直るかと思ったけど、朝起きたら38.4℃くらいあった。 医者に行って診察を受けてきて、下痢してるので整腸剤と、あと熱が上がって辛いときのための解熱剤を処方してもらう。インフルエンザではなさそうなのでちょっと安心。 解熱剤は飲まないつもりだったけど、夕方39℃を超えたので解熱剤を飲む。 飲んで寝てたら汗を沢山かいて熱が一気に37℃台まで下がって驚いた。解熱剤効きすぎでちょっと怖いよ。

λ. 風邪でダウン中 (2)

熱は37℃台のままで、下痢が止まらない。すべきことが色々と溜まっているのに困った……

ところで、「お腹を冷やすな」というのは比喩表現だと思ってたら、お腹って本当に冷えるんだね。手を当ててヒンヤリしたので驚いた。胴体の中心に近くて血管も沢山通ってるだろうから、凍死寸前でもなければ冷えたりなんかしないと思ってたよ……

λ. 参議院法務委員会での国籍法改正案の採択

• YouTube - 「音声とめて!」　民主党、千葉景子が国籍法をゴリ押し　（２分過ぎ）
• 国籍法改正案 採択　参議院法務委員会 音声上げてみた‐ニコニコ動画(冬)

改正国籍法の是非についてはともかく、意見に対して音声と速記を止めるってのはどうなの?　国会での慣行を知らんので何とも言えないのだけど、こういうことが行われているってのは結構ショックなんだけど……

λ. 風邪でダウン中 (3)

熱は37℃台のままだけど、お腹の調子が悪化中で一日中悶えていた。 今日は20回くらいはトイレに駆け込んだよ……

λ. ビッグ３公聴会：格付け会社「破綻回避７５０億ドル必要」

自家用ジェット機が批判されたからって、ミシガン州から800キロ超の距離を10時間以上かけてワシントンに入るって……

λ. 風邪でダウン中 (4)

熱も下がったし、お腹もだいぶ良くなってきたけど、相変わらずダウン中……

λ. ２次補正提出首相先送り表明　『ねじれ』足かせ　廃案回避へ苦渋

国会法の規定で通常国会は一月三十一日までに開会しなければならず、事実上、今国会は来年一月二十九日までしか延長できない。同二十九日までに「みなし否決→再可決」を行うには、関連法案を十一月三十日までに衆院通過させる必要があるが、既にそれは不可能だ。

二次補正を通常国会に先送りする理由がどうもわかり辛かった*1けど、こういう事情もあったのね。これは面白い。 そういえば、ちょっと前に「伊藤洋一のRound Up World Now!」か何かで、与野党の信頼関係が失われているのが問題というような意見があったが、これは与野党の信頼関係が失われていることによる実害の非常にわかりやすい例だと思った。

λ. ゴーストシップ

ホラー映画としてはいまいちだったけど、殺戮のシーンは全般的に良かったな。 例のワイヤーのシーンだけでなく、鍋に劇物をドバドバ投入してるシーンとかも結構好きだ。

• ゴーストシップ‐ニコニコ動画(冬)

λ. 風邪でダウン中 (5)

ようやくお粥とか消化のよいもの以外を食べられるようになった。これなら明日は復活出来そう。

しかし、今回は久しぶりに風邪でひどい目にあった。風邪はひくもんじゃないなぁ。

λ. 量子力学と量子暗号のかんたんなお話 by Kuniaki Igarashi

はじめてのにき(2008-12-10) - あんごう より。おお、これは分かりやすい。量子暗号ってどういう話なのか気になってたけど、そういう仕組みなのね。

λ. 国家公務員に冬のボーナス、３４００円減の平均６９万２９００円

国会議員にボーナスがあることを初めて知る。 「国会議員の歳費、旅費及び手当等に関する法律」の第十一条の二から第十一条の四によって定められているようだ。 ただ、業績や成果に報いるためのボーナスというわけではないようだし、通常の歳費と別にする必要は無い気もする。

λ. 今日は泳ぎに行かない

まだ病み上がりで体調が微妙なので、今日は泳ぎには行かずそのまま帰る。

λ. DrHylo: A tool for deriving hylomorphisms

DrHylo is a tool for deriving hylomorphisms from a restricted Haskell syntax. It is based on the algorithm first presented in the paper Deriving Structural Hylomorphisms From Recursive Definitions at ICFP'96 by Hu, Iwasaki, and Takeichi. The generated code can be run with Pointless Haskell, allowing the visualization of the recursion trees of Haskell functions.

【2009-11-04 追記】 まず、ホームページにある以下の例を試してみる。

module Sample where

swap :: (a,b) -> (b,a) 
swap (x,y) = (y,x) 

data Nat = Zero | Succ Nat 

len :: [a] -> Nat 
len [] = Zero 
len (h:t) = Succ (len t)

これに対して、DrHylo -iSample.hs とすると、以下のような感じでhylomorphismの三つ組み表現で出てきて、「おー！」という感じ。

{-# LANGUAGE TypeFamilies #-}
module Sample where
import Generics.Pointless.Combinators
import Generics.Pointless.Functors
import Generics.Pointless.RecursionPatterns

swap :: (a, b) -> (b, a)
swap = app . (((curry ((snd . snd) /\ (fst . snd))) . bang) /\ id)

data Nat = Zero
         | Succ Nat

type instance PF Nat = (:+:) (Const One) Id

instance Mu Nat where
        inn (Left (_)) = Zero
        inn (Right (v1)) = Succ v1
        out (Zero) = Left (_L)
        out (Succ v1) = Right (v1)

len :: [a] -> Nat
len
  = hylo
      (_L :: Fix ((:+:) (Const One) Id))
      (app . (((curry (app . ((eithr . ((curry (inn . (inl . bang))) /\ (curry (inn . (inr . snd))))) /\ snd))) . bang) /\ id))
      (app . (((curry (app . ((eithr . ((curry (inl . bang)) /\ (curry (inr . (snd . snd))))) /\ (out . snd)))) . bang) /\ id))

ただ、以下のような関数

plus :: Nat -> Nat -> Nat
plus m Zero = m
plus m (Succ n) = Succ (plus m n)

に対しては、

plus :: Nat -> Nat -> Nat
plus = app . (((fix . (curry (curry (curry (app . ((eithr . ((curry (fst . (((snd . fst) . fst) /\ (snd . fst)))) /\ (curry (inn . (inr . (app . ((app . ((((snd . fst) . fst) . fst) /\ (fst . (((snd . fst) . fst) /\ (snd . fst))))) /\ snd))))))) /\ (out . (snd . ((snd . fst) /\ snd))))))))) . bang) /\ id)

となってしまって、hylomorphismを導出できない。 他にも色々試してみたが、思ったほどにはhylomorphismを導出できない感じ。

λ. RHG読書会::東京 Practical Common Lisp 第十三回

前回が11月29日だったので、まだ二週間しか経ってなくて、「もう今日か」という感じだった。

λ. やつれたらしい

今週は何人かの人に「やつれたんじゃない?」と言われた。 やつれた自覚はなかったのだけど、確かに2,3日まともに食べれない・消化できない状態だったからなぁ。

λ. 第四十七回圏論勉強会

今日は圏論勉強会だった(写真)。 昨日RHG読書会で今日は圏論勉強会、二日連続はやっぱりちょっと疲れるね。

前回やりのこした6.4節の残りでは、テンパリー・リーブ圏TLに対してスターやダガーを定義して strict pivotal dagger category にして、3節で定義したDと strict pivotal dagger category として同型であることを示す。 それから、7節に入ってラムダ計算の導入。ここで考える型付け規則は線形ラムダ計算のものになっていて、次回はこれを pivotal category で解釈する模様。

KellyとLaplazaのCoherence for compact closed categoriesのPDFはElsevierにあるけど$31.50もする……

λ. 直観主義命題論理の意味論

直観主義命題論理のモデルって以下の三種類くらいあるのだけど、その関係を私はちゃんと考えたことがなかったので、ちょっとだけ考えてみた。

1. クリプキ・モデル
2. 位相空間の開集合系によるモデル
3. ハイティング代数によるモデル

クリプキ・モデルである論理式が真になる世界の集合は上に閉じた集合なのでAlexandrov位相の開集合になり、したがって位相空間によるモデルを得られる。〚A→B〛 は ∪{X∈O | X∩〚A〛⊆〚B〛} = int(〚A〛^c ∪ 〚B〛) となる。

一般に、位相空間の開集合系はフレームという代数をなすが、フレームは a→b = ∨{x | x∧a≦b} と定義することでハイティング代数になるので、位相空間によるモデルからハイティング代数によるモデルが得られる。 ので、位相空間によるモデルはハイティング代数によるモデルの特殊例。

次に、ハイティング代数 K によるモデルが与えられたとき、そのスペクトラムであるコヒーレント空間 Spec K を考えれば位相空間によるモデルが得られる*1。

最後に、位相空間によるモデルが与えられたとき、specialization (pre)order によって順序を入れれば、クリプキ・モデルを得られる。ただ、元の位相空間がT₀でない場合には、得られたクリプキ・モデルの到達可能性関係は半順序ではなくて前順序になってしまうので、半順序になるように商集合をとる必要がある(T₀化)。 半順序になるよう商集合をとる必要があるのは、多くの文献ではクリプキ・モデルの到達可能性関係に半順序という条件を付けているからなのだけど、実際にはこれは前順序に弱めてしまっても特に不都合はないはずで、なんで多くの文献では半順序として定義してるんだろうなぁ。

λ. Information Flow: The Logic of Distributed Systems 読了

2008-11-11に購入した Information Flow: The Logic of Distributed Systems (Cambridge Tracts in Theoretical Computer Science)(Jon Barwise/Jerry Seligman) を読み終えた。後半はざっとしか読めてないけど、これで心残りがひとつ片付いた。

λ. 帰りに泳いできた

今日は帰りに久しぶりに泳いできた。 先週と先々週は調子が悪かったのと病み上がりで泳ぎに行かなかったので、3週間ぶり。 使ってなかった筋肉を久しぶりに使ってる感があった。 1kmを25分くらいで。

λ. 『数理論理学』 (古川康一, 向井国昭)

半年くらい前に出た古川先生と向井先生の本をざっと読んだ。 「問題を論理を使って表現して、推論によって問題解決する」という古きよき視点から、命題論理、一階述語論理、論理プログラミング、発想論理プログラム、帰納論理プログラムについて入門者向けに解説した本で、この視点からは良く纏まっている。 厚くないので読みやすいのではないかと思う。 また、個人的には一般論理プログラムの安定モデルによる意味論などをちゃんと説明しているのは、ちょっと好印象。

ただ、論理と計算のしくみ(萩谷 昌己/西崎 真也)などと違って、計算機科学・情報科学での論理の応用を幅広く押さえた本にはなっていないので、そこには注意が必要だと思う。 これには厚さの都合もあるだろうけど、「コンピュータサイエンス教科書シリーズ」というシリーズの中の一冊という位置づけだから、というのもあるのかなぁ、等と思った。

λ. Gabaマンツーマン英会話の無料体験レッスン

Gabaマンツーマン英会話の無料体験レッスンを帰りに受講してきた。

最初に20分くらい日本人のカウンセラとのカウンセリングで、現在の自分で思っているレベルや、目的・ゴールや、気になっていることなどを確認。その後、ネイティブスピーカのインストラクタと40分弱のレッスンをする。最初に目標などの話をしていたので、今回はレッスン部分は通常よりも若干短かった。

目標に関しては、以下のような感じに。

• needs English at work (conferences)
  • discussion
  • deal with travel situations

それで、Level 6 (Low Intermediate) の Conversation Strategies というのを薦められ、Conversation Strategies: Pair and Group Activities for Developing Communicative Competence(David Kehe/Peggy Dustin Kehe/Andrew Toos) をテキストに本来のレッスンを。 今回はテキストの最初の項目だった Rejoinder について。 テキストを簡単に見た後に、適当なテーマについて雑談しながら、テキストに出てきた受け答えなどを使ってみる。

レッスンの結果の現状分析は以下のようになった。

• Positive Points
  • relatively strong base
  • stronger listening skills
  • comfortable with familiar language
• Points to Improve
  • speaking
    • vocabulary (natural + formal)
    • quick response
    • express smoothly and clearly

「Points to Improve」に挙がった点は、自分でも弱いと思っていた部分なので、納得。 また、ICレコーダを使ってレッスンを録音して聞きなおすと良いというアドバイスをもらった。そういうことをさせて貰えるものだとは思っていなかったので、ちょっと嬉しい驚き。

その後、カウンセラとインストラクタと三人で結果について確認し、それからカウンセラとコースや見積もりの話に。教育訓練給付制度の対象になるコースだと、どの教室でもレッスンを受けられるオプションを付けられなくなってしまうのが、悩み所。

カウンセラの人もインストラクタの人も非常に好印象だったのだけど、他の英会話学校を知らないと比較も出来ないので、とりあえず次は他の幾つかの英会話学校の無料体験レッスンを回ってみるつもり *1。

2008-12-30 追記

ずっと、「ギャバ」と読んでいたが、読みは「ガバ」らしい。 ぐぐる先生に教えて貰った。

λ. 『独房の修道女』 Paul L. Moorcraft

独房の修道女 (扶桑社ミステリー)(ポール・L. ムーアクラフト/Paul L. Moorcraft/野口 百合子) を読了。 ケッチャムみたいなのを期待してたんだけど、ケッチャムのような陰惨・凄絶な物語ではなく、普通のエンターテイメントとして楽しめた。

Quotation

p.215

マーダは完全な沈黙、完全な闇の中に残されたが、自分を誇らしく感じた。少し前までは、絶望的な恐怖に震えるでくのぼうにすぎなかった。いまは、あの狂人を哲学的議論に引き込むことになんとか成功した。彼のルールに従っているようにふるまえばいい。あの男は彼女の心身を支配したがるだろうが、支配できるのは体だけだ。心は自分のものだ。そして、彼のゲームで彼を打ち負かしてやる。

λ. iKnowの「旅に出よう！（出国＆街を歩く）」を完了

iKnowで2008-11-20に始めたコース「旅に出よう！（出国＆街を歩く）」が終わった。次は「旅を楽しもう！（レストラン＆ホテル）」をやる予定なので、「プロの英語（企業会計編）」はまだしばらくおあずけ。

ところで、私の知り合いで iKnow をやってる人がいましたら、よかったら一緒にやりませんか〜?
(⇒ 私のアカウント: <URL:http://www.iknow.co.jp/user/sakai>)

λ. お菓子補充

貯蔵していたお菓子が尽きたので補充。

λ. 落ち込んでいる

最近色々あってちょっと落ち込んでいる。 何かしてれば平気だけど、ふとしたときに思い出して、やるせない気分になる。 相変わらず打たれ弱いなぁ…… (ため息

λ. Universal Shell Programming（USP）向けシェル機能と実装 by 片山善夫 and 當仲寛哲

Unixのシェルスクリプトで業務開発というのを見て驚いた。 現状のUnix上のシェル環境では、たとえ拡張したとしても、やっぱり無理がある*1と思うが、元々のUnixの思想としては確かにこうあるべきなんだろうなぁ。

• 第162回 ソフトウェア工学研究発表会
• Universal Shell Programing Laboratory
• CiNii - Universal Shell Programming (USP)向けシェル機能と実装(シェルプログラミング・Webアプリケーション)
• 情報処理学会電子図書館 - Universal Shell Programming (USP)向けシェル機能と実装(シェルプログラミング・Webアプリケーション)

λ. 『世界金融危機』について by 苫米地英人

散歩道 : 世界金融危機のカラクリより。 恥ずかしながら、これを読んで初めてCDS怖いと思った。 オフバランスの取引、相対取引だけでここまで出来てしまうんだねぇ。 「今後は、CDSを相対取引ではなく取引所に上場して不正を厳しく取り締まっていくべき」というのは同感。

λ. ECC外語学院に行ってみた

先週木曜はGabaに行ったので、今日はECC外語学院に行ってみた。

今回はカウンセリングだけで体験レッスンは無し。 どうもカウンセリング受けて、レベルを確かめる試験を受けて、それからやっと体験レッスンという何とも面倒くさい流れになっているようだ。 レギュラーコースの場合の試験はTOEIC風の独自のものらしいのだけど、それならTOEICのスコアでとりあえず代用して、まずは体験レッスンを受けさせて欲しいものだと思った*1。

説明*2を受けてシステムについては良くわかったけど、実際のレッスンを体験していないので、なんとも言えない感じ。 単に会話に慣れるための方法としてはグループレッスンは費用対効果は良いのかもしれないと思ったんだけど、やっぱり体験してみないとなんともね。 あと、ちょっと不安に思ったのは、レギュラーコースの場合だとリスニングや文法など英会話学校以外で学ぶことが可能な項目にも、結構時間を割かれてしまいそうだったところ。

λ. 『層・圏・トポス—現代的集合像を求めて』

『層・圏・トポス—現代的集合像を求めて』をbonotakeさん経由で入手。 Andreas Blass の Seven trees in one を読んだときに、分類トポスやらグロタンディーク位相での強制法やらの話で挫折して、この辺りは勉強したいと思っていたので、ちょうど良いところで復刊してくれた感じ。

• 竹内外史・著『層・圏・トポス』 - 檜山正幸のキマイラ飼育記
• 層・圏・トポス—現代的集合像を求めて 購入 - たけをの日記＠天竺から帰ってきたよ

λ. “Perils of Transitive Trust in the Domain Name System” by Venugopalan Ramasubramanian and Emin Gün Sirer

• <URL:http://www.usenix.org/event/imc05/tech/ramasubramanian.html>

結構前に読んだ論文。スラッシュドット・ジャパン | ネットのドメインの85%は乗っ取り攻撃から逃れられない より。

DNSのアーキテクチャは委譲に基づいていて、伝統的には委譲先を増やすことによって冗長性を増やして堅牢に出来ると思われていたが、ドメイン乗っ取りのリスクを増やしているという話。

委譲先のネームサーバーの名前を解決するためには、そのネームサーバーのドメインが委譲しているネームサーバーが利用されることになり、それが繰り返されることによってネームサーバーの間に複雑な依存関係が生じている。 あるドメインを基点として、委譲関係によって生じる依存関係のDAGをTCB(Trusted Computing Base)と呼ぶ。 ある名前のTCBグラフのカットを押さえることが出来れば、その名前を完全に乗っ取れる。カットの一部しか押さえることが出来ない場合には、攻撃者はカットの残りの頂点に対してDoSすることによって、実質的に乗っ取りを行うことが出来る。

で、実際に調べてみたら、殆どのドメインでTCBの中に脆弱性を持ったネームサーバーが含まれていて、乗っ取り可能な状態にあったとか。

電車が空いていた。世間はもう冬休みなのかな。

λ. Data.List.intercalate

最近、Data.List モジュールに intercalate :: [a] -> [[a]] -> [a] という関数がある事を知った。これは intercalate x xs = concat (intersperse x xs) で定義される関数で、intercalate ", " ["a", "b", "c"] == "a, b, c" という感じ。

何度も自作していた関数だったのだけど、標準ライブラリにあったのね。 調べてみると、GHC-6.8になるときに既に入っていたようだ。 気づかなかった……

λ. メモ: 『層・圏・トポス』第一章「層」

(後でちょっとづつ書く)

p.13 Xを空でないとしているのは何故?

p.14 前層の第一の定義 ⇒ 第二の定義

1. Ef=Eg=∅ ⇒ f = f⌉Ef = f⌉∅ = g⌉∅ = g⌉Eg = g
2. r_UU(f) = f⌉U = f⌉Ef = f
3. (r_UV∘r_VW)(f) = f⌉V⌉U = f⌉(V∩U) = f⌉U = r_UW(f) (U⊆V より V∩U=U)

p.15 前層の第二の定義 ⇒ 第一の定義

• (0) a∈FU, b∈FV とすると、a⌉∅=r_∅U(a)∈F(∅) かつ b⌉∅=r_∅V(b)∈F(∅) で、F∅は一点集合なので a=b
• (1) a∈FW とすると a⌉Ea = a⌉W = r_WW(a) = a
• (2) a∈FW とすると E(a⌉U) = E(r_(W∩U),W(a)) = W∩U = Ea∩U
• (3) a∈FW とすると a⌉U⌉V = (r_{(U∩W)∩V,U∩W}∘r_U∩W,W)(a) = r_{(U∩V)∩W,W})(a) = a⌉(U∩V)

λ. ベルリッツの無料体験レッスンに行ってきた

先日のGabaとECCに続いて、今度はベルリッツの無料体験レッスンに行ってきた。 ベルリッツでは、まず紙のアンケートに答えたり簡単な確認をした後、(カウンセリングとかではなく)いきなり教師と会話してレベルチェックだった。 そして、レベルチェックの結果のレベル3のテキストでのレッスンを受け、その後カウンセラの人と結果の確認やシステムの説明や見積もりの話に、という流れだった。

内容については、レベルチェックでもレッスンでも、あるお題について自分から何か質問するのが結構あり、質問が思い浮かばずにちょっと大変だった。積極性を身に付けるには良いとは思うが。 また、単語ではなく文章で答えるように指導されるし、細かい文法的間違いについてもちゃんと直してくれたりで、これなら確かにビジネスシーンで使える英語が身に付きそう。

全体的に「カッチリした英語を教えてくれて、その分他と比べてちょっと高い」という印象。 また、Gabaが良くも悪くもカジュアルな感じだったのに対して、ベルリッツは良くも悪くもフォーマルな感じ。 ただ、レッスン結果や現状の分析については、Gabaの方がしっかり見て貰えていた気がする。

あと、テキストは独自のテキストでバインダーに綴じる形になっていた。これはこれで必要な部分だけを綴じておいたり、メモ用のリーフを綴じておいたり等のメリットがあるけど、ちょっとかさばりそうな気もする。それから、Gabaでアドバイスされたレッスンの録音について聞いてみたら、ベルリッツでもOKとのこと。 ちょっと気になったのは、今回行った教室では夜のレッスンは 6:15〜7:40, 7:45〜9:10 が予約枠になっていて、7:00からと8:30からの枠を単独で取れないこと。

λ. 第77回全日本フィギュアスケート選手権

武田奈也かわゆす。

λ. 言語雑談会

言語雑談会なるものがあったとか。メモ。

• 言語雑談会 2008-2 - 星の贈り物(2008年12月の日記)
• 年末 - 兼雑記(2008-12-30)

λ. 「伊藤洋一のRound Up World Now!」休止するのか

もう二年以上聴いている「伊藤洋一のRound Up World Now!」だけど、12月26日の放送を最後にいったん番組を休止するのか。 そのアナウンスで10年3ヶ月間も続いていた番組だと知り、そんなに長く続いていた番組なのかと驚いた*1。 とりあえず、これまでありがとうございました。 有料化されても月500円くらいだったら聴き続けたいとは思うが、どうなるやら……

【2009-01-11追記】 土日の勉強会への行き帰りで聞くことが多かったので、今日圏論勉強会に行くとき、ああ今週はないんだなと実感して、少し寂しかった。

λ. 『たのしいムーミン一家』 Tove Jansson

たのしいムーミン一家 [英語版ルビ訳付] 講談社ルビー・ブックス(トーベ ヤンソン/Tove Jansson/Elizabeth Portch/エリザベス ポーチ) を読了。 昔観たアニメ版は基本的にほのぼのしたイメージだった記憶しかないのだけど、この原作はちょっと奇妙で不気味なイメージもあって、違いが面白い。

Quotation (pp.144-145)

‘We sat just like this in the spring,’ said Moomintroll. ‘Do you remember, we had woken up from our winter sleep and it was the very first day? All the others were still asleep.’
Snufkin nodded. He was busy making reed boats and sailing them down the river.
‘Where are they going?’ asked Moomintroll.
‘To places where I'm not,’ Snufkin answered as, one after another, the little boats swirled away round the bend of the river and disappeared.

スナフキンが旅に出ることをムーミントロールに告げる直前のシーン。二人の胸のうちが想像出来て、味わい深い。

λ. 忘年会

いつもの芋蔵で忘年会。 今回呑んだのは「くじらのボトル」「山ねこ」「黒閻魔」「七夕」「たちばな」。

ダイナタンクス

λ. 「クリーニ代数入門」 by 古澤 仁 and 高井 利憲

• <URL:http://www.jstage.jst.go.jp/article/jssst/23/3/23_3_14/_article/-char/ja/>

二年前からの積読消化。 ちょっと前 に Topology via Logic の12章 Spectra of rings を読み返して、そこでquantaleに関係して「Conway [71] defines the notion of “standard Kleene algebra”, which is essentially the same as a quantale」と書かれていて、そういえばと思って読み始めたもの。 クリーニ代数に関しては「正規表現を公理化した代数らしい」というくらいの知識しか無かったんだけど、これは応用も沢山あり面白い。

ちょっとビックリしたのは、min-plus代数とトロピカル代数が同じもので、これがクリーニ代数の一例であること。 min-plus代数についてはPPL2008での発表 Modal μ-calculus on min-plus algebra N∞ で聞いていたし、トロピカル代数については檜山さんが時々日記に書いていた*1のを読んでいた。 どちらもちゃんと理解出来てはいない話だったのだけど、繋がってたのね……

min-plus代数を使って最短経路問題を解く話は面白かったので、自分でも試しに書いてみた。KleeneAlgebras.hs

また、自由代数に関しては、代数のクラスCが等式またはホーン節で定義される場合には集合からの自由生成が可能という話は、等式以外から自由生成することなんて考えたことが無かったので、「へぇ」と思った。

あと、KAT-MLという対話的定理証明器があるそうなので、遊んでみたい。