最終更新日時: Last modified: 2008-08-26
14:00 ～ 14:05
オープニング＋連絡など
14:05 ～ 14:45
藤尾 光彦（九州工業大学）
演題：
量子論理へのモルフォロジーの応用
梗概：
14:45 ～ 15:25
平井 洋一（東京大学大学院情報理工学系研究科）
演題：
Prover-skeptic Dialogue for MALL
梗概：
15:25 ～ 15:40 休憩
15:40 ～ 16:10
伊藤 隆浩（九州大学大学院数理学府）
演題：
抽象衝突系について
梗概：
抽象衝突系と言う新しい代数的遷移系を提案する。 抽象衝突系はビリヤードボール系の拡張の一つであり、 同時に、セルオートマトンや化学反応系の拡張であると考えることもできる。 まず、抽象衝突系を定義し、さらにビリヤードボール系を抽象衝突系を用いて再 定式化する。 また、1次元のセルオートマトンや巡回タグ系の模倣といった他の系との関係も 示す。 模倣は数学的な関数により厳密に定義されるので、 系のパラメータから模倣に必要なステップ数を正確に知ることができる。
16:10 ～ 16:50
河原 康雄（九州大学）
田中 覚次（九州大学）
演題：
Dedekind 圏における閉包系と閉包作用素
梗概：
10:30 ～ 11:00
中澤 巧爾（京都大学大学院情報学研究科）
演題：
Type Checking and Inference for Polymorphic and Existential Types
梗概：
型に二階の量化子を含むラムダ計算においては，所謂Curry流とChurch流の体 系の他に，それらの中間様式と位置付けられる体系が考えられる．本発表では， そのようないくつかの様式で形式化された多相型を含むラムダ計算，および， 存在型を含むラムダ計算について，型検査問題と型推論問題が決定不能である ことを証明する．
11:00 ～ 11:45
浅田 和之（京都大学数理解析研究所）
演題：
外延的全称型をもつ値呼び２階多相型付きλ計算
梗概：
外延的な全称型を持つ値呼びの２階多相型付きλ計算を導入する．値呼びでの 直積型や関数型と異なり，外延的全称型は型のβη同値関係を満たす．そして この体系に対するモナドを用いた圏論的意味論を与える．これによりHaskellの ようなモナドを持つ言語への応用も考えられる．また具体的なモデルを与える ためにリリヴァントパラメトリシティを満たすモデルを考える．このモデルに より，非停止，例外，状態，入出力，およびリストのモナドを使えることが保 証される．
11:45 ～ 13:30 休憩
13:30 ～ 14:00
高村 博紀（産総研 システム検証研究センター）
演題：
Powers of positive elements in constructive C*-algebras
梗概：
C*-環における小笠原の定理に対して、Bishop流の構成的数学に 基づく証明を与える。構成的数学では一般的にスペクトルに 扱いが難しいことが知られているが、発表者はそれを克服して 構成的C*-環を展開した。本発表はその続きとしてC*-環の正要素 の冪に関する小笠原の定理に対して構成的な証明を紹介する。
14:00 ～ 14:20
岡田 幸治（九州大学大学院数理学府）
演題：
ソーシャルブックマークのリンク共起情報に基づく概念グラフ
梗概：
一つのコミュニティ内部の階層構造を解析する新たな手法を提案し、ソーシャルブ ックマークを用いてウェブページ群の解析を行った。本稿では、概念グラフの考え 方を取り入れ、1つのウェブページを節とし、ユーザーのブックマークの共起情報に よって順序関係を定義し、それを枝とする有向グラフを作った。さらに、この順序 関係の全順序性を線形度と定義しその解析を行った。
14:20 ～ 14:50
石田 俊一（九州大学大学院システム情報科学府）
演題：
関数従属性と含意従属性の関係について
梗概：
2値データベースの特徴を捉える時、関数従属性や含意従属性が用いられる。 この両者の従属性集合が一致する条件など、関係性について考察した。
14:50 ～ 15:05 休憩
15:05 ～ 16:05
只木 孝太郎（中央大学 研究開発機構）
演題：
A statistical mechanical interpretation of algorithmic information theory
梗概：
In this talk, we develop a statistical mechanical interpretation of algorithmic information theory by introducing the notion of thermodynamic quantities, such as free energy, energy, statistical mechanical entropy, and specific heat, into algorithmic information theory. We investigate the properties of these quantities by means of program-size complexity from the point of view of algorithmic randomness. It is then discovered that, in the interpretation, the temperature plays a role as the compression rate of the values of all these thermodynamic quantities, which include the temperature itself. Reflecting this self-referential nature of the compression rate of the temperature, we obtain fixed point theorems on compression rate.
16:05 ～ 16:20 休憩
16:20 ～ 17:20
井田 哲雄（筑波大学システム情報工学研究科）
演題：
Models of computation for computational origami system EOS
梗概：
計算折紙システムEOSは，伝統的折紙の計算機による創作と折紙を用いた幾何 オブジェクトの作図と作図の正しさの自動証明を行うシステムである．EOSで 用いている，項書き換えシステム，グラフ書換システム，グロブナ基底を用い た定理の自動証明システムについて，概要を述べる．
18:30 ～ 懇親会
10:30 ～ 11:00
高井 利憲（産総研 システム検証研究センター）
演題：
木構造オートマトンによる木の描画の紹介
梗概：
11:00 ～ 11:30
長谷川 真人（京都大学数理解析研究所）
演題：
直観主義線形論理と古典線形論理の間のギャップについて
梗概：
わかっているようでいまだによくわからない、直観主義線形 論理と古典線形論理の関係について、圏論的なモデルを用い た結果を交え考察する。
11:30 ～ 11:50
白旗 優（慶應大学商学部）
演題：
The subobject classifier in the category of presheaves over an so-monoid.
梗概：
We study the subobjects and the subobject classifier in the category of Set^M where M is an so-monoid. We will observe that most of the constructions work smoothly as usual except the unit.
11:50 ～ 12:00
クロージング＋連絡など