日々の流転

λ. 婷婷と話してて、彼女の所属している研究会はずいぶん研究っぽい研究をしてるなぁと思いました。それに比べて……

λ. プログラミング言語論

Pascalのポインタ演算子は「^」(ハット)だと思ってたんだけど、本来は「↑」で、Pascalの教科書ではそう書いてあるのが多いらしい。

「型は、値の集合と、その値への操作から構成される」とあるけど、そういう素朴な概念だけではなくて、他のモデルについても示して欲しかったと思った。こないだ読んだ On Understanding Types, Data Abstraction, and Polymorphism の 3. Types are Set of Values の最後の方に、retract model と second-order λ-calculus の事が少し言及されていたので、気になっている。

λ. PTQ

片山さんのPrologによる実装が登場。公開をリクエストした甲斐があった。

λ. 情報数学Ⅱ

先週失敗したので欝だ。

λ. tomcatソース読み

研究会で、発表者がいなかったので、代わりに僕が src/share/org/apache/tomcat/util/http を読んだ。場所は、Javaを知らなくても全く問題なさそうな所を選んだ。それにしても小賢しい最適化が多くてウザい。

λ. kinukoレンジャ

某所ので行われたしょーもない会話。

• 「研究会の男女比を改善するのは来期の課題ってことで」
• 「でも、使えない人が入ってきてもらってもなー」
• 「逆に、安田さんみたいな人ばっかり入ってくるってのも、どうかと」
• 「研究室のドアを開けたら、5人の安田さんが振り向いたりして?」
• 「全員色違いだったりしてね」
• 「きぬこレンジャ?」
• 「安田ブラック、安田ブルー、安田レッド、安田ピンク、安田イエロー ...」
• ...

λ. Mita Logic Seminar

今日は三田で竹内外史の「Gödel Sentence」というタイトルの講演があったのだけど、授業があったので行けなかった。残念。こういうのって何で平日が多いのだろう。

λ. ソフトウェア基礎理論

離散数学やソフトウェア基礎論理学に関するページです。東大工学部の講義「ソフトウェア基礎理論」の内容とリンクしています。たくさんあるプログラミング言語の、根底の部分についてです。ソフトウェア設計やさんはこういう論理学についての知識を身につけておくと、きっと役に立つと思います。

遠山さんの日記より。

λ. Agda による選択公理の証明

--#include "Hedberg/Logic/Set.alfa"
open LogicSet use Prop, Forall, Exist
 
AC (|A::Set) (|B::A->Set) (|C::(x::A)->(y::B x)->Prop)
   (z :: Forall A (\(x::A) -> Exist (\(y::B x) -> C x y)))
  :: Exist (\(f::(x::A)->B x) -> Forall A (\(x::A) -> C x (f x)))
  = struct
      fst = \(x::A) -> (z x).fst
      snd = \(x::A) -> (z x).snd

以前に「ITT₀では選択公理も証明できる」と書いたが、その証明と本質的に同じもの。

ところで、Forallは量化される型が明示的な引数なのに、Existは量化される型が暗黙の引数なのは何故?　とても気持ち悪い。

ところで、この形の選択公理は証明できるけど、ZF集合論での場合と違って、選択公理から排中律を証明することは出来ない。何故ならば外延性公理に相当するものが仮定されていないから。

λ. ジョンQ —最後の決断—

を視た。

λ. RHG読書会: 鈴木さんを囲む会

寝坊したので諦めた。しょぼーん（´・ω・｀）

λ. A groupoid model refutes uniqueness of identity proofs. Martin Hofmann and Thomas Streicher.

• <URL:http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=316071>
• <URL:http://www.citeulike.org/article/602344>

を読んだ。groupoidの圏とfibrationを使って、Idの要素がequalityでなくgroupoidのendomorphismを表すようなモデルを作る話。そうすると、nontrivialなendomorphismが存在するgroupoidについてはIdは複数の要素を持つ。言っていることはそんなに難しくはないのだが、indexed-category とか presheaf とか fibration とか grothendieck construction とか 2 category とかに不慣れ*1なことと、一部にインフォーマルな表記がされていることから、きちんと追いかけるのが大変だった。大変だったけどその分これらに少しは馴染めたような気がするが……

まあ、なんにせよ、Propositional equality の証明の equalityでの悩みはとりあえず解決か。

λ. NやList(N)のUIP

上記論文によると、NやList(N)のような型に関しては「UIP is actually syntactically derivable in the presense of a universe」らしいのだが、どうやるのかわからん。とりあえずゼロの場合は以下のように証明出来たのだが……

--#include "Hedberg/SET.alfa"
open SET use Id, refId, Unit, tt, Nat, zero, succ

Lem (x,y::Nat) (p::Id x y) :: Set
  = case x of
      (zer  )-> case y of
                  (zer  )-> Id p (refId zero)
                  (suc m)-> Unit
      (suc m)-> Unit

