• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2020 年度 実施状況報告書

先進的な高階書き換え理論に基づく遅延評価関数型プログラムの検証

研究課題

研究課題/領域番号 19K11891
研究機関東北大学

研究代表者

菊池 健太郎  東北大学, 電気通信研究所, 助教 (40396528)

研究期間 (年度) 2019-04-01 – 2023-03-31
キーワード書き換えシステム / プログラム検証
研究実績の概要

昨年度までの研究により、第一階項書き換えシステムにおける帰納的定理の証明手法である潜在帰納法の適用のためには、合流性と局所十分完全性が本質的であるということが明らかになっている。本年度の研究では、それらの性質に関する以下の成果・知見が得られた。
(1) 束縛変数を伴う項を扱えるように第一階項書き換えシステムを拡張した名目書き換えシステムに対し、新たな合流性の成立条件等の提案を行った。具体的には、アトム変数を用いる書き換え規則によって定義される名目書き換えシステムの合流性とその一般化である可換性の成立条件を提案した。アトム変数を用いる書き換え規則によって定義される名目書き換えシステムは、書き換えの対象が基底名目項に制限されるものの、置換ではなく代入を用いて書き換えが定義されるため、従来の名目書き換えシステムよりも理解が容易である。帰納的定理の証明やプログラム変換の正当性に応用するためには、基底項に対する合流性を考えれば十分であるため、ここで得られた成果・知見は、第一階項書き換えシステムに基づく潜在帰納法等の手法を名目書き換えシステムに基づく手法へ拡張するにあたって重要になると考えられる。
(2) 局所十分完全性については、昨年度提案した判定のための導出システムと、自動判定に適した十分条件を整理・発展させることに取り組んだ。まず、自動判定に適した十分条件を洗練し、その正当性の証明を見通しの良い形に整理した。この十分条件を用いることにより、昨年度提案した導出システムでは判定困難な例に対しても局所十分完全性の成立を判定可能な場合が存在する。一方、導出システムのほうでは、局所十分完全性の対象となる項における最外の関数記号だけでなく、部分項の構造についても考慮されている。そのため、これら2つの手法を相補的に用いることにより、適用範囲の広い判定手続きが得られることが期待できる。

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

書き換えシステムに基づくプログラム検証手法を開発するために重要と考えられる合流性については、束縛変数を伴う書き換えシステムを対象とした成果・知見が、また、局所十分完全性については、判定手続きに関する知見がそれぞれ得られ、おおむね計画通りに研究を進めることができたため。

今後の研究の推進方策

局所十分完全性については、関連する手法に対して調査を行うとともに、第一階項書き換えシステムを拡張した体系における同様な性質についても検討する。また、具体例による実験の準備に取り掛かる。合流性については、束縛変数を伴う高階の書き換えシステムに対する新しい判定条件の提案を検討する。

次年度使用額が生じた理由

新型コロナウイルス感染拡大防止に伴う自粛の要請を受けて出張を控えたことにより、旅費の使用額にずれが生じたため。繰り越し分は次年度の助成金と合わせ研究環境整備に充てる予定である。

  • 研究成果

    (3件)

すべて 2021 2020

すべて 雑誌論文 (2件) (うち国際共著 2件、 査読あり 1件、 オープンアクセス 1件) 学会発表 (1件)

  • [雑誌論文] Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables2021

    • 著者名/発表者名
      Kikuchi Kentaro, Aoto Takahito
    • 雑誌名

      Proceedings of the 30th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2020)

      巻: 12561 ページ: 56-73

    • DOI

      10.1007/978-3-030-68446-4_3

    • 査読あり / 国際共著
  • [雑誌論文] The System SOL version 20202020

    • 著者名/発表者名
      Makoto Hamana, Kentaro Kikuchi, Date Yao Faustin Dieudonne, Kazuki Fuju
    • 雑誌名

      Proceedings of the 9th International Workshop on Confluence (IWC 2020)

      巻: - ページ: 81-81

    • オープンアクセス / 国際共著
  • [学会発表] 名目書き換えにおける強可換性を用いた合流性証明2020

    • 著者名/発表者名
      菊池健太郎
    • 学会等名
      日本ソフトウェア科学会第37回大会

URL: 

公開日: 2021-12-27  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi