2001-11-28
λ. 本日の現実逃避
- [ruby-ext:2005]
- WStringへのパッチ二つ
- wstring-wctrans.diff
- WString#transformという名前でtowctransのラッパーを作ってみました。"tolower"と"toupper"以外のマッピング名は実装依存なのですが、例えば、glibc2.2ならばWString.new('おはよう').transform('tojkata') #=> L"オハヨウ" というような事も出来ます。
- wstring-casecmp.diff
- WString#casecmpの実装。最初はwcsicmpかwcscasecmpが使える場合はそちらを使おうかと思ったのですが、これくらいなら自前で持った方が良いかなという気がして来たので、have_funcによるチェックはコメントアウトしてあります。
- mo.rb
- 書き込みをサポート
- Yet Another GetText
- mo.rbを使用したgettextもどき
2002-11-28
λ. 夢
不死の ゾッド(人間形態)にチェーンソーで襲われる夢- 夜の都市を飛び回る夢。空を飛ぶ夢は浮遊感が気持良い。 ただ、何故か知らないけど地上から大量に銃撃されてたけど。
λ. 予算編成論
来年の1/16の授業が田中康夫の講演になるそうです。
λ. 偏頭痛
偏頭痛がする。あらゆる事にイライラする。病的で破滅的な妄想が頭から離れない。こんな自分は嫌いだ。
λ. E.Moggi
MoggiのThe Partial Lambda-Calculus. に PhD thesis, University of Edinburgh, 1988 と書いてあったので、ひょっとして萩野先生と面識があるのではないかと思って萩野先生に訊いてみたらビンゴだった。ま、どうでも良いけど。
λ. レッシグたんのお話@東大ビジネスローセンター
を読んだ。
λ. ホームページのウンザリ度鑑定
憂鬱な昨日に猫キック 不安な明日に猫パンチ (2002-11-26) より。知り合いのサイトとかを鑑定してみるも、みんな0点なのでつまらないなぁ。
2003-11-28
λ. 学校に行く途中で、バスがバス停に止まり忘れてUターンしてた。
λ. 借りた本
- 『容赦なき戦争 ─ 太平洋戦争における人種差別』
- ジョン・ダワー (John W. Dower) [著] 猿谷 要, 斉藤 元一 [訳]
- 『国益とは何か』
- 今野 耿介 [著]
λ. A topological sum of localic systems is still localic.
Topology via Logic (p.79) の「A topological sum of localic systems is still localic.」の証明で、「To show that pt p is onto, take z ∈ pt Loc(∑λDλ). Then z ⊨ true = ∨λjλ(true), so for some μ, z ⊨ jμ(true).」の後の「It follows that if λ≠μ then z ⊭ jλ(true).」がどうやって導かれるのか2週間前から悩んでいたのだけど、ようやく解決した。
λ≠μ で z ⊨ jμ(true) かつ z ⊨ jλ(true) ならば、z ⊨ jμ(true)∧jλ(true) = false であり、これは矛盾。
2004-11-28
λ. "top-downのmemoization" と histomorphism
"top-downのmemoization" の一引数の場合というのは、V. Vene. Categorical programming with inductive and coinductive types.(2004-06-29の日記参照) の histomorphism に非常に近いなぁと思った。
まず、yts氏による定義は以下のようなものだった。
fib :: Int -> Int fib = memo1 ( xs -> case n of 0 -> 0 1 -> 1 _ -> xs !! 1 + xs !! 2) memo1 :: (Int -> [a] -> a) -> Int -> a memo1 f n = head $ memos1 f n memos1 :: (Int -> [a] -> a) -> Int -> [a] memos1 f n = rs where rs = m n rs m n ~xxs@(x:xs) = (f n xxs):m (n - 1) xs
これは少し複雑なので単純化する。
memos1
の f n xxs
に注目すると、
xxs
の先頭要素はf n xxs
自身になっているが、この先頭要素は普通使われないので、xxs
の代わりにxs
を渡すことにしよう。- 負の定義域を考慮しているためか、
xs
は無限リストになっている。定義域を自然数に限定してxs
を有限のリストにしてしまおう。 - そうすると、
xs
の長さからn
の情報が復元できるので、n
もパラメータとして渡す必要はない。
そうして単純化して少し書き換えると、以下の様な定義が得られる。
fib :: Int -> Int fib = histo phi where phi [] = 0 phi [_] = 1 phi (a:b:_) = a+b histo :: ([a] -> a) -> (Int -> a) histo phi = head . f where f 0 = phi [] : [] f (n+1) = phi xs : xs where xs = f n
正確な定義は省くが、このfib
のように定義されている関数はhistomorphismと呼ばれる。これは(Intで表現された)自然数に関するhistomorphismだけど、histomorphismの概念はリストや木といった帰納的なデータ型一般に適用することが出来る。前述の V. Vene. Categorical programming with inductive and coinductive types. ではpolytypicなhisto
を使ってfib
を以下のように定義していた。これも詳細は省くけど、対応しているのが分かると思う。
fib :: Nat -> Int fib = histo phi where phi Z = 0 phi (S x) = case tlCV x of Z -> 1 S y -> hdCV x + hdCV y
(2005-09-04 追記) ちなみに、Category extras パッケージ を用いると以下のようになる。やっていることは同じなのだけど、histoの型が「Fixpoint f t => (f (Strf f a) -> a) -> t -> a」になっていて、また「instance Fixpoint Maybe Int」と定義されているので、引数の型がNatではなくIntになっている。
import Control.Recursion import Data.BranchingStream fib :: Int -> Int fib = histo phi where phi Nothing = 0 phi (Just x) = case tlf x of Nothing -> 1 Just y -> hdf x + hdf y
2005-11-28
λ. Michael Tiemann がSFCにくるらしいよ
明日二限の情報リテラシーの授業でマイケル・ティーマン(Michael Tiemann)が講演するそうだ。教室はε22。
2006-11-28
λ. Agate—an Agda-to-Haskell compiler by Hiroyuki Ozaki, Makoto Takeyama and Yoshiki Kinoshita
を読んだ。型システムの違いをどう吸収するのかを期待していたら、untypedなものに変換してしまっていた。変換はHOASに基づいたstraightforwardなもの。AgateでHaskellに変換してGHCでコンパイルしたものは、GHCで直接コンパイルしたものに比べて、2倍〜6倍の実行時間。
λ. 今日のITシステム
- SVG関係で研究になりそうなことはあるか?
- 太田メソッド「スライドがないなら、発表しながら作れば良いじゃない」
- Bloom filter
2007-11-28
λ. SNS型英語学習サイト iKnow!
iKnow! は語学を学ぶ人のための、パーソナル学習アプリケーションを搭載したコミュニティーサイトです。脳科学に基づいて開発されたラーニング・エンジンが、あなたの学習パフォーマンスをすべてトラッキング。 最適な学習プランを自動的に提供するという画期的、かつ効果的な方法で、英語を学習していきます。
とおる。さんのところより。 早速登録してみた(http://www.iknow.co.jp/user/sakai)けど、結構良さそう。 ただ、問題なのは続くかどうかなんだよな。 僕の英語学習で続いてるのはESLPodだけで、他は英語漬けも単語力もNPRも英語日記もぜーんぶ続いてないからなぁ。
2008-11-28
λ. グーグル、絵文字を世界共通化へ—オープンソースプロジェクト開始
素晴らしい! しかし、グーグルのような会社が手を出すまで、誰もこういった取り組みをきちんとやろうとはしていなかったのは、やっぱりキャリア主導の垂直統合モデルの負の面じゃなかろうかと思う。
2009-11-28
λ. 『数学』を数学的に考える
某所で紹介されていたので、読んでみた。扱っている内容は以前に読んだ「算術的階層の厳密性と形式的手法の限界について」とほぼ同じなのかな。
帰納法をΣn論理式に制限した IΣn というのが出てくるのだけど、これが有限公理化可能と書いてあって驚く。 そのことをTwitterに書いたら、ytbさんが「Hajek-Pudlakのp78に載ってます(定理2.52)。Σn論理式に関する真理述語を使うと、IΣ1の有限部分理論において、Σn論理式をそのゲーデル数と同一視でき、Σn帰納法の公理図式を一つの公理として表現できるとか。」とサクっと答えてくれて、「おお、なるほどー」と思った。 もっとも、これが気になった理由は、有限公理化出来ると定理証明器的に嬉しいのではと思ったためだったので、Σn論理式に関する真理述語を使うとなると全然嬉しくなさそうだけどね。
それと、照井先生は「文レベルの局所的な循環性ではなく、対象数学とメタ数学の大域的な循環性に目を向けるべき」と言っていて、そういえばこないだの数学基礎論サマースクール2009の Cut-elimination and Algebraic Completion でも「個別に論理を作ってカット除去とかを証明してというのではなくて、そもそも証明論の限界とは?」という話をしていたのを思い出す。 すごく大域的な視野というかビジョンを持って数学をしている感じがして、やはり凄いと思った。
2013-11-28
λ. nonlinear-optimizationパッケージで遊ぶ
「自動微分を使って線形回帰をしてみる」の続きで、最急降下法を自分で書いてみるかと思ったのだけれど、そういえばHackageにnonlinear-optimizationパッケージというのがあったのを思い出した。以前から、一回試してみたいと思っていたパッケージだったので、せっかくなのでこれを試してみる。 試してみるバージョンは現時点での最新版の0.3.7で、Hager and Zhang *1 のアルゴリズムを同著者らが実装したCG_DESCENTライブラリのバインディングが提供されている。
nonlinear-optimizationパッケージのAPIはadパッケージのgradientDescent関数に比べるとちょっと面倒臭いAPIだけれど、前回のコードを書き換えてみたのが以下のコード。 nonlinear-optimizationパッケージは自動微分とかはしないので、勾配を計算する関数を明示的に渡す必要があり、adパッケージのgrad関数で自動微分した結果の関数を渡すようにしてある。
module Main where import Control.Monad import qualified Data.Vector as V import Numeric.AD import qualified Numeric.Optimization.Algorithms.HagerZhang05 as CG import Text.Printf import qualified Text.CSV as CSV main :: IO () main = do Right csv <- CSV.parseCSVFromFile "galton.csv" let samples :: [(Double, Double)] samples = [(read parent, read child) | [child,parent] <- tail csv] -- hypothesis h theta x = (theta V.! 0) + (theta V.! 1) * x -- cost function cost theta = mse [(realToFrac x, realToFrac y) | (x,y) <- samples] (h theta) (theta, result, stat) <- CG.optimize CG.defaultParameters{ CG.printFinal = True, CG.printParams = True, CG.verbose = CG.Verbose } 0.0000001 -- grad_tol (V.fromList [0::Double,0]) -- Initial guess (CG.VFunction cost) -- Function to be minimized. (CG.VGradient (grad cost)) -- Gradient of the function. Nothing -- (Optional) Combined function computing both the function and its gradient. print theta -- mean squared error mse :: Fractional y => [(x,y)] -> (x -> y) -> y mse samples h = sum [(h x - y)^(2::Int) | (x,y) <- samples] / fromIntegral (length samples)
で、これを実行してみると……
PARAMETERS: Wolfe line search parameter ..................... delta: 1.000000e-01 Wolfe line search parameter ..................... sigma: 9.000000e-01 decay factor for bracketing interval ............ gamma: 6.600000e-01 growth factor for bracket interval ................ rho: 5.000000e+00 growth factor for bracket interval after nan .. nan_rho: 1.300000e+00 truncation factor for cg beta ..................... eta: 1.000000e-02 perturbation parameter for function value ......... eps: 1.000000e-06 factor for computing average cost .............. Qdecay: 7.000000e-01 relative change in cost to stop quadstep ... QuadCufOff: 1.000000e-12 factor multiplying gradient in stop condition . StopFac: 0.000000e+00 cost change factor, approx Wolfe transition . AWolfeFac: 1.000000e-03 restart cg every restart_fac*n iterations . restart_fac: 1.000000e+00 stop when cost change <= feps*|f| ................. eps: 1.000000e-06 starting guess parameter in first iteration ...... psi0: 1.000000e-02 starting step in first iteration if nonzero ...... step: 0.000000e+00 factor multiply starting guess in quad step ...... psi1: 1.000000e-01 initial guess factor for general iteration ....... psi2: 2.000000e+00 max iterations is n*maxit_fac ............... maxit_fac: 1.797693e+308 max expansions in line search ................. nexpand: 50 max secant iterations in line search .......... nsecant: 50 print level (0 = none, 2 = maximum) ........ PrintLevel: 1 Logical parameters: Error estimate for function value is eps Use quadratic interpolation step Print final cost and statistics Print the parameter structure Wolfe line search ... switching to approximate Wolfe Stopping condition uses initial grad tolerance Do not check for decay of cost, debugger is off iter: 0 f = 4.642373e+03 gnorm = 9.306125e+03 AWolfe = 0 QuadOK: 1 initial a: 1.070618e-04 f0: 4.642373e+03 dphi: -8.662251e+07 Wolfe line search iter: 1 f = 5.391563e+00 gnorm = 3.269753e-02 AWolfe = 0 QuadOK: 1 initial a: 1.632104e+01 f0: 5.391563e+00 dphi: -1.069411e-03 Wolfe line search RESTART CG iter: 2 f = 5.387312e+00 gnorm = 1.558689e+01 AWolfe = 1 QuadOK: 0 initial a: 3.264209e+01 f0: 5.387312e+00 dphi: -2.430188e+02 Approximate Wolfe line search iter: 3 f = 5.374303e+00 gnorm = 3.196800e-02 AWolfe = 1 QuadOK: 1 initial a: 3.559386e+00 f0: 5.374303e+00 dphi: -1.022238e-03 Approximate Wolfe line search RESTART CG iter: 4 f = 5.288871e+00 gnorm = 2.808049e-02 AWolfe = 1 QuadOK: 1 initial a: 2.376426e+01 f0: 5.288871e+00 dphi: -7.887345e-04 Approximate Wolfe line search iter: 5 f = 5.279499e+00 gnorm = 1.301306e+01 AWolfe = 1 QuadOK: 0 initial a: 4.752853e+01 f0: 5.279499e+00 dphi: -1.693871e+02 Approximate Wolfe line search RESTART CG Termination status: 0 Convergence tolerance for gradient satisfied maximum norm for gradient: 5.513258e-09 function value: 5.000294e+00 cg iterations: 6 function evaluations: 15 gradient evaluations: 11 =================================== fromList [23.941530180694265,0.6462905819889333]
今度は一瞬で収束した! やった!
*1 Hager, W. W. and Zhang, H. A new conjugate gradient method with guaranteed descent and an efficient line search. Society of Industrial and Applied Mathematics Journal on Optimization, 16 (2005), 170-192.