lem (x,y::Nat) (p::Id x y) :: Lem x y p
  = case p of
      (ref z)-> case z of
                  (zer  )-> refId (refId z)
                  (suc m)-> tt

prop (p::Id zero zero) :: Id p (refId zero)
prop = lem zero zero p

【2006-05-18 追記】 二日くらい必死で考えてようやく証明できたが……これ死ねるよ*1。termination-checkerは通らないけど、引数が小さくなっているのは明らかだからとりあえず良いよね。綺麗に書き直すのはまた今度ということで。それはそうと、Universeの強力さを初めて実感した。

--#include "Hedberg/SET.alfa"
open SET use Id, refId, substId, Nat, zero, succ, Zero

uipNat (n::Nat) (p::Id n n) :: Id (refId n) p
uipNat =
    let T (|n1,|n2::Nat) (p::Id (succ n1) (succ n2)) (q::Id n1 n2) :: Set
          = case q of
              (ref x)-> Id (refId (succ x)) p 
        lemT (x,y::Nat) (p::Id x y) :: Set
          = case x of
              (zer   )->
                  case y of
                    (zer   )-> Id (refId zero) p 
                    (suc y')-> Zero
              (suc x')->
                  case y of
                    (zer   )-> Zero
                    (suc y')-> (q::Id x' y') -> T p q
        lem (x,y::Nat) (p::Id x y) :: lemT x y p
          = case p of
              (ref n)->
                  case n of
                    (zer  )-> refId (refId zero)
                    (suc m)->
                        \(q::Id m m) ->
                        let lem2 :: Id (refId m) q 
                            lem2 = uipNat m q
                            lem3 :: T p (refId m)
                            lem3 = refId (refId (succ m))
                            lem4 :: T p q
                            lem4 = substId (\q -> T p q) lem2 lem3
                        in lem4
    in case n of
         (zer  )-> lem n n p
         (suc m)-> lem n n p (refId m)

λ. 人狼審問 : (1453)ホームズからの挑戦状

観戦中。

関連リンク

• 「推理とは何か実験村」実行委員会
• B1/1453村 - 人狼ファンWiki
• マーガレット(raruさん)の感想

λ. 単相性制限 (monomorphism restriction)

<URL:http://d.hatena.ne.jp/a-san/20060511>の話。 普段は気にしないし、避けるのは難しくないのだけど、こういうときに説明に困ってしまうな。

メモ。

• <URL:http://www.sampou.org/haskell/tutorial-j/pitfalls.html#sect12.3>
• <URL:http://haskell.org/onlinereport/decls.html#sect:monomorphism-restriction>
• <URL:http://hackage.haskell.org/trac/haskell-prime/wiki/MonomorphismRestriction>

λ. ブルバキとモーニング娘。と

<URL:http://d.hatena.ne.jp/yaneurao/20060514> での「ブルバキみたいなやっちゃな」「そう、日本ではモーニング娘。ていうんだよ」というやり取りが少し面白かった。

λ. 2回目の夜勤明け

今日はお風呂に入って、寮の食堂で朝食。それから今日は分割睡眠を試してみる。 まず、午前中180分ほど寝て、それからプールと買い物に行き、午後にまた寝る。

12:30から40分ほどで今日も1km泳いだ。クロール50m・平泳ぎ50m・背泳ぎ50m・バタフライ25m・平泳ぎ25m のサイクルをまったりと繰り返しただけ。本当は全力で泳いだり、力を抜いて泳いだり、メリハリを付けたほうが良いのだろうな。

それから、ドアノブが取れてしまったので、直してもらった。

午後寝てたら、2時間くらいで悪夢で目を覚ます。 久しぶりに心底イヤな夢を見た。

λ. 多相レコード型に基づくRubyプログラムの型推論 by 松本宗太郎 and 南出靖彦

を読んだ。

λ. 「真理の度合理論は適切か？ 〜ファジイ論理と真理理論〜」 by 矢田部俊介

ytbさんに一度直接お会いしてみたくて、講演を聞きに行った。

• スライド
• ytbさんの日記でのの告知

本発表では、ファジイ論理の『真理値』の解釈の問題を題材に、真理に関する意味論的な見方と、公理論的な見方が対立する例を紹介する。

ファジイ論理は、『真理値』として[0,1]の実数をとる意味論によって定義され、その真理概念は伝統的に「真理の度合理論」によって説明されてきた。しかし、その『真理値』が何を意味しているかを巡っては、Suzko とDummett による議論以来、論争が続いている。発表者は、この問題に関し、搦め手からアプローチする。すなわち、「真理の度合い」を、ファジイ論理（の一例であるLukasiewicz無限値述語論理）上の公理的真理理論の枠組みでによって定式化し、形式化された度合い理論が（枠組みの真理理論がω-矛盾であることにより）成立しないことを示す。この結果は、公理的真理理論における真理概念は度合理論では説明できないことを示すものであり、[0,1]を真理値ととらえる意味論的な見方に否定的な結果であるといえる。