---
title: "A Natural Programming Calculus"
authors:
  - "Åke Hansson"
  - "Sten-Åke Tärnlund"
doi: ""
url: "https://ijcai.org/proceedings/1979/77"
pdf: "https://ijcai.org/proceedings/1979/0077.pdf"
venue: "Proceedings of the Sixth International Joint Conference on Artificial Intelligence"
year: 1979
pages: ""
track: ""
keywords:
---

# A Natural Programming Calculus

Åke Hansson, Sten-Åke Tärnlund

*Proceedings of the Sixth International Joint Conference on Artificial Intelligence*.

## Abstract

We shall lay down a programming calculus in which we develop a methodology for reasoning ab?ut data and programs. Our language, L, is ordinary first order predicate logic. A subset of th~s language, Lp, is our programming language that can be run efficiently in PROLOG . The calculus . consists of a natural deduction system that is used for deducing programs and a system for effcient computation of programs. The axioms of the calculus characterize the data structures. Definitions are used for program specifications and mappings between data structures. The programs are deduced from the axioms and the definitions. Examples of deduced programs are a LISP-program and a program that Burstall and Darlington could not obtain in their transformation system.

## Full text

## 1. INTRODUCTION

Our main purpose is to develop a methodology for reasoning about data and programs, and especially to enable us to arrive at a programming calculus. In this connection we shall take up a system of natural deduction invented by Jaskowski and Gentzen, and from this we shall deduce programs.

Natural deduction systems are natural in several ways. One important point is their characteriza­ tion of informal reasoning. In particular, the structure of unformalized reasoning preserves its structure when it is formalized. In fact, the suggestion by Lukasiewics to formalize reasoning from assumptions seems to be a first step towards

natural deduction systems.

We can think of a natural deduction system as a formalization of means-ends analysis in the GPS­ system (see Newell & Simon l 14]). Taking this view, a derivation of a program follows a general structure. An induction hypothesis is an initial state. A program specification together with axi­ oms of data structures or data structure mappings are operators that transform an initial state to a final state that is the program. The general structure of a deduction is of great interest not only for our understanding of program deductions but also for developing methods for automated reasoning. Unfortunately, we have to leave out the deductions for reasons of space. A detailed description of the deductions is found in Hansson

& Tiirnlund [ 7 ] .

We shall make use of Quine's [16] natural deduc­ tion system for classical logic. Natural deduction systems are not restricted to classical logic but apply also to many 0ther systems e.g., second order logic, modal logic and set theory. A compre­ hensive description of natural deduction systems as well as of their history ~s given by Prawitz [ 15].

Our language is first order predicate logic (L) defined in its standard way with bound and free variables, primitive signs for quantification (V and 3), conjunction(&), disjunction (v), conditio­ nal (~),negation(~) and bi-conditional (++), In section 2 this language is used for writing down axioms e.g., to characterize data structures, and in sections 3-5 for definitions of programs and data structure mappings. We use the inference rules of the natural deduction system to derive programs from the axioms, definitions and mappings.

The language L should be distinguished from the restricted language of Horn clauses Lp, which is our programming language (see Colmerauer et al. [ 6 ] , Hayes [ 8] and Kowalski [ 10]). Thus a de­ duction of a program starts from axioms and defi­ nitions in L and arrives at a Horn clause program in Lp. Horn clause programs do not restrict the set of computable functions (see Tarnlund [19]) and since the advent of PROLOG (see Roussel [18] and Warren [21]} they can also be run efficiently by a resolut ion-like theorem prover (see Robinson [17]).

The programming language evidently becomes an integrated part of a logic calculus, in the sence of Church [4), where the deductions are deter­ mined by inference rules and axioms. It should be noted that our system consists of a natural deduction system for reasoning and a resolution system for the efficient computation of programs.

*This work was supported by the Swedish Natural Science Research Council.

Sten-Ake Tarnlund

## 2. DATA STRUCTURES

We now turn to the notion of data structures, which are premises in our deductions. We shall have to write down these structures explicitly in order to make formal inferences from them. These formalizations are axioms in our calculus.

We shall take up four data structures: simple linear lists, difference lists, binary trees and ordered-binary trees. Our characterization of these data structures has already been introduced in Tarnlund [20].

