Set Operations for Recurrent Term Schematizations

Abstract. Reasoning on programs and automated deduction often require the manipulation of in nite sets of objects. Many formalisms have been proposed to handle such sets. Here we deal with the formalism of recurrent terms proposed by Chen and Hsiang and subsequently re ned by several authors. These terms contains iterated parts and counter variables to control the iteration, providing an important gain in expressive power. However, little work has been devoted to the study of these terms as a mechanism to represent sets of terms equipped with the corresponding operations union, intersection, inclusion, membership. In this paper, we focus on the set operations relevant for this schematization formalism and we discuss several possible de nitions of these operations. We show how intersection, membership and inclusion can be solved by previously known algorithms and we prove the decidability of the generalisation of two iterated terms, which is the analogy of set union. Moreover, we rene t...

• Type: Conference
• Year: 1997
• Where: TAPSOFT
• Authors: Ali Amaniss, Miki Hermann, Denis Lugiez
• Keywords: Iterated Terms, Many Formalisms, Recurrent Terms, Software Engineering, TAPSOFT 1997