第41回 記号論理と情報科学 研究集会（SLACS 2024）
2024年 8月 21日（水）～ 22日（木）
2024年 8月 21日（水）～ 22日（木）
「SLACS（スラックス）は，記号論理学と情報科学の境界領域に関する研究発表・研究討論の場を提供することを目的にして開催されている研究集会です．1985年1月に第１回が開催されて以来，毎年１回のペースで開催されています．SLACS は，堅苦しい研究会ではなく，その年の幹事を中心とした参加者自らの手作りによるフレンドリーな雰囲気を持った集会です．気軽に発表できる場ですから，研究が進行中の話題を持ってきて議論したり，学生さんが発表する場としても適当です．もちろん，発展を続けるこの分野の最先端の研究テーマに関する発表も数多く聞くことができます．参加者の資格は問いませんので，原則として，どなたでも講演発表・聴講いただけます．発表はごく少数の例外を除いて日本語です．」
講演申し込みをされる場合は，参加登録は不要です．
（両方登録されても問題はありません．）
懇親会を 8月 21日（水）の夜に行います．
【懇親会キャンセルされる方は，前日（20日）までにご連絡ください．】
8/21（水）
12:55 - 13:00 オープニング
13:00 - 13:40 佐藤雅彦（京都大学情報学研究科） 「λ-計算の代数と幾何」
概要：It is well-known that the set Λ of open terms of type-free λ-calculus dose not behave naturally when we regard Λ as an algebra equipped with the operation of function application. For example, the standard translation of λ-terms into combinatory terms does not admit the ξ-rule of the λ-calculus ([1; page 153]). To be more precise, the situation is that (1) for the Combinatory Logic, there are combinatory algebras which are sound and complete with respect to CL, but (2) these algebras are not sound for the λ-calculus because of the ξ-rule.
Selinger [2; page 558] introduced the notion of "absolute interpretation" and gave a lambda algebra which is closed under the ξ-rule. However, the ξ-rule still remains in the original λ-calculus.
In this talk, I will introduce a modified version of the λ-calculus without the ξ-rule but can prove exactly the same set of equations (under the β-equality) as those provable in the original λ-calculus.
The key idea is to re-define Λ as an algebra on which the free monoid generated by the set of variables acts. The idea is obtained by analyzing the difference between Frege style canonical judgments and Martin-Löf style hypothetical judgements.
[1] Barendregt, H. P. (1984) The Lambda Calculus, its Syntax and Semantics. 2nd edn. North-Holland.
[2] PETER SELINGER, The lambda calculus is algebraic, JFP 12 (6): 549–566, November 2002.
13:40 - 14:20 織田幸弘（東北大学） 「部分逆正当性のための論理」
概要：逆 Hoare 論理(reverse Hoare logic) または逆正当性論理(incorrectness logic)とは Hoare-style logic の一種で，与えられたプログラムに対して「任意の事後条件を満たしている状態 s' に対して，与えられた事前条件を満たしかつ s' へ至る実行経路が存在する状態 s の存在」を保証する形式体系である．この論理は非決定性プログラムの形式検証の観点で有用である．また，停止性をも保証しているという点で，「全体的」である．本講演では，この逆 Hoare 論理を「部分的」にした部分逆 Hoare 論理の証明体系を紹介する．
14:20 - 14:40 （20分休憩）
14:40 - 15:20 新家麗夏（奈良女子大学） 「ユークリッド幾何の問題への数式処理システムの応用」
概要：計算代数学と数式処理技術の進展で、以前は扱えなかった複雑な数式も計算可能になった。近藤・斎藤・竹島の線形写像法を用いて、平面ユークリッド幾何の最大最小問題を自動化することを目指している。現在、具体例を集積中である。本講演では、その現状を報告する。
15:20 - 16:00 谷口雅弥（理化学研究所） 「Lambek Calculus and Regular Grammar」
概要：In the 1990s, Noam Chomsky viewed the Lambek calculus (a type of substructural logic and linear logic) as a grammatical system—dubbed Lambek grammar—and posed the question: "Does the expressive power of this grammar fall within the realm of context-free grammars?" This problem was conclusively solved by Martin Pentus in 1993 and 1997, who answered in the affirmative.
This research aims to reverse this approach by exploring systems within the Lambek calculus that correspond to regular grammars, which are less powerful than context-free grammars. Intuitively, we suspect that the system corresponding to regular grammars is equivalent to a weaker form of Lambek calculus. Guided by this intuition, we introduce subsystems of the Lambek calculus and report on the constraints necessary to link the Lambek calculus with regular grammars. This study is a collaborative effort with Yusaku Nishimiya, a student trainee at RIKEN from the University of Illinois Springfield.
16:00 - 16:20 （20分休憩）
16:20 - 17:00 佐藤はづ希（奈良女子大学大学院人間文化総合科学研究科） 「線形論理とBDI logicを用いた自律エージェントの形式化」
概要：自律エージェントの動作を記述するためのBDI logicは、古典論理に心的オペレータを導入した様相論理である。古典論理に基づく推論では、必要に応じて同じ前提を何度も使うことができる。しかし、自律エージェントの動作を決定する推論において、一度使ったら消費される資源を表現する場合がある。現在のBDI logicに基づく推論では、一度使ったら消費されるはずの前提を何度も使ってしまう点が適切ではない。そこで、資源の消費を表すことができる線形論理をBDI logicと組み合わせ、新しい論理体系を提案し、適切な形式化を行う。
17:00 - 17:40 高木翼（JAIST） 「多ソート等式論理による量子計算の形式仕様記述」
概要：多ソート等式論理によって量子計算の仕様を形式的に記述し，それに基づいた量子計算の形式検証を行う．
17:40 - 18:00 （20分休憩）
18:00 （18:30からの懇親会へ出発）
8/22（木）
9:00 - 9:40 浅田和之（東北大学 電気通信研究所） 「Linear Algebraic Semantics of Linear Logic」
概要：A number of models of linear logic are based on or closely related to linear algebra, in the sense that morphisms are “matrices” over appropriate coefficient sets. Examples include models based on coherence spaces, finiteness spaces and probabilistic coherence spaces, as well as the relational and weighted relational models. This paper introduces a unified framework based on module theory, making the linear algebraic aspect of the above models more explicit. Specifically we consider modules over Σ-semirings R, which are ring-like structures with partially-defined countable sums, and show that morphisms in the above models are actually R-linear maps in the standard algebraic sense for appropriate R. An advantage of our algebraic treatment is that the category of R-modules is locally presentable, from which it easily follows that this category becomes a model of intuitionistic linear logic with the cofree exponential. We then discuss constructions of classical models and show that the above-mentioned models are examples of our constructions.
(Presented at LICS 22 (and POPL 24). Joint work with 塚田 武志.)
9:40 - 10:20 伊藤耀（東北大学情報科学研究科） 「係数環完備化と貼合せ・直交性に基づく線形論理のΣ加群モデルの再構成」概要：2022年に塚田・浅田はΣ半環R上の加群の圏による線形論理のモデルを与えた．係数環Rの選択に応じて，コヒーレンス空間のモデルやScott領域のモデルなど既存の多くのモデルと一致することが示され，2024年には量子FPCの完全抽象モデルが得られた．この係数環Rは和が無限項演算であると同時に部分関数であることが許され，和が全域なときに完備と呼ばれるが，完備でない係数環の加群モデルの分析は著しく複雑になる欠点があった．
本研究では，係数環Rの完備化に「貼合せと直交性」によるモデル構成法を組み合わせることで，R加群の圏の部分関数を用いない表現方法を与える．2003年にHylandとSchalkによって与えられた「貼合せと直交性」の手法は線形論理モデルの「部分モデル」を削り出す手法で，これにより係数環Rを完備化した係数環R'の加群モデルから元のR加群の圏を削り出す．現時点では同手法を適用した係数環R'の加群モデル上に係数環RにおけるMLLモデルを再構成できており，さらにRの完備化に限らず一定条件を満たす係数環においても同様の結果が得られている．
10:20 - 10:40 （20分休憩）
10:40 - 11:20 佐原悠太・三好博之（京都産業大学理学研究科数学専攻・理学部数理科学科） 「連続なCDU-categoriesについて」
概要：論文Jacobs-Kissinger-Zanasi(2021)では統計的因果推論を圏論的に扱うためにCDU-categoriesを導入しているが、有限確率のみを念頭に置いているので、本講演ではこれを連続確率に拡張する試みについて述べる。
11:20 - 12:00 中村卓武（東北大学情報科学研究科） 「機械学習におけるアーキテクチャ構成とその学習手法 の圏論的構造化」
概要：本発表では勾配に基づく学習の計算の持つ構造に着目し，その学習アルゴリズムを構成する操作を圏論を用いて定義する．そしてアルゴリズムの性質や訓練手法の圏論的な分析と一般化を試みる．このような学習アルゴリズムの構成は既存研究にて既に提案されていて，振舞いに基づく抽象化を重視するFongらの構成があり，本研究ではこれを一般化・モジュール化する．この新しい構成法では機械学習におけるアーキテクチャの結合と，アーキテクチャを用いた学習アルゴリズムの構成を同時に（順不同で）行うことができ，これらの構成の操作を同じ圏で表現できる．さらにstring diagramと呼ばれる形式的なグラフィカル言語を用いることで，これらの構成を一つの図の上で表現することが可能になる．これを応用して，教師強制と呼ばれる近似を用いた訓練法も図で表現する．そして学習アルゴリズムに限らず，あらゆる同形の計算に対して適用できるように，教師強制を一般化する．
12:00 - 13:20 （昼食）
13:20 - 14:00 中野圭介（東北大学） 「木オートマトン探索による単一非消去組合せ子計算の停止性の反証」
概要：項書換え系の停止性の反証法として，非停止性を特徴付ける非空集合を与える方法が知られている． EndrullisとZantemaは，この集合が木オートマトンで表される場合に限り，SATソルバを繰り返し用いることで発見できることを示した． 本発表では，彼らの手法を応用し，単一の非消去組合せ子によって与えられる計算体系の停止性の反証に成功したことについて報告する． 具体的には，まず，この計算体系の非停止性を特徴付ける木オートマトンについては特定の形を考えれば十分であることを示し，その形の木オートマトンであれば効率的な探索が可能になることを示す． この提案手法の実装により，これまで非停止性が明らかでなかったいくつかの組合せ子について停止性の反証に成功した． なお，本内容は CIAA 2024 において発表予定である．
14:00 - 14:40 鴨浩靖（奈良女子大学） 「近藤・斎藤・竹島の線形写像法による連立代数方程式の実数解の厳密解法のSingularでの実装」
概要：近藤・斎藤・竹島の線形写像法は連立代数方程式のすべての実数解を任意に与えられた精度で計算するアルゴリズムである。このアルゴリズムを数式処理システムSingularで実装した。
14:40 - 15:00 （20分休憩）
15:00 - 15:40 恩田直登（OMRON SINIC X） 「Automated Theorem Proving by HyperTree Proof Search with Retrieval-Augmented Tactic Generator」
概要：We propose an automated theorem prover (ATP) based on the HyperTree Proof Search (HTPS) enhanced by retrieval-augmented tactic generator (ReProver). This presentation is a joint research project with Sho Sonoda (RIKEN), Kei Tsukamoto (University of Tokyo), Fumiya Uchiyama (University of Tokyo), Akiyoshi Sannai (Kyoto University), and Wataru Kumagai (OSX).
15:40 - 16:20 中澤巧爾（名古屋大学） 「Relative Completeness of Incorrectness Separation Logic」
概要：Incorrectness Separation Logic (ISL) is a proof system that is tailored specifically to resolve problems of under-approximation in programs that manipulate heaps, and it primarily focuses on bug detection. This study establishes relative completeness by leveraging the expressiveness of the weakest postconditions. (This is joint work with Lee Yeonseok, and it will be presented at APLAS 2024.)
16:20 - 17:00 小島良太（数理解析研究所） 「neighborhood frame上の計算木論理」
概要： 非決定的システム（Kripke frame）に対するモデル検証のフレームワークとしてEmersonとClarkeによる計算木論理（CTL）は，その計算量的な優位性において，特別な位置を占めている．本研究はCTLのKripke frame上の意味論をneighborhood frame上へと拡張するものである．ScottやMontagueによって導入されたneighborhood frameは‘‘二重の’’非決定性を有し，それによって従来のKripke frameを包括するのみならず，失敗や介入などの‘‘予測不可能性’’を持ったシステムのモデリングにも応用できる．本研究では計算路（computation path）に代わる新たな概念，計算戦術（computation strategy）を導入することで，CTLがそのモデル検査の効率性を失わずにneighborhood frame上へと拡張できることを示す．
17:00 - 18:00 クロージング（＋継続議論）