A simple linear list is empty (¢) or constructed ( x. y) from an element x and a list y. We forma­ lize this idea in our first axiom.

## Axiom 1.

Vw{list(w) ++ w=¢ v 3x3y[w=x.y & element(x) & list (y)]}

We are using a dot, · , for list constructions which like the extensions of the elements are supposed to be defined elsewhere.

Generally, there are useful lemmas that could be derived from the axioms which make the deductions of programs shorter. Following Clark & Tarnlund [ 5 ] these lemmas consist of an induction step and a base. For reasons of space we have to leave them out.

Our next axiom characterizes a more complicated linear list called a difference list or a d-list for short. It is useful for direct access to the rear of a linear list and for concatenating two lists efficiently. We may think of a d-list as a pair <u,w> of linear lists u and w, where each element on w occurs in the same order at the rear of u e.g., u=a.b.c.x and w=c.x giving the pair <a.b.c.x,c.x>, which denotes the simple list a.b.¢. Our second axiom formalizes the idea of ad-list.

## Axiom 2.

Yw{d-list(w) ++ Yz3u3v[w=<u,z> & (u=z v u=v.z & element(v) v d-list(<u,v>) & d-list(<v,z>))]}

We assume that the pair constructor, < > , is already defined.

Binary trees are interesting and useful data structures not only for their own sake but also because any tree can be represented by a binary tree. An object is a binary tree if and only if it is empty or constructed t(x,y,z) where y is an element, moreover, the subtrees x and z are binary trees themselves. This idea is formalized in our third axiom.

## Axiom 3.

Yw{binary-tree(w) ++ w=¢ v 3x3y3z[w=t(x,y,z} & element(y) & binary-tree(x) & binary-tree(z)]} When unambiguous R binary tree is called a tree.

The concept of ordering is fundamental in pro­ gramming. We shall need a "belongs-to" relation­ ship in order to specify the idea of ordering.

An element u belongs to a list w if and only if w is identical with a simple list x.y and u is identical with x or u belongs to the list y. This is written more precisely in our fourth axiom.

## Axiom 4.

YuYz{u E z ++ list(z) & 3x3y[z=x.y & (u=x vuE y)]}

This inductive definition is naturally viewed from the front of the list towards the rear. However, it is equally natural to view a list from the rear towards the front. But in order to achieve the latter idea we have to make use of a d-list since a linear list does not work in the latter direction. The following picture might be useful for understanding our next axiom.

Fig.l Two d-lists.

![Image](https://ijcai.org/proceedings/1979/fulltext/77/image_000000_486a6a57e86e6bc40d5546c889ce91973e9f92d257156793bc5fc8a7de8050d5.png)

An element x belongs to a d-list <u,w> if and only if there exists a one-element shorter d-list <u,v.w> such that x is identical with v or be­ longs to ad-list <u,v.w>, We make this notion concise in an axiom.

## Axiom 5.

YxYz{x E z ++ 3z'[d-list(z) & d-list(z') & Yw3u3v[z=<u,w> & z'=<u,v.w> & (x=v v x E z')]]}

An element u belongs to a binary tree t(x,y,z) if and only if u is identical with y or u belongs to x or z. This idea is written precisely in an axiom.

## Axiom 6.

YuYw{u t w ++ binary-tree(w) & 3x3y3z[w=t(x,y,z) & (u Ex v u=y vuE z)]}

We finish this section with an axiomatization of an ordered binary tree; ob-tree for short. An empty tree is an ob-tree and a tree t(x,y,z) is ordered if and only if each element on the left subtree x i~ less than the element y and each element on the right subtree z is greater than y, moreover, the trees x and z are ob-trees.

## Axiom 7.

~{ob-tree(w) ++ binary-tree(w) & [w=¢ v 3x3y3z[w=t(x,y,z) & Yu[(u Ex+ u<y) & (u E z + y<u)] & ob-tree(x) & ob-tree ( z)])}

We shall also need to distinguish between an emp­ ty list and a constructed list i.e., ¢1x.y, as well as between an empty tree and a constructed tree i.e., ¢~t(x,y,z). We can now, for example, derive that there is no element on an empty list or on an empty tree i.e., ~(u E ¢).We shall also assume some standard axiomatization of arithmetic.

