日々の流転

λ. 今日の論理プログラミング等

あ〜、眠い。眠いね。今日の論理プログラミングは「経路探索」について。「深さ優先探索」は簡単だけど、他の探索方法はなかなか面倒だなぁ。宣言的に読みにくいし。プロジェクト総合講座はパブリック・ポシリーの話で結構面白かったけど、睡魔には勝てず、半分くらい眠ってしまった。線形の理論は、連立1次方程式の解法とか、n次元数ベクトル空間とか、ベクトルの1次独立性について。う〜む、線形の理論は一回復習しなくちゃな。帰りに生協で色々買おうと思ってたけど、眠かったので、速攻で帰って速攻で入眠。

λ. SFC Antenna

どうしてかなと思っていたら、今井さんの方で向こうのコードを調整していたからでした。どうもです。

λ. collar

white-collarをwhite-colorだと勘違いしていた事が発覚。ひ〜ん、恥ずかしいっす。

λ. ようやく重い腰をあげて Canbe (PC-9821 Cu13) を片付けた。高校に入学した時に買ってもらったPCなので、もう6年になる。長い間ご苦労さま。これまで本当にありがとう。

λ. EAC

Windows用のCDのRipper。chicaに教えてもらう。

λ. チェーン・リアクション

を観た。

λ. BitTorrent

某氏がBitTorrentの使用許可をとっていたので、なんとなくプロトコルを調べてみる。結構単純っぽいな。

• BitTorrent: Protocol Specification
• BitTorrent プロトコル仕様書

λ. マウス

