日々の流転

λ. 原さんに敬意を表して「ヒビルテ」というタイトルにしてみる。

λ. ウルト・ヒケウ 萌え。とか書いてみるテスト。(2006-05-18追記: Googleイメージ検索でウルト ヒケウで検索しても一件も引っかからないのは非常にけしからんと思う。)

λ. ts日記の「コトの真相（私見）」が興味深い。

λ. 三田絵美子さんの日記の5/15に「数学と論理のSAもだいぶありえない。つかえない…。」と書かれていて、自分の事かと一瞬びびった。

λ. WindowsディベロッパのLinux感

COMは，なぜもっと簡単に使えるように提供されなかったのかを考えると残念でなりません(stdioに近いレベルの概念になっていればよかったのに)．

結構同感。仕方ないとも思うけど、もう少しなんとかならなかったかなぁとも思うんだよなぁ。 簡単さといっても、開発環境がテンプレートとかの機能を充実させて実現されるような「簡単さ」じゃなくて、それこそstdioを使うくらい気軽に使えるようになっていれば……

λ. x += y

C等の言語では「+」のような2項演算子について、「x = x + y」を「x += y」と略記出来る。どうせならば、演算子に限らず、YのX上の任意のアクション f: X×Y→X について「x f= y 」と書けるようにしたらどうだろうかと一瞬思った。

λ. 今日のインストール

ocaml-3.04

-

Coq-7.2

config/coq_config.mlに「\n」が入ってしまって構文エラーになってしまうので、そこだけファイルを編集してコンパイル。本当はconfigureを編集すべきなんだけど、ocamlわかんないんで。
それから、例のお馬鹿lnへの対処。

λ. Classification と Infomorphoism の圏

情報射の条件として「f↓(b) ⊨_A α iff b ⊨_B f↑(α)」というのはやはり扱いにくい。そこで、⊨_Xを tok(X)×typ(X) から Ω = {true, false} への写像 ψ_X と考えて、射の同一性で言い換えると「すべての <α,b>: X→typ(A)×tok(B) について、ψ_A <f↓b, α> = ψ_B <b, f↑α>」になる。あんま変わらないか……

情報射を構成する写像を、最初は「f_typ, f_tok」と書いて、次に「f^∧, f^∨」と書くのが正しいと知って、昨日は書き易そうだったから「f↑, f↓」と書いてみたりと、色々な書き方をしてしまったけど、どうせならtypとtokをそれぞれ集合の圏への covariant functor と contravariant functor と考えてしまって、「typ(f), tok(f)」と書くのが良さそうな気がしてきた。何でこう表記しないんだろう。

functorといえば、4.Type-Token Dualityのflipも contravariant functor で、しかも involution だよね。

λ. あと、とりあえずは ruby-parted かなあ。。。

おぉ。libparted-rubyを引き取ってくれると嬉しいなぁ。

λ. ホーア論理

S氏の発表に関するメモ。やっぱ loop invariant って難しい。ところで、ホーア論理では再帰とかが扱えないってホント?

【2009-10-26 追記】 立石さんのコメント通りなのだけど、『算法表現論』(木村　泉，米澤　明憲)に再帰呼び出しに関する規則があったので、ちょっと長いが引用しておく。

ここでは細かい議論には立ち入らないが，再帰的な起動を許す手続きに関しては，帰納法(induction)に類する推論が必要で，たとえば次のような規則*

D7(再帰呼び出しの規則)

    
procedure S(var x~ ; v~); Q(S),  P {T(x~ ; v~)} R ⊢ P {Q(T)} R
────────────────────────────────
P {S(x~ ; v~)} R

が使われる．ただし A⊢B は，一般にAが証明されたと仮定するとBが証明されることを意味する．よって，前提の右側は，P {T(x~; v~)} R という命題が証明されたと仮定して(帰納法の仮説)，手続きSの本体Qの中でSを起動する部分をTで置き換えたもの，すなわちQ(T)の実行に関してP{Q(T)}Rが証明されることを意味する．このような前提が成立するならば，Sをそのまま起動しても実行の直前，直後でPとRが成立する．ただし，再帰的な手続きの実行が終了することは，別に証明しなければならない．

