Logic Program Derivation for a Class of First Order Logic Relations

LOGIC PROGRAM DERIVATION FOR A CLMS OF FIRST ORDER LOGIC RELATIONS

George Daya.ntis *

Cognitive Stndies Division, University of Sussex Falmer, Brighton, BNl 9QN G. BRITAIN

1980], [Hogger 1978, 1981] and [Vasey 1985] have been trying to deve1op transformation techniques, based on logical obj!ct-level deduction, for deriving (Hom) logic programs from first-order 1ogic specifications and also for increasing the effi.ciency of logic programs.

According to Hogger, logic procedure derivation refem to the task of showing that the statements (pro­ cedures) comprising a 1ogic program are true theorems about the problem domain implied by a fim-order axiomatic formulation of the problem, which constitutes the program's specification. In practice, this amounts to constructing a series of deductions (a derivation) treat­ ing the specification sentences as assumptions in order to prove each statement in the program. Additionally, proof of each statement is 1ogically independent of t:roofs of the other statements and of any assumptions about the behaviour of the program in execution.

We illustrate a general method for deriving Hom c1ause programs from standard 1ogic specifications by deriving such a program from the following specification of the :ubset re1ation:

Sl: subset(lJ,/2) ~ Vz (member(z,ll) ..;>member(z,/2))

S2: Vx -member<x,ni/)

S3: member( x,u.V ~ »- u or member( x,V

where ~ represent sets as lists with no duplicates. nil represents the empty list and u.l is the list with head u and tailL

The inference steps can be thought of as combining resolution with conversion to c1ausal form. Some of them are anak>g to the fold and unfold transformation operations devek>ped by lBUIBtall and Darlington 1977] in a recUIBive equations frame~rk.

We start by converting the if-half direction of Sl into c1ausal form. We get the nw c1auses:

Cl: subset<ll,/2), member(f.lJ,l2),ll) ~

CZ: subset<ll,/2) ~ member(f.lJ,/2),/2)

where f is a sko1em-function symbol. denoting an arbi­ trary function of l1 and 12.

Notice that Cl is a non-Hom c1ause.

The base c1ause of the recursive Hom program,

p 1: subset( nil,/2) ~

is directly obtained by resolving the c1ausal form of S2, ·~ member(x,nil)", with Cl. ·

