Correctness of context-moving transformations for term rewriting systems

Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

研究成果: Conference contribution

1 被引用数 (Scopus)

抄録

Proofs by induction are often incompatible with functions in tail-recursive form as the accumulator changes in the course of unfolding the definitions. Context-moving and context-splitting (Giesl, 2000) for functional programs transform tail-recursive programs into non tail-recursive ones which are more suitable for proofs by induction and thus for verification. In this paper, we formulate context-moving and context-splitting transformations in the framework of term rewriting systems, and prove their correctness with respect to both eager evaluation semantics and initial algebra semantics under some conditions on the programs to be transformed. The conditions for the correctness with respect to initial algebra semantics can be checked by automated methods for inductive theorem proving developed in the field of term rewriting systems.

本文言語English
ホスト出版物のタイトルLogic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Revised Selected Papers
編集者Moreno Falaschi
出版社Springer Verlag
ページ331-345
ページ数15
ISBN(印刷版)9783319274355
DOI
出版ステータスPublished - 2015
イベント25th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2015 - Siena, Italy
継続期間: 2015 7月 132015 7月 15

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
9527
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

Other

Other25th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2015
国/地域Italy
CitySiena
Period15/7/1315/7/15

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「Correctness of context-moving transformations for term rewriting systems」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル