SLACSとは

以下はSLACSのページの冒頭からの抜粋です。

「SLACS（スラックス）は，記号論理学と情報科学の境界領域に関する研究発表・研究討論の場を提供することを目的にして開催されている研究集会です．1985年1月に第１回が開催されて以来，毎年１回のペースで開催されています．SLACS は，堅苦しい研究会ではなく，その年の幹事を中心とした参加者自らの手作りによるフレンドリーな雰囲気を持った集会です．気軽に発表できる場ですから，研究が進行中の話題を持ってきて議論したり，学生さんが発表する場としても適当です．もちろん，発展を続けるこの分野の最先端の研究テーマに関する発表も数多く聞くことができます．参加者の資格は問いませんので，原則として，どなたでも講演発表・聴講いただけます．発表はごく少数の例外を除いて日本語です．」

2020年は以下の要領でオンラインで開催いたしますしました．

• 日時：2020年12月3日(木)から2020年12月4日(金)

• 場所：オンライン（Zoom）（講演の録画はいたしません）

• 参加費：無料

• 幹事：新屋良磨 （秋田大学, ryoma at math.akita-u.ac.jp）

2020年度は参加申込６８人（うち講演者１６人）と大変盛り上がりのある研究集会となりました．
参加していただいた皆様および講演者のみなさま、大変ありがとうございました．

講演予定者・講演概要リスト（申し込み順）

• 新屋 良磨 (秋田大学)「原始語予想 -- a survey」
  概要「原始語とは「自身より短い語の繰り返し」では表されない語 (文字の有限列) のことである． 任意の語はある原始語の繰り返しとして一意に分解することができ，そういった意味で原始語は 語の世界における素数のような対象で， 定義は単純であるが非常に奥深い性質を持っている． 本講演では「原始語の全体集合は非文脈自由か？」という予想[Domosi-Horvath-Ito 1991]についてこれまでの既存研究のアプローチを簡単に紹介する． さらに、密度的な視点から「なぜこの予想が難しいのか」について直感的な理由を解説し、講演者の最近のアプローチ についても説明したい．」

• 高木 翼 (JAIST)「A Multi-modal Logic for Quantum Finite Automata」
  概要「従来の量子論理を拡張した量子オブザーバブル依存論理を一種のMulti-modal Logicとして定式化する。」

• 谷口 雅弥 (JAIST)「CPS変換と多相範疇文法」
  概要「範疇文法にCPS変換を導入する．そのために型付きラムダ計算におけるCPS変換と同様に，範疇文法にも多相型を導入しCPS変換を範疇文法で扱えるように拡張する．」

• 福田 陽介 (千葉工業大学＆京都大学)「Extracting a formal system of typed combinators, informally」
  概要「SKIコンビネータに基づく型付き組み合わせ論理と，直観主義命題論理の含意断片に対するヒルベルト流演繹体系との間には，型付け可能性と証明可能性との間の対応のみならず，簡約と証明正規化をも考慮に入れた対応が考えられることはよく知られている．本発表では，この対応関係を含意以外の論理結合子に拡張するため，型付き組み合わせ論理の形式体系を非形式的な発想に基づいて定義する方法を議論する．」

• 田中 義人 (九州産業大学)「Homomorphisms of multi-relational Kripke frame」
  概要「Multi-relational Kripke framesのhomomorphismを定義し，その圏とmodal algebrasの圏との双対性を2通りの方法で示す．」

• 西村 進 (京都大学)「動的認識論理を用いた分散計算タスクの不可解性証明について」
  概要「特定の分散計算問題(タスク)がさまざまな故障モデルのもとで可解であるかどうかは、分散計算システムの計算能力の限界を示す根源的な指標であり、これまでは組合せトポロジーが手法を援用した方法などが研究されてきている。本講演ではまず、Goubaultらによって近年新しく提案された、論理的障害と呼ばれる動的認識論理の論理式を発見することによってタスクの不可解性を証明するための枠組みについて紹介する。この枠組のもとで、論理的障害を具体的に示すことによって、分散システムにおける集合合意問題が任意の敵対的故障モデルのもとで不可解であることを示す。この論理的障害は、西田が無待機故障モデルのもとでの集合合意問題の不可解性のために示した論理的障害を一般化したものである。講演の最後には、このような認識論理を用いた手法の現状と従来の組合せトポロジー的手法を比較し、将来の研究課題について述べたい。」

• 高木 研斗 (東京工業大学)「Strong Normalization of Natural Deduction for 2Int」
  概要「2Int とは、Wansing [1] によって導入された、co-implication を論理結合子として持つ一種の bi-intuitionistic logic である。「ならば」が仮定から結論への真の保存を内在するのに対し、2Int の co-implication は仮定から結論への偽の保存を内在する。本講演では 2Int の直観主義論理へ埋め込みを与え、強正規化定理を示す。 [1] H. Wansing, Falsification, natural deduction and bi-intuitionistic logic, Journal of Logic and Computation, 26: 425-450, 2016.」

• 間庭 彬仁 (東京工業大学)「Disjunction の両辺を対称に扱わない証明体系について」
  概要「古典論理や直観主義論理のよく知られた証明体系は, disjunction の両辺に関して対称的な規則を持つ. たとえば NJ においては, A と B どちらからでも A \/ B を導入することができる. 本発表では両辺に関して対称的でない規則による disjunction の形式化について考える.」

• 外丸 真一 (東京工業大学)「λ2の完全性について」
  概要「鹿島-松田-湯山は単純型付けラムダ計算においてある種の完全性を示した[1]。今回はこの結果を2階ラムダ計算（λ2）へ拡張したものについて論じる。参考文献[1]R.Kashima, N.Matsuda and T.Yuyama: Term-Space Semantics of Typed Lambda Calculus, Notre Dame Journal of Formal Logic (to appear).」

• 佐藤 隆「Algebraic Number Theory within Weak Fragments of Arithmetic」
  概要「代数学の逆数学についての研究です．二階算術の部分体系RCA*（Δ^0_1集合存在公理＋Σ^0_0帰納法）上で代数的整数論を展開させます，得られた主な結果は，1) 代数閉包の存在はRCA*で証明できる，2) イデアル論の基本定理（素イデアル分解定理）は一階算術の部分体系Elementary Function Arithmeticで証明できる，3) イデアル論の基本定理と数学的帰納法の同値性について，です．
  参考文献：
  Friedman, Simpson, and Smith, Countable Algebra and Set Existence Axioms, Annals of Pure and Applied Logic 25, 1983
  Simpson and Smith, Factorization of Polynomials and $\Sigma^0_1$-Induction, Annals of Pure and Applied Logic 31, 1986.
  Simpson, Subsystems of Second Order Arithmetic, second edition, 2009」

• 佐々木 克巳 (南山大学)「単純証明と様相論理の関係について」
  概要「推論規則としてカットのみをもつ体系は，「ならば」導入規則や「または」の除去規則などの一時的な仮定をもつ推論を含まず，単純な証明を表すと捉えられる．この体系では，無矛盾である限り，それらの一時的な仮定をもつ推論を導出できないことがわかっている．本発表では，その体系と様相論理との関係を明らかにする．」

• 池渕 未来 (MIT)「ホモロジー的方法による公理数の下界の導出」
  概要「群やブール代数などの公理系は一般に知られるものより少ない個数の公理で記述できることが既知である．本発表では，与えられた公理系/項書換系に対して，それを表示するのに必要な公理/書換規則の個数の下界を求める方法について論じる．下界の導出には代数理論のホモロジー代数を用いる．」

• 湯山 孝雄 (東京工業大学)「語の問題が制約オートマトンで認識される群のクラスについて」
  概要「制約オートマトン(constrained automaton)とは，有限オートマトンに``数を数 える''能力を付加した計算モデルである．制約オートマトンは正規言語より広い クラスの言語を認識できる表現力を持つ一方で，よい閉包性や決定可能性を持つ ことが知られている．
  有限生成群Gの語の問題(word problem)とは，生成系上の文字列であってGにおいて単位元に一致するもの全体の集合をいい，組合せ群論において基本的な概念で ある．これまでにいくつかの形式言語のクラスと群の代数的なクラスの対応が調 べられてきたが，制約オートマトンに対応する群のクラスを調べた研究はないように思われる．
  本発表では，語の問題がある制約オートマトンで認識されるような群の代数的なクラスが，実質的アーベル群(virtually abelian group)の全体に一致すること の，発表者による証明の概略を述べる．」

• 早乙女 献自 (名古屋大学)「分離論理の循環証明体系における帰納的述語の制限とカット除去」
  概要「帰納的述語を含む論理式のシークエント計算に対して帰納法を導入する手法として循環証明がある。この手法は、証明探索中に帰納法の仮定を置かなくていいことから、自動証明に向いていると考えられてきた。 しかし、一般に循環証明体系ではカット除去が出来ないことが示されている[Kimura+ 2019]。カット規則の適用にはカット論理式の発見的な探索が求められるため、この適用を可能な限り避けることが求められる。そこで、本研究ではカット規則なしで証明できる帰納的述語の範囲について調べてきた。 結果として、引数をもたない単純な帰納的述語に制限しても、その組み合わせ次第ではカット規則を除去できないことが分かったため、報告する。」

• 只木 孝太郎 (中部大学)「A refinement of the theory of quantum error-correction by algorithmic randomness」
  概要「The notion of probability plays a crucial role in quantum mechanics. It appears in quantum mechanics as the Born rule. In modern mathematics which describes quantum mechanics, however, probability theory means nothing other than measure theory, and therefore any operational characterization of the notion of probability is still missing in quantum mechanics. In our former works, based on the toolkit of algorithmic randomness, we presented a refinement of the Born rule, called the principle of typicality, for specifying the property of results of measurements in an operational way. In this talk, we make an application of our framework to the theory of quantum error-correction for refining it, in order to demonstrate how properly our framework works in practical problems in quantum mechanics.」

• 本多 雄樹 (名古屋大学)「書換え系の変換によるZ性の証明」
  概要「Z定理は書換え系の合流性を証明する手法の一つであり，Z性を満たす写像が存在するならば書換え系が合流性を持つことを保証する．例えば，ラムダ計算のベータ簡約については，ラムダ項中に存在するベータ簡約基を一度に簡約する写像である complete development がZ性を満たすので，Z定理によって合流性が証明できる．しかし，書換え系に対しZ性を持つ写像を構成することは，一般には容易ではない．本研究では，書換え系間の変換を用いて，既にZ性を満たすことが分かっている写像から，新たにZ性を満たす写像を構成する手法を提案する．また，この手法によって interpretation lemma のZ版に当たる定理が成り立つことを示す．さらに，この定理によって明示的代入を含むラムダ計算などの体系がZ性を満たすことを示す．」