というわけで新しいマウスを買ってきた。キーボードが変わっても作業効率はあんまし変わらないけど、マウスやジョイパッドが変わると作業効率落ちまくりですYO (おいおい

λ. 憂鬱

俺って屑だな。

λ. 正則性公理

<URL:http://d.hatena.ne.jp/kururu_goedel/20060608/1149748301>

数学ではともかく計算機科学では、正則性公理が直接役に立っている話はあまり聞かないし、むしろ循環構造を素直に集合として表現出来なくなるので、計算機科学では正則性公理はあんまし嬉しくない気がします。

そのような構造として例えばストリームがあります。 ストリームを集合論で扱うには、集合Aの要素からなるストリームの全体を「S = A×S を満たす最大のS」として、0,1,0,1,… というストリームは s = (0,(1,s)) という集合で扱うのが直観的で自然だと私は思います。しかし、これは反基礎の公理(AFA, Anti-Foundation Axiom)を公理にした集合論では可能ですが、正則性公理=基礎の公理(FA, Foundation Axiom)を公理にした集合論では不可能ですし。まあ、S = A×S ではなく S ≅ A×S に弱めれば正則性公理にも矛盾しないので、本質的な問題というよりはむしろ利便性の問題と思いますが。

おまけ

『反基礎の公理』について書こうとしたら、Myブログ軍師に「我が君･･･。『反基礎の公理』についてですか？　炎上も覚悟の上でしょうな 」と言われたので、やめておく。

追記 (2006-06-20)

くるるの数学ノート - Antifoundation で、Aczelの『Non-well-founded sets』のPDFが公開されていることを知った。原典は向井先生の本棚にあったのをパラパラめくったことしかなかったので、後でちゃんと読んでみたいところだ。

それから、かがみさんの日記に以下のように書かれていた。「推移的崩壊」(transitive collapse)って何だろう。

Axiom of regularity に関してもちょっと書きたいことありなのですが、ぼろぼろになりそうなので今度機会があったら...。ただし、AFA を認める立場で Axiom of regularity が adhoc であるという批判 は成り立たないと思います(もちろん nuc さんが AFA を認めないというなら話は別ですが)。明らかに AFA の方が adhoc だと思うし、そもそも Axiom of regularity からのアイディアと思われる「推移的崩壊」をちゃっかり借用してるし。

fj.sci.math のこのスレッドには以下のように書かれていて、transitive collapse というのは Mostowski's collapsing lemma に関係した概念のような気がするが…… Mostowski's collapsing lemma 自体よく知らないのでした……とほほ。

「うそつき」では、AFA のことを、「Mostowski の Collapsing Lemma を、グラフが well-founded という仮定をはずした形に拡張したようなものだ」というような感じ(この通りの書き方ではない)で説明していました。これはちょっと公理的集合論を知っている人にはわかりやすい説明だと思います。

追記 (2006-06-21)

<URL:http://en.wikipedia.org/wiki/Mostowski_collapse> 読んで、Mostowski's collapsing lemma がどういうものか少し分かってきた。

λ. 『ハツカネズミの時間』 冬目 景

閉塞感を淡々と描いているという印象を受けた。

λ. サンタクロース問題

最近、コードを全然書いていなかったのでリハビリのつもりでやってみた。 とりあえず、Concurrent Haskell + STM で安直に。 出力はかなり手を抜いていて、複数のスレッドの出力が混ざったりと散々w

module Main where

import Control.Monad
import Control.Concurrent
import Control.Concurrent.STM
import System.Random
import System.IO

main :: IO ()
main =
    do hSetBuffering stdout LineBuffering
       reindeerCh <- newTChanIO
       elfCh <- newTChanIO
       mapM_ (forkA reindeerCh) ["Reindeer("++show n++")" | n <- [1..9]]
       mapM_ (forkA elfCh) ["Elf("++[c]++")" | c <- ['A'..'J']]
       forkIO $ sequence_ $ repeat $ join $ atomically $ msum $
           [ do xs <- readN 9 reindeerCh
                return $ do putStrLn "Santa Claus goes with reindeers."
                            randomWait
                            mapM_ (flip putMVar ()) xs
           , do xs <- readN 3 elfCh
                return $ do putStrLn "Santa Claus solves elve's problem."
                            randomWait
                            mapM_ (flip putMVar ()) xs
           ]
       getChar
       return ()

forkA :: TChan (MVar ()) -> String -> IO ThreadId
forkA ch s =
    do v <- newEmptyMVar
       forkIO $ sequence_ $ repeat $
           do randomWait
              putStrLn (s ++ " comes.")
              atomically $ writeTChan ch v
              takeMVar v
              putStrLn (s ++ " goes away.")

randomWait :: IO ()
randomWait = randomRIO (500000, 2000000) >>= threadDelay

readN :: Int -> TChan a -> STM [a]
readN n = sequence . replicate n . readTChan

【追記】 らくがきえんじん(2007-06-09) でsyd_sydさんがこのコードについて解説してくださっているので、こちらもどうぞ。

λ. 『位相と論理』

先日 Topology via Logic も一応読み終わったし、似たようなタイトルということで『位相と論理 (日評数学選書)(田中 俊一)』に手を出してみる。 今日は、第一章「順序と束」を読んだ。環論についてよく知らなかったので、ブール代数のイデアルとブール環のイデアルの対応を丁寧に追っていたら、思ったよりも手間取ってしまった。

λ. “A constructive proof of equivalence of formalism od DCG's with the formalism of type 0 phrase-structure grammars” by Marica D. Prešić and Slavisa B. Prešić

We present a proof that definite clause grammars (DCG's) are equivalent in their generative power to type 0 phrase-structure grammars. The proof is constructive and it actually describes an algorithm for transferring from a language description by type 0 grammar to DCG characterization. The proof has been inspired by the proof given in [MA93] but our approach is considerably simpler and the constructed DCG grammar is much more efficient. The paper also suggests how computer implementation of the algorithm can be developed.

以前にTwitterで「DCGの言語クラスはtype-0」と書いたときに持ち出した論文を読んだ*1。 記法がよく分からないのだけど、引数の項で記号列を持って、書き換え規則を全て引数の項を書き換える形の規則にするということか。 そうすると、確かに0型文法をDCGで表現すること自体は自明だが、そのままだとProlog等の深さ優先でのSLD導出じゃちゃんと列挙出来ないのでは?*2

λ. 風神録Normalを魔理沙(B)で初クリア

世間はすっかり新作だと思うけど、そういえばまだ風神録あんまりやってなかったなぁと思い、まだNormalをクリアしてなかった魔理沙(貫通装備)でNormalをクリアしてみた。 久しぶりなこともあって、いつも以上にボロボロ。

th10_04.rpy

東方風神録 リプレイファイル情報
Version 1.00a
Name hiro    
Date 08/06/08 23:22
Chara MarisaB
Rank Normal 
Stage All Clear
Score 29768812
Slow Rate 0.18