2007-09-18 [長年日記]
λ. 矛盾を表す型
<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。先日の「パースの論理式」 では矛盾の表現としてこれを使ってみた。 この場合の除去規則については自明。
*1 けど、この機能を活用している人ってどれだけいるのだろうか? 予め循環する深さ等が決まっていないと書けないのでは、あまり使い道は無さそうな……
*2 <URL:http://caml.inria.fr/pub/docs/manual-ocaml/expr.html#pattern-matching>によるとパターンは一個以上必要
*3 これは∀を使って帰納的データ型をエンコードしたものになっている
λ. 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 変換に類似した新しい変換による意味論である。古典的証明の研究では二重否定変換やその変種が用いられることが多いが，我々の変換はゲーム意味論にヒントを得たもので，二重否定変換とは異なる発想に基づく全く新しいものである。
[ツッコミを入れる]
