10/14(水) 13:30--14:30（特別講演）
　バイアマン=A.（ミュンスター大学）
　　「ゲーデルの体系Ｔの計算列の長さの厳しい上限」

休憩

14:45--15:15
　志村立矢（日本大学理工学部）
　　「A semantics of Kashima's connection calculus for the logic of constant domain」

　鹿島は constant domain であるような Kripke frame 全体で特徴付けられる中間述語 論理 LD に対し、connection 付きの sequent という概念を導入して cut 消去定理の成 立する体系を与えることに成功した。しかし、その証明は純粋に syntactical なもので connection という概念の意味論的解釈は与えられていない。
　本講演では、この connection 付きの sequent に対するひとつの解釈を与え、ラベル 付きの論理式を用いたタブロー法を介することで、Sch\"utte の方法により鹿島の体系が cut-free であること及び LD が constant domain であるような subordination frame に関し完全であることが同時に証明できることを示す。

15:15--16:05
　永山操（東京女子大学文理学部）岡田光弘（慶応大学文学部）
　　「Graph-theoretic characterizations of proof nets in non-commutative linear logics and their computational complexity」

乗法非交換的線型論理、巡回的線型論理、アブリュシの非交換的線型論理に対して、証明 ネットの妥当性に関する簡単な条件を与える。

休憩

16:20--16:50
　亘理修、宮腰政明（北海道大学大学院工学研究科）中戸川孝治（北海道大学文学部）
　　「Multiplicative / Additive Connectives for Deontic Logic」

　義務・許可・禁止といった様相を扱う規範論理(Deontic Logic, DL)に対し、 Multiplicative / Additive connectives が、どのような形で導入できるかを考察する。
　さらに、Multiplicative とAdditive の区別を設けることが適切であるような具体的な 状況を探る。

16:50--17:40
　下田守（下関市立大学）
　　「ファジィ同値関係をめぐって」

　ファジィ集合・ファジィ関係の基本的な概念は，ある完備ハイティング代数を真理値集 合とする直観主義的集合論の階層モデルにおいて解釈するのが最も自然であることを，講 演者は明らかにしてきた．今回は，ファジィ同値関係および関連する概念について，同様 に自然な解釈が可能なことを示す予定である．

