Declarative Distirbuted Programming based on Combinatorial Topology

近年、分散並列計算の組合せ幾何的モデルと、動的認識論理のKripkeモデルが相互に深く関連していることが明らかとなり、この2つの分野の交流による研究が盛んになってきている。組合せ幾何的モデルでは、分散計算問題の可解性を単体的複体モデルにおける高次元の連結性に帰着して議論するが、一定の条件の下で同様の議論を単体的複体モデルと同型なKripkeモデル上で認識論理を用いて行うことができる。特にGoubaultらは、障害論理式、すなわち分散並列システムに対応するKripkeモデルでは成り立つが実現したい分散並列計算に対応するKripkeモデルでは成り立たないような認識論理式をひとつ発見することによって、分散計算問題の不可解性を立証できることを示した。しかしながら、認識論理を用いる方法は基礎的な適用例が少し明らかになったばかりであり、計算モデルの精密化や適用範囲を拡張するための研究が進行しているところである。本年度は、前年度から継続の、並列分散システム中のプロセスが何度でも情報を交換できる複ラウンド計算モデルに対して認識論理の拡張である認識μ計算を用いてk集合合意問題の不可解性を示す研究を完成させ、2022年初夏にパリで開催された研究集会で発表した。その内容をまとめた論文を現在国際誌に投稿中である。さらに、分散同期メッセージ通信プロトコルによって分散合意問題が不可解であることを障害論理式を用いて示した。(大学院生2名との共同研究) この不可解性自体はすでに組合せ幾何的モデルで知られた結果であったが、認識論理の枠組みでは示されていなかった。本研究において、Goubaultらが示した分散同期メッセージ通信の単体的複体モデルに適合したKripkeモデルに対して、障害論理式を適用するのに必要な動的認識モデルの構成に必要な積更新モデルの構成方法を与えることによってこれを達成した。

近年、分散並列計算の組合せ幾何的モデルと、動的認識論理のKripkeモデルが相互に深く関連していることが明らかとなり、この2つの分野の交流による研究が盛んになってきている。組合せ幾何的モデルでは、分散計算問題の可解性を単体的複体モデルにおける高次元の連結性に帰着して議論するが、一定の条件の下で同様の議論を単体的複体モデルと同型なKripkeモデル上で認識論理を用いて行うことができる。特にGoubaultらは、障害論理式、すなわち分散並列システムに対応するKripkeモデルでは成り立つが実現したい分散並列計算に対応するKripkeモデルでは成り立たないような認識論理式をひとつ発見することによって、分散計算問題の不可解性を立証できることを示した。しかしながら、認識論理を用いる方法は基礎的な適用例が少し明らかになったばかりであり、計算モデルの精密化や適用範囲を拡張するための研究が進行しているところである。本年度は、前年度から継続の、並列分散システム中のプロセスが何度でも情報を交換できる複ラウンド計算モデルに対して認識論理の拡張である認識μ計算を用いてk集合合意問題の不可解性を示す研究を完成させ、2022年初夏にパリで開催された研究集会で発表した。その内容をまとめた論文を現在国際誌に投稿中である。さらに、分散同期メッセージ通信プロトコルによって分散合意問題が不可解であることを障害論理式を用いて示した。(大学院生2名との共同研究) この不可解性自体はすでに組合せ幾何的モデルで知られた結果であったが、認識論理の枠組みでは示されていなかった。本研究において、Goubaultらが示した分散同期メッセージ通信の単体的複体モデルに適合したKripkeモデルに対して、障害論理式を適用するのに必要な動的認識モデルの構成に必要な積更新モデルの構成方法を与えることによってこれを達成した。