## 3. DEDUCTION FROM INDUCTIVE ASSUMPTIONS

The intention of our programming calculus is to arrive at systematic methods for deducing programs. Generally speaking, a deduction of a program follows from a program specification and from the axioms of data structures given in section 2 or mappings between data structures. These axioms, specifications and mappings are written in our first order language L. By contrast, a program is written in the language Lp, which usually is Horn clauses and a subset of L.

A deduction is built up on the inference rules in Quine's natural deduction system [16]. In addi­ tion we shall also make use of rules for identity.

It is a point of methodological interest that the programs are written inductively on a data struc­ ture. This fact is used for deducing programs from their specification by an inductive argument i.e., a program is deduced from an induction hypothesis. Moreover, this method of deducing programs gives a correctness proof of the programs for free. A simple example will shed light on these ideas.

Suppose we wish to deduce a program which checks whether or not an element x is less than all ele­ ments of a list l. We owe this "lessall"-program to Manna & Waldinger [12]. First, we write down a definition in the language L which is a precise specification of the program.

## Definition 1.

VxVl{lessall(x,l) ++ element(x) & list(l) & Vz[z E 1 + x<z]}

This definition is explicit in contrast to an implicit one written inductively on a data struc­ ture. As we shall see explicit definitions con­ tain more alternative programs than implicit de­ finitions and so we consider them more abstract.

We observe that definition 1 contains a simple list as data structure. In fact, a data structure provides a general rule for generating the struc­ ture of a program deduction. First, we assume that there is a program on the data structure e.g., lessall(x,l), where xis an element and 1 a con­ structed list. From this assumption a consequent is deduced e.g., lessall(x,u.l), where u.l con­ tains one element more than 1. In this way, by the deduction theorem, we can deduce a part of a program, which is an induction step. Secondly, we can readily complete the program by an induction base e.g., lessall(x,¢).

We can sum up our deductions in Hansson & Tarn­ lund [ 7 ] in the following theorem, which is a program that checks whether or not an element and a list satisfy the "lessall"-relationship.

## Theorem 1.

lessall(x,¢) + element(x)

lessall(x,u.l) + x<u & element(u) & lessall(x,l)

We follow a con¥enient convention for logic pro­ grams and omit universal quantifiers whose scope is the entire sentence. We can omit the "type"­ checks if we assume that the program is used with respect to its intended interpretation. In this way we arrive at the following simple program which we can run efficiently in PROLOG.

lessall(x,¢)

lessall(x,u.l) + x<u & lessall(x,l)

## 3. 1 Program correctness·

It is to be noticed that the deduction of our program ensures that the program is correct. For example, a correctness statement of the "lessall "­ program is:

VxVl{element(x) & list(l) & lessall(x,l) + Vz{z E 1 + x<z}}

A meta-argument tells us that this statement is already proved during the deduction of the pro­ gram. A central idea about the deduction is that it is an induction argument on lists consisting of a base case and an induction step i.e.,

## P(¢) & VxVy[.P(y) + P(x.y)] + VzP(z)

where the antecedent consists of the base case and the induction step of the "lessall" program respectively. So, by induction we prove that the program is true of exactly all elements and lists in the "less all "-relationship, i.e. , we have a model of

lessall(x,l)

which by definition is true for

Vz{z E 1 + x<z}

It remains to be proved that the program termi­ nates. We can, in fact, do this by induction on the data structure following methods developed in Clark & Tarnlund [ 5 ] .

## 4. DEDUCTION FROM AN ABSTRACT SPECIFICATION

Deductions of programs from specifications usual­ ly contain several alternatives of data structures as well as a choice between operations on data structures. We shall say that a specification is less abstract when it provides fewer deductions. In this way an abstract specification gives more power and a natural idea would be to write down just abstract definitions. Up to a point such a development has great advantages, as we shall see in section 4.1, where different programs are deduced from alternative assumptions about data structures and in section 4.3, where new programs are deduced from a choice between operations on data structures.

