[kisoron-ml] SLACS2012プログラムおよび梗概(9/9 ver.)

[Hiroyuki Miyoshi]

SLACS2012講演者および参加を考慮されている皆様，

プログラムおよび梗概をお送り致します。

京都産業大学理学部数理科学科
三好博之
hxm at cc.kyoto-su.ac.jp

----------------------------------------------------------

9/15（土曜日）

13:00-13:30
鴨浩靖，萩尾由貴子，溝口涼子（講演者）（奈良女子大学理学部）
題目：三角形に関する平面ユークリッド幾何への数式処理の応用
梗概：未定

13:35-14:05
吉村和人（JAIST）
題目：オラクルの圏論的記述―終対象の一般化として―TTE
(Type-2 Theory of Effectivity) は計算可能解析学の枠組みの一
つである．TTEでの初等的な事実の一つとして，(計算可能性概念の
導入された) ある種の位相空間の間の写像に対してはオラクル計算
可能性と位相的連続性が一致するというものがある．本発表では左
記事実の圏論的特徴づけについて現状得られている結果の紹介を行
う ．具体的には，factorization systemを伴う圏のうち適当な性
質を満たすものの上で: オラクルの概念の再現; オラクル計算可能
性と位相的連続性の一致に相当する命題の特徴づけ: 左記2点を吟
味する．

14:10-14:40
江口直日（東北大学理学研究科）
題目：Rewriting Apploaches to Computational Complexity and
Complexity Analysiss by Rewriting 梗概：関数型言語により定義
できる関数の多くは停止性を持つ項書き換えシステムとして表現す
ることができる．現在まで多項式解釈，行列解釈，リダクション順
序など項書き換えシステムの停止性を証明する方法が知られている．
こうした停止性の証明により，しばしば停止性だけでなく時間計算
量と深く関係する書き換え回数の上限を求めることができる．本講
演では経路順序と呼ばれるリダクション順序による計算量解析法に
ついてM. Avanzini, G. Moser (共に University of Innsbruck)と
の共同研究の成果を報告する．さらに新しく導入する経路順序は多
項式時間計算量に対して完全となることを説明する．

14:40-15:00 休憩20分

15:00-15:30
河野友亮
題目：論理CDの補完定理について梗概：中間論理のひとつであるCD
において、クレイグの補間定理が成り立たないことが[1]によって
証明された。そのおおまかな内容の解説に加え、CDを少し変えた論
理でもクレイグの補間定理が成り立たないことが[1]と同様の手法
で証明できることを示す。

[1] Failure of interpolation in the intuitionistic logic of
constant domains, Grigori Mints, Grigory Olkhovikov,
Alasdair Urquhart

15:35-16:05
岩波克（東京工業大学情報理工学研究科）
題目：様相Lukasiewicz論理の公理化について
梗概：Lukasiewicz論理の様相論理化にはいくつかの流儀が知られ
ているが、最も自然と思われる、Kripke modelを用いて様相論理化
したものの公理について考える。

14:40-15:00 休憩20分

16:10-16:40
龍田真（国立情報学研究所）
題目：Non-Commutative First-Order Sequent Calculus 梗概：非
可換一階シーケント計算NCLKについて講演する。まず、非可換
positive fragment を普通の一階シーケント計算で前件にグループ
があり右交換規則のない論理体系LK-に拡張する。次のことを示す。
(1) NCLK は LJ に同等、(2) NCLKに交換規則を追加するとLKに同
等になる、(3) LK-はLJに同等、(4) LK-とNCLKの間の翻訳。

16:45-17:15
龍田真（国立情報学研究所）
題目：TLCA未解決問題20番: 遺伝的置換子の型梗概：TLCA未解決問
題20番とは遺伝的置換子を特徴付ける型システムを見つけよという
問題である．本講演はこれに答える．まず，遺伝的置換子全体が枚
挙不可能であることを示すことにより，そのような型システムが存
在しないことを証明する．次に，最善解として，可算無限個の型を
与え，項がそのすべての型をもつこととその項が遺伝的置換子であ
ることが同等であることを証明する．本講演はLICS2008と同じ内容
である。

