2001-11-01
λ. うー。1時間ちょいしか寝れなかった。しんどー
λ. Windows版Rubyでシンボルがexportされる仕組み
なるほど。.defファイルを自動生成してるのですか。それなら納得です。ちなみに僕が「拡張ライブラリ側」と書いたのは、ruby〜.dllのシンボルをimportする側って事っす。
拡張ライブラリで.defを用意できるようになったのは[ruby-ext:01664]のスレッドの話で、たしか1.6.5には入ってたと思います。
λ. 情報数学Ⅰ
休講。めずらしい。
λ. 朝鮮語
明日ワークショップなのに殆ど準備が出来てない…やばいっす。しかも、来週の火曜は中間試験。こっちもやばーい。
λ. 帰納論理プログラミング
演習の続き。古川先生と雑談してたら何も出来ずに時間が終ってしまった。
λ. 研究会
運賃表の話はあっさり終って、FFSについての発表など。
λ. wstring
[ruby-list:32032]には誰も反応してないけど結構良い感じだと思う。それと、codecvt_byname<wchar_t,char,mbstate_t>クラスを使うと、global localeを汚さずに、任意のlocaleでmbとwcとの変換が出来て良いかもしれないと思った。
2002-11-01
λ. 言語の意味論
無駄に徹夜して中間レポートを書き上げて提出。
遅刻してしまったので、一般限量子(generalized quantifier)の話を聞き逃してしまった。
内包論理ILのモデル論は簡単。
λ. 『ラブやん (1)』 田丸浩史
を読んだ。「痛い漫画」らしい。
λ. Java/C++ integration
を読んだ。大体は想像した通りだった。
λ. Plan9
LinuxWorldの付録CDから起動して遊ぶ。ipconfigでDHCPからIPアドレスを取得してきてくれる。特にすることもないので、とりあえずvtでsshして(以下略)
λ. vnode
について質問してみるみる。saimuneさんに訊くのが一番なんだろうけど、入れ違いになってしまって訊けなかった。
λ. ukasiewicz の公理系
Łukasiewicz (ウカシェヴィッチ) の公理系の話とか。
λ. 夕食
倉吉
λ. 帰り
バスで寝過ごした。帰ったら速攻で寝た。
λ. ディレクトリ構造を理解してるやつはオタだ
「ディレクトリ構造を理解してるやつはオタだ」 by chiko
2004-11-01
λ. Re: 正格性解析
sum' = foldl (+) 0 がIntやIだと余計なメモリを食わず、Integerだと余計なメモリを食ってしまう理由ですが、原因はfoldlがインライン展開されるかどうかの違いですね(GHC 6.2.1 で確認)。IntやIだとfoldlがインライン展開されて、(+)の正格性に基づいた最適化がされてます。それにしても、なんでIntegerだとfoldlがインライン展開されないんだろう……
それはそうと、以下の3つの型は領域(domain)が同型なので、add (I x) (I y) = I (x + y) とかは(少なくとも理論的には)無意味だと思います。
data I = I !Integernewtype I = I IntegerInteger
[追記] あうぅ。領域が同型であっても、newtypeとdataではパターンマッチの方のセマンティクスが違うのを忘れてました(Haskellはややこしいなぁ)。(+)がもし仮に非正格でも、この方法で定義したaddは正格になるので、意味はありますね。すんまそん。
λ. 風邪
先週末から少し調子悪いなと思ってたら、風邪をひいてしまった。今日が慶早戦による休講で助かった。
2005-11-01
λ. Wang's Algorithm
ふと、Wang's Algorithm (ワンのアルゴリズム) を素朴に書いてみた。 が、イマイチ。
import Control.Monad (guard,msum)
import Data.List (intersect)
import Data.Maybe (isJust, listToMaybe)
data Formula x
= Atom x
| Not !(Formula x)
| Imply !(Formula x) !(Formula x)
| And !(Formula x) !(Formula x)
| Or !(Formula x) !(Formula x)
deriving Eq
type Sequent x = ([Formula x], [Formula x])
isValid :: Eq x => Sequent x -> Bool
isValid = isJust . isValid'
isValid' :: Eq x => Sequent x -> Maybe ()
isValid' (l,r) =
do xs <- listToMaybe $ msum $
[ do let i = intersect l r
guard $ not $ null i
return []
, do (Not p, r) <- pick r
return [(p:l,r)]
, do (Not p, l) <- pick l
return [(l,p:r)]
, do (Imply p q, r) <- pick r
return [(p:l,q:r)]
, do (Or p q, r) <- pick r
return [(l,p:q:r)]
, do (And p q, l) <- pick l
return [(p:q:l,r)]
, do (Or p q, l) <- pick l
return [(p:l,r), (q:l,r)]
, do (And p q, r) <- pick r
return [(l,p:r), (l,q:r)]
, do (Imply p q, l) <- pick l
return [(q:l,r), (l,p:r)]
]
mapM_ isValid' xs
return ()
pick :: [x] -> [(x,[x])]
pick [] = []
pick (x:xs) = (x,xs) : [(y,x:ys) | (y,ys) <- pick xs]
λ. IT System: SVG with constraints (CSVG)
メモ。
- <URL:http://www.www2004.org/proceedings/docs/2p310.pdf>
- <URL:http://www.csse.monash.edu.au/~clm/csvg/>
ところで、Googleはすごいなぁ
λ. SML#
Zeta版って……(笑
2006-11-01
λ. *-autonomous category
これまで「名前からしてきっと難しいに違いない! クワバラクワバラ」とか思って近づいていなかったんだが、檜山さんの「論理とはなにか？ (4:完) -- 論理から圏へ」で出てきたので調べてみたら、単に symmetric monoidal closed category に dualizing object ⊥ を追加しただけだった。拍子抜けした……
2007-11-01
λ. WikiCFP
直江さんが「今までに見つけた中で一番究極なCFP List」 と絶賛していたので試してみるが、便利さはまだよく分からない。 とりあえず、Calls For Papers on Programming Languages のフィードは Google Reader に登録しておこう。
2008-11-01
λ. 防衛相、現役空幕長を更迭 政府見解に反すると判断
アパグループ第一回「真の近現代史観」懸賞論文募集 から田母神俊雄氏の「日本は侵略国家であったのか」を読んでみたけど、論文というよりはエッセイとかそういった部類のものだと思った。 同意できる部分もあるけど、全体としてはかなり微妙。
田母神俊雄氏のしたことは非常に軽率な行動だし、「防衛省は職員が外部に職務に関する意見を発表する際、書面による届け出を義務づけているが、田母神氏は届け出ず防衛相は知らなかった」ということで内規違反ということなら、まあ更迭も仕方がないかなと思う*1。
関連
*1 ただ、入学式・卒業式での日の丸・君が代問題で、職務命令に反した教師への処分を思想・良心の自由を理由に批判していた人たちは、同じ理由から今回の処分も批判すべきだろう。
ψ 小澤 [std::localeとstd::codecvtでやろうと思ったんですけど、gcc 2.9xのlibstdc++には..]