プログラムの模倣合同性の危険対解析による自動判定

点击翻译按钮获取中文摘要

本研究は、模倣合同性の立証手法を提案・自動化することにより、プログラム等価性の自動証明手法を与えることを目指すものである。本年度では、制限つきの項書き換え系において模倣合同性の立証手法を定式化し、それに基づいて自動判定アルゴリズムを構築することを目標として研究を行い、制限つきの項書き換え系として「項評価系」を提案した。この項評価系について、項書き換え系に関するワークショップ58th TRS Meeting (2023年2月)での発表を行った。プログラムの実行を項書き換え系で表現するためには、既知の2種類の制限を加える必要があると予想されていた。1つ目は書き換えの場所を制限する手法(Lucas 1995)であり、2つ目は書き換え対象を構文的に制限する手法(Hamana et al. 2020)である。ところが、必要な制限はこの2つだけではなく、書き換えの順序を制限する手法が新たに必要であることが分かった。プログラム実行のモデリングにおいては、評価文脈を用いて書き換えの場所・順序を制限する手法が主流となっている。そこで、項書き換え系に評価文脈を組み合わせることで、書き換えの場所・順序が制限できるような新たな系を開発し、項評価系と名づけた。この成果は、項書き換え系理論の知見をプログラム意味論へ応用する上での大きなステップと捉えられる。プログラム実行がしばしば項書き換え系と見なされうるにも関わらず、項書き換え系理論からプログラム意味論への知見・技術の移植は進んでいない現状がある。項評価系という本年度の研究成果は、そのような状況に対して、プログラム意味論で基本的な概念である評価文脈が項書き換え系には欠如していることが根本的な原因であることを示唆するものである。項評価系に項書き換え系の技術を移転することで、項書き換え系の技術をプログラム意味論へ応用することが可能になると考えられる。