The recursive c1ause of the program can be derived more naturally by reasoning with the ~cification in standard form. By: matching the atoms member( z,lJ)" and "member( x,u.lJ" in Sl (only its if-half) and S3 respectively (wtjblding) ~ obtain:

S4: subset<u.l,/2)~ Vz({ZJ- u ormember(z,VJ.:>member(z./2))

ABSTRACI'

Logic programming has been an attempt to bridge the gap be~en specification and programming language and thus to simplify the software deve1opment process. Even though the only d,itference between a specification and a program in a 1ogic programming frame~rlc. is that of effi.ciency, there is still some conceptual distance to be covered be~en a naive, intuitively correct specification and an effi.ciently executable version of it. And even though some mechanical tools have been developed to assist in covering this distance, no fully automatic system for this purpose is :yet known. In this raper ~ present a general class of first-order 1ogic re1a­ tions, which is a subset of the extended Hom c1ause subset of 1ogic, for which ~ give mechanical means for deriving Hom 1ogic programs, which are guaranteed to be correct and complete with respect to the initial specifications.

I. INTRODUC110N

A. Logic progmm derivation.

Logic programming is an attempt to bridge the gap be~en specification and programming language requirements. By making a clear sepuation be~en 1ogic and control. it makes it possib1e for the program­ mer to deal initially with the 1ogic of his problem and then derive more effi.cient, stillk>gically equivalent, ver­ sions of it by altering the contror accordingly. The apparently simple operational semantics of Hom-clausal 1ogic and its various effi.cient implementations, mainly in the form of PROLOG interpretem and compilem, makes it quite appealing as a programming language.

Of coume, even though it has been shown that any t:roblem expreS11ed in first order predicate 1ogic can be reformulated using only Hom c1auses, expressing prob1ems in Hom c1auses is certainly not c1aimed to be very natural Various attempts have been made - [Bo~n 1982], [Murray 1982], [Stickell984] -to implement full first-order 1ogic as a programming language but, aplrt from effi.ciency considerations, the lack of intuitively clear operational semantics for full first-order 1ogic makes them unusable.

On the other hand, [C1arlc. & Sickel 1977], [Hannson

· ltcaean:h aupponod by 1hc Orcek S1a1o Schollllhlpa Pouncla11on.

. Now 't\e begin to oonvert S4 into clausal form: S5: subset< u.l,/2) «- Vz {z;. u ~ 11l217lber( z,/2)] & Vz {1112171ber(z,l) ~ 11l217lber( z,/2)]

Any further conversion "WWuld result in non-Hom clauses. Fortunately the t\\U non-atomic oonditions in S5 can be replaced by equivalent atomic ones using the equivalences:

S6: Vz {21- u ~1112171ber(z,l2)] <:-;>1112171ber(u,l2)

S7: Vz {m£mber(z,l) ~1112171ber(z,l2)] <:--;:>subset(l,/2)

The first equivalence is a special case of the substitu.. tivity of equality, while the second one is an instance of Sl and its application oorresponds to folding. Thus "We easily obtain the rest of the program:

P2: subset( u.l,/2) «- 11l217lber( u,/2), subset( l,/2)

Some of the inference steps presented here and other more oomplex ones needed for more difficult derivations can be easily mechanised, but there remains a significant portion of them, which seems to require some inventiveness. It should be emphasised here that no oomplete inference system exists yet for such deriva­ tions. The same applies to transformation techniques for improving the efficiency of logic programs.

Thus, although deduction is a logically sufficient tool for creating logic programs from specifications or from other programs, this tool requires intelligent oon­ trol in order to be practical. An attempt towards the implementation of a semi-automatic tool for ass!sting with such manipulations is reported in [Vasey 1985]. In this paper, ho't\ever, 'We restrict our attention to a specific class of relations, which 't\e identify in section ll and, for which fully automatic program derivation is p:>ssible, as 't\e shall show. And because 't\e find that a systematic treatment of data types in :logic is necessary for the adequate formalisation of our results, 't\e present such a treatment below.

B. Characterising data types in logic.

Clatk and Tamlund in [Clatk & Tamlund 1977] ~re the first ones to present a uniform way to charac­ terise and deal with data types within the frame"WWrlt. of first-order logic. Different treatments of data types in logic also appear in [Vasey 1985]. Here, ho't\ever, 'We restrict our attention to recursively defined data types and present a general axiomatic way of characterising them, which serves as the basis for formalising some results in the next section.

By data type - or sort - 't\e mean a oollection of values, a subset of the Herbrand Universe. A simple way to characterise data types without detmtifig from first-order :logic is to use predicates, since any relation can be thought of as defining data types for its argu­ ments ,Le. the sets of values that belong to the relation. For example, oonsider the unary predicate no.tural, such that natuirzt x) is true if and only if x is a natural number - belongs to the data type natural. This data type can be axiomatised with a recursive definition: mturaJf x) <-> »- 1 emr /y ( naturali.y) & »- suaiy)) and an equality axiom: suaix>- suaiy) <:--;:>»- y, where exor is the symbol for exclusive or, 1 is a oon­ stant and SJCC is the successor function; 1 and SJCC are the t\\U oonstructors of the type. Notice that the ele­ ments of this type are of the form : 1, suaf1), s.«:rf suaf 1)),... for any finite time of 'succ' occurrences. Similarly 'We can axiomatise the oommon types of lists end trees - used in following examples.

lid.(/) <:--;:> l- nil emr

Jlh /It ( e/emenl( lh) & lm( It) & l- lh.lt)

and lhl.ltl- lh2.1t2 <:-;>lhl- lh2 & Ill- lt2'

where nil and '.' are the term oonstructors of our representation of lists and element is an arbitraty type.

tree( x) <:--;:> »- null emr

/xl /w /::rr (tree( xl) & 1Vde( w) & tree( ::rr) & & »- t(xl, w,::rr))

and t(xJ,J,wl,::rrl)- t(xl2,w2,xr2) <:-;>wl- w2 & xll- xl2 & & ::rrl- xr2

where ra.dl and t are our tree-representation oonstructors and node is an arbitraty type.

In general. in order to axiomatise an arbitraty data type with a recursive definition 'We assume the existence of~ oonstructor predicate·s A1 and A2, such that: Redypir) <:-;>AJ(r) emr

where~ (ul'".,uJ, ~ (vl'".,v ) (u and v can be tuples of variables) and·~ i' ;,.. 1, ·· ,'lA, denote arbitraty types. Al, the base OOilS1%'UCTOr, establishes a bottom element for the type and A2, the main oonstructor, builds new elements of the type out of okl ones. A kind of an equality axiom may also be added: /ul Jvl Vu Vv(A2(r,u,v) ~u- ul & '\a- vl).

Naturally 'We associate an induction schema with any so defined data type, which enables us to reason about any relation defined over such a type. For Any Formula P :

Vr{(AJ(r) ..:;>/(r)) &

Vu Vv(A2(r,u,v) ~(I(u 1 ) & ··· & /(u ) ~/(r)))]'t1- Vr(Reaype(r) ~/(r)) n ·

If now, for example, 'We define a relation even: ever{ x) ~ /y ~ Z"y , and 'We wish it to have meaning only when xis a natural number, 't\e can can use the oonditional definition:

Vx(natunzix) ...:;>(ever{x) ~/y~ Z"y)).

In general. in· order to denote that a specific argument x of a relation R can only range over some data type Sometype, 'We use a conditional definition for R :

Vx(Sometype(x) ...:;>(R(x,y) ~Defi,niens)) ,

where Deftniens stands for the definiens and y for any other arguments.

This means that R has meaning only for those first arguments that satisfy Sometype - are of this type.

In the case where Sometype is a Reaype the definition of R can be put into one of the forms:

R( x,y) <-;>[AI( x) & R~ x,y) 1 or

or or /u /v [A2( x,u, v) & R~ u, v,y) 1

R(x,y) <--;>/u /v [A71x,u,v) & R4(u,v,y)1

II. A CLASS OF FIRST-QRDER LOGIC RELATIONS

In [Kowalski 1985] an extension of Horn clauses is identified, called the extended Hom dause subset of logic, which offers more expressive po-wer than the Horn clause subset and admits efficient computations. A clause belongs to the extended Horn clause subset of logic if and only if its condition contains a universally quantified Horn clause. Additionally, -we say that a rela­ tion is defined with an. extended Hom dause if and only if the if-half of its definition is an extended Horn clause. Quite a number of common relations, some of which are presented below, fall naturally within this class. Here -we identify a class of first-order relations, which can be defiried with a subset of the extended Horn clause subset of logic and for which -we present means for mechanically transforming their definition into Horn clausal form. First -we present a few examples of rela­ tions in this class and explain the relationship with their corresponding programs.

A. Examples.

a) The s.tbset relation.

This has already been presented in (1), but here -we slightly alter the format in the member specification so as to conform to our general schema of specifying relations over recursive data structures presented in 0). Both arguments of s.tbset are assumed to be of type list.

S1: subseL(lJ,l2) <-> Vz (member(z,ll) -;>member(z,l2))

S2: ~member(x,V <:-~nil

S3: member( x,V <----;>/lh /It ( ~ lh.lt & ( »- lh or member( x,lt)))

Notice that s.tbset is defined with an extended Horn clause and member is defined recursively on its second argument L S2 is the base case, since lis instantiated to nil, and S3 contains the recursive occurrence of member with b- lt, the tail of the original list. The -well­ definedness can be easily proved by induction on lists. The corresponding program for s.tbset, as inferred above, is:

Pl: s.dJset( nil,/.2) <- P2: s.dJset( u.l,/.2) <- member{ u,/.2) & s.Wset<l,/.2)

Notice that this is a recursive program on the first argu­ ment; Pl is the base case clause and P2 the recursive one, since it contains a recursive call to s.tbset with its first argument being the tail of the original list. Termi­ nation can be proved by induction on lists. It is essen­ tially the recursion of the first occurrence of member in the initial specification - which has been eliminated in the above program - that has been transferred onto s.dr set. And, as it will be shown below, one could avoid all the trouble of formally inferring this program - as -we did in (I) - and write it down, more or less directly, fol­ lowing some syntactic rules.

b) The max relation.

mtdl,x) holds when l is of type list, x of type element and x is the maximum e1ement of l with respect to some ordering relation('<') defined on elements.

S1: mo.x(L,x) <-;>member<x,V & Vz(member(z,l) -;>z<:t> S2, S3: as in the above exam]ie.

Similarly here max is defined with a,n extended Horn clause and if -we first isolate the second conj..mct in Sl: S4: upperbound(l,x) <-..:;> Vz (member(z,V -> z<:t> -we can obtain the following recursive program for upper­

which does not involve the relation member and for which the same observations can be made as in the

bound: P2: upperf>ound( n.il,:t> <- P3: upperbound(u.l,:t> <- u<x & upperbound(l,x) above example.

Thus, -we get the following program for max: P 1: max( l,:t> <- member( x,V & upperbound( l,:t> together with P2, P3.

c) The orrltree relation.

ordtree( x) holds when x is of type tree and its nodes are ordered with respect to an ordering relation ' < '. lejtof u, v,xJ holds when node u is on the left of node v in tree x. belong:/ u,x) holds when u is a node of tree x.

S1: ordtree(:t) <:--;:> Vu Vv (1£jtofu,v,x> -;>u < v)

S2: ~kjtofu,v,x) <:-»-null

S3: kjtofu,v,x) <-;>}xi /w /xr(»- t<xi,w,xr) &

[ (u- w& belo~v,xr)) or ( v- w & belo~ u,:xl)) or(belo~u,xi) & & beiDn&i v,xr)) or kjtofu,v,xi) orkjtofu,v,xr)

