日々の流転

λ. STモナドとSTRefをHaskell上で実装する

[FAQ]Haskellには副作用があるのか、ないのか の話。 kazu-yamamotoさんはSTモナドを、「処理系の力を借りないといけないモナド」で、副作用や参照透明性の観点からはStateモナドと本質的に違うものだと主張している。 だけど、STモナドが処理系に組み込まれている理由は効率のためであって、意味的にはStateモナドと大差ないし、効率とあと細かい点を気にしなければHaskellレベルでも実装できるはず。 というわけで書いてみたのが以下のコード。

{-# LANGUAGE Rank2Types, ExistentialQuantification #-}
import Control.Monad.State
import qualified Data.IntMap as IntMap
import Unsafe.Coerce

type ST s a = State (IntMap.IntMap U) a
data U = forall a. U a
newtype STRef s a = STRef Int

runST :: (forall s. ST s a) -> a
runST m = evalState m IntMap.empty

newSTRef :: a -> ST s (STRef s a)
newSTRef x = do
  h <- get
  let key = IntMap.size h
  put (IntMap.insert key (U x) h)
  return (STRef key)

readSTRef :: STRef s a -> ST s a
readSTRef (STRef key) = do
  h <- get
  case h IntMap.! key of
    U x -> return (unsafeCoerce x)

writeSTRef :: STRef s a -> a -> ST s ()
writeSTRef (STRef key) x = modify (IntMap.insert key (U x))

あくまで proof of concept なので、コードを単純にするためにIntが溢れることとかは無視している。 それから、細かい点と書いたのは反則技である unsafeCoerce を使ってしまっているところ。ここでは等しい型と分かっている型の間でしか変換しないので、安全ではあるんだけれどね。

関連

• 関数型プログラマにとっての副作用
• Referential transparency, definiteness and unfoldability

λ. Whyでバブルソートの正当性を示す

計算機言語で定理証明 (Proof Party.JP)のときには、Jahobというツールを使って色々やってみたが、最近Whyという似たツールを知ったので、こっちでも同じようなことをやってみる。 まずは、Jahobでも試したバブルソートの例*1。

BubbleSort.java

これを gwhy BubbleSort.java としてgwhyを起動すると、Proof Obligation が抽出されて一覧されるので、あとはメニューから「Proof」「Prove all obligations」とかを選べば定理証明器などが走って証明をしてくれる。 定理照明器としては、Alt-Ergoしかインストールしていなかったけれど、この例ではあっさり全 Proof Obligation が証明された。

以下が結果の画面。 gwhyのこのインターフェースはテストツールに似せてあるのだろうけど、良いなぁ。

参考

• Whyツールの習得について - Formal Methods Forum | Google グループ
• Whyインストールメモ - kencobaの日記

【2010-06-24追記】

マニュアルを一応読んで、異なる要素が保存されている事を追加してみた。 同じ要素の数が変化するかどうかは書けていない。 今度は Alto-Ergo では証明に失敗するのがあったので、CVC3も使ってみたら、片方ですべてを証明するのは無理だったけど、どちらかでは全部証明できた。

• BubbleSort2.java

【2010-07-20追記】

要素の個数の保存についても書いてみたが、これは証明がタイムアウトしてしまい、うまくいっていない。

• BubbleSort3.java

λ. The ICFP Programming Contest 2010

今年もThe ICFP Programming Contest 2010 に参加していた。期間は日本時間の 6/18(金) 21:00 から 6:21(月) 21:00 までの72時間。 チーム名はいつもの Team Sampou というチーム名で、メンバーもいつものようなメンバー。

やっていたことを簡単に時系列にまとめておく。

6/18(金) 夜

とりあえず、問題は読んだものの、サーバーが重く、ログインしようとしても Internal Error とか言われるので、ログインは諦める。 Ternary Streams を考えるのはまだ無理そうなので、回路記述の構文について考える。

最初は、以下のサンプルで、最初と

• 最後以外の各行がノードで、
• 同じ「数字(L|R)」の箇所同士がワイヤーで結ばれていて、
• 両側の端点がともにXになっている、X18L0#X7Lが外界を表す「external gate」

なのかと思った。 だけど、それだとLとR、そして最初と最後の「19L」の意味がわからない。

19L:
12R13R0#1R12R,
14R0L0#4R9L,
9R10R0#3L8L,
2L17R0#5L9R,
15R1L0#10R13R,
3L18R0#6L15L,
5L11R0#13L12L,
19R16R0#11R8R,
2R7R0#11L10L,
1R3R0#18L2L,
8R4L0#16L2R,
8L7L0#15R6R,
6R0R0#14L0L,
6L4R0#14R0R,
12L13L0#17L1L,
5R11L0#16R4L,
10L15L0#17R7R,
14L16L0#18R3R,
9L17L0#19R5R,
X18L0#X7L:
19L

ログインできるようになったので、自分で色々書いて食わせてみるも、inconsistent input connection ではねられてしまうので、諦めて寝る。

6/19(土)

午前中は歯医者に行くなどする。 そういえば去年もICFPC中に歯医者に行ったなぁ。

0#の部分がゲートの種類を表しているのではないかと思い、その部分を変更してみるも、unknown kind of node というエラーに。このエラーメッセージからするとノードの種類は色々あるのか? と疑うも成果なし。

池上さんが以下の記述で inconsistent input connection でエラーにならず、this is an illegal prefix でエラーになるのを発見するも、結局構文は分からず。

0L:
X0R0#X0R:
0L

午後は某所でオフラインミーティング。 問題を説明して議論しているうちに、nobsunが回路の記述の正しいフォーマットに気づく。0#の左側の「数字(L|R)」は入力が何行目のノードのどちらの出力からきたかで、右側の「数字(L|R)」は出力が何行目のノードのどちらの入力に繋がっているかを表しているのね。そして、0#の左側のXは環境からの入力を表し、右側のXは環境への出力を表すと。 Task Description では外界がひとつのゲートとして抽象化されている的なことが書いてあったのに……しくしく。

それに基づいてinconsistent input connection でエラーにならず、this is an illegal prefix でエラーになる幾つかの小さな例を作る。

そして、上の写真中の4つの回路(1),(2),(3),(4)をサーバーに食わせたときの出力列をもとに、

1. 逆方向のワイヤの初期値
2. ゲートの関数
3. サーバで回路に与えている入力

の3つを同時に求めることに。 これは色々試行錯誤したが、最終的には制約をAlloyに突っ込んだ(solve-op.als)ら、すべてを一意に決定してくれた。これだけで一意に決まる自信はなかったので、ちょっと驚いた*1。

というわけで、逆方向のワイヤの初期値は 0 で、ゲートの関数は以下のような関数。サーバでの入力は 01202101210201202 。

op|  0     1     2
--+-----------------
0 |(0,2) (2,2) (1,2)
1 |(1,2) (0,0) (2,1)
2 |(2,2) (1,1) (0,0)

ゲートの関数がわかったので、Task Description の回路をオートマトンArrowで実装し、サーバで与えている入力を与える。これをサーバの出力と比較することで、遅延が発生するワイヤは、下に書いてあるノードから上に書いてあるノードへとつながるワイヤであって、その逆ではないことを得た。そんでもって、そのオートマトンArrowで実装した回路に Task Description で指定された入力を与える事でキーをゲット。

キーをゲットしたは良いものの、ゲートの関数が意味不明すぎて、これでどうやってキーを出力する回路を組んだら良いかさっぱりわからず。 多分、これを組み合わせて色々なプリミティブを実装するんだろうなぁ、と思いつつ、みんなでご飯を食べにいき解散。

ここまでの成果: Circuit.hs

帰りの電車の中でも色々試してみるが、心持ち電車が空いているなぁ、と思ったら、ワールドカップの日本戦か。

長い一日だった。

6/20 (日)

Alloyを使ったプリミティブの合成の試みと、ゲートの性質を考える事を、並行して行う。

Alloyを使った試みでは、入力を複数回使うことを許して組み合わせ回路を合成すると、色々できるけれど、入力を複数回使う事を許さないと何も面白いものは作れないということに気づき、挫折。 そこで、まずは入力を複製する回路を合成する事を考えるけれど、これも小規模な組み合わせ回路の範囲では存在せず、やっぱり挫折。

やっぱり順序回路を考えないとダメかぁ、などと思いつつ、ゲートの関数opの性質を考えていて、第一出力に着目すると、fst (op (x,y)) = (x-y) `mod` 3 になっていることに気づく。 さらに、少し遅れて、第二出力に着目すると、snd (op (x,y)) = (x*y+2) `mod` 3 だということに気づく。

この時点で既に夕方 orz

ゲートの関数がこういう風に表せるということが分かるとだいぶ考えやすくなって、特定の値を特定の値へと変換するだけの簡単な順序回路を幾つか作ってみる。 ただし、入力を複製したり、出力を捨てて定数にしたりといった回路は作れなかった。 というあたりで量子計算を量子回路で書いているのを連想したりする。

……とかグダグダ考えているうちに、出力したいデータを s = s1 s2 ... sn とすると、

というような回路を考えて、

• s1 = f1(0)
• s2 = f1(f2(0))
• …
• sn = f1(…fn(0)…)

を満たすように、f1,…,fnを決めれば良いと言うことに気づく。 例えば、fiとして状態を持たず入力をインクリメントする回路を適当な回数繰り返すようなものを使うことにすれば、絶対に作れる。

で、入力をインクリメントするような回路を作ったと思って、それを使ってオートマトンArrowを使って回路を構成してみたんだけど、実際に動かしてみると答えが合わない。 調べてみると、状態を持たずに入力をインクリメントする回路を作れてなくて、状態を持って変な動作をする回路になってしまっていた。 しょうがないのでで手で無理やり辻褄をあわせて、キーを出力する回路を作れた。

オートマトンArrowを使って書いたのを、手で回路記述言語に落とすのはやる気が起こらなかったので、ここまでを一般化・自動化して、任意の3進列を回路へエンコードするプログラムが書いた。

• GenCircuit.als
• CircuitEncoder.als

ここで、さあサーバーにsubmitするぞと思ったら、サーバーさんがお亡くなりに……orz

しばらくしたら、投稿出来て…… やたっ! 通った!!

You have submitted fuel for car 219 with size 54. A special comment for you:
circuit output starts with
   11021210112101221
this is a legal prefix
Congratulations.
You have submitted a circuit that produces the key prefix.

というところでこの日は終了。

6/21(月)

車と燃料のデータがどう3進列にエンコードされているのかを調べる。 これは一人で作業していて、かなりめげそうになった。

車の方のエンコーディングは複雑そうなのに対して、燃料の方はタンクの数だけ非負係数の行列が並んでいるだけだろうから、[[[N]]]で表現されていると考えるのが自然だろう、と思い色々な3進列を生成してはサーバーに投稿してみる。最初はまったく規則性が見えず途方にくれていたけれど、長い事やっているうちにエラーにならなかった入力のプリフィックスとメッセージ中の「for 1 tanks」、「using 1 ingredients of air」、それから「dimension mismatch」「fuel coefficients missing for tank 1」「c_{1,1} must be >= 1」といったメッセージの間に規則性があることに気付く。

これでなんとかなりそうな気がしてきた。 で、これをもとに考えていたのだけど、どうしても思いつけなかった。 リストというからには常識的に考えて再帰的な構造になっているはず*2だが……

かなりの時間をかけてもどうしても思いつけなかったので、さきほどはエラーにならない入力をあまり作れてなかった2を含むtritsについてもエラーにならない入力を色々作ってみて、prefixと結果の関係の分析を続ける。 それで、リストが全然再帰的な構造になっていなかった事に気付く。これはさっきは気付けなかったわけだ。 で、最終的には以下のように符号化されてそうだと推定するところまでは行ったが、この時点でもう既に夕方 orx

class Trits a where
 toTrits :: a -> [Int]

instance Trits Int where
 toTrits 0 = [0]
 toTrits _ = undefined

instance Trits a => Trits [a] where
 toTrits xs =
   case length xs of
     0 -> [0]
     1 -> 1 : concatMap toTrits xs
     2 -> [2,2,0] ++ concatMap toTrits xs
     3 -> [2,2,1,0] ++ concatMap toTrits xs
     4 -> [2,2,1,1] ++ concatMap toTrits xs
     5 -> [2,2,1,2] ++ concatMap toTrits xs
     6 -> [2,2,2,2,0] ++ concatMap toTrits xs
     _ -> undefined

このまま分析を続ける手もあったけど、それよりは思い、簡単そうな車に、この範囲であてずっぽで作った燃料を供給してみる。 タンクが1個の車はそれでも通るし、タンクが2個のやつも少しだけ通った。

車が多すぎて供給できる車を探すのが大変なので、さすがにこれは自動化プログラムを書くべきと思ったが、そこまでは手が回らなかった。 そして、車のフォーマットの解析もしないとなぁ。とか思っているうちに終了。

フォーマットの解析が終わって、始めて制約を解く本質的な勝負に入れたはずなのに、結局そのスタート地点にも立てずに終了したという感じ。楽しかったけど、やっぱり悔しい。

関連

• ICFP Programming Contest 2007 - ヒビルテ(2007-07-20)
• ICFP Programming Contest 2008 終了 - ヒビルテ(2008-07-15)
• ICFP Programming Contest 2009
• 他の方の感想など

λ. 日常

今日は歯医者に行って、床屋に行って、それから数学基礎論講演会、CLTT読書会と、なかなか忙しかった。

λ. 第３回数学基礎論講演会「ゲーデルの定理　その後１」

題目

ゲーデルの定理　その後１

講師

田中 一之 （東北大学）

内容

この講演会は，同講師による数学基礎論入門シリーズの第３回です．今回と次回（秋予定）はゲーデルの不完全性定理のいろいろな証明について勉強します．

前回に続いて、田中先生の講演第三弾。今回も場所は東工大。 前半はほとんど雑談で、面白かったんだけど、配布資料にそのスライドが含まれていなかったのがちょっと残念。 あと、途中で抜けてCLTT読書会に行こうと思っていたが、雑談のやこれまでの繰り返しの部分が長くて、それはそれで面白いのだけど、なかなか聞きたい話に入らず、抜けるに抜けれなかった。

• ルネ・マグリット(René François Ghislain Magritte)はエッシャー(Maurits Cornelis Escher)と同じ1898年に生まれ。エッシャーよりもむしろマグリットの絵の方が不完全性定理的ではないか。
• こうした循環的な構図というのは昔からある。
• ヤン・ファン・エイク（Jan van Eyck) 「アルノルフィーニ夫妻像」
• シェークスピアと唯名論と劇中劇。当時の舞台では女性が演じるという慣習がなく、女性役も男性が演じていた。男性が女性を演じ、その女性役が劇中劇で男装し……
• カントールはシェークスピアとベーコンが同一人物という論文を書いている。
• 直観主義からの攻撃があったから、論理主義や形式主義がしっかりしたものになっていったという面もあるのではないか。
• 無限の立場 (ルディ・ラッカー)
• クロネッカーは自然数の絶対的実在性を主張。代数的数唯名論的存在、他は研究に値しない。
• 集合論 vs アンチ集合論
• 藤沢 利喜太郎 はクロネッカーに師事し、彼の主張を日本に広めた
• ゲーデルコーディングは、記号を数といつかみ所のないところに移しているのであって、その逆ではない。
• 前回のω無矛盾性と健全性の関係についての質問への回答
  • ω無矛盾 → Π₃健全
  • ω無矛盾 /→ Σ₃健全