Unfortunately, all specifications are not abstract enough to provide alternative deductions of pro­ grams. This is certainly true of specifications that are very close to being programs themselves. In order to arrive at alternative programs in this situation we can of course try to write down a more powerful specification, but then we are faced with the problem of showing that the original specification satisfies the more abstract one. However, we can also deduce an alternative pro­ gram from the original specification by introdu­ cing a mapping between data structures. We take up this idea in section 4.2.

## 4 .1 Hypothesis About Alternative Data Structures

Evidently we can make use of our natural deduction system for hypothetical reasoning introduced in the preceding section and thus systematically de­ duce programs from alternative hypothesis.

Let us get a firmer idea by an example. Suppose t hat we have an abstract definition of programs f or computing a list of factorials. Let us further as sume that we first of all want to deduce a pro­ gram with the factorials in descending order in t he list and, secondly, to deduce a program with t he factorials in ascending order. We owe the f i r st of these programs to Burstall & Darlington [2). The idea of putting each factorial at the front of the list is a stack operation in charac­ t er and leads to a list of factorials in descen­ di ng order. By contrast, the idea of putting each new factorial at the rear of the list is a queue operation in nature and gives the factorials in ascending order. These broad outlines of deducing programs from abstract specifications with alter­ native hypothesis about data structures are de­ pict ed in figure 2.

Fig.2 Deductions of alternative programs from the same specification

