日々の流転

λ. 研究室紹介ポスター展示

正直言って新入生向けに紹介してもあまり意味が無い気がするが、他の研究室のポスターを見れてなかなか面白かった。WIDE系の研究室は「インターネットの研究会で〜す」とかキャッチーな声のかけ方をしていた。対抗して「Webの研究会で〜す」*1とでも言えばよかったかも*2。

それから、小熊研のポスターが笑えた。

λ. 圏論の解析結果

<URL:http://seibun.nosv.org/?p=%B7%F7%CF%C0>より。

圏論の99%はやらしさで出来ています
圏論の1%は心の壁で出来ています

ちょっwww

λ. 上座

上座=電源に近い席、らしい。知らなかった。

λ. RHG読書会::東京 Revolution::ふつうのLinuxプログラミング 第八回

RHGは Ruby・Haskell・Gauche の略だそうです。

λ. length xs + length ys = length (xs ++ ys) の証明

RHG読書会の飲み会で即興で書いた証明。

--#include "Hedberg/SET.alfa"
--#include "Hedberg/Op/Nat.alfa"
open SET use Id, refId, mapId, Nat
open OpNat use zero, succ, (+)

(++) (|X::Set) (xs::List X) (ys::List X) :: List X
  = case xs of 
    (Nil    )-> ys
    (x : xs')-> x : (xs' ++ ys)

length (|X::Set) (xs::List X) :: Nat
  = case xs of 
    (Nil    )-> zero
    (x : xs')-> succ (length xs')

prop (|X::Set) (xs::List X) (ys::List X)
  :: Id (length xs + length ys) (length (xs ++ ys))
  = case xs of 
    (Nil    )-> refId (length ys)
    (x : xs')-> mapId succ (prop xs' ys)

λ. 人狼審問 : (1296)学者の村

久しぶりに参加。今回はキャラはハーヴェイを選択。 役職希望は「おまかせ」を選んだのにまた霊能者になり、確定したために、またまとめ役に。推理を間違いまくるも、他の村人のおかげで勝利。しかも最後はランダムだった。

関連リンク

• B1/1296村 - 人狼ファンWiki
• 他の方の感想
  • stinさん (マンジロー)
  • らるさん (ヘンリエッタ)
  • KONNIEさん (リック)
  • hatoさん (ユージーン): 1, 2
  • EMERADAさん (ラッセル)
  • TickTackさん (フレディ)

村人としての反省点

やはり推理を間違え続けたことかな。

ことに、>>8:114で「正直ユージーンさんもフレディさんも人間としか思えなくなってきました。コーネリアスさんが人狼なのでしょうか……」とかいいつつ、人狼のコーネリアスさんではなく、人間のフレディさんに投票してしまったのは、最高にかっこ悪かった。 ユージーンさんやフレディさんは、コーネリアスさんの思考放棄的な部分や、迎合に動いた点を良く見ていたが、私はコーネリアスさんの特異なスタイルに振り回され、そういった点にあまり注目していなかった。それが、コーネリアス人狼を見抜くことが出来なかった理由の一つではないかと思う。

また、5日目の最後にリック吊りを選んでしまった理由は>>9:104に書いた通りで、「リック・ステラが人狼という可能性は低い」「リック・ニーナが人狼と言う可能性は低い」という推理をしていたから、リックを吊ることが情報になると思ったため。これらの推理自体は間違ってはいなかったが「もしこれらの推理をしていなかったら、発言から情報を得にくかった人狼を吊ることが出来たかも知れない」と思うと少し悔しい。「判断の正しさは、持っている情報に対して単調でない」というのは理屈では分かってはいたが、体感してみて良く分かった。

それから、ユージーンさんが5日目に 2006/04/09 00:10:05 の独り言 で言っていた「ボクの占いや吊りの希望がいつも、数人の後にその人達の希望に重ねて出してばかり」という点に気づいていなかったのもちょっと悔しい。ユージーンさんが人間だったからよかったものの…

まとめ役として、序盤で占い師の人に「自分が人狼と仮定した場合の人狼予想」をしてもらい、後半では>>7:35で灰の人向けに「人狼CO」*1という議題を出した。しかし、それらに対する回答をあまり直接的に推理に生かせなかったのが残念。自分の中での印象面への影響はそれなりにあったけど、それを推理と言う形で結実することは出来なかった。「こういった議題は人狼にとって答えにくい部分がある」という考え自体は捨てていないが、訊かれた側が「推理に使われるわけでもない無意味なことを訊かれて、面倒だった」とか思ったりしない*2よう工夫や配慮が何か必要だったのではないか？*3

(追記予定)

そういや、ラッセルさん(Russel)やモーガンさん(de Morgan)に数学ネタで絡もうと思っていたのに、すっかり忘れていた。これは、ま、いっか。

まとめ役としての反省点

まとめ役っぽいことをやるのはこれで5度目くらいになるが、いまだに慣れないね。今回は決定にさほど重責を感じずに割とサクサク決めていけたのは進歩した点だと思う。それも、優秀な他の参加者のおかげと、あと判断にあまり悩む状況が無かったせいではあるんだけどね。

占い結果発表方法の指示ミス

二日目の占い結果の発表時間を事前にきちんと指示していなかった点。そのため同時発表が出来ず、狂人が黒だししやすい環境を作ってしまった。結果としては関係なかったけど、まずかった。

決定時間について

仮決定についてはユージーンさんが>>2:61で「24時間前仮決定は、議論の進み具合を見て　まとめ役が出せそうだなーと思ったら出せば良いと思う」と言っていたので、明示的に時間を指定することはしなかったが、これは失敗だったかも。議事録の読み込みや考察はキリがないので、時間を指定してそれまでにある程度意見を出してもらう方向に誘導しないと、「24時間前仮決定」はまず無理。 個人的な感覚としては遅くとも更新がある日の朝くらいまでには暫定的な意見が出揃っていると良かったのではないかと思った。 また、マンジローさんも8日目に 2006/04/15 01:02:54 の呻き で「そもそも、本決定で覆る可能性のある仮決定を出すなら、反論するだけの充分な時間が必要」と言っていたが、これについても完全に同意。

本決定についても、時間をきちんと決めておかなかったために、更新直前にゴタゴタしてしまったことがあった。これも失敗だったと思う。

ヘンリエッタさんが5日目に2006/04/07 23:52:29 の独り言で言っていた「仮決定を何度も出す」については、ヘンリエッタさんこと、らるさんがmixi日記で補足していた。『「村の流れはこうだ」と言うのは常に意識させないといけない』というのは至言だと思う。

意見を引き出す方向に誘導すべきだった

>>5:142でも書いたが、もっとみんなの吊り意見を引き出す方向に誘導すべきだった。明確な吊り候補がいるような時には、意図的に意見を引き出す方向に誘導しないと、推理に使えるような情報は出てこない。

ヘンリエッタさんが5日目に2006/04/07 23:52:29 の独り言で言っていた「仮決定を何度も出す」というのも、時間に余裕があるときは、みんなの意見を引き出すためには有効だったのではないかと思う。今度試してみるか。

まだ整理できていない点

これも何点かある。 次に参加するまでには自分なりに少し考えておきたいところ。

狂人っぽい人にだけ黒だしされたパンダを吊るべきか？

エピローグの>>9:378で書いたけど、あそこでグレンさんを吊らずに灰を吊るという選択肢はどうっただろうか。マンジローが真ならば、残るは最後の人狼だけだし、急いで吊る必要は無かったのだから。

グレンさんはとりあえず放置して、マンジローさんが襲撃されたら、それまでの情報に基づいて吊るべきかを考える。そうしている間にマンジローさんが偽確定すればグレンさんは白確定。あるいはモーガンさんorウェンディさんが襲われた場合も、それまでの情報に基づいて吊るべきか考える。

守護者や結社員を吊りに挙げてしまう危険もあったし、情報を確定させないまま状況を進めるのはリスキーではあるけど、総合的にはそう悪い選択ではなかったのではないかとは思う。

その場合、人狼側としてはやっぱり真占い師のモーガン襲撃だっただろうか？　それとも先に確定霊能者のハーヴェイ襲撃だっただろうか？

最終日にはまとめ役は決定を出すべきか？

私は >>8:92で『それから、今日って決定はいらないよね？　人狼は当然自分に有利な投票をするだろうし、村人だって「こいつを吊ったら負ける」と思ったら別の人に投票するでしょうから』と言ったが……

λ. 狂人占い師のおさらい

学者の村のマンジローさんが1日目に 2006/03/31 18:30:13 の独り言で言っていた「おさらい」は良くまとまっていると思うので引用。前回狂人で占い師を騙ったときは大失敗だったので、次に狂人で占い師を騙るときにはこの辺りを肝に銘じよう。

はい、おさらい。

１．真ぽく振舞うべし

「真占い師ですよー」という姿勢、「喰われちゃう！」という恐怖を体現する。それで信用得られればＯＫ、狼と思われて吊られるもＯＫ。

２．狂人アピールは早めに

信用得られてるぽいなー、と思ったら、早めに黒出す。偽確定で吊られ上等。それ僕の仕事。

この辺が、狂人としての最初の課題かな。

λ. f (f x) == -x

今日の一行より。向井さんがなにやら悩んでるけど、単に虚数単位をかける関数で良い。

import Complex

f :: RealFloat a => Complex a -> Complex a
f x = x * (0 :+ 1)

ツッコミにあるように「実数関数」だったので、これじゃ全然良くなかった。仕方ないので少し真面目に考える。

• 条件からf²は全単射
• そこから、fが単射であることと、fが全射であることが言えるので、fもやはり全単射
• f(-x) = f(f(f(x))) = -f(x)
• 零と正の実数に対する値だけ定義すれば、負の実数に対する値は自動的に定まる
• 特に f(0)=-f(0) なので、f(0) = 0
• 0以外の数に対しては「x ↦ f(x) ↦ -x ↦ -f(x) ↦ x」という周期4のサイクル

したがって、正の実数を二つの同型な集合A,Bに分割出来ればよい(A≅B, A∪B=正の実数, A∩B=∅)。 そのような集合A,Bと全単射g:A->Bが与えられたとすると、以下のような関数が条件を満たすことは明らか。

f 0 = 0
f x
  | x<0  = - f (-x)
  | x∈A = g x
  | x∈B = - (g^{-1} x)

したがって、問題はこのようなA,B,gを見つけることに還元される。

そのようなA,B,gの選び方は複数存在するけど、一つの方法は整数の偶奇を利用する方法。

• A = {x∈R | 0<x, odd (ceiling x) }
• B = {x∈R | 0<x, even (ceiling x) }
• g(x) = x+1

他の方法として…

(続く?)

λ. Building SVG-based Interactive Web-Estimated System

• <URL:http://www.pfu.fujitsu.com/techreview/no29/pdf/29-8.pdf>

λ. 「Objective Caml NG集 − 型推論とオブジェクト指向の複雑な関係」. Jacques Garrigue

<URL:http://www.math.nagoya-u.ac.jp/~garrigue/papers/ocaml-ng.pdf>

を読んだ。バグの実例が面白い。

λ. ジャンプが読めるのは萩野・服部研だけ!

