2001-09-19
λ. JRuby
JRubyのソースを読んでみたり。そういえば、Javaのソースコードを読むのって、すごい久しぶり。Javaをだいぶ忘れてて焦る。まあ、Javaでは Hello World 以上のプログラムを書いたことが無いので、忘れてて当然かも。(^^;;
λ. CGI
最近RubyでCGIを少し勉強したんだけど、Perlで書かれた酷いプログラムを結構見かけてあきれてしまった。Last-Modified:ヘッダは出力しないし、Content-Type:ヘッダにはcharsetパラメータをつけないし、掲示板で投稿されたデータをメールにして送る場合でもMessage-Id:やIn-Reply-To:等のヘッダはつけないし、標準ライブラリにあるような車輪を再発明してたりするし、せっかくのドキュメントはPODになってないし… (以下略)
僕はPerlはほとんど分からないけど、Perlがちゃんと分かる人が見たらこれどころじゃないんだろうなぁ。
λ. 読んだ本
- 天使な小生意気 10
- 西森博之[著]
- 小説 まもって守護月天! XI - いつまでも君のそばに
- 藤崎あゆな[著] 桜野みねね[原作]
- 悠久幻想曲 2nd Album
- たきもとまさし[著]
λ. TV
- 覗く女
- アルスラーン戦記
- アルスラーン戦記 Ⅱ
2002-09-19
λ. 久しぶりに早起き。
λ. adjointって面白いなぁ
adjoint(随伴)って面白いなぁ。と今ごろになって思う。
λ. 借りた本
- 小説すばる 2002年4月号
- -
- 『ブギーポップ・ミッシング ペパーミントの魔術士』
- 上遠野 浩平[著] 緒方 剛志[イラスト]
- 『ベッカー教授の 経済学ではこう考える』 (THE ECONOMICS OF LIFE)
- ゲーリー・S・ベッカー(Gary S. Becker), ギティ・N・ベッカー(Guilty Nashat Becker) [著] 鞍谷雅敏, 岡田滋行 [訳]
- 『眼球綺譚』
- 綾辻行人[著]
- 『英語で日記を書いてみる』
- 石原真弓[著]
λ. 夕食
家族でニュー・トーキョーへ。
λ. Ruby-GNOME2
副メンテナになることになりました。よろしくお願いします。
λ. [ruby-gnome2-devel-ja] Obsoleteな関数の扱い
Gtk::TextやGtk::Treeは、Gtk::TextViewやGtk::TreeView周りが実装されたら、削除する予定です。無くなると困るという方は今のうちに声をあげて下さい。
そうでした。Gtk::CTreeとかGtk::CListといったGTK_DISABLE_DEPRECATEDなのもです。
2003-09-19
λ. 親知らず
親知らずを抜歯。多少痛む。
λ. pcl-cvs
cvsコマンドを直接使うのが馬鹿らしくなったので、pcl-cvsを使ってみる。しかし、MeadowからCygwinのsshにパスフレーズを渡すことは出来ないみたい(MeadowがCygwinのptyを扱えないのはまぁ当然だよね)。ssh-agentを使えば良いみたいだけど、どうせなのでwin-ssh-askpassというのを使ってみる。なかなか便利。
λ. 分類と情報射のなす圏のexponential (PDF)
そのままじゃ存在しないよね。忘れないうちにメモしておく。
[2005-03-27 追記] distributive category でないことを示しすことによって間接的に証明した方がスマートだと思う。
2007-09-19
λ. SLACS 2007 (2日目)
二日目。
飲み会の時に、夏のプログラミングシンポジウムでの浜地さんの発表資料「Code Golf について」が少し話題になった。
SLACS 2007 への言及
λ. 菊池健太郎（東北大）：ベータ簡約を模倣するカット除去手続き
シーケント計算LJの中で型付きラムダ項全体と同型になる部分を特定し，ベータ簡約があるカット除去手続きによって健全かつ完全に模倣されることを説明する。
λ. 和手正道（了徳寺大）：直観主義論理の証明可能性の決定時間について
Gentzen流直観主義論理において与えられたsequentが証明可能か否かの判定は可能であることは明らかであるが,その判定に要する時間がsequentの長さの関数としてどの程度の時間があれば十分かを論ずる.
λ. 坂川航（東工大）：一般化された体系におけるcut除去定理の成立条件
論理記号や推論規則が一般化されたシークエント計算の体系において，cut除去定理が本質的に成り立つための必要十分条件が2006年に Ciabattoni, 照井によって与えられた。そこでは統語論的，意味論的な条件が別々に与えられ，それらの等価性も示された。本発表では特にその統語論的な条件に着目し，体系の定義をさらに一般化させた時にどのような問題が発生するかを指摘し，その解決策を述べる。
λ. 向井国昭（慶応大）：PrologへのMontague普遍文法に基づくeval述語の導入
講義資料作りのために日常的に使う主なソフト/言語は, Emacs, pTeX，HTML/JavaScript/Ajax, およびPrologである。とくにProlog(SWI-Prolog)は全体を束ねる中心的な言語として使用している。計算言語理論，数式処理，定理証明，オートマトン理論，Prologプログラミングなど，担当授業の性格上どれも，複雑な式変形を伴う計算量の多い教材作りが必要である。このためだけでもPrologは必須の道具であるが，それだけにとどまらない。Emacs バッファのLaTeX テキストの編集とコンパイル実行もPrologとEmacs-lispの間の通信により，Prologの述語として定義・制御できるようにした。つまり， Prologの限定節によりEmacs-バッファ上のテキスト編集機能を記述する。
発表では，関数型評価述語 eval，項書き換え述語 reduce 充足可能述語 models, そして，簡易版のラムダ計算 beta_liteの４つの述語を中心に紹介する。いずれの述語も問題が決まればそれに応じて個別に書けるものであるが，問題に共通するパターンを抽象化して，汎用の規則解釈述語とした。個別の問題はいわゆるソートあるいはクラスとして一定の形の規則で与える。
関数型言語としてのProlog限定節の解釈, モンタギュ普遍文法とその上の翻訳理論からのevalの解釈（発表タイトル），等式論理規則(paramodulation) の解釈器としてreduce述語の説明, など，上述の規則に明快な意味論的解釈および根拠を持たせた。 発表ではこれらの結果を，いちおうのまとまりをみせてきた現状のシステムのデモを交えて説明する。
λ. 木村大輔（NII）：Duality between Call-by-value and Call-by-name, Extended
We extend Wadler's work that showed duality between call-by-value and call-by-name by giving mutual translations between the λμ-calculus and the dual calculus. We extend the λμ-calculus and the dual calculus through two stages. We first add a fixed-point operator and an iteration operator to the call-by-name and call-by-value systems respectively. Secondly, we add recursive types, ⊤, and ⊥ types to these systems. The extended duality between call-by-name with recursion and call-by-value with iteration has been suggested by Kakutani. He followed Selinger's category-theoretic approach. We completely follow Wadler's syntactic approach. We give mutual translations between our extended λμ-calculus and dual calculus by extending Wadler's translations, and also show that our translations form an equational correspondence, which was defined by Sabry and Felleisen. By composing our translations with duality on the dual calculus, we obtain a duality on our extended λμ-calculus. Wadler's duality on the λμ-calculus was an involution, and our duality on our extended λμ-calculus is also an involution.
急病のためにキャンセル
λ. Matthew de Brecht（京大）, 小林正典（首都大）, 徳永浩雄（首都大）, 山本章博（京大）：多項式環におけるイデアルの正データからの帰納推論
多項式環のイデアルが有限基底を持つという性質が，機械学習理論の一つである正データからの帰納推論と密接に関係しているという事実は論理の視点からも注目されている。本講では，正データからの帰納推論からみた多項式環におけるイデアルの性質，さらには，その一般化を普遍代数における閉包演算を用いて行う方法について，発表者のグループが最近数年間で明らかにしてきた結果を報告する。
λ. Matthew de Brecht and Akihiro Yamamoto（京大）：Mind Change Complexity More Than ωω in Inductive Inference From Positive Data
In the context of machine learning, ordinal numbers are used for representing mind change complexity of classes of formal languages in inductive inference from positive data. The mind change complexity of a class means how often a learning machine is allowed to change its conjecture during the learning process. All previously investigated natural classes of languages (known to the authors) have had mind change bounds less than the ordinal ωω. In this talk, we will show that learning unbounded unions of a subclass of pattern languages requires ordinal mind change bound up to ωωω. We will also show a connection between proof theory and mind change complexity.
2008-09-19
λ. The Transactional Memory / Garbage Collection Analogy
The Transactional Memory / Garbage Collection Analogy by Dan Grossman
Transactional memory (TM) is to shared-memory concurrency as garbage collection (GC) is to memory management.
The Transactional Memory / Garbage Collection Analogy | Lambda the Ultimate より。
A unified theory of garbage collection のようなものを期待していたら、本当にただのアナロジーだった。 もっとも、著者がCycloneの作者の一人であることもあって、非常に説得力のあるアナロジーではあるのだけど。
あと、X10, Fortress, Chapel といった次世代の言語ではトランザクショナルメモリが言語の一部になっているそうな。X10とFortressは知ってたけど、Chapelってのもあるのね。
λ. 量子誤り訂正符号
decoherenceによる問題は量子誤り訂正符号で常に回避可能なものなのだろうか? 回避可能だとして、それはGCのように普段はその存在を意識しないで構わないものになるのだろうか? それともトランザクショナルメモリーのように抽象的にではあっても存在を意識する必要があるものになるのだろうか? 知人と量子計算について話していてちょっとそんなことを思った。まだ量子誤り訂正符号がどんなものなのか私は全然理解してないけど。
λ. シュシュ
シュシュって何かと思ったら、ヘアアクセサリなのね。 シュッ・シュッとは関係ないと。