![Image](https://ijcai.org/proceedings/1979/fulltext/77/image_000001_d9e2a6b66020f28197f786fbef908da01dc321f3f09b71839eb7041cca871799.png)

We shall use bounded quantifiers. We say that V F(y) is equivalent to F(1) & F(2) ·.. & F(n) and 1\_9'~il

3 F(y) is equivalent to F(1) v F(2) ··. v F(n). 19'~n

Let us now write down an abstract specification of factlist.

## Definition 2.

VnVl{factlist(n)=l ++ n=O & 1=¢ v n>1 &

![Image](https://ijcai.org/proceedings/1979/fulltext/77/image_000002_de8c9000fb66b10ad957a4dfaa4f5c710804e473fab3e48584e1c41fae5c87a8.png)

Obviously, the elements in the list could have any property. In fact, the only information we use about the factorials is that "fact" is a function from element to element. We have

fact: element~ element

We can now deduce the two programs factlist and FACTLIST respectively. The deductions are identi­ cal for the first 7 steps but branch as illustra­ ted in figure 2, when we make assumptions about data structures. The left branch follows from the assumption that the data structure is a simple list and the right branch from the assumption that it is ad-list (see Hansson & Tarnlund [7]), We obtain the following program.

## Theorem 2.

factlist(O)=¢

factlist(n+1)=u.l + n>O & list(l) & fict (n+1)=u & factlist(n)=l

In Hansson & Tarnlund [7] we also have a deduc­ tion of a FACTLIST-program.

## Theorem 3.

FACTLIST(O)=<u,u> FACTLIST(n+1)=<u,w> + n>O & d-list(<u,v.w>) & fact(n+1)~v & FACTLIST(n)=<u,v.w>

We recall from section 3 that the deductions of theorems 2 and 3 also give us correctness of these programs.

Our second deduction of the FACTLIST-program that computes a list of factorials in ascending order is particularly interesting since Burstall & Darlington [2] write frankly "Notice, however, that to do factlist in ascending order is not easy with our technique and seems to require an extension of the rules. We are currently investi­ gating the problem".

Moreover, we want to call attention to the dotted line in fig.2 which is supposed to illustrate another deduction of a FACTLIST-program. This deduction makes use of mappings between the data structures simple list and the d-list. We shall take up this deduction in the next section.

## 4.2 Data Structure Mappinss

According to the dotted line in fig.2 a deduction requires a correspondence between the data struc­ ture simple list and d-list respectively. This one-to-one correspondence between the element in a stack and a queue is depicted in our next figure.

![Image](https://ijcai.org/proceedings/1979/fulltext/77/image_000003_acf8111e301293ff3e8d145f0b73d405561348aa2bdf2de937d03ae7bcce4ef8.png)

Fig.3 A one-to-one correspondence between a simple list x.y and a d-list <u,w>.

Let us give these correspondences names, domains and ranges in a usual w~.

map1 : simple list+ d-list

map2: d-list + simple list.

We now have to define these correspondences more precisely in order to carry out a deduction from the factlist program with factorials in descending order to a program with factorials in ascending order.

## Definition 3.

V1Vq{map1(l)=q ++ 1=~ & Vu(q=<u,u>) v

3x3yVw3u[list(l) & l=x.y &

d-list(q) & q=<u,w> & map1(y)=<u,x.w>]}

A definition of map2 is straightforward when we have map1.

## Definition 4.

VqVl{map2(q)=l ++ map1(l)=q}

We have two functions: factlist and FACTLIST.

fact list: element + simple list

FACTLIST: element + d-list.

This brings us to the following definitions of these functions.

## Definition 5.

VnVq{FACTLIST(n)=q ++

3l[factlist(n)=l & map1(l)=q]}

## Definition 6.

VnVl{factlist(n)=l ++

3q[FACTLIST(n)=q & map2(q)=l]}

These definitions and the following factlist program:

factlist(O)=~ factlist(n+l)=m.l + n~O & fact(n+l)=v & list(l) & factlist(n)=l

give a FACTLIST-program again. Hence, we have ob­ tained theorem 3 twice, but this time by a mapping between data structures (see Hansson & Tarnlund [ 7]).

We can, of course, deduce the factlist program in theorem 2 in an analogous way from FACTLIST. Consequently, the programs factlist and FACTLIST are equivalent.

## 4.3 HyPOtheses About Alternative Operations on a Data Structure

We shall now treat the idea of keeping the same data structure but making alternative hypotheses about operations on the data structure. In this way, a program is first deduced which inserts a new element into an empty subtree of an ordered binary tree such that the new tree is also order­ ed. Secondly, a program is deduced which inserts a new element into the root of an ordered binary tree and keeps the new tree ordered.

The important point about these programs is their operation on their data structure. The first pro­ gram inserts the new element in one of its sub­ trees until an empty tree is reached. By contrast, the second program inserts its new element into the root of the binary tree and reorganizes the subtrees so that they st~ ordered. We owe this program to Keith Clark.

Let us now write down an abstract specification of these programs. We are in fact, a bit strict and make the definition true only for ordered binary trees. We think of an insert relation be­ tween individuals u, v and w if and only if u is an ob-tree, v is an element and w is an ob-tree, moreover, each element on w is on u or is ident i­ cal to v.

## Definition J.

VuVvVw{insert(u,v,w) ++ ob-tree(u) & element(v) & ob-tree(w) & Vz[z E w ++ z=v v z E u]}

In Hansson & Tarnlund [7] we first deduce one case of a leaf insert program and secondly one case of a root insert program. The first 14 steps in the deductions are identical until we make a choice between operations on the data structure. We have, thus, the following case of a leaf in­ sert program.

## Tbeorem 4.

insert(t(x,y,z),v,t(x' ,y,z')) + v<y & z=z' & ob-tree(t(x,y,z)) & insert(x,v,x')

Let us now write down a corresponding case for a root insert program.

## Theorem 5.

insert(t(x,y,z) ,v,t(x' ,v,t(x" ,y,z))) + v<y & x2=t(x' ,v,x") & x=x1 & ob-tree(t(x,y,z)) & insert(x,,v,x2)

We depict a relationship between input and out­ put in our root insert program in the next figure. Notice that subtree x is partitioned in two subtrees so that x' contains all elements less than v and x" all elements greater than v.

![Image](https://ijcai.org/proceedings/1979/fulltext/77/image_000004_4d4c344a2dee7b083ebc50098f1e0939958d8ad80e5c56821cd95b247b463cd7.png)

In this w~ we can deduce the entire programs for leaf insert and root insert, respectively.

## Theorem 6.

insert(t(x,y,z),v,t(x',y,z')) + v<y & z=z' & ob-tree(t(x,y,z)) & insert(x,v,x') insert(t(x,y,z),v,t(x' ,y,z')) + y<v & x=x' & ob-tree(t(x,y,z)) & insert(z,v,z') insert(t(x,y,z),v,t(x' ,y,z')) + v=y & x=x' & z=z' & ob-tree(t(x,y,z)) insert(¢,v,t(¢,v,¢))

## Theorem J,

insert(t(x,y,z) ,v,t(x' ,v,t(x" ,y,z))) + v<y & x 2 =t(x' ,v,x") & x=x1 & ob-tree(t(x,y,z)) & insert ( x1, v ,x2) insert(t(x,y,z),v,t(t(x,y,z'),v,z")) + y<v & z2=t(z' ,v,z") & z=z1 & ob-tree(t(x,y,z)) & insert(z,,v,z2) insert(t(x,y,z),v,t(x' ,v,z')) + v=y & x=x' & z=z' & ob-tree(t(x,y,z)) insert(¢,v,t(¢,v,¢))

We recall that we obtain a correctness proof of the programs.

## 5. DEDUCTION FROM A NON-ABSTRACT SPECIFICATION

The abstract character of the specification of factlist in the preceding section gives the ad­ vantage of two methods of deducing a program, namely, by choice of data structure or by data structure mapping. Unfortunately, there are quite natural specifications that are less abstract e.g., already bound to a data structure. This situation obviously eliminates the method that provides choices between data structures for deduction of alternative programs. In such a case we can either redefine our specification more abstractly or use the method of data structure mapping, shown in section 4.2. We shall take up the latter method again on a specification of a twist relation. We owe this program to Burstall & Darlington [2].

## 5.1 Data Structure Mappings for Deducing Alternative Programs

The twist program is a function. twist: binary tree +binary tree

An example of this program is displ~ed below. twist: ~

![Image](https://ijcai.org/proceedings/1979/fulltext/77/image_000005_4a94f0ba7cec4267a5d199f41b77a8093ce6dc849d5dfddfee35af6e1169cd5c.png)

Let us now consider the problem of substituting this data structure for a "LISP"-tree structure and in this w~ arrive at a TWIST-program, which "TWISTs" a LISP-tree. Thus we want to deduce a TWIST-program, which is a function from LISP­ trees to LISP-trees i.e.,

TWIST: LISP-tree + LISP-tree

An example of the TWIST-function is displ~ed in ~he next figure.

Fig.6 TWIST of a LISP-tree

![Image](https://ijcai.org/proceedings/1979/fulltext/77/image_000006_c13c0ca6f50e38c7de74f9b1f4fe664a03f63d3e2599d6a005d925e6eb67ac6a.png)

This TWIST-program, although written in logic and potentially run in PROLOG, is a LISP-program in character, and thus it is natural to ask for a LISP-program. At this point three sub-problems demand solution, a definition of a mapping between a binary tree and a LISP-tree, a definition of TWIST in twist and an axiomatization of relevant LISP-functions. Let us sum up this situation in a figure.

![Image](https://ijcai.org/proceedings/1979/fulltext/77/image_000007_5d3dd023f152d31ef6a990ec83170837466aaa1b11cacdd1582274424d5385ca.png)

Informally, we need a one-to-one correspondence between the data structures binary tree and LISP­ tree.

Fig.8 FUnctions between data structures

![Image](https://ijcai.org/proceedings/1979/fulltext/77/image_000008_264b26d43a9bee79833b72d521e60bc05cd32cdffaf8b77a50c268c30d8b595d.png)

Before we can write down this correspondence more precisely we shall have to axiomatize a data structure LISP-tree built up on a LISP-list cons(x,y), and so we have to introduce the latter data structure.

## Axiom 8.

VxVy3z{cons(x,y)=z ++ (element(x) v 3u3w cons(u,w)=x) & (y=nil v 3u3w cons(u,w)=y)}

A LISP-tree is a subset of a LISP-list. In fact, it is either nil or constructed, cons(x,cons(u,y)), where x is a LISP-tree, u an element andy a LISP­ tree. We have:

## Axiom 9.

Vl{LISP-tree(l) ++ l=nil v 3x3y3u[l=cons(x,cons(u,y)) & element(u) & LISP-tree(x) & LISP-tree(y))}

As usual we distinguish between an empty list and a constructed list.

## Axiom 10.

VxVy~{cons(x,y)=nil}

We can now write down the functions map1 and map2.

## Definition 6.

V1Vt{map1(l)=t ++ l=nil & t=¢ v 3u31,3123t 13t2[l=cons(l 1 ,cons(u,l 2 )) & LISP-tree(l) & binary-tree(t) & t=t(t1,u,t2l & map1(11l=t1 & map1(12l=t2l}

We get map2 immediately from map1.

## Definition 1.

V1Vt{map2(t)=l ++ map1(l)=t}

Let us now specify twist on binary trees, in fact, the definition is quite natural although it is not abstract enough to provide a deduction of TWIST, without the mappings map1 and map2.

## Definition 8.

vt,vt2{twist(t1)=t2 ++ t1=¢ & t2=¢ v 3u3t113t 123t213t22[t 1=t(t 11 ,u,t 12 ) & t2=t(t22 ,u,tz1l & binary-tree(t 1) & binary-tree(t2) & twist(t11l=t21 & twist(t12l=t22l}

We can now define TWIST by three mappings. First, from a LISP-tree l1 to a binary tree t 1 ·

map 1 : 11 -+ t 1

Secondly, from a binary tree t1 to a (twisted) binary tree t2.

twist: t1 -+ t 2

Finally, from a binary tree t 2 to a LISP-tree 12. map2: t 2 -+ 1 2

We are now ready to define TWIST precisely.

## Definition 9.

Vl1Vl2{TWIST(l1)=12 ++ 3t 1 3tz[map1(11)=t1 & twist(t1J=t2 & map2(t2)=12]}

We still have to deduce a TWIST-program which is independent of twist and the functions map1 and map2. We can deduce the following program that "TWISTs" a LISP-tree, without any mapping function (see Hansson & Tarnlund [ 7 ] ) .

## Theorem 8.

TWIST(nil)=nil

TWIST(cons(x,cons(y,z)))=cons(z' ,cons(y,x' )) + TWIST(x)=x' & TWIST(z)=z'

Moreover, our inductive proof shows that the TWIST-program is total, i.e.,

## Lemma 1.

Vw3u[LISP-tree(w) -+ TWIST(w)=u]

Before proceeding to a derivation of a LISP-pro­ gram let us pause a moment for a comment on the deductions. Although they are made by hand several of them have also been deduced in Weyrauch's FOL system [22]. For example see appendix 1 in Hansson & Tii.rnlund [ 7 ] for a deduction in FOL of the TWIST-program in theorem 8. It is of course a na­ tural development to get these deductions automa­ tically. However, FOL is useful for systematic developments of programs, and in addition it checks the inference and ensures that we arrive at correct programs.

## 5.2 Deduction of a LISP-program

It is a natural development within our calculus to go a little further and deduce a LISP-program that twists a tree. In order to carry out this program we need an axiomatization of the LISP functions car and cdr.

## Axiom 11.

VxVy{car(x)=y ++ 3w cons(y,w)=x}

## Axiom 12.

VxVy{cdr(x)=y ++ 3w cons(w,y)=x}

We shall make use of a LISP-syntax containing "if ·.. then ... else .·· " as proposed by McCarthy [13]. So we have to define this form.

## Definition 10.

VxVy{B(if A then x else y) ++ (A-+ B(x)) & (~A -+ B(y))}

In this way we do not extend our natural deduction system which we might have done and thus introduce an inference rule for "if ··· then ..· else ... " introduction and elimination respectively (see Manna [11]). We get the following LISP-program for TWIST (see Hansson & Tii.rnlund [ '( ] ) ·

## Theorem 9.

TWIST(w)= if w=nil then nil else cons(TWIST(cdr(cdr(w))),cons(car(cdr(w)), TWIST(car(w))))

It is worthwhile noting that our method laid down in this paper also applies to arbitrary programming languages provided their programming constructs are axiomatized like axioms 11 and 12. This axio­ matic method seems to be a new approach to pro­ gram verification.

Unfortunately, no other programming language than pure LISP, except logic itself, of course, has been given a treatment that is rigorous and precise enough for a programming calculus (see Boyer & Moore [1], Cartwright [3] and McCarthy [13]). In particular, the specification of PASCAL (see Hoare & Wirth [ 9]) does not suffice. It is obviously undesirable to restrict the generality of pro­ gramming languages so they do not fit into a pro­ gramming calculus. Therefore, developments of new programming languages should demand solution of two problems; design of the language and axioma­ tization of the language constructs, for example, as outlined above.

## 6. CONCLUSION

A methodology for reasoning about programs and for systematic development of programs is of great inte­ rest. In this connection we have employed a deduc­ tive methodology and obtained a calculus for pro­ gramming without a detour for a formalization of the programming language. Thus, it is an important point that our language for data structures and program specifications is first order predicate logic, a subset of which is our programming langu­ age. This is of great advantage when we deduce programs. Unfortunately, we have not, for reasons of space, displayed any deductions. In fact, they are all examples of hypothetical reasoning forma­ lized in a natural deduction system. By contrast, a program is executed by a PROLOG-like system. Hence, the calculus consists of two distinct logi­ cal systems. We have focused on a methodology for systematic development of programs, but it should be noted that the deductive methodology ensures that a derived program is correct. Consequently, we also obtain a methodology for proving that pro­ grams are correct.

## References

1. Boyer R. & Moore J.S., Proving Theorems about LISP Functions, JACM vol 22 no 1, 1975
2. Burstall R.M & Darlington J., A Transforma- tion System for Developing Recursive Pro- grams, JACM vol 24 no 1, 1977
3. Cartwright R.S., A Practical Formal Semantic Definition for Typed LISP, Computer Science Dept. Stanford University, 1977
4. Church A., Introduction to Mathematical Logic, Princeton, 1956
5. Clark K. & Tarnlund S-A., A First Order Theory of Data and Programs, IFIP-77, Torontc
6. Colmerauer A. et al., Un Syst~me de Communi- cation Homme-Machine en Franiais, Groupe d'intelligence Artificielle U.E.R de Luminy Universite d'Aix-Marseille, Luminy, 1972
7. Hansson A. & Tarnlund S-A., A Natural Pro- gramming calculus, Dept. of Computer Science University of Stockholm and The Royal Insti- tute of Technology, 1979
8. Hayes P., Computation and Deduction, Proc. MFCS Conference Czechoslovakian Academy of Sciences, 1973
9. Hoare C.A.R. & Wirth N., An Axiomatic Defi- nition of the Programming Language PASCAL, Acta Informatica 2, 1973
10. Kowalski R., Predicate Logic as Programming Language, Proc. IFIP-74, North-Holland, 1974
11. Manna Z., Mathematical Theory of Computation, McGraw-Hill Inc., 1974
12. Manna z. & Waldinger R., Synthesis: Dreams= Programs, Memo AIM-302, AI-lab., Computer Science Dept. Stanford University, 1977
13. McCarthy J., Representation of Recursive Programs in First Order Logic, Draft, AI-lab., Computer Science Dept. Stanford University, 1977
14. Newell A. & Simon H.A., Human Problem Solving, Englewood Clif~s. N.J. Prentice-Hall, 1972
15. Prawitz D., Natural Deduction, A Proof- Theoretical Study, Almqvist & Wiksell, Stock- holm, 1965
16. Quine W.V., Methods of Logic, Second Edition Routledge & Kegan Paul, London, 1959
17. Robinson J.A., A Machine-Oriented Logic Based on the Resolution Principle, JACM vol 12 no 1, 1965
18. Roussel P., PROLOG: Manuel de R~ference et d'utilisation, Groupe d'intelligence Artifi- cielle, U.E.R de Lurniny, Marseille, 1975
19. Tarnlund S-A., Horn Clause Computability, BIT 17, 2, 1977
20. Tarnlund S-A., An Axiomatic Data Base Theory, in Logic and Data Bases (eds.) Gallaire H. and Minker J., Plenum Press N.Y. 1979
21. Warren D., Implementing PROLOG-Compiling Predicate Logic Programs, Dept of Artificial Intelligence, Edinburgh University, No 39, 1977
22. Weyhrauch R.W. & Filman R.E., An FOL Primer, Stanford AI-lab, Memo AIM-288, Computer Science Dept. Stanford University, 1976