• コルモゴロフ複雑性
• チャイティンの主張の問題点
  • 彼の不完全性定理は、定理の複雑さについては何も言っておらず、複雑さについての定理である。実際、「K(s)>n」の形の真なる言明はnより大きい複雑さをもつことは明らかであるが、その言明の証明不可能性の要因が、言明の複雑さであるとはいえない。
  • 定理が公理よりも大きい複雑さを持ちえる。例えば「すべての列xについて，x=x」を唯一の公理として持つ理論は非常に複雑性が低いが、この理論の定理の中にはどんな複雑な列sに対する「s = s」の形の言明もある。それゆえ定理の複雑性は非有界。
  • 決定不能な命題が必ずしも自己言及的言明の形式化である必要はないことを強調したことは重要であが、この点はディオファントス方程式の決定不能製によってもすでに十分例証されている。
• チャイティンの主張: Ωの重要性
  • チャイティンは次のようにいう: オメガのビット並びは論理的に既約、つまりそれよりも単純な公理からは導くことはできない「原子的」な数学的事実、互いに関係を持たずいわば「理由なく真である」ような事実の無限列である。
  • しかし、「オメガのn番目のビットがiである」という言明は、自明でも明らかに真でもない。「より単純な公理から得られない」と主張する根拠も明らかではない。さらに、公理が定理より簡単でなくてはならないという見方は、チャイティンの別の考えに反する。
  • 絶対的な意味で、何が証明できるか否か、説明できるか否か、理由を与えられるか否かについて論ずる理論的な根拠はない。
• パリス＝ハーリントンの命題
  • 集合論のモデルの研究で巨大基数について研究していて、算術についても同じようなことがあるというのをパリスがみつけた。
  • ハーリントンがそれを組み合わせに結びつけた。
  • ラムゼイの定理をちょっと直してパリス=ハーリントンの命題が得られる。
• ヘラクレスとヒドラの戦い
  • 上には伸びないで横に広がるだけ
  • 上の方を切って行けばそのうち退治できる
• 超限順序数
  • 対数の目盛りにするようなもの
• グッドスタイン列
• ゲンツェンが自然数論の無矛盾性を証明したのもε0までの超限帰納法を使って
• 急増加関数f_α
  • リカージョンをα回繰り返して得られる関数
  • f_ωはだいたいアッケルマン関数
• 次回予告: 2010年10月頃「不完全性定理　その後2　—モデル論的議論—」

λ. CLTT読書会 第3回

というわけで、こっちには遅刻。 やっていたのは、 1.4 Cloven and split fibrations 。 定義1.4.8のUFam(ω-Sets)が圏になっていることを理解するのに、みんなちょっとつまずいていた。

• CLTT読書会 第3回 : ATND
• 私が来た後の板書の写真
• 前回

二次会

• 熱力学と圏（１）
• 熱力学と圏（２）

