Proof and Computation Workshop in AKITA

3月23日(月)--3月25日(水)に秋田大学にて開催予定でした証明論と計算論のワークショップは、新型コロナウイルスの感染拡大防止対策の政府方針を受け、開催を延期いたします．

コロナウィルスが落ち着いたころに開催したいと思いますので，日程は現時点で未定です．続報をお待ち下さい．


日時・場所

  • 日時：2020年3月23日(月) 13:00 -- 3月25日(水) 16:30
  • 場所：〒010-8502 秋田市手形学園町1番1号 秋田大学手形キャンパス総合研究棟 1階講義室 (学内地図)
  • 世話人：新屋良磨 (秋田大学 数理科学コース)
  • 連絡先： ryoma@math.akita-u.ac.jp
  • 備考：23日(月)の講演は13:00からの開始ですが，東京から秋田への移動には新幹線で4時間ほどかかるのでご注意ください．

講演予定者(決定順・敬称略)

  • 新屋良磨(秋田大) ：「語の組合せ論入門：WQOとオートマトン」(チュートリアル講演, 40分)
  • 松田直祐(神奈川大) ：「Curry-Howard対応入門(仮)」(チュートリアル講演, 40分) および「中間論理の公理とオーダーの関係」(50分)
  • 藤原誠(明治大) ：「On the relation between Weihrauch reducibility in computable analysis and constructive reverse mathematics」(50分)
  • 山﨑紗紀子(首都大) ：「直観主義論理の線形論理への埋め込み－後件複数なG3-styleでない直観主義論理のシークエント計算を用いて」 (30分)
  • 鹿島亮(東工大) ：「様相μ計算入門」(チュートリアル講演)(40分)
  • 間庭彬仁(東工大) ：「Intuitionistic Provability Logic IGL の Natural Deduction」(30分)
  • 木原貴行(名古屋大) ：「BQO理論: ボレル可測関数の組合せ構造として」(75分)
  • 小川瑞史(JAIST) ：「WQO and regularity」(60分)
  • 塚田武志(東大) ：「高階不動点演算子とゲーム量化子」(50分)
  • 横山啓太(JAIST) ：「算術における組み合わせ論と停止性検証」 (50分)
  • 高木研斗(東工大) ：「A natural deduction for bi-intuitionistic logic derived from truth tables」(40分)
  • 木村大輔(東邦大) ：TBA (50分)
  • Leonardo Pacheco(東北大) ：「An introduction to mu-arithmetic and difference hierarchy」(30分)
  • 水野雅之(東北大) ：「Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion」(30分)
  • 市川航士郎(東工大附属) ：「順序数解析とその応用」(40分)
  • 益岡幸弘(NII) ：「Introduction to Cyclic Proof System」(40分)
  • 中野圭介(東北大) ：「対合チューリング機械とその性質」 (50分)
  • 中林美郷(NTT) ：「暗号技術と形式検証」(30分)

プログラム(2月3日版)

3月23日(月)

  • 12:30：開場
  • 12:50--13:00：開会
  • 13:00--13:40：松田直祐(神奈川大) ：「Curry-Howard対応入門(仮)」(チュートリアル講演)
  • 13:50--14:30：新屋良磨(秋田大) ：「語の組合せ論入門：WQOとオートマトン」(チュートリアル講演)
  • 14:50--15:30：鹿島亮(東工大) ：「様相μ計算入門」(チュートリアル講演)
  • 15:40--16:50：学生セッション1
    • Leonardo Pacheco(東北大) ：「An introduction to mu-arithmetic and difference hierarchy」
    • 市川航士郎(東工大附属) ： 「順序数解析とその応用」
  • 16:50--17:20：中林美郷 ：「暗号技術と形式検証」
  • 17:30--18:20：横山啓太(JAIST) ：「算術における組み合わせ論と停止性検証」
  • 18:30--20:00：交流会@秋田大学大学会館「クレール」2F