---

* この他に，公理 P {S(x~; v~)} P (ただしx~の中の変数はPの変数として現れない)なども必要となる．

通常の帰納法や余帰納法のような条件がなく、こんな風に証明しようとしている規則をそのまま使っていいのかな?、と疑問になる。 しかし、そのような条件が必要になるのは、停止しないような場合を避けるためで、一方ここで考えているホーア論理の部分正当性ではそもそも停止しない場合のことは考えなくて良いので問題ない。

また、この規則は領域理論の不動点帰納法:

P(⊥)  ∀x. P(x)→P(f(x))  P chain-complete
──────────────────────
P(fix f)

からも得られる。

State を変数から値への関数の空間、Prog を State から平坦ドメイン State_⊥ への関数の空間として、Prog 上の述語 P(C) = {Q1}C{Q2} = ∀s:State. Q1(s)∧(C(s)≠⊥) → Q2(C(s)) を考えると、部分正当性の定義から P(⊥) は常に成り立ち、P が chain-complete であることも容易に示せるので、

∀C:Prog. {Q1}C{Q2} → {Q1}F(C){Q2}
──────────────────
{Q1}fix F{Q2}

が得られる。 これは引数を持たない(再帰呼び出しがある)サブルーチンの、部分正当性の規則とほぼ同じ。

λ. 夕食

ファカルティで「カルビ丼定食」。向井先生のおごり。ごちそうさまでした。

λ. 小沢一郎氏、民主党代表就任を辞退・年金「未加入」判明

なんか、政治責任とか小泉首相と刺し違える云々よりも、未加入云々は単に口実で、参院選の責任を取らされるのを恐れて日和ったんじゃないか。って印象を受けたんだけど、ひねくれてますかね?

λ. case on non-var!?

Propositional Equality の型である Id の使い方がいまいち良くわからない。例えば、

Cat :: #2
  = sig
      Obj :: Type
      Hom :: (A::Obj) -> (B::Obj) -> Set
      id  :: (A::Obj) |-> Hom A A
      o   :: (A::Obj) |-> (B::Obj) |-> (C::Obj) |->
             (f::Hom B C) -> (g::Hom A B) -> Hom A C
      leftUnit  :: (A::Obj) |-> (B::Obj) |-> (f::Hom A B) -> Id (id `o` f) f
      rightUnit :: (A::Obj) |-> (B::Obj) |-> (f::Hom A B) -> Id (f `o` id) f
      Assoc :: (A::Obj) |-> (B::Obj) |-> (C::Obj) |-> (D::Obj) |->
               (f::Hom C D) -> (g::Hom B C) -> (h::Hom A B) ->
               Id ((f `o` g) `o` h) (f `o` (g `o` h))
 
test1 (C::Cat) (A,B::C.Obj) (f::C.Hom A B) :: { }150
  = {C.leftUnit f }151
 
test2 (C::Cat) (A,B::C.Obj) (f,g::C.Hom A B) (z::Id f g) :: { }152
  = {z }153

という状態で、goal 151 で C-c C-c しても、「case on non-var C.leftUnit |? |? f」と言われてしまう。「C.leftUnit f」を「C.leftUnit |A |B f」としても、やはり「case on non-var C.leftUnit |A |B f」と言われてしまう。letを使って一度変数に入れても同じエラーが出る。一方、goal 153 で C-c C-c すると、ちゃんとcaseが挿入される。どっちも型は同じなのに、何故このようになるのだろう?

