Equivalent transformation by safe extension of data structures

Abstract

Equivalent transformation has been proposed as a methodology for providing programs with appropriate data structures. For instance, logic programs which use lists are transformed into equivalent programs that use difference-lists. However lists and difference-lists are both usual terms and in this sense no new data structures are introduced in the transformation. Since logic programming has fixed data structure called terms, no one can develop theoretical foundations for introducing new data structures into programs as far as only logic programs are discussed. In this paper we develop a theoretical foundation of equivalent transformation that introduces new data structures. We introduce a parameter Γ for data structures, by which many languages with different data structures are characterized. By changing this parameter (say from Γ1 to Γ2) we can discuss data structure change for programs. We define a concept of safe extension of data structures, and prove that the meaning of a program on a data structure is preserved by safe extension of the data structure. © Springer-Verlag Berlin Heidelberg 2001.