日々の流転

λ. 今朝は3時間の睡眠を2回とった。分割睡眠も悪くないな。

λ. 朝、生け花を見て、何故かSMを連想。いやらしい。

λ. 読書

ブギーポップ・ウィキッド 「エンブリオ炎生」

上遠野浩平[著] 緒方剛志[イラスト]

λ. あなたがネコになっちゃったら?

あなたは、遊びネコタイプです。

贅沢なものを好み、宵越しの金は持たないようなあなたは、ネコの世界では「遊び人」ならぬ「遊びネコ」タイプです。暇さえあれば、悪いネコ友達と一緒に賭け事に興じていたりします。

しかし、ここ一番の勝負にはちょっと弱く、さらに贅沢なものを好むこともあって、宵越しの金を持てないこともあります。地道に努力すると運が開けます。あと、ネコ友達はくれぐれも大切に。いざというときに力になってくれるでしょう。

現実のあなたは、…うーん、どうなんでしょうか？上のコメントは、あくまでも「ネコ」の場合だし…。

λ. PROJECT METATRON

.

λ. Happy Squeaking!!

来週豊田さんの発表があるので、予習しとこと思って。

λ. 銀歯が取れた

久野君が買ってきた夕張メロン味のハイチューを噛んでいたら銀歯が取れてしまった。これは久野君の陰謀に違いないと思う(笑)のだけど、久野君は恐いので何も言えません。

λ. 「日本経済の現状と金融政策」

というタイトルで、植田和男(日本銀行政策委員会審議委員)の講演があったので、聴いてきました。

λ. Smalltalkと継続

「SmalltalkにもContinuationがあって、云々」という話がどうもピンと来なかったので、検索してみたら Continuation (Smalltalk Textbook 27) というページを見つけた。これだと、確かにCPSで書かれてはいるけど、言語として first class continuation をサポートしているとは言えないような……

と思ったけど、http://minnow.cc.gatech.edu/squeak/2119を見ると、Squeakにはcall/ccがあるのか。なるほどなるほど。

λ. レッシグの講演

そういえば、明日ネットワーク社会論でローレンス・レッシグ氏の講演があるそうです。あぁ、こんなことならCODEとコモンズ読んどけば良かった……

でも、そもそも予算編成論と重なってるんだよなぁ。こっちは財務省財務総合政策研究所研究部総括主任研究官の田中秀明氏で、こっちはこっちで聴いてみたいしなぁ……

λ. 足利銀と北朝鮮の関係とは

メモ。

λ. [ruby-dev:22234] Re: yet another inconsistency about EOF between StringIO and IO

ruby本体へのパッチを送るのは初めてなのでちょっと緊張した。

λ. 偽弦「スードストラディヴァリウス」 & 幻神「飯綱権現降臨」

偽弦「スードストラディヴァリウス」 と 幻神「飯綱権現降臨」をゲット。これで、132/141。

λ. hugs-i18n

日本語がまともに使える処理系がないのは嘆かわしいので、Hugsを国際化(というかUnicode化)すべくちょっとだけHack中。まだ、Lexer/Parserに手を入れていないので、これくらいしか出来ない。

% export LC_ALL=ja_JP.eucJP
% echo '
main :: IO ()
main = 
    do s <- getContents
       putStrLn (show (length s))
' > test.hs
% echo -n 'こんにちは世界' > test.txt
% runhugs test.hs < test.txt
7

λ. HaskellでScheme処理系を実装 (2)

多値を実装。(call-with-values producer consumer) は consumer への参照を含む特別なフレームをコントロールスタックにプッシュして、producerを呼び出すことにした。(values arg1 arg2 ...) でコントロールスタックのスタックトップを確認して、それがcall-with-valuesによって作られたフレームだったら、引数をそのまま引き渡す形でconsumerにジャンプする。

何も考えずに実装しちゃったけど、こんなのでいいのかな?

λ. 第二回圏論勉強会

というわけで、先日書いた通り、圏論勉強会の二回目がありました。人数も増えて結構盛り上がったし、とても楽しかったです。

• CategoryTheory:圏論勉強会 (sampou.org, Programming in Haskell)

λ. Shortcut fusion is correct by Patricia Johann

以前から読まなくちゃと思ってはいたのだけど、<URL:http://d.hatena.ne.jp/m-a-o/20061206#p1>で見かけたのをきっかけに読んでみた。操作的(operational)なモノの見方に慣れていなかったので苦戦。証明は追えたけど、いまいち実感がわかない。

TT-closedness の定義は面白い。 スタックの関係と項の関係の間の s^T⊇s ⇔ r⊆r^T という随伴から定義されるclosure。

「lazy PolyPCF」の lazy の意味は lazy λ-calculus (20040102#p03 を参照)のと同じ意味。lazy PolyPCF を扱うには、Free Theorems in the Presence of seq でのように inequational logical relation にすればよいのだろうけど、もう結果は出てるのかな?

結局、operational に考えることのメリットは何か?　impredicative polymorphism があるとモデルを考えるのが大変なのに対して、operational semantics と contextual equivalence に基づけば、複雑なモデルを考えなくて済むということか? しかし、fix と impredicative polymorphism を持つ言語のモデルで、admissibleな関係に限定したparametricityが成り立つモデルは知られていないのだろうか?　もしそのようなモデルが知られているのなら、同程度の労力で short-cut fusion の正しさを示すことは可能であるように思う(TT-closednessを示すのも領域理論的なadmissibilityを示すのも似たようなものだろう)。

λ. Wellfounded induction in Agda2

Coqの整礎帰納法(Wellfounded induction)はどうやって実現されているのか見てみたら、accessibility predicate を定義して、それに対する通常の帰納法になっているようだった。 なるほど、整礎帰納法は accessibility predicate に関する通常の帰納法になってしまうのね。面白い。 Coqはまだ良くわからないので、とりあえずAgda2で似たようなもの(?)を書いてみる。

Rel : Set -> Set1
Rel X = X -> X -> Set

-- The accessibility predicate
data Acc {X : Set} (_<_ : Rel X) (x : X) : Set where 
  AccIntro : ((y : X) -> y < x -> Acc _<_ y) -> Acc _<_ x

-- A relation is wellfounded if every element is accessible
Wellfounded : {X : Set} -> (R : Rel X) -> Set
Wellfounded {X} R = (x : X) -> Acc R x

-- Wellfounded induction
wInd : {X : Set} -> {_<_ : Rel X} -> (wf : Wellfounded _<_) ->
       {P : X -> Set} ->
       ((x : X) -> ((y : X) -> y < x -> P y) -> P x) ->
       (x : X) -> P x
wInd {X} {_<_} wf {P} F x = f x (wf x)
  where
    f : (x : X) -> (Acc _<_ x) -> P x
    f x (AccIntro ch) = F x (\y r -> f y (ch y r))

これを length (filter p xs) ≦ length xs の証明 と組み合わせると、ようやく停止性の証明されたクイックソートが書けそうw

あと、一階述語論理と違ってCoqやAgdaで整礎性を表現できるのは、単なる不動点ではなく最小不動点を定義できるからか。一階述語論理の「Acc(x) ⇔ ∀y. y < x → Acc(y)」だと最小不動点であることを表現できないのが問題になる。

関連

• 整礎性は一階述語論理では表現できないのね - ヒビルテ(2007-12-05)

λ. DrHylo: A tool for deriving hylomorphisms

DrHylo is a tool for deriving hylomorphisms from a restricted Haskell syntax. It is based on the algorithm first presented in the paper Deriving Structural Hylomorphisms From Recursive Definitions at ICFP'96 by Hu, Iwasaki, and Takeichi. The generated code can be run with Pointless Haskell, allowing the visualization of the recursion trees of Haskell functions.

【2009-11-04 追記】 まず、ホームページにある以下の例を試してみる。

module Sample where

swap :: (a,b) -> (b,a) 
swap (x,y) = (y,x) 

data Nat = Zero | Succ Nat 

len :: [a] -> Nat 
len [] = Zero 
len (h:t) = Succ (len t)

これに対して、DrHylo -iSample.hs とすると、以下のような感じでhylomorphismの三つ組み表現で出てきて、「おー！」という感じ。

{-# LANGUAGE TypeFamilies #-}
module Sample where
import Generics.Pointless.Combinators
import Generics.Pointless.Functors
import Generics.Pointless.RecursionPatterns

swap :: (a, b) -> (b, a)
swap = app . (((curry ((snd . snd) /\ (fst . snd))) . bang) /\ id)

data Nat = Zero
         | Succ Nat

type instance PF Nat = (:+:) (Const One) Id

instance Mu Nat where
        inn (Left (_)) = Zero
        inn (Right (v1)) = Succ v1
        out (Zero) = Left (_L)
        out (Succ v1) = Right (v1)

len :: [a] -> Nat
len
  = hylo
      (_L :: Fix ((:+:) (Const One) Id))
      (app . (((curry (app . ((eithr . ((curry (inn . (inl . bang))) /\ (curry (inn . (inr . snd))))) /\ snd))) . bang) /\ id))
      (app . (((curry (app . ((eithr . ((curry (inl . bang)) /\ (curry (inr . (snd . snd))))) /\ (out . snd)))) . bang) /\ id))

ただ、以下のような関数

plus :: Nat -> Nat -> Nat
plus m Zero = m
plus m (Succ n) = Succ (plus m n)

に対しては、

plus :: Nat -> Nat -> Nat
plus = app . (((fix . (curry (curry (curry (app . ((eithr . ((curry (fst . (((snd . fst) . fst) /\ (snd . fst)))) /\ (curry (inn . (inr . (app . ((app . ((((snd . fst) . fst) . fst) /\ (fst . (((snd . fst) . fst) /\ (snd . fst))))) /\ snd))))))) /\ (out . (snd . ((snd . fst) /\ snd))))))))) . bang) /\ id)

となってしまって、hylomorphismを導出できない。 他にも色々試してみたが、思ったほどにはhylomorphismを導出できない感じ。

λ. 「最強の時間管理術」 by パク・ジョアン・スックチャ

文字通りの時間管理術を期待して聞きに行ったら、IMDの国際競争力ランキングとかワークライフバランスとかみたいな聞きあきた話がメインで、肝心の時間管理の話は手帳の使い方とかTODOリストとかの、これも良くある話だけだったので、ちょっとガッカリ。

あと、「定時退社で早く帰ってもやることがなくて困る人が多いはず」というような、大企業の仕事人間へのステレオタイプで話してたけど、聴衆にほとんどそういう反応をしている人がいなくて、ちょっと可笑しかった。定時退社で仕事が終わらなくて困るというのは分かるけど、やる事ややりたい事がなくて困るというのは正直想像がつかないな。