「ジャンプが読めるのは萩野・服部研だけ!」らしい。 みんな研究室にジャンプを読みにやってきています(ぉぃ

λ. 『博士の愛した数式』, 小川 洋子 [原作], くりた 陸 [漫画]

まだ、小説も読んでないし、映画も観ていないのだけど、漫画にもなってたのか。素敵な話ではあると思ったけど、数学とか数学者へのイメージはあまりピンとこなかった。

Quotation

p.66 より。

さあ、どう思う？

みんなバラバラ
あ、それに2だけ偶数だね

その通り
素数の中で偶数は一個だけだ

さびしくないのかな

心配にはおよばない
さびしくなったら、偶数の世界に行けばいいんだ

λ. 人狼のなく頃に 第459話　『強い妖戦士編』

• ログ
• 第459話　『強い妖戦士編』 - ひぐらし人狼まとめサイト

鬼側すごいな。 きっかけこそ偶然だったが、その後の作戦は見事。 「これぞ、スーパーステルス(SS)」という感じで、鮮やかだった。

λ. 避難所作成

研究室のサーバが落ちているので、 避難所を作成してみた。

λ. 人狼審問 : (1371)いんげんおいしいよね村　桜だ！

学者の村のエピローグで「いんげん村」について紹介されたので、観戦してみることにした。色々と面白そう。

ツッコミルール

クインジーが>>1:504で提案しているツッコミルールが独特で面白い。

■10. 占吊の決定は基本的に多数決で決める。俺が生きている間は明日から以下のツッコミルールを適用する事を提案する。

• 誰かの占い希望もしくは吊り希望どちらかにツッコミを入れなければならない。ツッコミ入れない人は占い希望および吊り希望の両方をカウントしない。
• ツッコミは自分の占い希望と吊り希望の両方出してからする事。
• ツッコミが入ったら、反論するか希望を変えること。どちらもしない場合は、その希望（占い希望へのツッコミであれば、占い希望）はカウントしない。
• 各自、何時までツッコミが受け付けられるか明示する事。そして、それまでに必ず占い希望と吊り希望を出す事。
• 目的は議論の早回しと議論の活性化ね。ある程度時間を拘束するけど。

守護者の護衛先騙り

なんて作戦があるとは思いもしなかった。人狼は襲撃失敗の理由が守護者の護衛によるものか襲撃先が妖魔だったからかを区別できない。そのため、護衛に成功した守護者が護衛先を騙ると、人狼からすると襲撃先が妖魔だったかのように見える。それによって、状況によっては人狼の妖魔告発を誘うことが出来る。具体的にはヘンリエッタの>>5:33と>>5:167を参照。

λ. f(f(n)) = n+1

以下のような関数 f が存在する場合は実装し、 存在しない場合はそのことを証明せよ:

1. nが整数なら f(n) は整数
2. nが整数なら、f(f(n))=n+1

• f(x+1) = f(f(f(x))) = f(x)+1 for x∈Z
• よって、f(x) = f(0)+x for x∈Z
• したがって、1 = f(f(0)) = f(0)+f(0) = 2 f(0) より f(0) = 1/2 だが、これは条件1に矛盾
• ゆえに、そのような関数は存在しない

λ. 風邪

風邪ひいたっぽい。 喉が痛いし、なんだかだるい。

λ. 超準解析のモナド

Wikipediaのモナドのエントリによると、超準解析では「ある与えられた超実数に対して無限に近い全ての超実数の集合」という意味でモナド(Monad)という言葉が使われているそうだ。知らなかった。そういえば以前ファンクターさんがmixi日記で書いていたモナドはこのモナドだったのだろうか……

λ. 間違い探しゲーム (5 Spots)

何度もプレイしてると、流石に絵を覚えてしまう。現在のスコアは以下の通り。

level

175

score

2184765

λ. 「Haskellによる関数プログラミング入門」

日経ソフトウェアの6月号*1に「Haskellによる関数プログラミング入門」という記事を書かせていただきました。もうすぐ発売なので、もし良かったら読んでみてください。この日記の読者は関数型言語を既に知っている人が多いと思うので、そういう人には不要かも知れませんが(笑

「やさしい Haskell 入門」はあまりまじめに読んだことなかったんだが、自分で入門記事を書いてみて、あれは良く書けてるなと思った。分かり易いかといえばまた別だとは思うけど。

【2006-04-24追記】 発売されました。 補足や訂正などはおいおいwiki:Haskellによる関数プログラミング入門の方にでも書こうと思います。

Amazon.co.jp

λ. 読書速度を測ろう - 目指せ速読

ひげぽん OSとか作っちゃうかMona- (2006-04-26) より。 読書速度測定で自分の読書速度を測ることができるそうなので、試してみた。

結果

まあ、こんなもんか。 このテストだと、一行が結構短いせいで視点を上下にあまり移動せずに読める分、普通の文章を読むときよりも高い数字が出ている気がする。

他の方の結果

• あろはさん
• 佐野さん
• alphaさん

λ. The Logical Way to Be Artificially Intelligent

月曜の知識発見法の授業はR.Kowalski氏の講義だそうですよ。

Speaker

Robert Kowalski (Imperial College London)

Title

The Logical Way to Be Artificially Intelligent

Abstract.

Abductive logic programming (ALP) can be used to model reactive, proactive and pre-active thinking in intelligent agents. Reactive thinking assimilates observations of changes in the environment, whereas proactive thinking reduces goals to sub-goals and ultimately to candidate actions. Pre-active thinking generates logical consequences of candidate actions, to help in deciding between the alternatives. These different ways of thinking are compatible with any way of deciding between alternatives, including the use of both decision theory and heuristics.

The different forms of thinking can be performed as they are needed, or they can be performed in advance, transforming high-level goals and beliefs into lower-level condition-action rule form, which can be implemented in neural networks. Moreover, the higher-level and lower-level representations can operate in tandem, as they do in dual-process models of thinking. In dual process models, intuitive processes form judgements rapidly, sub-consciously and in parallel, while deliberative processes form and monitor judgements slowly, consciously and serially.

ALP used in this way can not only provide a framework for constructing artificial agents, but can also be used as a cognitive model of human agents. As a cognitive model, it combines both a descriptive model of how humans actually think with a normative model of humans can think more effectively.

実は私、発想推論って良く分かってない。よく推論には「演繹推論」「帰納推論」「発想推論」の三つがあるという。演繹推論に基づいた言語にはPrologのような言語があり、帰納推論のシステムとしてはProgol等のILP(Inductive Logic Programming,帰納論理プログラミング)がある。ALPは同様に発想推論に基づいた何かなんだろうか……。そういえば、向井先生の論理プログラミングの授業の講義資料でも、メタプログラミングの章で題材として発想推論が取り上げられていた。

BTW: Kowalski氏の講義は以前にもあった。

λ. Re: Y combinator is forbidden in Haskell!?

Haskellでは以下のようなコードでY-Combinatorを表現することが出来ます。

newtype T a = PsiInv{ psi :: T a -> a }

fix :: (a -> a) -> a
fix f = g (PsiInv g)
  where g x = f (psi x x)

この T a という型は、T a の値と T a -> a の値が一対一に対応するように作った型で、このような型が存在すると不動点コンビネータが表現可能なことが知られています。このことは理論的にはLawvere の不動点定理を使って説明することができ、「自己言及の論理と計算」等で詳しい説明がされています。

ただ、プラクティカルにはこのような型の存在は問題を引き起こしがちです。例えば現在のGHCは上記のコードを食うと暴走するし、agdaにもこのようなコードの停止性検査が正しく行えないという問題があります。

【2010-05-21 追記】 GHCの問題はNOINLINEプラグマを利用することでこの問題を回避可能とのこと。具体的にはリンク先を参照。

λ. equi-recursive type と special final coalgebra theorem

Y-Combinator の話で思い出した。 少し前に sumiiの日記「不動点演算子ふたたび」 で equi-recursive type とか iso-recursive type という言葉を知ったが、この対比は特殊終余代数定理(special final coalgebra theorem)と一般化された終余代数定理(final coalgebra theorem)の対比に少し似ていると思った。

λ. “全線建設”はこうして決まった・道路公団民営化半年の攻防▽交渉の舞台裏

今日のNHKスペシャルを横で見ていて「なんかなぁ」と思った。 真面目に見ていなかったので勘違いしてるかも知れないが、色々と政治くさい話はおいておくとして…

• 採算性も重要だが、便益と比較せずに採算性だけを論じるのは無意味。将来の料金収入も含めた財政的制約の中で便益を最大にするよう建設計画を考えるべき。
• サンクコストを無視せよ。「すでに一部建築してしまったから」なんて理由で継続するなんて論外。

λ. Haskell on a Shared-Memory Multiprocessor. Tim Harris, Simon Marlow, Simon Peyton Jones

• <URL:http://research.microsoft.com/~simonpj/papers/parallel/>
• <URL:http://jp.citeulike.org/article/342280>

をざっと読んだ。

まず復習(以下ではSTGマシンの知識は仮定)。これまでのGHCのネイティブスレッドへの対応はジャイアントロックを使った対応だった。つまり、外部のコードとかは複数のネイティブスレッドで同時に実行できるけど、同時にHaskellコードを実行するネイティブスレッドはただ一つだけだった*1。これだとSMPでもあまり嬉しくないので、より細粒度のロックにして並列度を上げたい。ただ、各サンクにロックを用意して操作毎にロックすることにすると、無茶苦茶オーバーヘッドがかかる。

で、「どうすんだろな〜」と思ってたんだが、この論文では、割と楽観的な前提に基づいて「そもそもサンクに対して厳密な排他制御は不要」と言っている。私がこの分野についてあまり知らないからかもしれないが、コロンブスの卵みたいで随分感心した。

まず、サンクを評価結果(へのindirection)で上書きする際にポインタを書き込む領域を別に用意することで、サンク上の他のデータが評価結果の書き込みで壊れないようにする。これで複数のスレッドが同時に同一のサンクを実行しても問題なくなる。ただ、複数のスレッドが同時に同じサンクを実行すると、計算を重複して行うことになってしまう。副作用のある計算は複数回実行するとまずいので真面目に排他制御するが、大多数の純粋な計算は何度実行しようと意味論的には問題ない。

もちろん、意味論的に問題なくても計算量的には問題になる。そこで各スレッドは定期的な lazy black-holing のタイミングでサンクを排他的に所有しようとし、それによって重複する計算を検出する。で、検出された重複する計算は捨てる。この処理にはサンクに対する排他制御が必要になるが、lazy black-holing の頻度は通常のサンク操作の頻度よりもずっと低いため、各操作毎に排他制御するよりもオーバーヘッドはずっと低い。また、すぐに計算が終了するようなサンクは排他制御無しで実行できる*2し、計算に時間がかかるようなサンクの場合も無駄な計算は一定時間で破棄できることが保証される。

あとは、複数のスレッドが同時に同じサンクを実行する可能性を極力下げれば良い。そのために、サンクに制御を移す時点での eager black-holing (ここでは grey-holing と呼んでいる) も提案している。これも排他制御無しで行え、これによって複数のスレッドが同時に同じサンクを実行してしまう可能性を限りなく小さく出来る。ただ、このタイミングでのサンクへの書き込みは通常のアクセスパターンから外れているので、キャッシュのスラッシング(cache-thrashing)を引き起こす可能性もあり、これによって逆に性能が低下することも有り得る。

とかとか。

他にもいろんなテクニックを使ってるけど、特に面白かった部分は以上の話。

λ. google:アルキメデスの卵

ふと検索してみたら、2件ひっかかった。

λ. The “Curry view” and the “Church view” of polymorphic λ-calculus

the “Curry view” of polymorphic λ-calculus

Pure terms of the λ-calculus are assigned type expressions involving universal quantifiers.

the “Church view” of polymorphic λ-calculus

Terms and types are defined simultaneously to produce typed term.

という二つの見方があるんだそうな。 Type reconstruction in finite-rank fragments of the polymorphic λ-calculus. より。

λ. 五月病

一足早いけど、五月病っぽい。

頭痛い。気持ち悪い。何もしたくない。

λ. read "1" :: Rational

しょぼーん。 文字列で与えられたRationalのリテラルをevalする簡単な方法はないだろうか?　hs-pluginsでevalするってのは無しね。

Prelude> 1 :: Rational
1%1
Prelude> read "1" :: Rational
*** Exception: Prelude.read: no parse

何が悲しかったか、もう少し説明する。「123」のようなリテラルは概念的には「fromInteger (123::Integer)」として扱われるので、そのような文字列からNumに属する任意の型の値を得るには「fromInteger (read "123")」とすればよかった。それに対して、「1.23」のようなリテラルは概念的には「fromRational (1.23::Rational)」として扱われる。そのような文字列からFractionalに属する型の任意の値を得るためには、「fromRational (read "1.23")」とすれば良いのではないかと類推したのだが、これは正しくなかったのだった。

λ. Agdaの紹介Flash

やねうらおさんのswf形式で動画キャプチャで紹介されていたCam Studioを使ってみたくなったので、Agdaでの簡単な証明風景をキャプチャしてみた。

ネタは、あろはさんが最近The Coq Proof Assistant A Tutorial (3) Minimal Logicで (A->B->C)->(A->B)->A->C の証明をやっていたので、それを使わせてもらった。ついでに、A->B->Aも証明*1。Setと書いた部分はPropと書いたほうが論理っぽいんだけど、AgdaではPropはSetの別名に過ぎないし、Propを定義してるライブラリを読み込みたくなかったので、Setで通した。

それから、分かり易いように各種のコマンドは固有のキーバインディングは使わず、メニューとM-xから実行してみた。まあ、細かいことはともかく、これを見るとCoqをコマンドラインから使う場合に比べ、ゴールの管理が非常に直観的なことがわかると思う。もちろん、CoqでもCoqIDEやProof Generalを使えば同じくらい直観的に使えるんだと思うけど、試したことないんでよく知らない。誰かそれらを使った証明風景をキャプチャして紹介してくれると嬉しい。

【2024-09-01】 Flashはサポートが終了しているので、YouTubeにもアップロードしてみた。

他の証明環境の紹介動画

• Twelfでの証明行為 (hyさん)
• Coq-IDEでの証明行為 (hyさん)
• Coqでニコニコ :-] (yoshihiroさん)
  • <URL:http://www.nicovideo.jp/watch/sm1276083>
  • <URL:http://jp.youtube.com/watch?v=f9XOdpmeJ0o>

λ. JSON in Haskell

激しく今更だが、ふとJSONのパーサをParsecを使って書いてみた。JSONはシンプルでいいね。コードは思ったよりも長くなってしまったので、添削きぼー。

• 最新版 JSON.hs
  • 文字をエスケープするか判断する関数を渡せるように変更
  • サロゲートペアをデコードするように変更
• 古いの
  • JSON-3.hs
  • JSON-2.hs
  • JSON-1.hs

λ. 有限モノイドへの準同型写像への逆像としての正規言語の定式化

有限モノイドへの準同型写像への逆像 : 村田　真のチャンネル -北国tvからメモ。

正規言語の定式化の一つとして、有限モノイドへの準同型 写像への逆像を用いるものがあります。(中略) 文字列の集合Lが正規であるのは、適当な有限モノイドM、 準同型f, Mの部分集合Nがあって、L = {u | f(u) はNに属する } が成立するときです。

檜山正幸のキマイラ飼育記 - 長文の反応に驚き！でも書かれてるけど、非常にスマートな定義だと思った。

λ. javascriptでRDFをパース

やっぱし、やっている人はいるもんだな。 何かに使えそうな気がするのでメモ。

• Simple javascript RDF Parser and query thingy
• Javascript-RDF Testbed

λ. (forall x. ((x->r)->r)->x) -> Either a (a->r)

今日ちょっと混乱したことを元にクイズにしてみた。多分その手の人にはピンとくる問題。表記はHaskellのものを使ったが、実際には多相ラムダ計算の問題と考えていい。

問題

1. 「(forall x. ((x->r)->r)->x) -> Either a (a->r)」という型を持つ関数を定義せよ。(ただし⊥が途中で現れたりする定義は禁止)
2. この関数は何を表しているのだろうか?

解答編

問題の関数はこんな感じで定義できる。

notNotEM :: ((Either a (a->r)) -> r) -> r
notNotEM k = k (Right (\a -> k (Left a)))

dn2EM :: (forall x. ((x->r)->r)->x) -> Either a (a->r)
dn2EM dn = dn notNotEM

で、これが表しているのは何かだが……二重否定除去規則から排中律(The Law of excluded middle)を導く証明の計算的な表現だったりする。型はちょっと一般化してあるので、以下のようにより具体的な型にすると分かり易いかも*1。

data Absurd
type Not p = p -> Absurd
type Or = Either

notNotEM :: Not (Not (p `Or` Not p))  
dn2EM :: (forall x. Not (Not x) -> x) -> p `Or` Not p

で、面倒なので詳しい説明は省略するが、例えばNK(自然演繹の体系NJに二重否定除去規則を追加した体系)で排中律を証明すると、この関数の構造を反映した証明図が得られる*2。

[1: P]
------------- (∨I左)
  P ∨ ¬P              [2: ¬(P ∨ ¬P)]
------------------------------------------- (¬E)
  ⊥
------------- (¬I{1})
  ¬P
------------- (∨I右)
  P ∨ ¬ P             [2: ¬(P ∨ ¬P)]
------------------------------------------- (¬E)
  ⊥
------------------ (¬I{2})
  ¬¬(P ∨ ¬P)
------------------ (¬¬E)
  P ∨ ¬P

他の体系での証明は誰かにまかせた。あろはさんはこの証明をCoqで表現してみると良い勉強になるかも。ついでに古典論理のうさんくささをもっと感じられるかもw

余談

ちなみに、色々と細かいことを抜きにすれば、否定は継続に対応し、二重否定除去規則に対応するものはcall/ccで実現できる。Haskellにはそれらは存在しないので多少回りくどい表現になっているが、一級継続とcall/ccが存在する言語では直接それらを使って排中律に相当するものを表現することが出来る。例えばSchemeだと以下のような感じだろうか*3。

(define (left x)  (list #t x))
(define (right x) (list #f x))

(call-with-current-continuation
  (lambda (k) (k (right (lambda (a) (k (left a)))))))

しかし、それにしても奇妙な定義と振る舞いである。これに関係して、Philip Wadler, Call-by-value is dual to call-by-name. Proc. ICFP 2003, pp. 189-201. <URL:http://homepages.inf.ed.ac.uk/wadler/topics/dual.html> に載っていたお伽噺が面白かったので、引用する。

Once upon a time, the devil approached a man and made an offer: “Either (a) I will give you one billion dollars, or (b) I will grant you any wish if you pay me one billion dollars. Of course, I get to choose whether I offer (a) or (b).”

The man was wary. Did he need to sign over his soul? No, said the devil, all the man need do is accept the offer.

The man pondered. If he was offered (b) it was unlikely that he would ever be able to buy the wish, but what was the harm in having the opportunity available?

“I accept,” said the man at last. “Do I get (a) or (b)?”

The devil paused. “I choose (b).”

The man was disappointed but not surprised. That was that, he thought. But the offer gnawed at him. Imagine what he could do with his wish! Many years passed, and the man began to accumulate money. To get the money he sometimes did bad things, and dimly he realized that this must be what the devil had in mind. Eventually he had his billion dollars, and the devil appeared again.

“Here is a billion dollars,” said the man, handing over a valise containing the money. “Grant me my wish!”

The devil took possession of the valise. Then he said,“Oh, did I say (b) before? I’m so sorry. I meant (a). It is my great pleasure to give you one billion dollars.” And the devil handed back to the man the same valise that the man had just handed to him.

関連リンク

• 等価変換な日々
  • The Coq Proof Assistant A Tutorial (9) 排中律の証明
  • The Coq Proof Assistant A Tutorial (11) 排中律の証明 (完結編)
• sumiiの日記 - callccによる排中律の証明
• d.y.d.
  • d.y.d. - Curry-Howard Isomorphism
  • カリー・ハワード
• 欝っぽい日記 - ブラウアーの考えたこと

λ. 第十六回圏論勉強会

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

Olegさん凄いな。 Context Reduction がeagerかlazyかだとか、その場合の Functional Dependency の扱いとか、僕なんかは出来るだけ避けて通りたいと思うような点について、嬉々として語っていたのが印象的だった。

• 圏論勉強会へ行ってきました (sydさん)
• 圏論勉強会 (日下部；）さん