日々の流転

λ. 「トランプの和と積のパズル」と様相論理

どう書く？.org に「トランプの和と積のパズル」という問題があった。

プログラムを書いて答えを求めることは難しくないのだけど、この手の問題を見るたびに様相論理で一般的に扱えないのかなと思ってしまう。 思っただけでちゃんと考えたことがなかったので、少し考えてみようと思う。

知識論理

こういうのを扱う様相論理として知識論理(Epistemic logic)がある。 知識論理は様相論理の一種で、□φを「φであることを知っている」と解釈する。 そして、知識論理の □ は様相論理でいうところの S5 様相になっていることが仮定される。これはつまり、以下の形の論理式が成り立つということである(ただし、◇φ := ¬□¬φ)。

K(φ,ψ) := □(φ→ψ) → □φ → □ψ

φ→ψ であることを知っていて、更に φ であることを知っているなら、ψ であることも知っている。

T(φ) := □φ → φ

φであることを知っているのなら、φである。

5(φ) := ◇φ → □◇φ

「φでないことを知らない」のなら、そのことを知っている。

さらに、ここから以下のようなことも言える。

D(φ) := □φ→◇φ

φであることを知っているなら、φでないことは知らない。

B(φ) := φ→□◇φ

φならば、「φでないことを知らない」ということを知っている。

4(φ) := □φ→□□φ

φであることを知っているなら、そのことを知っている。

背景知識

Num := {1..13} として、原子論理式の集合 { N({m,n}), S(m+n), P(m×n) | m,n∈Num } が与えられているとする。それぞれの意図している意味は次の通りである。

N({m,n})

二枚のカードの数字がm,nである。

S(n)

二枚のカードの数字の和がnである。

P(n)

二枚のカードの数字の積がnである。

以下のような論理式の集合Φが成り立つことを仮定する。

• ∨{ N({m,n}) | m,n∈Num }
• { N({m,n})→¬N({m',n'}) | m,m',n,n'∈Num, {m,n}≠{m',n'} }
• { N({m,n}) → S(m+n) | m,n∈Num }
• { N({m,n}) → P(m×n) | m,n∈Num }
• { S(n)→¬S(m) | m,n∈Num, m≠n }
• { P(n)→¬P(m) | m,n∈Num, m≠n }

問題の記述

これでようやく問題が記述できる。

ここでは複数の人が登場するので「φであることをXさんが知っている」ということを [X]φ で表す(各 [X] はそれぞれS5様相だとする)。 そうすると、Xさんが数字を分かることは α(X) := ∨{ [X]N({m,n}) | m,n∈Num } で表すことが出来る。

• Aさんは積を知っているので ∨{ [A]P(m×n) | m,n∈Num }
• 同様に、Bさんは和を知っているので ∨{ [B]S(m+n) | m,n∈Num }
• Aさんは(この情報だけでは)数字が分からないので ¬α(A)
• Bさんも(この情報だけでは)数字が分からないので ¬α(B)
• BさんはAさんが「分かりません」というのは分かっていたので [B]¬α(A)

これを聞いたあとのAさんが知っているということは、元のAさんが知っているということとは別なので、[A1] という様相で扱うことにする。

• Aさんが元々知っていた事はすべて知っているので、[A]φ → [A1]φ
• 今聞いた情報を知っているので [A1](¬α(B) ∧ [B]¬α(A))
• それを聞いて答えがわかっているので α(A1)

同様に、これを聞いたあとのBさんが知っているということを [B1] という様相で扱うことにする。

• Bさんが元々知っていた事はすべて知っているので [B]φ → [B1]φ
• 「Aさんに話した内容をAさんが知っている」ことを知っているので、[B1][A1](¬α(B) ∧ [B]¬α(A))
• 今聞いた情報を知っているので [B1]α(A1)
• それを聞いて答えがわかっているので α(B1)

どうやって解くか

こうやって論理式で記述できたら、後は定理証明器やモデル検査で答えが求まらないものだろうか。 それはまた今度考える。

λ. Modal Algebras

昔、途中で挫折した First Steps in Modal Logic を再び読んでいるのだが、命題 3.4 の自然言語で書かれた証明に頭がこんがらがってきた。以前に読んだ時にはあっさり理解できたはずなのだが……。

これはどういう命題かというと、遷移関係が

1. 反射的(reflexive)
2. 推移的(transitive)
3. pathetic: a R b ⇒ a=b
4. 稠密(dense): a R b ⇒ ∃x. a R x R b

であることと、□X = {a | ∀x. a R x ⇒ x∈X} で定義される演算子 □ が

