Correctness Proofs of Transformation Schemas

Halime B?uy?uky?ld?z and Pierre Flener

Department of Computer Engineering and Information Science Faculty of Engineering, Bilkent University, 06533, Bilkent, Ankara, Turkey Email correspondence to: [email protected]

Abstract

Schema-based logic program transformation has proven to be an effective technique for the optimization of programs. Some transformation schemas were given in [3]; they pre-compile some widely used transformation techniques from an input program schema that abstracts a particular family of programs into an output program schema that abstracts another family of programs.

This report presents the correctness proofs of these transformation schemas, based on a correctness definition of transformation schemas. A transformation schema is correct iff the templates of its input and output program schemas are equivalent wrt the specification of the top-level relation defined in these program schemas, under the applicability conditions of this transformation schema.

1 Introduction

In this introductory section, we give the definitions of the notions that are needed to prove the correctness of the transformation schemas in [3]. The transformation schemas proved in this report are pre-compilations of the accumulation strategy [2], of tupling generalization, which is a special case of structural generalization [4], of a combination of the previous two techniques, and of the first duality law of the fold operators in functional programming [1]. For a detailed explanation of these transformation schemas and examples of the definitions below, the reader is invited to consult [3].

Throughout this report, the word program (resp. procedure) is used to mean typed definite program (resp. procedure). An open program is a program where some of the relations appearing in the clause bodies are not appearing in any heads of clauses, and these relations are called undefined (or open) relations. If all the relations appearing in the program are defined, then the program is called a closed program. A formal specification of a program for a relation r of arity 2 is a first-order formula written in the format:

8X : X : 8Y : Y: Ir(X) ) [r(X; Y ) , Or(X; Y )]

where X and Y are the sorts (or: types) of X and Y , respectively, Ir(X) denotes the input condition that must be fulfilled before the execution of the program, and Or(X; Y ) denotes the output condition that will be fulfilled after the execution. All the definitions are given only for programs in closed frameworks. So, we first give the definition of frameworks.

Definition 1 (Frameworks)
A framework F is a full first-order logical theory (with identity) with an intended model. An open framework consists of:

* a (many-sorted) signature of

- both defined and open sort names;

- function declarations, for declaring both defined and open constant and function names;

- relation declarations, for declaring both defined and open relation names;

* a set of first-order axioms each for the (declared) defined and open function and relation names, the former possibly containing induction schemas;

* a set of theorems.

An open framework F is also denoted by F(?), where ? are the open names, or parameters, of F . The definition of a closed framework is the same as the definition of an open framework, except that a closed framework has no open names. Therefore, a closed framework is just an extreme case of an open one, namely where ? is empty.
Now, we give the definitions of correctness of a logic program and equivalence of two programs, which will be used in the equivalence definition of two program schemas.