2021 Fiscal Year Research-status Report
Declarative Distirbuted Programming based on Combinatorial Topology
| Project/Area Number |
20K11678
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
西村 進 京都大学, 理学研究科, 准教授 (10283681)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Keywords | 並行分散計算 / 分散計算の数理論理モデル / 認識μ計算 / 宣言的プログラミング |
|---|
| Outline of Annual Research Achievements |
並列分散プログラムの宣言的な記述のためには、並列分散プログラムに関わる計算構造の本質的な理解が必要不可欠である。本研究では並列分散計算を単体的複体の変形として捉える組合せ幾何的手法を元にしてこれを達成しようとしている。その際、非自明な幾何分野の定理の適用が必要となる。このような議論をこれまでの記号計算を中心とする従来のプログラミング手法と融合する方法は明らかでなく、これが幾何的手法からの知見を宣言的並列分散プログラミングとして実現するときの障害となっている。
本年度の研究では、前年から引き続き分散並列計算の認識論理モデルについて研究を行った。前年までに、認識論理を用いた手法によって並列分散計算理論の重要な問題のひとつであるk集合合意問題が不可解であることを示した。しかしながらこの成果は、並列分散システム中のプロセスが一度だけしか互いに情報を交換できない単ラウンド計算モデルにしか適用できなかった。本年度の研究では、認識論理の体系を、様相μ計算の変種である認識μ計算に拡張することで、(プロセスが何度でも互いに情報を交換できる)複ラウンド計算モデルの場合でもk集合合意問題が不可解であることを示した。
上記の成果は、幾何的手法と従来のプログラミングの理論における記号計算の橋渡しを示すという点で重要である。k集合合意問題の不可解性を、幾何的手法ではSperner補題と呼ばれる非自明な組合せ幾何の定理を用いて示すところを、本研究ではこのSperner補題の元々の証明を幾何的連結性に関する議論に翻訳し直すことによって、認識μ計算の論理式で記号的に表すことに成功した。またこの論理式は不可解性の理由を、幾何的な証明と比べてより直接的に与えているという点でも大変興味深いものである。
この成果の発表・公表は年度内には間に合わなかったが、近々開催される国際研究集会で発表を行う予定である。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
本年度の研究では、前年度に提案した並列分散計算の認識論理モデルを拡張し、認識μ計算によってk集合合意問題の不可解性を示すことに成功した。前年の提案では、並列分散システム中のプロセスが一度だけしか互いに情報を交換できないというあまり現実的でない制限があったが、今年度の成果によってそのような制限は取り払われ、より現実に近いシステムについての議論が可能になった。なおこの結果は、従来の幾何的手法において証明の中核となっている高次元連結性に関する議論を、認識μ計算が提供する最大不動点演算子によって表現することによって、記号計算で高次元連結性の議論を行うことを可能にしているものである。これによって、並列分散プログラムの宣言的記述との親和性を高めることができた。
上記の研究結果は、当初の証明に含まれていた間違いの修正を要したことや、新型コロナ感染症による機会の喪失等によって公表が遅れている。しかしながらこの成果は近日開催される国際研究集会において発表予定である。
|
| Strategy for Future Research Activity |
並列分散計算の認識論理モデルはごく近年に提案された研究トピックで、未整備ではあるが活発に研究が行われており、本研究で実現した複ラウンド計算モデルだけではなく、その他さまざまな並列分散計算モデルの拡張に対する適用が提案・期待されている。本研究で提案した認識μ計算を利用することで、これら拡張のいくつかに対して同様の成果を見出すことに貢献したい。
また、現在までの知見では、認識論理や認識μ計算がどの程度の並列分散計算を記述できる能力があるのかは曖昧である。認識論理体系がそれぞれの変種毎にどのくらいの記述能力があるのかを考察することによって、宣言的並行分散論理型プログラミングのふさわしい形を見出したいと考えている。
これらの研究の推進に際しては、前述の国際研究集会への出席等を通して、並列分散計算の認識論理モデルの創始者グループと議論・情報交換も行っていきたい。
|
| Causes of Carryover |
昨年度に引き続き、新型コロナ感染症の流行により学会出席・研究出張が困難になったために旅費をほとんど執行できなかったのが主たる理由である。
幸い現在のところ新型コロナ感染症の流行による渡航制限等も緩和されてきているので、近日開催の国際研究集会に出席・発表の予定である。また夏には別の国際研究集会において研究講演を依頼されている。これらの活動を通して、前年度できなかった分の執行を進めていく予定である。これらの研究集会への出席は、関連研究分野の研究者と久しぶりに直接議論・情報交換できる重要な機会であり有効活用していきたい。
|