1. Deflationary: □X⊆X
2. Nearly inflationary: □X⊆□□X
3. Inflationary: X⊆□X
4. Nearly deflationary: □□X⊆□X

であることが、それぞれ同値だという命題。

それで、「頭がこんがらがるのは自然言語で証明が書かれているからだ」と思い、Agdaで書いてみた(ModalAlgebras.agda)　一応、頭はスッキリしたが、かえってややこしくなっている気もしないでもない。

追記

ちなみに、反射律を「a=b ⇒ aRb」と書くと、patheticであることと双対の関係にあることが分かる。 同様に、推移律を「(∃x. a R x R b) ⇒ a R b」と書くと、稠密性と双対の関係にあることが分かる。 考えてみれば当たり前だけど、最近まで気付いていなかった。

λ. うな重＠うな新

朝もウナギ食べたんだけど……コレステロールが不安だ。

λ. Lightweight Language Spirit

講演や発表それ自体も面白かったが、それ以上に色々な人とお会いすることが出来たのが楽しかった。 そういう意味では休憩時間が長めにとってたったのが非常に良かったと思う。

久しぶりにお会いしたsyd_sydさんの紹介で、OCaml-Nagoyaの小笠原啓さん、今井宜洋さんにお会いした。 浜地さんはRHG読書会で見かけたことはあったけど、マトモに話すのは初めて。 “Lambda the Ultimate” T-シャツ が目立っていた 日記を書く[・ _ゝ・]はやみずさん にもお会いした(Lambda the Ultimate の関係者かと思ったw)。 他にも色々な人にお会い出来た。 野中さんにも久しぶりにお会いしたかったけど、お会いできず残念。それから、sshiさんやTheoriaさんのような方にもお会いしたかったなぁ。

基調講演

和田先生の基調講演。 そういえば、生の和田先生を見るのは初めてだ。

「denotational semantics で書いてあるけど動く Scheme」がどういう意味なのかちょっと困惑したのだけど、多分「基本的な意味領域とその領域に対する基本的な操作をまず実装し、処理系全体を統語領域から意味領域への(帰納的に定義される)関数の形で記述した」というだけなのだと思う。 昼休みのときに「再帰はどうるんだろう?」みたいな話もあったけど、不動点をとる部分も基本的な操作として実装されているのだろう。

Language Update

弾さんの発表 で「Perl6はとりあえずポロロッカ星人のみなさんにまかせて」とあったが、元ネタがわからず悔しかった。ポロロッカといったら、これしか思い浮かばんかったよ。