17:15-17:30
ビジネスミーティング（次回開催について）

18:00-20:00
懇親会

9/16（日曜日）

10:00-11:00
丸山善宏（Oxford University）
題目：Duality, Quantum Symmetry and Categorical Logic
梗概：After an introduction to duality theory, this talk is
two-fold while duality works as a unifying theme. In the
first part, we aim at articulating Chu Duality hidden in
Categorical Quantum Mechanics (i.e., dagger-compact
categories), thereby giving coalgebraic and logical
characterizations of quantum symmetries. In the second part,
we develop the framework of Categorical Universal Logic
building upon Lawvere's idea of hyperdoctrine, in which
duality theory can be exploited to find various models of
logic and set theory. From this perspective, we discuss the
following issues: Lawvere-Tierney topology; the tripos-topos
construction; and categorical quantum logic.

11:10-12:10
Nonstandard Static Analysis: Discrete Verification Methodologies
蓮尾一郎（東京大学情報理工学研究科）
題目：Nonstandard Static Analysis: Discrete Verification
Methodologies Transferred to Hybrid Applications 梗概：
*Hybrid systems* are those which exhibit both discrete
"jump" and continuous "flow" dynamics. Their importance---as
components of *cyber-physical systems*---is paramount now
that more and more physical systems (cars, airplanes, etc.)
are controlled with computers.

There are naturally two directions towards the study of
hybrid systems: *control theory* (typically continuous) and
*formal verification* (typically discrete). For us from the
formal verification community, therefore, the big challenge
is how to incorporate continuous "flow" dynamics. Many
existing techniques---such as hybrid automaton or Platzer’s
differential dynamic logic---include differential equations
explicitly. This incurs a difficult (and very interesting)
question of how to handle differential equations.

In our project we take a different path of *turning flow
into jump*---more precisely into infinitely many jumps each
of which is infinitesimal (i.e. infinitely small). This
makes everything discrete jump dynamics, to which all the
discrete techniques accumulated in the community of formal
verification readily apply. This venture is mathematically
supported by *nonstandard analysis*, where we can rigorously
speak about infinites and infinitesimals.

In the talk I will lay out: 1) our framework of a
while-language and a Hoare-style program logic, augmented
with an infinitesimal constant, for modeling and
verification of hybrid systems; 2) how discrete verification
techniques can be *transferred*, as they are, to hybrid
applications, via the celebrated *transfer principle* in
nonstandard analysis; and 3) the overview of our prototype
automatic prover.

The talk is based on the joint work with Kohei Suenaga,
Kyoto University. References:

[1] Kohei Suenaga and Ichiro Hasuo. Programming with
Infinitesimals: A While-Language for Hybrid System
Modeling. Proc. ICALP 2011, Track B.  LNCS 6756,
p. 392-403. Springer-Verlag.

[2] Ichiro Hasuo and Kohei Suenaga. Exercises in Nonstandard
Static Analysis of Hybrid Systems. To appear in Proc. CAV
2012.

12:10-13:30 昼食

13:30-14:15
Michele Basaldella (JAIST) （この講演は英語で行われます）
演題：An interactive semantics for classical arithmetic
梗概：In this talk, we introduce a sequent calculus which is
a variant of some well-known proof-systems introduced by
Novikoff, Tait, Coquand, and Herbelin.  A common - and
perhaps the most interesting - aspect of these kinds of
calculi is that they can be used to provide a simple and
elegant formulation of syntactical derivability for first
order classical arithmetic... at a reasonable price: we have
to consider infinitary formulas and infinitary derivations,
rather than the usual finitary ones.  In more detail, we
will talk about a calculus which has the following features:
* we derive sequents (finite multisets) of infinitary
propositional formulas, * some inference rules may have an
infinite number of premises, * derivations are infinitary
trees made of sequents.  We also require that both formulas
and derivations are (infinitary) well-founded objects, which
means that both formulas and derivations can be defined
inductively.  The main purpose of this talk is to define an
interactive semantics for derivations strongly inspired by
Girard's ludics.  The target of this analysis is not the
derivability predicate 'the formula A is derivable' as
traditionally in logic, but the more subtle - and deeper -
statement 'p is a proof of the formula A'.  Specifically, we
define a notion of untyped derivation and a procedure of
interaction (a kind of cut-elimination procedure) between
these untyped objects.  Next, we we define two relations
'PROVES' and 'INTERACTIVELY' between untyped derivations 'p'
and formulas 'A' such that * 'p PROVES A' is defined
inductively, it corresponds to 'p is a proof of the formula
A' in the sequent calculus.  * 'p INTERACTIVELY A' holds
whenever the interaction between 'p' and all the tests for
'A' (special derivations associated to 'A' ) terminates.  We
finally show a soundeness-and-completeness theorem: 'p
PROVES A' if and only if 'p INTERACTIVELY A'.