λ. 不動点演算子はチャーチ数での無限大?

@mametterさん が「Church numerals で無限大を考えるとしたら、Y コンビネータと同じになるのだろうか」と書いていたので、考えてみた。

普通の自然数の型は Nat = μX. X+1 で、集合の世界で考えるとこれには無限大は含まれない一方、その双対の CoNat = νX. X+1 は集合の世界で考えると自然数の集合に無限大∞を付加してやったような集合になるので、これを使って考えてやれば良いのではないかというのを最初に考えた。

ただ、チャーチ数の型 ∀X. (X⇒X)⇒X⇒X はNatのチャーチエンコーディング ∀X. (X+1⇒X)⇒X を変形したものであって、CoNatのチャーチエンコーディング ∃Y. Y×(Y⇒Y+1) = ∀X. (∀Y.Y×(Y⇒Y+1)⇒X)⇒X とは違い、そのままではうまくいかないので、結局NatとCoNatが一致するような世界で考える必要がある。領域理論的な世界ではそれが言える。

Haskellで自然数型とチャーチ数の型、それらの間の対応、そして無限大を以下のように定義する。 Haskellに対応する圏では本物の直和がないので、上の話とはちょっと違っちゃうんだけど、まあそれはそれ。

{-# LANGUAGE Rank2Types #-}

data Nat = Succ Nat | Zero
type ChurchNumeral = forall a. (a->a)->(a->a)

build :: ChurchNumeral -> Nat
build c = c Succ Zero

unbuild :: Nat -> ChurchNumeral
unbuild n s z = foldNat s z n

foldNat :: (a -> a) -> a -> Nat -> a
foldNat s z Zero = z
foldNat s z (Succ n) = s (foldNat s z n)

infinity :: Nat
infinity = Succ infinity

なお、infinity は Succ の唯一の不動点である(CoNatのfinalityから言える)。

ここで、不動点結合子を使って無限大っぽいチャーチ数を定義してみる。

infinity' :: ChurchNumeral
infinity' s z = fix s

すると、build infinity' = infinity' Succ Zero = fix Succ で、infinityはSuccの唯一の不動点なので、build infinity' = infinity となる。

逆に infinity をチャーチ数に変換してみると、unbuild infinity s z = foldNat s z infinity = foldNat s z (Succ infinity) = s (foldNat s z infinity) となるので、unbuild infinity s z は s の不動点。また、最小不動点である事も領域理論的な推論で容易に示す事ができる。

というわけで、まあ、不動点演算子はチャーチ数での無限大と言って良さそうだ。

この辺りをもっとちゃんと考えると、P.S. Mulry. Strong monads, algebras and fixed points のような話になるのだと思うけど、この論文、読もう読もうと思いつつずっと読んでなかった……