S4: ~belo~ u,x) <- »- null S5: belon&iu,x> <:--;:>}xi }w lxr (»- t(xl,w,xr) & ( u- w or belon&i u,:xl) or belo~ u,xr)))

The corresponding program is:

P 1: ordtree( null) <:-

P2: ordtree(t(xl,w,xr)) <:- auxill(xl,w) & auxil2(w,xr) &

& auxil3(xi,xr) &

& ordtree( xi) & ordtree( xr)

P3: auxill(null,w) <:-

P4: auxilJ(t(xi,wl,xr),w) <:- wl <w &

& auxill(xi,w) & auxill(xr,w)

P5: auxi/2(w,null) <:- P6: auxi/2(w,t<xl,wl,xr)) <:- w<wl &

& auxil2( w,xi) & auxil2( w,xr)

P7:auxil3(null,x) <- P8: auxil3(t(xi,w,xr),x) <:- auxil2(w,:t> & & auxiJ3( xi,:t> & auxil3( xr,:t>

which is recursive, does not involve leftof and belongs, but introduces three new relations - auxill,auxi12,auxil3 -, which are again recursively defined. Here the p!SSage from the specificationS to the program Pis not as obvi­ ous as in the previous 1\\Q examples mainly due to the nested recursions. Nevertheless S and P are equivalent under the dosed 'WOrld assum¢on and a simple syntactic transformation suffices to obtain P from S, as -we shall show later.

B. Fonnal resultB

Firstly~ define a class of re1ations, which we call RR ( R~y-defined Relations). We consider re1a­ tions of at 1east hiD arguments - either of which can stand for a tuple of arguments - which parameterise the class. A third argument is added in the representation of these re1ations to stand for any other - if any - argu­ ments, which are uninteresting for our purposes.

Definition 1 : A re1ation R belongs to RR i1f it belongs to one of the classes RRO, RRl, RR2, RR3, RR4.

A re1ation R belongs to RRO[r,q] i1f it can be defined as: SO: R( r,q ,s) ?-.;:> q- I r), for some arbitrary function f.

A relation R belongs to RRl[r,q] i1f it can be defined as: Sl: ~ R( r,q ,s) <C- A1( r)

S2: R( r,q ,s) «-.;> lu lv ( A2( r,u, v) &

[R2<u,v,q,s) or

R( u 1 ,q ,s) ... or R( un,q ,s)])

where: i) Al, A2 are constructor predicates for a recur­ sive data type (see I.B) ii) R2 belongs to RR[x,q], where x can be any of its other argwnents (apart from q) or a function of these.

