日々の流転

λ. 扇屋の牛乳まんじゅう。

λ. 買ったもの

MACH POWER - MPX -

ついに念願(笑)のデジカメゲッチュ。さくらやNetsで¥12,800。情報サンキュー > チカ

λ. モーニング娘

どうでもいいけど、最近加護ちゃんかわいいですね。
あの辺の年齢はどんどん化けるので、将来が楽しみです
同様の理由で、辻ちゃんにも期待
新規加入した娘。は正直わからんし、どーでもよいです

そんな直江先生は、辻加護判別ゲームなど余裕に違いない。(とか書いてみる)

λ. signal_connect("destroy"){}

「ruby -rgtk2 -e 'Gtk.init; Gtk::Button.new.signal_connect("destroy"){} '」で落ちる問題、とりあえず解決。原因は前から分かっていて、

1. Rubyの終了処理開始
2. Ruby側のオブジェクトが開放される
3. glib/gtk側のオブジェクトがunrefされる
4. glib/gtk側のオブジェクトのリファレンスカウンタが0になる
5. destroyシグナルが発生して、signal_connectのブロックを呼ぼうとする
6. しかし、Ruby側はすでに通常の実行状態ではないので、正しく呼べない
7. Segmentation Fault

という事が起こっていた。

Rubyが終了処理に入っていたらブロックを呼ばない事にすれば良いのだけど、「Rubyが終了処理に入っている」事をどうやって知れば良いかで数日悩んでいた。で、今日ふとrb_set_end_proc()で登録した関数内でフラグを立てればいいということに気が付いたので、解決。

この件についてはもっと対処が必要な気もするけど、落ちることだけはなくなるはずなので、残りは後回しでいいや。

λ. Relator

Functorの概念を使っているプログラミング言語は多いけど、Relatorの概念を使っている言語はあるか? (高階の論理型言語とか?)

λ. 読書

『天国に涙はいらない 9 - ふんどし汁繁盛記』

佐藤ケイ[著] さがのあおい[イラスト]

λ. 矛盾を表す型

<URL:http://d.hatena.ne.jp/sumii/20070912/p1> から、<URL:http://shuns.sakura.ne.jp/?%BD%B5%B5%AD> の話。そういや、OCamlの let rec はそんなことが出来るのだった*1。

それはさておき、「type void = V of void」はこのような問題はあれど、除去規則については「let rec f x = match x with V x -> f x ;;」という形で一応は帰納的に定義できる。それに対して「type void」はこのような問題はないけど、自然な除去規則「let f x = match x with ;;」が構文エラーになってしまって*2イマイチ。

また、多相ラムダ計算の表現力を持つ言語では、矛盾を「∀X. X」で表現することも出来る*3。先日の「パースの論理式」 では矛盾の表現としてこれを使ってみた。 この場合の除去規則については自明。

λ. 『寄生獣 (3)』 by 岩明 均

「ったく薄情なヤツだな」「…………情なんてないよ」という掛け合いが良かった。

λ. SLACS 2007 (1日目)

一日目。

λ. 佐藤圭祐（東工大）：λ記号の加わった様相論理に関する研究

2002年にMelvin Fittingが提唱した「λ記号の加わった様相述語論理」に対し，ツリー・シークエントによる証明体系を与え，体系Kにλ記号の加わったKλおよび，さらにいくつかの公理型が加わった諸体系について，その健全性と完全性を示す。

Melvin Fitting が提唱した「λ記号の加わった様相述語論理」というのは、Modal Logics Between Propositional and First Order か。

λ. 小島健介（京大）：next, always をもつ直観主義線形時相論理

多段階計算のための型システム λ^○□ (Yuse and Igarashi, 2006) に Curry-Howard 同型対応する論理についての考察を行う。この論理は，next と always の二つの時相演算子をもつ直観主義線形時相論理とみることができる。本発表では，その sequent calculus による定式化と Kripke semantics を与え，完全性について考察する。

λ. 田中覚次（九大）：関係代数の拡張体系の表現定理について

A.Tarski　によって考えられた二項関係を表現する代数的構造を，拡張しそこでの表現可能性について検討する。ストーンの表現定理の拡張について主に述べるが，二項関係の全体への表現へ拡張できればそれについても触れる予定である。

λ. 根元多佳子（東北大）：Infinite games from a intuitionistic point of view

無限ゲームの決定性の直感主義数学における取扱いと，2^ω×{0,1}上の長さ 2 のゲームの決定性について。

λ. 小林聡（京産大）：極限計算可能数学のためのゲーム意味論と変換意味論

極限計算可能数学(Limit Computable Mathematics, LCM)とは，おおよそ構成的数学に非常に弱い形の排中律をつけ加えたものとして与えられる体系である。本研究では，LCM の証明からアルゴリズムを抽出するための2つのアプローチを示す。1つは，1-backtrack と呼ばれる弱いバックトラック規則を持つゲーム意味論である。2つめは，Friedman 変換に類似した新しい変換による意味論である。古典的証明の研究では二重否定変換やその変種が用いられることが多いが，我々の変換はゲーム意味論にヒントを得たもので，二重否定変換とは異なる発想に基づく全く新しいものである。

λ. ダークナイト

ダークナイト見てきた。ヒース・レジャーの演じるジョーカーがかっこ良かった(＞＜)

λ. SPINによるモデル検査 (1) by 野中さん

メモ。 野中さんによるSPINチュートリアル。 非常によくまとまっている。

λ. “First-Order Logic as a Lightweight Software Specification Language - The ETPTP Toolkit” by Michel Rijnders

面白かったのは以下の日記で書いた点。

• 推移閉包が一階述語論理で表現できないことの証明 - ヒビルテ(2009-09-15)
• 有限領域での推移閉包の公理化 - ヒビルテ(2009-09-16)

λ. CLTT読書会 第6回

今回は、1.7 Categories of fibrations の Lemma 1.7.6 後の 2 categorical struture のところから Exercise 1.7.2 くらいまで。

• CLTT読書会 第6回 : ATND
• 前回