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.