3月24日(火)

  • 9:30：開場
  • 10:00--11:00：小川瑞史(JAIST) ：「WQO and regularity」
  • 11:15--12:30：木原貴行(名古屋大) ：「BQO理論: ボレル可測関数の組合せ構造として」
  • 12:30--14:20：お昼休憩
  • 14:20--15:30：学生セッション2
    • 益岡幸弘(NII) ：「Introduction to Cyclic Proof System」
    • 水野雅之(東北大) ：「Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion」
  • 15:40--16:30：藤原誠(明治大) ：「On the relation between Weihrauch reducibility in computable analysis and constructive reverse mathematics」
  • 16:40--17:30：塚田武志(東大) ：「高階不動点演算子とゲーム量化子」
  • 17:40--18:30：中野圭介(東北大) ：「対合チューリング機械とその性質」
  • 19:00--21:00：懇親会 (場所未定)


3月25日(水)

  • 9:30：開場
  • 10:00--10:50：松田直祐(神奈川大) ：「中間論理の公理とオーダーの関係」
  • 11:00--11:50：木村大輔(東邦大) ：TBA
  • 11:50--13:20：お昼休み
  • 13:20--15:00 ：学生セッション3
    • 間庭彬仁(東工大) ：「Intuitionistic Provability Logic IGL の Natural Deduction」
    • 高木研斗(東工大) ：「A natural deduction for bi-intuitionistic logic derived from truth tables」
    • 山﨑紗紀子(首都大) ：TBA (30分)
  • 15:20--16:20 ：未解決問題共有・議論会
  • 16:20--16:30：閉会

交流会・懇親会への参加

23日に18:30~20:00にかけて秋田大学生協にて簡単な交流会(参加費1000円程度，軽食とドリンク付き)を，24日は懇親会(参加費3000円--5000円程度，飲み放題夕食込み)を行う予定です．

人数を把握する必要があるため，交流会・懇親会への参加を希望されるかたは，参加希望の旨を3月6日(金)までに新屋( ryoma@math.akita-u.ac.jp )にご連絡よろしくお願いします．

講演概要

  • 松田直祐(神奈川大) ：「Curry-Howard対応入門(仮)」(チュートリアル講演)

TBA


  • 新屋良磨(秋田大) ：「語の組合せ論入門：WQOとオートマトン」(チュートリアル講演)

正規言語は「有限状態で計算できる語の集合」という非常に単純な定義を持つが、その単純さゆえに計算論に留まらずさまざまな分野での道具を用いて定式化できる対象である．本チュートリアルでは組合せ論的な導入から well-quasi-order (WQO)と呼ばれる順序概念を説明し、「Lが正規 iff Lはある単調なWQOの上方集合(upward closed set)」という Ehrenfeucht-Haussler-Rozenbergの定理の証明を解説する．


鹿島亮(東工大) ：「様相μ計算入門」(チュートリアル講演)

様相ミュー計算は「計算」という名前が付いているが論理の体系である。これは単純な様相論理K（またはそのmultimodal版）に不動点演算子を加えたものであり，不動点演算子の働きによって非常に強力な記述力を持つ。本チュートリアルでは様相ミュー計算の状態遷移系（クリプキフレーム）による基本的な意味論およびゲーム意味論を解説する。さらに公理系の完全性についても簡単に説明する。


Leonardo Pacheco(東北大) ：「An introduction to mu-arithmetic and difference hierarchy」

TBA


市川航士郎(東工大附属) ： 「順序数解析とその応用」

本講演では, 公理系の強さを証明論的順序数(proof-theretic ordinal)という不変量を持って比較する順序数解析(ordinal analysis)という分野について紹介する. 順序数解析のメソッド, そしてその応用を, Gentzenのカット除去定理から 順に説明する.


中林美郷(NTT) ：「暗号技術と形式検証」

現代の暗号技術の安全性は、数学的な証明によって保証されている。しかし、暗号技術の安全性証明は一般的に煩雑であり、後からミスや脆弱性

が見つかることもある。

そのため、コンピュータを用いて形式的に暗号技術の安全性を検証・証明する形式検証に関する研究が盛んに行われている。

本発表では、確率Hoare論理を用いた暗号技術の安全性証明と最新の事例である耐量子暗号技術の形式検証について紹介する。


