日々の流転

λ. どっかの国の議会で核テロを実行する夢を見ました。まる。

λ. 読んだ本

『GUILTY GEAR X 4コマKINGS VOL.2』

秋月しょう, 石, 加曽利あおりんご, 草薙 明, 神武ひろよし, 左澤一威, スミノヒルネ, せつらりま, 銭形たいむ, 辰巳 仁, なかべ江, 破弓 翔, 濱谷 涼, 真島 圭, 人参So., 望月和臣[著]

『常習盗賊改め方　ひなぎく見参!　3』

桜野みねね[著]

λ. 夢

夏の暑い日に海岸に遊びに行ったら、小さな卵のようなものを見つけた。海水と砂と一緒に水槽に入れて持ち帰ったら、数日して卵がかえって、小さな亀が水槽のなかを泳いでいた。

λ. 웃지않는 수학자 (その2)

以前に『笑わない数学者』韓国版が見つからないと書いたが、aladdin.co.krで探したら見つかった。だからどうだと言うわけではないのだけど。

λ. tdiary-mode

を使いはじめる。便利だ。

λ. 夕食

김치 찌개 (きむち ちげ)

λ. Digest認証

現在のweb.sfc.keio.ac.jpではDigest認証は使えないのか。

λ. 自動定義されるメソッド

Ruby-GNOME2ではプロパティにアクセスするメソッドなどは実行時にリフレクション機能を使って定義してる。当然これらのメソッドの定義はソースコード上には直接は現れない。で、これらの機能が実装されていないと勘違いしてパッチを送ってくる人が後を絶たないのだ。これにはちょっと、う・ん・ざ・り。HACKINGみたいなファイルを作って、そこに注意を書いておくべきか。

λ. Practical Foundations of Mathematics

Digital Nietzsche(2003-10-17) より。こういうのがWebで公開されているのは本当にありがたい。Algebra with Dependent Types なんて興味をそそられるじゃないですか。

λ. Proofs and Types

0521371813 同じく Digital Nietzsche(2003-10-17) より。

λ. ESLPod (English as a Second Language Podcast)

登録してみた。

• English as a Second Language Podcast
• TOEFL Podcast
• English Through Stories

【2006-07-26追記】 mixiでESLポッドキャスト攻略法というコミュニティを発見。

λ. 姉ちゃんにふくしゅうを

なんか研究室で話題になってたので読んでみた。 ネタかリアルか知らないけどVIPPERってすごいね、と思った。 もし実話だったらお幸せに。

λ. Partial co-recursive functions, Yves Bertot

• <URL:http://types2004.lri.fr/abstracts/abstract11.txt>
• <URL:http://types2004.lri.fr/SLIDES/bertot.pdf>

を読んだ。Guarded corecursion について大体理解できた。

λ. 第 315 回 PTT

に行ってきた。

• <URL:http://www.ipl.t.u-tokyo.ac.jp/~kaz/ptt/arc/315/315.html>
• soyBasic

メモ

• 携帯の文字入力
  • 普通の文章を打つには快適
  • プログラムを打つにはちょっと……
  • プログラミング言語のreduncuncy
  • 規則性が高いのでそういうのに特化した入力方式があるといいかも?
• SOY BASIC
  • 携帯で動くBASICは他にもあるが、行番号がないのが許せない
  • BASICというからには、変数はやっぱり一文字なの?
    • さすがに違う。
    • 作者が最初にBASICをさわったときは二文字だった
• 「1から0までのキー」という言い方が面白い
• 携帯のキーは同時押しは出来るのか?
  • あんまし
• 変数の候補をだす
  • 9がwxyz, 8が...
  • ワンタッチ入力
• 間違えて入れたのも辞書に登録されてしまう
• BASICで使いそうなのを最初から登録しておくとかは考えなかったのか?
• 補完
  • いきなり変数名を打つと、イコールがでてきて、代入文になる
  • 配列だと分かっている場合には、それようのがでてくる
    • 二次元配列にはまだ対応していない。
• 実装
  • iアプリ
  • FOMAの一個前のバージョンの携帯
  • ムーバの一番新しいやつでも動く
  • 30Kになんとか収めた
    • jarファイル圧縮ツール
    • 28K
• どこに保存されているか?
  • ウェブサーバに保存される
    • 認証を何もしていないw
    • セキュリティは(ry
  • 携帯のメモリにも保存可能
    • スクラッチパッド
    • 名前をつけないで保存するとスクラッチパッドに
    • FOMA専用になったら、複数のファイルをちゃんと扱えるように
• なぜBASICなのか?
  • 制限が厳しい言語
  • 式文が存在しない
  • 入力できるものに制限がいっぱい
  • 補完しやすい
  • すべての命令が固定 = 書式が網羅できる
  • 処理系が単純
  • 正しいBASICの保護活動 ;-)
• これを使ってソフトを書いてみた
  • いまのところはゲームくらい
  • ちゃんと携帯で入力した