A relation R belongs to RR2[r,q] i1f it can be defined as: S3: R(r,q,s) <e-.;>(A1(r) & R1(r,q,s)) or

lu lv ( A2( r,u, v) &

[R2<u,v,q,s) or

R(u 1 ,q,s) ... orR(un,q,s)])

.

where Al,A2,R2 are as abOve and the same holds for Rl as for R2.

A relation R belongs to RR3[r,q] i1f it can be defined as: S4: R( r,q ,s) «-.;> R 1( r,q 1 ,s) & R2( r,q2,s) where g- (Jl,q2) (an arbitrary split) and Rl, R2 belong to RR[r,ql and RR[r,q2] respectively.

A relation R belongs to RR4[r,q] i1f it can be defined as: S5: R( r,q,s) «-.;> R 1( r,q,s) or R2<rjq,s) where Rl, R2 belong to RR[r,q. 0

The re1ations member, leftof and belongs are examples of RR-relations.

Notice that, if we consider only the · <-· 4lalf of any of the above definitions for the re1ation R, it can be directly expressed in Hom clausal fonn, thus providing us with a logic program for computing any instance of the relation R - given a Hom-logic interpreter like PRO­ LOG -, which is not only correct but also compkte with respect to the initial speciftcation. The correctness fol­ lows trivially from the truth of: A?-;>B ~ A?-B. For the completeness we also need the dosed 'Hmid as:!UITI.Jr tion (c.w.a.); that is, if there aren't any other clauses with head A, which means that the only way to establish A is by showing B - A is true only if B is -, it follows that: A<-B ~ B?-A and thus: A?-B ~A ?-;>B.

The programs corresponding to the above classes are:

RRO: R(r,q,s) <C- q-fr) or slmpzy: R(r,fr),s) <C-

