2022 Fiscal Year Research-status Report
| Project/Area Number |
22K17850
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
室屋 晃子 京都大学, 数理解析研究所, 助教 (00827454)
|
|---|
| Project Period (FY) |
2022-04-01 – 2025-03-31
|
| Keywords | 項書き換え系 / 危険対解析 / 文脈等価性 / プログラム等価性 |
|---|
| Outline of Annual Research Achievements |
本研究は、模倣合同性の立証手法を提案・自動化することにより、プログラム等価性の自動証明手法を与えることを目指すものである。本年度では、制限つきの項書き換え系において模倣合同性の立証手法を定式化し、それに基づいて自動判定アルゴリズムを構築することを目標として研究を行い、制限つきの項書き換え系として「項評価系」を提案した。この項評価系について、項書き換え系に関するワークショップ58th TRS Meeting (2023年2月)での発表を行った。
プログラムの実行を項書き換え系で表現するためには、既知の2種類の制限を加える必要があると予想されていた。1つ目は書き換えの場所を制限する手法(Lucas 1995)であり、2つ目は書き換え対象を構文的に制限する手法(Hamana et al. 2020)である。ところが、必要な制限はこの2つだけではなく、書き換えの順序を制限する手法が新たに必要であることが分かった。プログラム実行のモデリングにおいては、評価文脈を用いて書き換えの場所・順序を制限する手法が主流となっている。そこで、項書き換え系に評価文脈を組み合わせることで、書き換えの場所・順序が制限できるような新たな系を開発し、項評価系と名づけた。
この成果は、項書き換え系理論の知見をプログラム意味論へ応用する上での大きなステップと捉えられる。プログラム実行がしばしば項書き換え系と見なされうるにも関わらず、項書き換え系理論からプログラム意味論への知見・技術の移植は進んでいない現状がある。項評価系という本年度の研究成果は、そのような状況に対して、プログラム意味論で基本的な概念である評価文脈が項書き換え系には欠如していることが根本的な原因であることを示唆するものである。項評価系に項書き換え系の技術を移転することで、項書き換え系の技術をプログラム意味論へ応用することが可能になると考えられる。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
当初計画では、本年度は制限つき項書き換え系において模倣合同性の立証手法を構築・自動化する予定であった。制限つき項書き換え系は既知の2種類の制限(Lucas 1995, Hamana et al. 2020)を組み合わせることで得られるという予想を立てていたが、この予想に反し、評価文脈という基本的かつ新たな制限が必要であることが明らかになった。
本年度はまず、よりシンプルな一階の項評価系を構築することに注力し、プログラム実行のモデリングに必要となる高階の項評価系の構築には至らなかった。それに伴い、一階の項評価系での模倣合同性の立証手法を考察することはできたものの、高階の項評価系での模倣合同性の立証手法を提案・自動化するには至らなかった。
|
| Strategy for Future Research Activity |
次年度以降は、模倣性の具体的定義を拡張することで提案手法の適用範囲を広げる研究を行う予定であったが、本年度の積み残しに優先的に取り組み、その後に当初予定の研究を続行する計画である。
本年度の積み残しの1つ目は、高階の項評価系を構築することである。これは一階の項評価系を元に比較的容易に構築できると考えられる。積み残しの2つ目は、模倣合同性の立証手法を提案・自動化することである。本年度、一階の項評価系において模倣合同性の立証手法を考察した結果、標準的な危険対解析を用いることのできる項評価系のクラスは予想よりも限定的であることが明らかになった。より広範な項評価系に提案手法を適用するには、危険対解析そのものも併せて拡張する必要があることが示唆された。
次年度は、まず限定的な項評価系での標準的な危険対解析を実装し、それにより模倣合同性の立証手法を提案・自動化することを行う。並行して危険対解析の拡張を模索する。ここでは、一階の項書き換え系から高階の項書き換え系に危険対解析を拡張する標準的な手法に、項書き換え系から実用的な項評価系に危険対解析を拡張する新たな手法を組み合わせることになる。
|
| Causes of Carryover |
コロナ禍の影響により国際学会への参加を見合わせたこと、また研究の進捗がアルゴリズム実装に至らなかったためにRAの雇用を見合わせたことで、次年度使用額が発生した。国際学会への積極的な参加、及びアルゴリズム実装のためのRAの雇用を行うことでこれらの助成金を使用する計画である。
|
