プログラム
8月31日（土）
9:45 〜 10:00 オープニング＋連絡など
10:00 ～ 12:00
1. 招待講演: 勝股 審也 (国立情報学研究所 ERATO蓮尾メタ数理システムデザインプロジェクト)
題目: 物理情報システムへの数学的アプローチ
梗概:
ERATO蓮尾メタ数理システムデザインプロジェクトでは、ソフトウェアシステム開発のため形式手法を、物理情報システムの開発に拡張し、安全で高品質な工業製品の作成に、理論・応用の両面から貢献することを目指しております。本プロジェクトのメタ理論的統合グループ(グループ0)では、物理情報システムの形式化と構築において基礎となる概念の数学的定式化と分析を進めています。講演ではプロジェクトの紹介と、本グループで得られた以下の結果についてご紹介します。
・双模倣関係のゲームによる特徴づけの一般化 [小森田ら LICS'19]
状態遷移系内の二つの状態の等価性として広く用いられているのが双模倣関係です。いくつかのタイプの状態遷移系においては、それらの上の双模倣関係を二人ゲームの勝利可能位置により特徴づけることが可能ですが、この結果を一般化する方法は知られていませんでした。本研究では状態遷移系を余代数に、関係の概念をファイバー圏により一般化し、関手の余稠密持ち上げ[SprungerらCMCS '18]が定める双模倣関係に対して、それを勝利可能位置として特徴づけるゲームが構成できることを示しました。
・リカレントニューラルネットワークの微分 [Sprunger & 勝股 LICS'19]
リカレントニューラルネットワーク(RNN)は時系列データを処理するようにニューラルネットを拡張したもので、Mealy機械と類似の構造を持ちます。本研究ではニューラルネットのパラメータ調整に欠かせない微分演算をRNNに拡張する方法を与えました。この微分演算はCockettらの微分圏の公理を満たし、またRNNを微分して有限展開したものが、RNNを有限展開して微分するBackpropagation through time (BPTT)と呼ばれる操作と一致することを示しました。
2. Devi Rahmah Sope (近畿大学)
題目: On a Fuzzification and Comparison of Clustering Indices.
梗概:
Fuzzy clustering is given by assigning to each data a set of membership degree to clusters. Quality of such a clustering is evaluated by measuring compactness and separateness. In crisp clustering, many clustering indices are proposed. In this article, we try to fuzzify these clustering indices by using membership degrees with higher order exponent and evaluate the effect in optimization problem.
3. 冨田 悠 (京都大学 数理解析研究所)
題目: Constructing non-symmetric closed categories from planar combinatory algebra
梗概:
Realizabilityにおいて用いられるassembly、modest setの圏の構成を平面ラムダ計算や、対応する組合せ代数に適用することにより、Cartesian closed catalogueやsymmetric monoidal closed categoryよりも弱い構造であるclosed category、closed multi-categoryなどが得られる。これら圏構造を与えるための、構成の基となる組合せ代数に要求される必要条件や十分条件を述べる。
12:00 ～ 14:00 昼食
14:00〜15:30
1. 招待講演: 竹内 泉(産業技術総合研究所)
題目: 数学と変数
梗概:
Mathematics has various usages of variables. There arise a question: Although mathematics has various kinds of variables, how did Frege banish such variables and represent mathematics by his predicate logic with only bound variables? In industrial words of the same question: How do we express various kinds of variables in formal proof systems, such as Coq, Isabelle, and so on, which have only free variables and bound variables? Analysing such usages and interpreting them into predicate logic have the following two significance. The first significance is an academic one. The analysis of usages of variables helps the studies of the histories of mathematics, logic and philosophy. By using the usages of variables as a clue, we can compare the theories by Aristotle, Leibniz and Frege. The other one is industrial. By proving mathematical theorems in formal proof systems, we can verify the specifications of softwares. This study shows the interpretations of various kinds of variables into predicate logic.
2. 本浦 庄太 (日本電気株式会社)
題目: On Logic for Conditional Probabilities of Propositional Formulae
梗概:
Popper proposed, in his work (Popper, 1959), a notion of conditional probability whose arguments are propositional formulae, which is called a Popper function. In this talk, we first explain that an instance of many-sorted monadic second-order logic can define the class of Popper functions, up to isomorphism. We then prove that, for any first-order formula in which any occurrence of a propositional formula is an argument of the predicate symbol for Popper function, it is decidable whether or not the formula is valid. At the end of the talk, we mention a technique to calculate the range of the value of a given conditional probability under given conditions expressed by such first-order formulae.
15:30 ～ 16:00 休憩
16:00 ～ 17:30
1. 藤井 宗一郎 (京都大学 数理解析研究所)
題目: Enriched categories and tropical mathematics
梗概:
We point out a connection of enriched category theory over a quantale and tropical mathematics. Quantales or complete idempotent semirings, as well as matrices with coefficients in them, are fundamental concepts in both fields. We show that standard category-theoretic constructions on matrices, namely composition, right extension, right lifting and the Isbell hull, can unify various notions in tropical mathematics and related fields.
2. 安田 康史 (神奈川大学)
題目: Relationship among orders, semigroups, and quantales
梗概:
Nishizawa and Furusawa showed a relational embedding of powerset quantales in RAMiCS 2012. To analyze the embedding, we studied the relationship among orders, semigroups, and quantales.
3. 西澤 弘毅 (神奈川大学)
題目: Correspondences among classes of weak preorders, partial semigroups, and quantales
梗概:
Our goal is to extend the relational embedding of powerset quantales to a dual equivalence between the category of powerset quantales and the category of some class of preorders. In this talk, we define 6 pullbacks in Cat meaning correspondences among classes of weak preorders, partial semigroups, and quantales.
19:10 ～
意見交換会 @ 漁師小屋
参加登録を締め切りました。参加を希望される方は24日までに お問い合わせは kawamura AT inf.kyushu-u.ac.jp または nishizawa AT kanagawa-u.ac.jp まで。
9月1日（日）
10:00 ～ 12:00
1. 招待講演: 長谷川 勇 (スクウェア・エニックス)
題目: ゲーム開発への代数・論理・幾何と情報科学の適用
梗概:
近年のゲームの大規模化に伴い，ゲーム開発や，それらの品質保証にかかる工数が増大し，ゲーム開発における問題の一つとなっている．こうした開発工数の増大への対策として，ゲーム開発に数学・情報科学を組み合わせた手法を適用することで，これまで機械化が難しく人手に頼っていた工程を自動化し，生産性を向上できる可能性がある．本講演では，モデル検査によるスクリプトの検証など，ゲーム開発に数学・情報科学を適用した事例を紹介する．
2. 塚田 武志 (東京大学)
題目: 不動点算術とプログラム検証
梗概: Program verification is a family of problems to decide if a given program satisfies a given specification. A major approach to problem verification is a logical approach that reduced the verification problem to a logical problem such as satisfiability, validity and model checking problems and then invokes a solver of the logical problem. This approach has been extensively studied for a class of specifications known as safety properties; the verification problem for this class can be naturally reduced to a well-known logical problem, the satisfiability problem of constrained Horn clauses. In this talk, we focus on a fairly general class of specifications, namely omega-regular properties, and see its tight connection to fixed-point arithmetic. The validity problem for fixed-point arithmetic is a natural extension
of the satisfiability problem for constrained Horn clauses, and is polynomial-time equivalent to the verification problem. The latter is a remarkable properties that no existing logical approach has.
3. 立木 秀樹 (京都大学 人間・環境学研究科)
題目: 非構成的対象を扱った証明からのプログラム抽出
梗概: Extraction of programs from proofs about abstract mathematical objects. IFP (Intuitionistic Fixed Point Logic) is a logical system for program extraction developed by Ulrich Berger of Swansea University and his collaborators, and I am also engaged in the project.
IFP is a multi-sorted intuitionistic first order logic extended with induction and coinduction. In IFP, one can extract a program from a proof about abstract mathematical objects defined through axioms, like the set of real numbers. Here, abstract means that we do not fix a representation of an object and representation itself is also extracted from a proof. In this talk, we explain uniform treatment of quantifiers which is a fundamental idea that allows such treatment of mathematical objects, and show some examples of extraction.
12:00 ～ 14:00 昼食
14:00 ～ 15:30
1. 招待講演: 前原 貴憲 (理化学研究所)
題目: 代数的・幾何的・論理的制約下の劣モジュラ関数最大化
梗概:
劣モジュラ集合関数を近似最大化する問題は基本的な組合せ最適化問題であり，機械学習・データマイニングなど幅広い領域に応用をもつ．近年我々はこの問題を集合よりも複雑な制約領域，たとえば束・復体・論理式で指定されるグラフなどに拡張してきた．本発表では現在劣モジュラ最大化がどのような制約で解かれているかを代数・幾何・論理との関係を中心に紹介する．
2. 田中康平 (信州大学 経法学部)
題目: Topological and combinatorial methods in symmetric motion planning
梗概:
M. Farberによって導入されたtopological complexityはロボットモーションの設計に関わる位相不変量である．Farberらはその後，対称性を考慮したsymmetric topological complexityを導入した．本講演では，symmetric topological complexityの組合せ論的近似，およびその精密化について，loop-free categoryを用いた考察を紹介したい．
15:30 ～ 16:00 休憩
16:00 ～ 17:00
1. 山形賴之 (産業技術総合研究所)
題目: Recent progress of consistency proofs of equational systems inside bounded arithmetics
梗概:
We report some results extending a consistency proof of Cook and Urqhart’s PV minus induction inside S22.
17:00 ～ 17:15 クロージング+連絡など