10/15(木) 9:45--10:15
　高木理(京都産業大学）
　　「帰納的定義を持つ算術の自然演繹に関する正規化性について」

　原始帰納的な整列順序集合上の再帰的な定義 TRD を公理として持つ構成的な算術 TRDB の自然演繹に対して、ある帰約を定義し、その帰約に対する強正規化性定理について説明 する。また、TRDにおける論理式に対する論理限定子に関する制限と、TRDBの正規化の関 係についても述べる。

10:15--10:45
　平井崇晴（神戸大学自然科学研究科）
　　「Temporal Linear Logic と Timed Petri Net について」

　近年 Petri net は発火に遅延時間を組み込むなど, 時間による拡張がなされtimed Petri net と呼ばれている. Petri net の marking から marking への到達可能性は linear logic の sequent の証明可能性と対応がついている. そこで linear logic に離 散時間を導入した temporal linear logic を考えtimed Petri net との対応について述 べる.

10:45--11:15
　田辺誠（科学技術振興事業団さきがけ２１／(財)京都高度技術研究所）
　　「リアクティブシステムの観察：直観主義様相論理によるアプローチ」

　古典的様相論理はこれまでリアクティブシステムの仕様記述や検証に応用されてきたが、 直観主義様相論理のコンピュータサイエンスへの応用はあまり見られない。
　本発表では、リアクティブシステムの実行時にイベントの時系列として観察される状態 変化を、直観主義様相論理(IML)を用いて記述することにより、IML の応用の可能性を示 唆する。
　イベントの部分列の性質を IML の論理式を用いて明示的に表現できること、時系列全 体の性質を二重否定された論理式によって表現できることを示す。

11:30-12:00
　渡邊宏（電子技術総合研究所）
　　「遷移系と双模倣準同型の圏の構造」

　集合圏上の自己函手 P_omega の余代数(coalgebra)の圏 P_omega-coalg の構造につい て述べる．これは対象が遷移系で射が双模倣準同型(functional bisimulation)で与えら れる圏である．この圏は完備かつ余完備な対称閉単圏であり，分類子(subobject classifier)が存在する．これらの諸性質は余代数を構成する基底圏と自己函手の性質か ら導かれる．
　ラベル付き遷移系圏での対称閉単圏構造の例と，遷移系圏における分類子の概観を見せ る．

12:00-12:30
　佐藤伸也（東京理科大学理工学研究科）杉本徹（東京理科大学理工学部）
　　「線形論理の計算的解釈に基づく並列実行可能なλ計算の call-by-value 評価器」

　Abramsky は古典線形論理におけるカット除去に対応して，proof expression と Linear CHemical Abstract Machine (CHAM)からなる計算体系を提案した．Girard による 直観主義論理の線形論理への埋め込みを用いることで，型付きλ計算をこの体系に埋め込 むことができる．本研究では，Linear CHAM によってλ計算の call-by-value 評価に相 当する簡約が行えることを示す．Linear CHAM の簡約は並列に実行できるので，この結果 から，λ計算の並列実行可能な call-by-value 評価器の設計が可能となる．

休憩

13:30--14:30（特別講演）
　ウェイナー=S.S.（リーズ大学）
　　「証明論と複雑さ」

休憩

14:45--15:15
　藤田憲悦（九州工業大学情報工学部）
　　「2nd Order Lambda-Mu-Calculus of Call-by-Value」

　型の情報が明示的に付加されている2階の call-by-value λμ計算を導入する. これは, Curry-style の多相型言語においては, callcc や μ-operator などの制御オペレータに 関する計算規則が矛盾なく定義できないという考察に基づくものである. この体系から Girard の F への CPS-変換規則を与えて, その健全性を示す. そして, CPS-変換を利用 して, この体系の強正規化性が得られることも示す.

15:15--16:15
　小方一郎（電子技術総合研究所）
　　「LK の cut elimination としてのλμ計算」

　Gentzen-style の古典論理 LK の上の cut elimination には強停止性はあるものの、 合流性はない。しかし LKの推論規則にある種の制限を加えた古典論理（LKT/LKQ -- Danos et. al. 1997）を考えることで合流性を回復できるという証明論の成果がある。こ の LKT/LKQ の推論規則を項の構成規則とし、 cut-elimination を模倣するようにλμ計 算の計算ルールを構成すると、LKT には Parigot の名前呼び (CBN) λμ計算、LKQ には Ong の値呼び(CBV) λμ計算にそれぞれほぼ対応していることを示す。さらに LKT/LKQ の intuitinistic decoration を考えることにより、continuation passing style の型 付λ計算(CBN/CBV)が上記のλμ計算と isomorphic であることを示す。

休憩

16:30--17:00
　亀山幸義（京都大学情報学研究科）
　　「古典的 Catch/Throw 体系の強正規化可能性の簡単な証明」

　中野の Catch/Throw 体系を古典論理に拡張したもの，および佐藤の古典論理的な Catch/Throw 体系に対して，Parigot のλμ計算の変種への解釈を与える．これにより， これらの体系の強正規化可能性の簡単な証明を与える．

17:00--17:30
　馬場謙介（九州大学システム情報科学研究科）、廣川佐千男、藤田憲悦
　　「λμ計算における並行変換」

　Parigotによって定義されたλμ計算における並行変換では、λ計算の合流性の証明に 一般的に用いられる「亀の甲」の論法が成り立たない。そこで、λμ計算の変換規則のう ち、renaming と複数回の structural reduction をあわせたものをあらためて１ステッ プの並行変換と定義すると、この並行変換は強い意味での合流性を持ち、λμ計算の合流 性の証明が得られる。

懇親会

10/16(金) 9:25--10:05
　只木孝太郎（北海道大学理学研究科）
　　「Kolmogorov complexity とフラクタル集合」

　Kolmogorov complexity は、対象をアルゴリズムによって生成する際に要求される補助 情報の量を表す概念である。
Euclid 空間の点を二進展開し、Kolmogorov complexity を使ってその圧縮率を考える。 このとき、Cantor 集合や Koch 曲線等おなじみのフラクタル集合を含む或るクラスの自 己相似集合に対して、この圧縮率の最大値が、Hausdorff 次元に一致することを示す。そ して、その系として、prefix-free な有限集合の元から作られる無限列の Kolmogorov complexity に対し、漸近評価を与える。また、Chaitin の停止確率Ωの“D 次元版”で あるΩ^D を導入し、その性質を議論することにより、停止問題に関係した自己相似集合 の Hausdorff 次元が、1 であることを示す。

10:05--10:35
　鴨浩靖（奈良女子大学理学部）
　　「計算可能距離空間の Hausdorff 距離の計算可能性」

　距離空間の空でないコンパクト部分集合全体が Hausdorff 距離で距離空間をなすこと が知られている。Weihrauch は「計算可能距離空間」を、距離空間に番号付けられた稠密 部分集合を加えたものとして定義した。本講演では、計算可能距離空間の空でないコンパ クト部分集合全体が計算可能距離空間をなすことができることを示す。また、その応用の いくつかを紹介する。

10:35--11:05
　立木秀樹（京都大学総合人間学部）
　　「グレイコードによる実数ＰＣＦ」

　Real PCF は、PCF に実数の型を追加し、無限制度での実数計算を可能にしたもので、 Escardo よって提唱された。Real PCF での実数計算は、PCF の他の部分の様に記号処理 的ではなく、有理数のペアによる区間や、そのような区間の join を基本演算としていた。 この講演では、Gray Code 実数表現を用いることにより、実数を Bool の列として表現し、 join も記号的に処理する Real PCF の変形を提唱し、オリジナルの Real PCF との同等 性を示す。

休憩

11:20--12:00
　田口研治（九州大学システム情報科学研究科）
　佐藤周行（東京大学大型計算機センター）
　　「セルを操作する計算系　―セル計算―」

　Cardelli と Gordon は広域ネットワークにおける計算のモデルとして Mobile Ambients という計算系を提案した。ambients は名前を持ち、プロセスをそれ自身に包括 する構造である。様々な機能は capability と呼ばれる演算として、操作的意味が与えら れる。
　我々は Mobile Ambients に対して、名前を単一に制限するという、構造の抽象化を行 ない、その構造に対して様々な capability を与えた場合、どのような計算能力が得られ るかを、いくつかの例を基に示す。

12:00--12:30
　龍田真（京都大学理学研究科）
　　「グラフモデルと部分関数モデルの一様連続性」

　対と自然数をもつ部分コンビネータ代数に対する一様連続性 MCONT とは、そ の上の有限型構造において、type 2 関数からその associate を一様に計算す る関数が存在することである。この講演では、部分関数モデルもグラフモデル も性質 MCONT をもたないことを示す。

休憩

13:30--14:00
　白旗優（慶応大学商学部）
　　「Pier -- a proof interactive editor --」

コンピュータ上で証明図を描くためのグラフィックなエディターPierについて紹介する。 Pierはホームページで使用するJavaアプレットであり、クリック・アンド・ドラッグで自 然演繹体系の証明図を描くことができる。論理学を計算機上で扱う研究では、自動定理証 明などが主流であるが、この発表では論理学研究と教育のための補助手段と言う観点から、 ユーザ・インターフェイス開発の重要性についても論じてみたい。

14:00--14:15
　立木秀樹（京都大学総合人間学部）竹内泉（京都大学情報学研究科）
　　「自己相似図形の作図のネットワーク上での実装」

　河邑の学位論文には、［０，１］区間の実数の二進小数展開によって自己相似図形を作 図する公式がある。本研究では、この公式が標準的二進小数展開ばかりでなく、反転小数 展開やグレイコードによる二進小数展開にも拡張できることを示す。
　また、この公式を用いて、のネットワーク上に自己相似図形の作図を実装したものを紹 介する。

13:30--15:05
　住友亮翼（神戸大学自然科学研究科）
　　「証明アニメーション支援環境について」

　一般的に大規模な証明の構築には多大のコストがかかるのであるが、その原因の一つに， 証明途中で設定する補題や定理の誤りといった``非形式的な意図を形式化する際に起きる 誤り''がある。この問題を解決するために，``証明アニメーション''という技法が提案さ れた。この技法では，プログラムをテストするように証明をテストすることにより証明を デバッグするというものである. 本研究では証明アニメーションを支援するための証明 開発環境を作成した。本発表では、初等整数論の簡単な定理を例として用いて、このシス テムでのデモンストレーションを行う。

休憩

15:20--16:00
　中野浩（龍谷大学理工学部）
　　「A realizability interpretation of self-referential types」

　型の再帰的な定義に負の自己参照を許すと、いわゆる Russell's paradox と呼ばれる 矛盾を体系が含んでしまうことがよく知られている。 計算コストの概略を表現できる型 付けシステムとその実現可能性解釈を与えて、この矛盾を回避しながら、再帰的に定義さ れた型(あるいはプログラムの仕様)の自然な解釈が可能であることを示す。さらに、この 体系での型は Y コンビネータなどの不動点演算子の公理的な意味をよく表現しており、 不動点演算子の型情報のみを使ってそれを利用した再帰的なプログラムの構築が可能なこ とを示す。

16:00--16:50
　林晋（神戸大学工学部）
　　「Beeson の q-realizability のプログラム抽出への有効性」

Beeson は、集合概念を含む構成的数学の形式系(IZF, T_0, etc)の existence property を証明するため、doubling variables による q-realizability 解釈を導入した。龍田は Feferman の T_0 の特殊ケースに対しては、completion という技法で、Beeson の技法を 補完できることを示し、completion は program extraction に使えるが、doubling variables は使えないと主張した。本講演では、この主張に反し doubling variables が program extraction に使えることを示す。