RRl: R(r,q,s) <C- A2<r,u,v), R2(u,v,q,s) R(r,q,s) <- A2<r,u,v), R(u 1 ~q,s) (~ 1, ... ,n)

RR2: R(r,q,s) <C- A1(r), R1(r,q,s)

R(r,q,s) <C- A2<r,u,v), R2<u,v,q,s)

R(r,q,s) <C- A2<r,u,v), R(ul'q,s) · (~ 1,.:.,n)

RR3: R(r,q,s) <C- Rl(r,q1,s), R2<r,q2,s)

RR4: R(r,q,s) <C- Rl(r,q,s)

R( r,q ,s) <C- R2( r,q ,s)

It should be noted that in all of the above programs we assume the existence of logic JX'C)grams for the intro­ duced re1ations Rl and R2, a fact that follows from our definitions - formally by induction.

Now 'We define another class of relations, which ~ call ERR ( ExtentJed RR). Relations in this class have at least one argument, which pe.rameterises the class, and a ·seco~d argument is added as in the pevious classes.

Deftnitkm 2 : A relation Q bek>ngs to ERR[r] i1f its definition can be put in the fonn :

Q(r,s> ?-;>Vq (.R(r,q,s) ...:;>..6/q,s))

where R belongs to RR[r,q] and A is an arbitrary rela­ tion, for which ~ can obtain a Hom logic program. 0

The relations subset, u~ and ordtree are examples of ERR-relations.

Notice that for this class a Hom logic program cannot be obtained directly, that is, simply by converting into clausal fonn as above. Ho'Wever, the following theorem provides us with an easy way to get such a 1ogic pro­ gram, which is correct and complete with respect to its specification.