横山啓太(JAIST) ：「算術における組み合わせ論と停止性検証

TBA


小川瑞史(JAIST) ：「WQO and regularity」

TBA


木原貴行(名古屋大) ：「BQO理論: ボレル可測関数の組合せ構造として」

TBA


益岡幸弘(NII) ：「Introduction to Cyclic Proof System」

TBA


水野雅之(東北大) ：「Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion」

TBA


藤原誠(明治大) ：「On the relation between Weihrauch reducibility in computable analysis and constructive reverse mathematics」

We formalize the primitive recursive variants of Weihrauch reduction between existence statements in finite-type arithmetic and show a meta-theorem stating that the primitive recursive Weihrauch reducibility verifiably in a classical finite-type arithmetic is identical with the formal reducibility in the corresponding (nearly) intuitionistic finite-type arithmetic for all existence statements formalized with existential free formulas.

In addition, we study the primitive recursive variants of Weihrauch reduction for the parallelizations of existence statements, which are extensively investigated in computable analysis and also studied in classical reverse mathematics.

Then we demonstrate that our meta-theorem is applicable in some concrete examples from classical and constructive reverse mathematics.

This kind of work should shed light on the correspondence between computable analysis and constructive reverse mathematics which have been developed independently until recently.

This talk would be given in Japanese with the presentation slides written in English.



塚田武志(東大) ：「高階不動点演算子とゲーム量化子」

TBA


中野圭介(東北大) ：「対合チューリング機械とその性質」

自分自身が逆関数となる関数，すなわち，任意の入力 x に対して f(f(x)) = x を満たす関数 f を対合とよぶ．本講演では，対合である計算可能関数を過不足なく表現できる計算モデルとして「対合チューリング機械」を提案し，その性質や応用を紹介する．また，本研究への理解を深めるため，今回のアイデアの元となった可逆チューリング機械とその性質に関する結果についても併せて紹介する．


松田直祐(神奈川大) ：「中間論理の公理とオーダーの関係」

型理論において，単純型（含意論理式）のオーダーとは，以下で与えられる指標である：

Ord(p) = 1,

Ord(A -> B) = max{Ord(A)+1, Ord(B)}.

本講演では，オーダーの観点から中間論理の公理に対して考察を与え，任意の中間論理 L（ただし，直観主義論理を除く）

に対し以下が成り立つことを示す

(1) L の公理化には，オーダー4の公理が必要である，

(2) L の公理化は，オーダー4以下の公理だけで可能である．

なお，本講演は東京工業大学中村誠希氏との共同研究に基づく．


木村大輔(東邦大) ：TBA

TBA


間庭彬仁(東工大) ：「Intuitionistic Provability Logic IGL の Natural Deduction」

Intuitionistic provability logic IGL は IK を公理□(□A→A)→□A によって拡張したものである. 本発表では Pfenning and Wong (1995) が IS4 の natural deduction を定義する際に用いた形式化に基づいて, IGL の natural deduction を与える. また, この term calculus が不動点演算の性質を適切に捉えていることを示す.


高木研斗(東工大) ：「A natural deduction for bi-intuitionistic logic derived from truth tables」

Geuvers and Hurkens (2017) は直観主義論理のクリプキ意味論を真理値表に基づく一般の論理結合子に拡張し，それに関して完全な自然演繹を与えた．本発表では，bi-intuitionistic logic に関しても，クリプキ意味論と Tranchini (2017) による自然演繹 NBI が真理値表に基づく一般の論理結合子に拡張できることを示す．


山﨑紗紀子(首都大) ：直観主義論理の線形論理への埋め込み－後件複数なG3-styleでない直観主義論理のシークエント計算を用いて」

直観主義論理が線形論理にある種の翻訳のもとで埋め込み可能であることはよく知られた結果である。このとき用いられる直観主義論理の体系は、一般的には後件が一つのシークエント計算である。しかし、直観主義論理には後件が複数なシークエント計算の体系も存在することが知られている。本発表では、直観主義論理の線形論理への埋め込みを、後件が複数な直観主義論理のシークエント計算を用いて証明論的に示す。

過去の秋田新春ワークショップ