正規表現のtrieを用いた最適化の話は「これまでやってなかったんかい」と思った。しかし、それにしても、Perlは相変わらずキモイなぁ(笑

Rubyは「ありゃ、いつのまにこんな計画になったんだっけ!?　これ今年中に全部やるなんて正気か?」と思ったら、案の定なオチ。笑った。

shinhさんの発表していたIoは、BNFが5行*1で「おぉー」と思った。 それから、引数があるときだけ実行が遅延されるとか、その邪悪さっぷりが素敵。

昼休み

久しぶりにお会いした上野さんに、SML#のことを色々と教えてもらっていた。 私はSML#のランク1多相について誤解していた。 それとデータ表現とインタオペラビリティの話。 あと、「重要なのはsyntaxではなくsemanticsと実装技術。でもそれだけじゃなかなか使ってもらえない」という話でハードウェア記述言語のBlueSpecを連想。 BlueSpecの文法は元々は拡張Haskellだった(参考: Bluespec -- Designer's Perspective)のをマーケティングの観点から拡張Verilogだか拡張SystemCだかに変えたが、SML#の文法はMLであり続けるのだろうか。

普通にお昼を食べていたら、次の「オレ様言語の作りかた」には遅刻してしまい、少し残念。

飲み会

何か良くわからない集まりだ(笑　ここでも色々な人にお会いできて楽しかった。

某氏が線形論理の入門に良い文献を探していたが、照井先生の「線形論理の誕生」等はどうだろうか。

λ. 様相論理のシーケント計算

First Steps in Modal Logic はずっとヒルベルト流の演繹体系で通してたので知らなかったが、論理と計算のしくみ(萩谷 昌己/西崎 真也) で様相論理にもシーケント計算での証明系があることを知る。やっぱりあるのね。これは通常の命題論理のシーケント計算に、以下の必然化の推論規則を追加したもの。

A1, …, An ├ B
─────────────── (必然化)
□A1, …, □An, Γ ├ Δ, □B

ちなみに、First Steps in Modal Logic でのヒルベルト流の必然化の推論規則は以下のようなものだったので、少し趣が異なっている*1。

φ
─── (Ni)
□φ

さらに、ワンのアルゴリズムを拡張した決定手続きも載っていた。いいね。

ただ、ここでは素の様相論理のシーケント計算だけしか載っていなくて、様々な公理を追加したときにどうするかというのが分からなかった。 T(φ) := □φ→φ の形の論理式を公理として追加した場合には簡単で、以下のような推論規則を追加すればよいのだと思う。

Γ, □φ, φ ├ Δ
──────────
Γ, □φ ├ Δ

しかし、4(φ) := □φ→□□φ のような形の論理式や、より一般的な (i,j,k,l)-confluence <i>[j]φ→[k]<l>φ の場合には、どのように追加すれば良いかは良くわからなかった。例えば、4に対応する推論規則として以下を追加すると、前述の決定手続きがうまく働かなくなりそう……*2

Γ ├ Δ, □□φ, □φ
────────────
Γ ├ Δ, □□φ

私はシーケント計算とか良く知らないのだけど、シーケント計算に詳しい人にはこういうのもすぐわかったりするのだろうか。あと、様相論理の証明系の話とかは頭腐の宮本賢治さんが詳しそうだなぁ……

8/7 追記

線形論理の ! がS4様相だという話を思い出した。 4に関しては ! の規則と同様に以下のような推論規則にすれば良いはず。

□Γ ├ φ
──────
□Γ ├ □φ

ただ、5(φ) := ◇φ → □◇φ に関してはこんな風にはいかなそう。 Deep Inference and the Calculus of Structures - Modal Logic にある“The Design of Modal Proof Theories: The Case of S5”を見ると、カット除去が成り立つような S5 の推論規則にはやはり deep inference が必要なようだ。

λ. 文字列検索の性能

こないだの ICFP Programming Contest 2007 の時に以下のような文字列検索関数を書いた(実際にはリストではなくData.Sequenceが対象だったけど)。 書いたときは「文字列上を逆に戻ることが無いから、少しは速そう」とか思っていたんだけど、そもそも比較回数は全然減っていないので全然速くない。アホだ、私。

findSubstring :: Eq a => [a] -> [a] -> Maybe Int
findSubstring [] = const (Just 0)
findSubstring pat = f [] 0
  where
    f ([]:_) n _ = Just $ n - length pat
    f s n xs =
        case xs of
          (x:xs') -> f [s' | (c:s') <- (s++[pat]), x==c] (n+1) xs'
          [] -> Nothing

毎日HaskellのKMP法検索(2006-05-03)とBM法検索(2006-06-16)と比較してみる。

Prelude Test> findSubstring (replicate 1000 'a' ++ ['b']) (replicate 10000 'a')
Nothing
(2.54 secs, 253290572 bytes)
Prelude Test> kmp_search (replicate 1000 'a' ++ ['b']) (replicate 10000 'a')
False
(0.03 secs, 525604 bytes)
Prelude Test> bm_search (replicate 1000 'a' ++ ['b']) (replicate 10000 'a')
False
(0.21 secs, 2622592 bytes)

この程度の短い文字列でも最悪ケースだと全然性能が違うんだな。

λ. Djinn, a theorem prover in Haskell, for Haskell.

今更ながら Djinn を試してみた。 Djinnは「型を入力として受け取り、その型を持つ関数を(もし存在すれば)返す」ようなプログラム。これはカリーハワード対応によって「論理式を受け取って、その証明を(もし存在すれば)返す」ことに対応するので、仕組みは定理証明機で、証明をHaskellプログラムとして書いてくれている考えることもできる。

まずは自明な例を試してみる。

Djinn> id ? a -> a
id :: a -> a
id a = a
Djinn> k ? a -> b -> a
k :: a -> b -> a
k a _ = a
Djinn> s ? (a -> b -> c) -> (a -> b) -> (a -> c)
s :: (a -> b -> c) -> (a -> b) -> a -> c
s a b c = a c (b c)
Djinn> bindMaybe ? Maybe a -> (a -> Maybe b) -> Maybe b
bindMaybe :: Maybe a -> (a -> Maybe b) -> Maybe b
bindMaybe a b =
            case a of
            Nothing -> Nothing
            Just c -> b c

当然動作する。 これが出来るのは当たり前なのだけど、実際に見ると楽しいな。 それと、bindMaybeで定数関数じゃない方の関数が先に出て来るようになっているのはちょっと賢いかも。

再帰的データ型を試そうとしたが、これは対応していないようだ。

Djinn> data List a = Nil | Cons a (List a)
Error: Recursive types are not allowed: List

ついでに少し意地悪な例を試してみる(20060429#p02 より)。

Djinn> dn :: Not (Not a) -> a
Djinn> em ? Either a (Not a)
-- em cannot be realized.

起動時のメッセージには「If the Djinn says the type is not realizable it is because there is no (total) expression of the given type.」と出てくるが、実際には完全ではない?

どんな決定手続きを使っているのか気になるところ。 LtUにはこう書いてある。

For the curious, Djinn uses a decision procedure for intuitionistic propositional calculus due to Roy Dyckhoff. It's a variation of Gentzen's LJ system. This means that (in theory) Djinn will always find a function if one exists, and if one doesn't exist Djinn will terminate telling you so.

また、ljt.p というPrologのコードがついていて、こっちには「Incorporates the Vorobëv-Hudelmaier etc calculus (I call it LJT). See RD's paper in JSL 1992: "Contraction-free calculi for intuitionistic logic"」と書いてあった。 LJTについては、<URL:http://www.computational-logic.org/iccl/events/WPT-2004/> にある“Normalising Permutations in Sequent Calculus”の概要に以下のように書いてあったので、自然演繹とうまく対応するシーケント計算ということのようだ。

In Prawitz's translation from the sequent calculus LJ to natural deduction, many proofs are mapped to the same one and only differ by the order in which inference rules are applied. One can be transformed into another by simple permutations of these rules. By the use of focusing conditions, a canonical proof can be elected in each permutation class, thus forming Herbelin's permutation-free calculus LJT, which is in bijection with proofs in natural deduction.

そういえば、自然演繹とシーケント計算の対応の問題については、去年のSLACSの A subsystem of sequent calculus isomorphic to natural deduction でも取り上げられていたな。私はあまり理解できていなかったけど。

関連

• Advanced Topics in Programming Languages Series: Parametric Polymorphism by Phil Gossett - ヒビルテ (2007-04-28)

【2011-07-27 追記】

スタートHaskellの @pi8027 さんのLT「型から項を作る」で思い出して、再度試してみる。 Djinnのバージョンはリリースされたばかりの2011.7.23。

上で上手くいかなかった例は、型を具体化してみたら、うまくいった。

Welcome to Djinn version 2011-07-23.
Type :h to get help.
Djinn> dn :: Not (Not (Either a (Not a))) -> Either a (Not a)
Djinn> em ? Either a (Not a)
em :: Either a (Not a)
em =
     case dn (\ a -> void (a (Right (\ b -> a (Left b))))) of
     Left c -> Left c
     Right d -> Right d

ただし、型変数名が違うとダメ。

Djinn> :clear
Djinn> dn :: Not (Not (Either b (Not b))) -> Either b (Not b)
Djinn> em ? Either a (Not a)
-- em cannot be realized.

要は多相型には対応していないということね。 そりゃそうかと納得した。

λ. slideshare

slideshare というサービスを池上さんのところで知ったので、LLRingの発表資料などをアップロード(My Slidespace)して、日記にも貼り付けてみた。 例えばこんな感じになる。

おぎろぐはてな - Powerpointの資料をキレイにSlideShareにアップする で紹介されているように、フォントを埋め込んだPDFを作ってアップロードすると良いようだ。

【2007-09-30追記】 YouTubeに対するFlowPlayerのように、スタンドアローン(?)で使えるプレーヤーもあると良いのにな。と思ったが、OpenOffice.org Impress はswfを出力できたはずだから、それを使えばよいのか。

λ. “Topoi: The Categorial Analysis of Logic” by Robert Goldblatt

たけをさんのところでも書いたが、この本の古い版を The Cornell Library Historical Mathematics Monographs - Topoi, the categorial analysis of logic で読むことが出来る。

それで、ローカルでも読みたかったので、とりあえず各ページのPDFを全部落してきて、pdfpdfpdf.com (pdfc)で連結してみた。 15MバイトくらいのPDFが出来た。

λ. H↔Provable([H]) な H の真偽

不動点定理によって、任意の一変数論理式P(X)に対して、ある論理式Qが存在して ⊢ Q↔P([Q]) が成り立つ。ゲーデル文Gはそうして作った ⊢ G↔¬Provable([G]) を満たす論理式だった。ゲーデル文は直観的には「この文は証明できない」と解釈でき、この意味から(標準モデルで)真であることがわかる。

では、同様に不動点定理を使って作った ⊢ H↔Provable([H]) を満たす論理式 H の真偽はどうなっているだろうか?　直観的には「この文は証明出来る」という解釈できるのだが、別にそこから真偽が決まるわけでもなく……

最近知って、ちょっと面白かった話(答えは知ってます→20070916#p01)。

λ. length (filter p xs) ≦ length xs の証明

syd_sydさんの「Coqでクイックソート (未完)」を見て、length (filter p xs) ≦ length xs をAgdaで証明してみた(Filter.agda)。 ここから以下の2つを示すことが出来、クイックソートでの再帰呼び出しで引数が小さくなっていることを示すことが出来る。

• length (filter (\y -> y < x) xs) ≦ length xs < length (x:xs)
• length (filter (\y -> x <= y) xs) ≦ length xs < length (x:xs)

λ. 大堀流のランク1多相についての勘違い

Lightweight Languge Spirit のときに、疑問と誤解が解けた話。

私は value restriction や値多相(value polymorphism)*1をよく知らなかったことから、大堀流のランク1多相の目的は、直積や直和の成分を多相型に出来ること自体だと思い込んでいた。 そして、Haskell(GHC)の場合、その際に問題になったのは型変数、特に (,) :: ∀a b. a -> b -> (a, b) のようなコンストラクタの型に現れる型変数を多相型でインスタンス化することを許すかどうか、つまり非可述的多相(impredicative polymorphism)の問題だった(GHC and impredicativity)。それなのに、MLでは何故ランクの話になるのだろう???　……と疑問に思っていたのだった。

実際には、コンストラクタは普通の関数とは別扱いで、コンストラクタの型に現れる型変数を多相型でインスタンス化しているわけではないそうだ。考えてみれば、上記のようなコンストラクタの型変数を多相型でインスタンス化するとランク2の型になってしまうしな。

で、何故コンストラクタが普通の関数と別扱いになっているかというと、もともと値多相では式にexpansiveな式とnon-expansiveな式という区別があり、non-expansiveな式のみが多相型を持てるようになっているため。 一般の関数適用はexpansiveな式だけど、コンストラクタの適用は引数がnon-expansiveならばnon-expansiveになるので、区別されていた。 そして、大堀流のランク1多相は、直積や直和の成分を多相的にすることが直接の目的ではなく、値多相による制限を緩和することが目的なので、それに応じた設計になっていると。

λ. 床屋

に行ってきた。

λ. ¬(∀x.P(x)) → ∃x.¬P(x)

非常にしょーもないのだが、ふと ¬(∀x.P(x)) → ∃x.¬P(x) の証明を自然演繹で書こうとして苦戦。こんな基本的な事で苦戦するなんて色々やばいな。 結局、callccを使ったプログラムを思い浮かべて証明した。 古典論理はやっぱり変態的だと思った。

Agdaでの証明

postulate callCC (|X::Set) :: Not (Not X) -> X

prop (!D::Set) (!P::D->Set)
    :: Not ((x::D) -> P x) -> Exist (\(x::D)-> Not (P x))
prop k1 =
    callCC (\(k2::Not (Exist (\(x::D) -> Not (P x)))) ->
        let f :: (x::D) -> P x
            f x = callCC (\(k3::Not (P x)) ->
                      let e :: Exist (\(x::D) -> Not (P x))
                          e = struct
                                fst :: D
                                fst = x
                                snd :: Not (P x)
                                snd = k3
                      in k2 e)
        in k1 f)

自然演繹での証明

Agdaによる証明をそのまま翻訳したもの。

[¬P(x)]:3
───── (∃I)
∃x.¬P(x)    [¬∃x.¬P(x)]:2
─────────────── (¬E)
⊥
───── (¬I{3})
¬¬P(x)
───── (¬¬)
P(x)
───── (∀I)
∀x. P(x)       [¬∀x.P(x)]:1
─────────────── (¬E)
⊥
─────── (¬I{2})
¬¬∃x.¬P(x)
─────── (¬¬)
∃x.¬P(x)
─────────────── (→I{1})
¬∀x.P(x) → ∃x.¬P(x)

シーケント計算での証明

自然演繹だとややこしかったけど、シーケント計算だと実は簡単。

P(a) ├ P(a)
──────── (├ ¬)
├ P(a), ¬P(a)
──────── (├ ∃)
├ P(a), ∃x.¬P(x)
────────── (├ ∀)
├ ∀x.P(x), ∃x.¬P(x)
──────────── (¬ ├)
¬∀x.P(x) ├ ∃x.¬P(x)
─────────────── (├ →)
├ ¬∀x.P(x) → ∃x.¬P(x)

λ. 第三十二回圏論勉強会

今日は圏論勉強会だった。

λ. 『ηなのに夢のよう』 森博嗣

Gシリーズはやっぱり西之園萌絵の成長がテーマだったのだなと思った。 綺麗な終わり方。 肝心のところは引っ張っるだけ引っ張ってそのままだけど。

λ. OSConでのSimon Peyton Jonesの講演

<URL:http://d.hatena.ne.jp/desumasu/20070811/1186838102> よりメモ。 長いので、ちょっとだけ見た。

• スライド
• OSCON 2007 - Simon Peyton-Jones - A Taste of Haskell Part I
• OSCON 2007 - Simon Peyton-Jones - A Taste of Haskell Part II

λ. パースの論理式

パースの論理式(Peirce's formula)*1「((P→Q)→P)→P」というのを直観主義論理に加えると古典論理になるそうだ。 なので、二重否定の除去と同値になることを、簡単な haskell プログラムを書いて確かめてみた*2。

type Absurd = forall a. a
type Not a = a -> Absurd

prop1 :: forall a b. (forall a. Not (Not a) -> a) -> (((a->b)->a)->a)
prop1 callCC f = callCC (\(k :: Not a)-> k (f (k :: a->b)))

prop2 :: forall a. (forall a b. ((a->b)->a)->a) -> (Not (Not a) -> a)
prop2 p k1 = p (k1 :: Not a -> a)

λ. オーシャンズ13

を観てきた。

λ. 利付国庫債券(5年) 第65回

前々から、現金や株だけでなく債権にも投資しようと思っていたので、何となく 利付国庫債券(5年) 第65回 の購入申し込みをしてみた。 もっとも、利上げもありそうだし、とりあえず10万円だけだけど。

λ. 『もやしもん』3巻&4巻 by 石川 雅之

哀れUFO研。

λ. Maude

Maude is a high-performance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications. Maude has been influenced in important ways by the OBJ3 language, which can be regarded as an equational logic sublanguage. Besides supporting equational specification and programming, Maude also supports rewriting logic computation.

henjin1goさんお気に入りのMaudeに手を出してみる。 コンパイルは若干面倒くさいのだが、The MOMENT ProjectがWindows版のバイナリを配布していたので、これを使う。

λ. チャーチ・ロッサーの定理の証明に挫折

ここ数日Agdaでチャーチ・ロッサーの定理を証明することに熱中していたのだけど、なんか上手くいかずに詰まっていた。チャーチロッサーの定理の証明の流れの本質的な部分はすぐに書けていたのだけど、細かい部分で色々とひっかかったり嵌ったりとか。

特に任意のラムダ式 M1[x,y], M2[y], M3 に対して M1[x:=M2[y]][y:=M3] = M1[y:=M3][x:=M2[y:=M3]] が成り立つことの証明。構造帰納法で示せば良いのだけど、実際にAgdaで証明を書こうとするとラムダ抽象の場合が面倒過ぎで……。 その後、ラムダ式のデータ型「data Term a = Var a | App (Term a) (Term a) | Lam (Term (Maybe a))」*1がモナドになっている事を証明出来れば良く、直接証明するよりもその方が筋が良さそうという事に気付いたのだけど、「(m >>= f) >>= g = m >>= (\x -> f x >>= g)」の証明のラムダ抽象の場合がやっぱり面倒過ぎで……

結局、まだその部分の証明は書けていないけど、燃え尽きたので中断。

λ. 『謎の彼女X (2)』 植芝 理一

いつの間にか二巻が出ていた。

λ. IPA未踏ソフトウェア創造事業2006年度下期千葉PM採択プロジェクト最終成果報告会

未踏千葉PM採択の4案件について、事業の最終成果報告を行う。形式はスクール形式の会場において、プレゼンテーションおよび質疑応答とする。4案件は、「SELinuxによるPostgreSQLのアクセス制御強化」、「Ruby用仮想マシンYARVの完成度向上」、「ウェアラブルコンピューティングのためのイベント駆動型ミドルウェア開発」、「Web上で動作するモデリング環境 Kodougu の開発」である。

今回4案件の報告それぞれについて関連深い分野より著名ゲストを招き、入門者にも深く配慮したチュートリアル等の実践的セッションを行っていただくこととした。千葉PM登壇のパネルディスカッションと併せ、現在最新の技術潮流を解説していく。

<URL:http://www.atdot.net/~ko1/diary/200708.html#d22> より。 おお、面白そう。 会社休んで行こうかしら。 ……と思ってたら、(仕事上の)予定が入ってしまった。残念。

あと、笹田さんの写真がカッコイイ。

λ. チャーチ・ロッサーの定理の証明

先日は「燃え尽きたので中断する」と書いたが、どうにも気になって頭から離れずモヤモヤしていたら、今日の飲み会中にアイディアを思いついて、結局証明できた。 まだ整理できていない部分が多いが、こんな感じになっている。

• Prelude.agda
• Confluence.agda
• Term.agda
• ChurchRosser.agda

【2007-09-09追記】 Frank Pfenning が A Proof of the Church-Rosser Theorem and its Representation in a Logical Framework で LF (の実装のElf)で証明を表現している。後で比較する?

λ. 同期飲み会

λ. 旅行 一日目

天竜船下り。 「てんりゅう」と言えば某tenryuとその元ネタである天龍寺を連想するのだけど、別に関係は無いのか。 水が少なく迫力はあまり無かった。

妻籠宿。 こういう古い町並みはいいなぁ。

下呂温泉に宿泊。

λ. 旅行 二日目

高山陣屋。

白川郷。「そういえばひぐらしの雛見沢のモデルだっけ」と思い、舞台となった場所を少し探してみたが、あまり見つからず。一応、朝にみょふ〜会の雛見沢村聖地巡礼・小野さん捜索編を簡単に見てはいたのだけど、オチに地図が載っているのを見落としてた……残念。

おみやげ「かわいいさるぼぼ伝説」

λ. Do you know that the S combinator is injective?

たまたま見たShin-Cheng Mu氏のページに「Do you know that the S combinator is injective?」と書いてあった。 「へー、そうなのか」と思い暗算で確認してみたが、どうせなのでagdaでも示してみる。

s (A,B,C::Set) :: (A->B->C) -> (A->B) -> (A->C)
s f g a =  f a (g a)

z (A,B,C::Set) :: ((A->B) -> (A->C)) -> (A->B->C)
z h a b = h (\(x::A) -> b) a

prop (A,B,C::Set) (!f::A->B->C) :: Id (z (s f)) f
prop = refId f

どうでも良いが、zの型は一種の functional completeness っぽい感じ?

λ. ビジネス実務マナー技能検定試験2級

合格していた。

λ. Paradoxes of classical predicate calculus

The Coq Proof Assistant - A Tutorial の「Paradoxes of classical predicate calculus」のところが面白い。古典一階述語論理だと Smullyan's drinkers' paradox 「In any non-empty bar, there is a person such that if she drinks, then everyone drinks」が証明できてしまうそうだ。 へぇ。

例によってagdaで示してみる。

drinker (!D::Set) (!d::D)
        (!EM::(X::Set) -> Either X (Not X))
        (!P::D->Set)
    :: Exist (\(x::D)-> P x -> (y::D) -> P y)
drinker =
    case EM (Exist (\(x::D) -> Not (P x))) of
      (Left e  )->
          struct
            fst :: D
            fst = e.fst
            snd :: P fst -> (y::D) -> P y
            snd = \(px::P fst) -> case e.snd px of { }
      (Right ne)->
          let f (!x::D) :: P x
              f = case EM (P x) of
                    (Left px  )-> px
                    (Right npx)->
                        let e :: Exist (\(x::D) -> Not (P x))
                            e  = struct
                                   fst :: D
                                   fst = x
                                   snd :: Not (P fst)
                                   snd = npx
                        in case ne e of { }
          in struct
               fst :: D
               fst = d
               snd :: P fst -> (y::D) -> P y
               snd = \(z::P d) -> f

ところで、zyxwvさんが謎と思っているのはどの部分なんだろう?　一階述語論理の推論規則の話だろうか?

一階述語論理の推論規則には 「∀x.P[x] から P[t] を導く規則」や「P[t] から ∃x.P[x] を導く規則」が含まれている(ヒルベルト流でも自然演繹でもシーケント計算でも)。 ここでビミョーなのが一階述語論理では勝手に自由変数を置いて使える点。 そのため、一階述語論理では勝手に置いた自由変数tについて (∀x.P[x]) → P[t] が証明出来る。同様に P[t] → (∃x.P[x]) も証明できるため、それらから (∀x.P[x]) → (∃x.P[x]) も証明出来る。 しかし、論理式の意味を考えると、∀x.P[x] は領域が空なら真である一方で、∃x.P[x] は領域が空なら偽だし、さらに P[t] は領域が空なら解釈不能になってしまう。 これらの矛盾を避けるため、一階述語論理のモデル論では領域Dは空集合でないこと前提とされている。

一方、Coq等の基づいている型理論では自由変数を勝手に置いたり出来無いため、これらを一階述語論理の場合と同様に証明する証明することは出来ないし、またDが空集合である場合も許される。 そのため、ここでは一階述語論理を模すため、Dの要素dの存在を明示的に仮定している。

(追記: 「定数記号」と書いていた部分を「自由変数」に変更した)

λ. 『すもももももも - 地上最強のヨメ (8)』 大高 忍

読んだ。

λ. W-typesによる帰納的データ型の表現

まずは W-types の定義と除去規則を示す。

data W (A::Set) (B::A->Set) = sup (a::A) (x::B a->W A B)

elimW (|A::Set) (|B::A->Set)
      (!C::W A B -> Set) 
      (!d::(a::A) -> (f::B a -> W A B) ->
           (g::(b::B a) -> C (f b)) -> C (sup a f))
      (!c::W A B)
      :: C c
elimW = case c of (sup a f)-> d a f (\(b::B a)-> elimW C d (f b))

W-types という名前は Wellorderings から来ていて、順序数(っぽい何か)を整礎な木として構成したものになっている。Martin-Löf の Intuitionistic Type Theory での説明:

The concept of wellordering and the principle of transfinite induction were first introduced by Cantor. Once they had been formulated in ZF, however, they lost their original computational content. We can construct ordinals intuitionistically as wellfounded trees, which means they are no longer totally ordered.

この型それ自体も面白いのだけど、この型を使った面白い事として外延的な型理論ではこれを使って帰納的なデータ型を表現する事が出来るという事が知られている。なので、これをagdaでも表現してみたい。 だが、agdaの型理論は外延的ではないので、まずは「関数は全ての引数に対する値が等しければ等しい」ことを公準として追加する。 ついでに後で使う定義も追加。

postulate ext :: (X,Y::Set) |-> (f,g::X->Y) ->
                 ((x::X) -> Id (f x) (g x)) -> Id f g

data Empty =
data Unit = tt

uu (X::Set) :: Empty -> X
uu e = case e of { }

uu_lemma (X::Set) (!f::Empty -> X) :: Id uu f
uu_lemma = let eid (!e::Empty) :: Id (uu e) (f e)
               eid = case e of { }
           in ext uu f eid

tt_lemma (X::Set) (!f::Unit -> X) :: Id (\(t::Unit)-> f tt) f
tt_lemma = let eid (!t::Unit) :: Id (f tt) (f t)
               eid = case t of (tt)-> refId (f tt)
           in ext (\(t::Unit) -> f tt) f eid

リストの例

例えばリスト型は以下のように表現する事が出来る。

data Maybe (X::Set) = Nothing | Just (x::X)

L (A::Set) :: Maybe A -> Set
L x = case x of
        (Nothing)-> Empty
        (Just a )-> Unit

List' :: Set -> Set
List' A = W (Maybe A) L

Nil' (A::Set) :: List' A
Nil' = sup Nothing uu

Cons' (A::Set) :: A -> List' A -> List' A
Cons' x xs = sup (Just x) (\(t::Unit) -> xs)

elimList' (X::Set)
          (!C::List' X -> Set)
          (!n::C Nil')
          (!c::(x::X) -> (xs::List' X) -> C xs -> C (Cons' x xs))
          (!xs::List' X)
  :: C xs
elimList' =
    let h :: (a::Maybe X) ->
             (f::L a -> W (Maybe X) L) ->
             (g::(b::L a) -> C (f b)) ->
             C (sup a f)
        h a f g =
            case a of
              (Nothing)->
                  substId (\(f'::Empty -> W (Maybe X) L) ->
                           C (sup Nothing f'))
                          (uu_lemma f) n
              (Just x )->
                  let lem :: C (Cons' x (f tt))
                      lem = c x (f tt) (g tt)
                  in substId (\(f'::(t::Unit) -> W (Maybe X) L) ->
                              C (sup (Just x) f'))
                             (tt_lemma f) lem
    in elimW C h xs

ちなみに、substId が必要になっているのは、agdaでは Unit や Empty→X の要素が自動的に同一視される(それらの間に definitional equality が成り立つ)ことはないため。外延的な型理論の中にはこれらが自動的に同一視されるものもある。

コンテナ

コンテナ(Container)の概念を使った場合について後で書く。

参考

• “Representing inductively defined sets by wellorderings in Martin-Löf's type theory” by Peter Dybjer
• “Representing Nested Inductive Types using W-types” by Michael Abbott, Thorsten Altenkirch, and Neil Ghani

λ. ATM = automatic teller machine

ATM は automatic teller machine の略なのか。 これまで automatic transaction machine の略だと思い込んでいた。

λ. NPR (National Public Radio)

英語の学習に NPR (National Public Radio) が良いという話を聞いた。「Podcastはあるかな?」と思って見てみたら、500以上もあって、どれを聞いたら良いか迷って困る……

【2007-10-28追記】 最近は以下の二つを少し聴いている。

• WNYC's Soundcheck
• NPR: Story of the Day