• ベンチマーク
  • 入力が遅いという問題はどれくらい解決できたか?
  • 普通に携帯でいれた場合と、PCでいれた場合とで比較
  • 「携帯で自然言語を入力する際のロス > 携帯でプログラムを入力する際のロス」なら良いのではないか? (比較優位)
    • 効率だけでなくモチベーションは? (e.g. 彼女にメール書く)
    • PCで入力する場合との時間の比: 日本語 6.8倍 > SOY BASIC 2.6倍
    • 勝った!　日本語を入力するよりはるかに快適!
    • 眉唾なところ
      • 作者本人が入力している。
      • 作者は携帯であまり文章を打たない。
      • 女子高生に打たせたらどうなるか?
  • 入力している途中で内容を忘れちゃうのでは?
• 議論
  • 目指すは携帯版eclipse
• ...

λ. Type Theory with First-Order Data Types and Size-Change Termination, David Wahlstedt

• <URL:http://types2004.lri.fr/abstracts/abstract59.txt>
• <URL:http://types2004.lri.fr/SLIDES/wahlstedt.pdf>

Size-Change Termination (SCT) 面白い。

λ. Categorical Semantics of Linear Logic For All by Valeria de Paiva

線形論理の圏論的なモデルに関して良くまとまっている。 また、論理の圏論的なモデルがどういうものかを知るにも良いと思う。

良く分からなかった部分

• 「categorical duality will produce a model of classical linear logic from one of intuitionistic linear logic, automatically.」という部分。
• DILL category に関する話での「Function spaces in the cartesian category can be induced from the linear ones.」の部分。
  • Andrew Graham Barber の Linear Type Theories, Semantics and Action Calculi や Dual Intuitionistic Linear Logic あたりを読めばよいのだろうけど……
• セオリーの圏に関係する部分。

λ. 米田の補題と多相ラムダ計算

米田の補題の話をしていたので、多相ラムダ計算で対応するものを示してみる。

任意の F:*→* と C:* とが与えられていて、mapF: ∀X:*, Y:*. (X→Y)→(F X → F Y) が関手の条件を満たすとする。(∀X:*. (X → C) → F X) ≅ F C を示す。

id : ∀X:*. X→X
id = (ΛX:*. λx:X. x)

Φ : (∀X:*. (C→X) → F X) → F C
Φ = λα:(∀X:*. (C→X) → F X). α C (id C)

Ψ : F C → (∀X:*. (C→X) → F X)
Ψ = λx:F C. ΛX:*. λf:C→X. mapF C X f x

λα:(∀X:*. (C→X) → F X). Ψ (Φ α)
= {- β reduction -}
  λα:(∀X:*. (C→X) → F X). ΛX:*. λf:C→X. mapF C X f (α C (id C)) 
= {- parametricity -}
  λα:(∀X:*. (C→X) → F X). ΛX:*. λf:C→X. α X (λc:C. f (id C c)
= {- β reduction and η conversion -}
  λα:(∀X:*. (C→X) → F X). ΛX:*. λf:C→X. α X f
= {- η conversion -}
  id (∀X:*. (C→X) → F X)

λx:F C. Φ (Ψ x)
= {- β reduction -}
  λx:F C. mapF C C (id C) x
= {- functor law -}
  λx:F C. id (F C) x
= {- η conversion -}
  id (F C)

λ. 東方風神録、封印装備でノーマルクリア

封印装備でもクリア(th10_02.rpy)。 相変わらずボロボロ。No.59 秘術「グレイソーマタージ」は一応とれた。

東方風神録 リプレイファイル情報
Version 1.00a
Name hiro    
Date 07/10/27 16:35
Chara ReimuC 
Rank Normal 
Stage All Clear
Score 32824661
Slow Rate 0.31

λ. Amazon.co.jp、3000円以上の和書ポイント5倍還元

Amazonが 和書ストア 3000円（税込）以上の商品【Amazonポイント5倍還元】（一部商品を除く） というキャンペーンをやっていたので、前から欲しかった本を一冊購入。

Amazonポイント最大5倍還元Amazon.co.jp 和書ストアでは、通常1％のポイント還元のところを、3000円（税込）以上の商品に限り、【Amazonポイント5倍還元】キャンペーンを実施中（一部商品を除く） 。2008年1月31日（木）まで。

λ. ファイル名から U+200E LEFT-TO-RIGHT MARK を取り除く

Google Docs から Google Docs: Download と DownThemAll でダウンロードしたファイルのファイル名の先頭に、何故か U+200E LEFT-TO-RIGHT MARK が追加されてしまっていたので、簡単なスクリプトで取り除いた。

require 'win32ole'
WIN32OLE.codepage = WIN32OLE::CP_UTF8

# U+200E LEFT-TO-RIGHT MARK
re = /#{[0x200e].pack('U')}/u

fs = WIN32OLE.new("Scripting.FileSystemObject")
dir = fs.getFolder(".")
files = dir.Files
files.extend(Enumerable)
files = files.to_a

files.each{|f|
  fname = f.Name
  if fname = fname.gsub!(re, '')
    puts fname
    f.name = fname
  end
}