·lPEOREM : If a relation bek>ngs to ERR tllen it can re~xpressed in a :logically eqwValent way {under the

c. w.a.) using only Hom clauses. More speciftcally, if Q bek>ngs to ERR[r] and thus can be defined as: S : Q( r,S.> ?-.;:> Vq ( R( r,q,s> ...:;> Al q,s)) then the corresponding _programs are as follows: . 1) if R be:Jongs to RRO[r,qf then P: Q(r,s> ?- Alfr),s) 2) if R bek>ngs to RRl[r,q] then Pl: Q(r,s) <C- Al(r) P2: Q(r,s) <C- A2<r,u,v), Q2(u,v,s), Q(u 1 ,s), ... , Q(un,s) '\\here AS: Q2<u,v,s) «-;> Vq (R2(u,v,q;J ..::;> A(q,s)J (!-tAP) 3) if R be1ongs to RR2[r,q} then Pl: Q(r,s) <C- Al(r), Ql(r,s) P2: Q(r,s) <C- A2<r,u,v), Q2(u,v,s), Q(u 1 ,s), ... , Q(un~ '\\here ASl: Ql(r,s) «-;> Vq (Rl(r,q,s) .;:;>A/q,s)J (H API) and AS2: Q2<u,v,s) eM> Vq (R2(u,v,q,s) ..:o>Alq,s)) (l-tAP2) 4) if R be1ongs to RR3[r,q] then AS: Q( r,s) ?-.;:> Vq ( Rl( r,q,sJ ..:;>Ql( r,sJ) where ASl: Ql(r,sJ <-..:;>~ (R:z<r,q,s) ..:;>Aq,s)) S) if R be1ongs to RR4[r,q[ then P:Q(r,s> ?-Ql(r,s), Q~r.s) where ASl: Qf(r,s> ?-.;:> Vq (Rl(r,q,s) ..:;>Alq,s)) and AS2: Q2<' r,sJ ?-.;:> Vq ( R:z< r,q,s) ...:;> Al q,s)) 0

PROOF : For each of the above ftve cases ~ shan show that the relationship that ho1ds between the pro­ gram and its specification is that of logical equivalence (under the c.w.a.), from which the correctne88 and com­ pleteness results follow trivially.

formally by induction - that a logic program can be ulti­ mately deduced.

5) From S and S5 easily follows that [Q( r,s) <-> Vq ( R 1( r,q ,s) or R2( r,q ,s) ->A( q ,s)) 1 1--l 1-I[Q(r,s) <-> Vq (RJ(r,q,s) ->A(q,s)) & Vq (R2(r,q,s) ->A(q,s)) 1 from which Pfollows (by using ASJ, AS2).

The same as for the previous case applies here. Q.E.D.

The identification and synthesis process for the ERR class of relations described in the above theorem has been implemented in PROLOG, thus providing with an a'!ltomatic tool for synthesising (naive) programs for such relations.

III. CONCLUDING REMARKS

We have identified a subset of the extended Horn clause subset of logic, for which we proved that it can be reexpressed in Horn clausal form. Thus, for rela­ tions that are defined with clauses belonging to this sub­ set we gave mechanical means for obtaining a directly _executable (by standard PROLOG interpreters) pro­ gram.

The significance of this transformation largely depends on t\\0 factors.

The first is the generality of this class: how many rela­ tions are naturally expressed in this way? In [Kowalski 1985] it is argued that the extended Horn clause subset of logic has great expressive power and many examples, as the ones presented above, can be found that fall within this class. Moreover our subset is still general enough; the only requirement is that the antecedent of the universally quantified Horn clause is recursively defined with an ultimate direct instantiation of the universally quantified variables. Such a case is very common when dealing with recursively defined domains as indicated by the examples presented.

The second is whether the recursive Horn clausal form, which is the end product of this transformation is really more efficiently executable than the initial specification. As it is pointed out in [Kowalski 1985] one can build interpreters that encomp!SS the extended Horn clause subset of logic: ·By translating the universal quantifier into double negation and interpreting negation by failure such clauses can be executed both correctly and efficiently, though incompletely". The source of incompleteness is the introduction of negation, which means that we cannot get all possible answers to a query. For example in the case of the 'subset' example this method will 'IDrk only for queries with both argu­ ments instantiated - to test if the relation holds between t\\0 known sets -, while execution 'IDn't terminate in any other use. This, of course, is a severe limitation given our expectations from a logic programming language that is supposed to offer input-output non­ ~terminism, and it can be overcome using the recur­ Slve programs.

Furthermore, it is argued that such an iterative execu­ tion - effectively generating every instance of the universally quantified variables that satisfies the antecedent and checking if it also satisfies the conse­ quent - is more efficient than a recursive one, since it does not require a stack. Given that there are efficient ways of implementing recursion -tail-recursion in par­ ticular_ can be turned into iteration -we argue that the recurnve programs that result from our transformation are in general more efficient than the corresponding iterative execution of the initial specifications. Addi­ tionally they do not require any extra sophistication from the logic interpreter for their execution.

In the -light of the above discussion a link between iteration and recursion should become apparent. Furth­ ermore, it should be . realised that the above result depends very much upon the nature of recursion and it is unlikely that similar results can be obtained for more general subsets of logic. Obviously, additional domain­ specific knowledge and intelligent manipulation is neces­ sary for the derivation of efficient Horn clause programs from arbitrary first-order logic specifications.