(2005-09-11 追記) 「型は同じ」と書いたが全然同じじゃないな(汗)。
ところで、落ち着いて考えてみて、何らかの制約があること自体は当然だと気づいた。何故ならば、「case (Id α β) of { ref x -> ... }」という式の「...」の部分はα=β(=x)を仮定して型検査を行うわけだけど、α,βに任意の式を許すと型検査が決定可能でなくなってしまうから。
では、どのくらいの制約が必要か?　αとβがユニフィケーション可能な式であるならば良さそうに思える。だが、実際にはAgdaはαとβが相異なる変数の場合しか受け付けない。これは必要以上に強い制約に思えるが、何故こうなっているのだろうか?

ちなみに、HaskellのGADTはユニフィケーション可能な型でありさえすれば良かったはず。なので、例えば以下のような定義は正しい。

data T a b where
    T :: x -> T x x
 
test :: (T (a,Int) (Int,b)) -> Int
test x =
    case x of
    T (a,b) -> a+b

(2005-09-18 追記) 「ユニフィケーション可能な式ならば〜」というのは安易だった。Haskellの型の場合と違って、higher-order unification が必要だから、決定不可能になってしまう。Functional Programming with Overloading and Higher-Order Polymorphism には higher-order unification が不要な理由として「This is possible because the language of constructors is built up from constants and applications; in particular, there are no abstractions.」と書いてあったのを読んでいたのに、何を馬鹿なことを考えてるんだ、俺は……

——となると、残る疑問はαとβが同じ変数の場合が何故ダメかだな。池上さんが紹介してくれたスライドに「Use elimination rules and not case for inductive families.」と書いてあったし、単に「idata に対しては case よりも elimination rule を使わせる方針なので、case は elimination rule を実装するのに十分な最小限の実装しかされていない」という可能性もあるけど、何か他の理由はあるだろうか?

(2005-09-28 追記) あ、いや、αとβが同じ変数の場合も、一般のidataを考えると無理っぽいな。だいたい納得。

λ. Saunders Mac Lane 1909-2005

亡くなっていたとは知りませんでした。ご冥福をお祈りします。

λ. Towards Observational Type Theory. Thorsten Altenkirch and Conor McBride

• <URL:http://www.cs.nott.ac.uk/~ctm/ott.pdf>
• <URL:http://www.citeulike.org/user/msakai/article/585944>

Extensional Equality in Intensional Type Theory の話を発展させたもの。前の論文では proof irrelevance が本質的な役割を果たしていると思っていたが、実際にはそれほど本質的ではないというのにまず驚いた。

(詳しくは後で書く)

OTTは理論的にも面白いし、実用的にも便利そうな型理論だと思う。Epigramを使ってみたくなった。

λ. 高校の勉強ムズス

• 接弦定理なんて知らね
• 漢文の返り点の結合順位を誰か教えてくれ

λ. 4回目の夜勤明け

ようやく4日間の夜勤が終わった。疲れた……

「工場萌え」とか言ってる人は、工場で実際に働いてみればいいと思った。

しかし、今日明日はせっかくの休日なのに天気がいまいちのようだ。 残念。

生活サイクルを戻すために、午前中に少しだけ睡眠をとり、午後からは買い物に行ったり。

昼食はジャスコの中にあったカジャという韓国料理の店。海鮮かた焼きそばみたいなのを食べたのだが、微妙だった。まずくはなかったけど、ほとんどキムチの味しかしないし、そもそも量が多すぎ……。焼肉とかは普通に美味しかったみたいなので、無難なものを注文していればよかったと後悔。

今日もプールでは1km泳いできた。

夜、さっく〜氏のところでやっていた焼酎試飲会に参加。

そのときに、工場労働者は平均余命が短いという話を又聞きくらいで聞いた。私の知る限り、日本には産業別・職業別の平均余命のまともな統計は存在しないので、実際のところはわからない。ただ、有り得ないことではないと思った。そして、皆あんなにいい人たちなのに……とやりきれない気持ちになる。

λ. 相棒 ―劇場版―

帰りに映画館によってみた。 時間通りに行ったら20分ぐらい予告編で辟易。 内容は、どうにも犯人側の行動や戦略に合理性と一貫性が欠落しているように思えて、あまり納得のいかない終わり方だった。 本仮屋ユイカはかわいかたけど。