トップ «前の日(11-27) 最新 次の日(11-29)» 追記

日々の流転


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もどき
Tags: ruby

2002-11-28

λ.

  • 不死の(ノスフェラトゥ)ゾッド(人間形態)にチェーンソーで襲われる夢
  • 夜の都市を飛び回る夢。空を飛ぶ夢は浮遊感が気持良い。 ただ、何故か知らないけど地上から大量に銃撃されてたけど。

λ. 予算編成論

来年の1/16の授業が田中康夫の講演になるそうです。

λ. 偏頭痛

偏頭痛がする。あらゆる事にイライラする。病的で破滅的な妄想が頭から離れない。こんな自分は嫌いだ。

λ. E.Moggi

MoggiのThe Partial Lambda-Calculus. に PhD thesis, University of Edinburgh, 1988 と書いてあったので、ひょっとして萩野先生と面識があるのではないかと思って萩野先生に訊いてみたらビンゴだった。ま、どうでも良いけど。

λ. 龍田真さん

proof.styの作者って、『型理論』の著者の龍田真さんだったのか。Moggiの事といい「世間って案外狭いのかも」と今日は少し思った。

λ. ホームページのウンザリ度鑑定

憂鬱な昨日に猫キック 不安な明日に猫パンチ (2002-11-26) より。知り合いのサイトとかを鑑定してみるも、みんな0点なのでつまらないなぁ。


2003-11-28

λ. 学校に行く途中で、バスがバス停に止まり忘れてUターンしてた。

λ. 借りた本

『容赦なき戦争 ─ 太平洋戦争における人種差別』
ジョン・ダワー (John W. Dower) [著] 猿谷 要, 斉藤 元一 [訳]
『国益とは何か』
今野 耿介 [著]

小熊さんに紹介された『容赦なき戦争』を借りてきた。

Tags:

λ. 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

これは少し複雑なので単純化する。 memos1f 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
Tags: haskell

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システム

Tags: tom

2007-11-28

λ. SNS型英語学習サイト iKnow!

iKnow! は語学を学ぶ人のための、パーソナル学習アプリケーションを搭載したコミュニティーサイトです。脳科学に基づいて開発されたラーニング・エンジンが、あなたの学習パフォーマンスをすべてトラッキング。 最適な学習プランを自動的に提供するという画期的、かつ効果的な方法で、英語を学習していきます。

とおる。さんのところより。 早速登録してみた(http://www.iknow.co.jp/user/sakai)けど、結構良さそう。 ただ、問題なのは続くかどうかなんだよな。 僕の英語学習で続いてるのはESLPodだけで、他は英語漬けも単語力もNPRも英語日記もぜーんぶ続いてないからなぁ。

Tags: 英語

2008-11-28

λ. グーグル、絵文字を世界共通化へ—オープンソースプロジェクト開始

素晴らしい! しかし、グーグルのような会社が手を出すまで、誰もこういった取り組みをきちんとやろうとはしていなかったのは、やっぱりキャリア主導の垂直統合モデルの負の面じゃなかろうかと思う。

Tags: 時事

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 でも「個別に論理を作ってカット除去とかを証明してというのではなくて、そもそも証明論の限界とは?」という話をしていたのを思い出す。 すごく大域的な視野というかビジョンを持って数学をしている感じがして、やはり凄いと思った。

Tags: logic


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.