14:15-15:00
木原貴行(JAIST)
題目：On some variants of the Jayne-Rogers THeorem via the
Posner-Robinson Join THeorem
梗概：位相空間上の関数 F が (m,n)-可測であるとは，ボレル階層
の第 m 段階に属す集合の F による逆像が常にボレル階層の第 n 
段階に属すことである．20世紀初頭，ルージンは任意のボレル可測
関数は可算個の連続関数に分解可能か，すなわち可算的連続かどう
か尋ねた．ルージン問題は1930年代に否定的解決が与えられ，現在
では，m が n 未満ならば，可算的連続でない (m,n)-可測関数が存
在することが知られている．その一方，Jayne-Rogers (1984) は，
(2,2)-可測性と区分的連続性が同値であることを示した．
Jayne-Rogers の定理の(n,n)-可測性への拡張，乃至，ボレル可測
関数の階層における可算的連続性の境界の発見は，現代の実解析学
における重要な問題の一つである．本発表では，連続的(n,n)-可測
性の概念を定義し，チューリング次数の代数的構造に関する 
Posner-Robinson Join Theorem (1981) を介して，次の 5条件の同
値性を与える：「連続的 (n+1,n+1)-可測」「連続的(2,n+1)-可測
かつ可算的連続」「離散ベール第 n 類」「 n 世代神託学習によっ
て同定可能」「第 n 階区分的連続」

15:05-15:35
宮部賢志（京都大学数理解析研究所）
題目：ゲーム論的確率論入門
梗概：ゲーム論的確率論では測度を使わずに確率の理論を展開する．
その手法はランダムネスの理論に強く影響を受けており，証明では
多くの場面でアルゴリズムを作ることが要求される．そこで何らか
の形でコンピュータ科学にも参考になることを期待して，ゲーム論
的確率論の基本的な考え方を解説する．

15:35-15:55 休憩20分

15:55-16:40
松尾亮太（名古屋大学大学院情報科学研究科計算機数理科学専攻）
題目：戦略的論理式
梗概：戦略の定義を、Strategic formulaによって表現されるよう
な写像のことと改めることによって、自然な戦略の理論の構築を目
指す。R_G,n という命題論理の言語を定め、ここの論理式の内で戦
略を表現するようなものをStarategic formula と呼ぶ。この枠組
みによって、人が事実上用いることができる戦略の定義や、戦略の
複雑さの妥当な定義が可能となる。我々の方法の応用として、ゲー
ム理論における最も有名な定理の一つであり、哲学的な問題点も併
せ持った、The perfect folk theorem の解析を試みる。

16:45-17:30
小林聡（京都産業大学コンピュータ理工学部）
題目：未定
梗概：未定

17:35-18:35
佐藤雅大（名古屋大学多元数理科学研究科）
題目：未定（Coqによる数学について）
梗概：今回は私がCoqを用いて直観主義的集合論に基づいた数学の
理論を構築したことについて発表する。Coqで集合論を展開すると
いう試みはたくさん存在するが、今回は「Coqで集合論を展開した」
ということより「Coqで展開できた集合論の上でどのように数学が
展開できたか」という点に焦点を置いて発表したい。

18:35-18:40
次回予定アナウンスおよび挨拶