A Network of Communicating Logic Programs and Its Semantics

A NETWORK OF COMMUNICATING LOGIC PROGRAMS AND ITS SEMANTICS

* Susumu Yamasaki

Department of Information Science, Kyoto University Sakyo, Kyoto, Japan

**

In this paper, a network of ccmnunicating logic programs is proposed as a rrodel for parallel/ concurrent progranming .based on logic programs. This network is regarded as an extension of Kahn's prre dataflow in the sense that nodes are logic programs which have atans for receiving am. serrling messages as well as queues to accept am. memorize them. The nodes' behaviour is unboundedly noooeterministic. On the assumption that the channels' denotations should be defined by using sequence danains, the main concern of the present paper is whether or not mathematical semantics is always well-defined for a given network even when it is of unbounded norX!eterminism.

This paper will show that the proposed network is reduced to a dataflow when a kioo of 'fairness' is asked for nondeter­ minism in which logic programs receive inputs am. produce outputs based on their c::cmpltations. The network, then, has a (least) fixpoint semantics; it is regarded as one of mathematical semantics of the network, since it can satisfy the recursive relations among the channels' denotations .

It is also stated that the network with fair merge opera­ tors is applicable to the realization of a canputational mechanism for sequential ligic programs.

Kahn · s prre dataflow network is one of the established rrodels for parallel/concurrent progranrning in the sense that its mathematical semantics is clearly defined by the least fixpoint solution to the set of equations associated with the channels of the network [ 4, 5].

When establishing a rrodel for parallel/concurrent pro­ granrning based on logic programs, Kahn's prre dataflow can be extended to a network whose nodes are not functional but relational in accordance with logic programs. If we establish a network according to such a rrodel, there would be a strict question as to whether or not mathematical semantics of the network is well-defined even when it is of unbounded noooeter­ minism. The question arises fran the staOO.point that mathe­ matical semantics should be made clear in order for operation­ al semantics to be given so that implementation of the system is possible. In both Pl\RLOG [2,3] and Concurrent Prolog [10] the channels' semantics are iooirectly defined, hence the camunications between processes seem canplicated.

In general, unbounded noooeterminism due to the canputation of logic programs should be respected and mathematical seman­ tics should be defined based on the relations among the denota­ * Present Affiliation: Department of Information Science, Okayama University, Okayama, Japan.

**This report describes work initiated at Department of can­ puter Science, University of Warwick, the United Kingdcrn. It was supported in part by Yamada Science FourX!ation.

lions of channels. Hence the fixpoint theory in [4] is not appropriate in this case. Even theories concerning power­ danain constructions in [9,11] are unsuccessful for the net­ work we interXI to define, since, in essence, the network is described by relations among the denotations of the chan­ nels.

On the other hand, one way to extend Kahn's rrodel to a rrore general one is to establish a class of noooeterministic canputing networks whose nodes are either asynchronous, conti­ nuous functions or fair merge operators. Fixpoint semantics of such networks is well-defined in [8]. The 'fairness' applied to such networks might be useful to solve the question of mathematical semantics of the unbounded nondeterministic network of logic programs. However, it seems that nodes consisting of logic programs contain rrore nondeterminism than the fair merge operations, since the choices of outputs produced by their canputations are not only due to the rel­ ative timings of inputs but due to the decisions concerning their relations. At the same time, there is a crucial problem of how 'fairness' can be realized for nondeterminism in which logic programs are c::cmplted.

In this paper, we have a fair sequence in which any natural number occurs an arbitrary nunt>er of times; By means of the fair sequence it will be shown that fairness is well realized for nondeterministic receiving of messages, am. serrling of messages related to the c::cmpltations of logic programs, in the network. The network consisting of ccrmu­ nicating logic programs might be reduced to a dataflow when fairness due to the fair sequence is asked. Thus, the net­ work has a (least) fixpoint semantics for the reduced da­ taflow, according to [8]. The fixpoint semantics could be regarded as one of the mathematical semantics for the original network. According to the fixpoint semantics , an operational semantics will be shown on the condition that logic programs in the network are fairly nondeterministic in receiving inputs and sending outputs. If the interX!ed network has fair merge operators, it can express a canputational mechanism for se­ quential logic programs. It means that the semantics of sequential logic programs might be defined by applying the semantics of our network with fair merge operators.

The outline of the network is as follows : The network consists of channels am. processes. The channels are only ways by which the processes may ccmnunicate with each other. There may be channels for inputs aOO./or outputs. The message is transmitted one way through each channel within a suffi­ ciently short time. Each process is a logic program con­ sisting of definite clauses with atans corresponding to re­ ceiving and serrling messages as well as unbounded FIFO queues each of which is connected with an input channel transmitting messages. In each process, the messages in the nondeterminis­ tically chosen positions of the queues are received for the canputation of the logic programs, simultaneously.

After the logic program's finite c::cmpltation, each process nondeterministically provides either one of possible outputs or no output .

A logic program is a set of definite Horn clauses. A defi­ nite Ho:rn clause is either an expression A<-B ··· B or A<­ for atans A arxl B, . An atan is an expression \(\~ ··· ,t ), where P is a proolcate symbol arxl \, ··· , t are tenns. mlf P(t) is an atan for a term t, P is called mmonadic. A term is defined recursively as follows : (1) A constant or a variable is a term. (2) f(\, ... ·\) is a term if f is a function symbol arxl t 1 , ... ,\ are terms.

'!he a tan on the left-harrl side of <- in a definite Ho:rn clause is called the head of the clause. '!he set of atans (which might be empty) on the right-harrl side of <- in a definite Ho:rn clause is called its txxiy.

• A !!_ett.o:>rk of £CI'I'Uilicating !ogic ~ams (!DR) is N=(C,L,I,O,Combi,CombO),

where:

(1) c= {c , ··· ,c} is a set of channels.

• J J J ( i) S . is a logic program such that
• ( 2) L= {L , ··· ,f. } ism a set of logic programs with queues. For l~j~n, L . ~(S , ,q , Y, where
• (a) i\: contains the atans whose predicate symbols are Sek-D .k (monadic) for D.k inC (D.kni is empty, k=l, ··· ,n ,, J J J J arxl D jk(\ D jh is empty iff JQ'h) in the heads of sane clauses in s ·' arxl
• c J (b) it might contain the atans Re-ce(xe) for channels arxl variables x in the bodies of sane clauses in S . , e (ii) e J qj is a tuple of unboun:l.ed queues.
• I is a subset of c, called an inp.tt channel set. 0 is a subset of c, called an outp.tt channe~ set.
• ( 4) Comb! is a function fran L to 2 such that for . CcxriJI(L . )= { c I Re-c appears in s . } · J e c e J

CanbO is a relation on Lx2 such that for each L . , is in Ccmt:O. Fran now on, that (Lj,Djk) is in CanbO. J CombO(Lj,Djk) is used

It is assumed in the present paper that the logic programs in ICU' are camunicating based on their finite oanp.1tations. en this assumption, the semantics of logic programs are given by their minimal Herbrarxl models [3,12].

3.1. Senentic Danain

• ( 1) Hu denotes the Herbrarxl universe constructed over the set of constants arxl function symbols in s 1 , ... ,sn and in the channels of I.
• H means the Herbrand base formed by the predicate symbols iJ' s , ··· ,s arxl by the terms in Hu.
• Let \i be na special symbol not in Hu. (Note that hi is a hiaton used in [8], which is to denote a time-delay.)
• Let D=Hu V{ hi} , and l e t o 00 denote the set of all finite and infinite sequences fran D. A denotes the empty sequence in 0 00 · A partial order t on D 00 is defined by : u tv for u, v in 0 00 iff v=uw for sane wino 00 ·

Note that any chain { u t u 2 t · · · t u } has a least upper bound, which is denotecl by t u · n

P P . n '!he partial order t is extended to the one on (0 00 ) by: <u 1 , ··· ,un) t (v 1 , ··· ,vn) iff up t vp for l~~n.

• w denotes the set of natural numbers.

3.2. Denotatials of O>annels

For i=l, ··· ,m, X. in D 00 means the denotation of C. in C, which is to be d~fined by the relations as shown in ~.4.

3.3. Denotatioos of Logic Programs

For j=l, .·. ,n,

(1) (i) the denotation of q . is d-q ,=( E(Xj 1 ), ··· ,E(Xjh)) where (a) { c. 1 , ··· ,c .h }=Combt(L.), and J J J

(b) E: D 00 -> Hu 00 is recursively defined by: E( A )= A; E(hi.u)=E(u); E(a.u)=a.E(u) for ajlhi,

• (ii) Q .-c .. means E(X .. ) of d-q , , for C . . in Combi(L . ), J J1 J1 J J1 J
• the denotation of sj, for the inp.tts of length p, is defined by

where V/r 1 , ... ,rh,d-qj)~(min I)Tj(r 1 , ... ,rh,d-qj,I)

for

T.: w·hx (Hu 00 )#Combi(Lj)XPow(H )->Pow(H) J H B B set 2 8 , IIY: the cardinal number of a set ( Pow(H 8 ): the Y), defined by

arxl for

3.4. Relatioos 8llaliJ Denotatials of O>annels

if I E(X ) I ~ ( I u I means the length of u) for sane e such that C !s in Combi(L . ) or if iiCombi(L. )=0, arxl e J J

'!he semantics of the nett.o:>rk N is ( E(X 1 ), ·· · ,E(Xm) for (X 1 , ··· ,Xm) which is in

Note that for ci in Djk such that canbi(Lj,Djk), there are 1+11( U WJ'k(r 1 , ··· ,rh,d-qJ,) ) choices for ( ) r 1 , ··· ,r. <p xi P · tr'

SUch ncndetenninism is due to

1. what nunbers r 1 , ... ,rh are chosen aroonq{ 1, ··· ,p}, to indicate the positicns of queues of q . on which the denotations of 1 Re-c 1 -atans deperrl, and J
2. e (2) what element is chosen in W.k<r 1 , ... ,rh,d-q , )~hi }, to indicate the denotation of 1 Se-D jk 1 -~. J

'lberefore, there may be as an infinitely many rn.nber of choices as W, \o'hen X. is fixed.

We shall have a clfss of fair sequences in U.l W as oracles in order that the choices for the positicns on the queues and for the atans 1 denotaticns may be made fairly uroer such ncndetenninism. If the oracles are used, the denotaticns of channels can be described by a continuous, asynchronous function fran a direct product of 0 00 to itself.

4.1. Fair Sequence in w w

DEFINITictl 1 u in w W is fair iff for any k in w and for any h in w, k occurs in u, h tilres.

DEFINITictl 2 Let Sf denote one of sequences in wW , provided by the net..-ork as shown below, \o'here: (1) T: W 00 -> w 00 is defined by

T( A )= A ; T(a.u)=(a+l).T(u) for u in woo.

1. FM: w"" X w 00 -> w 00 neans a fair merge operator, that is, FM(u1v)'"W iff w is a sequence obtained by inter­ leaving u and v in a fairly nondeterministic way. (For the fair merge, see [6,7,8]).

DEFINITictl 3 A functioo. F: D 00 -> Hu 00 is asynchronous if F(E(u))=F(u) for any u in D 00 · F is continuous if F( t u ) { u 1 t u 2 t · · · t u n t ··· } p · P

l'RClFOOITictl 1

1. Sf is fair in wW
2. Sf(j)+l~_j.

Proof ( 1) Note that S =() +. u for sane u in w W Now ---- f let Occur(k,h) mean that k occurs h tilres in u.

• (i) It is seen that Occur(O,h) for any h in W , because 0 W is an inp>t of FM and thus 0 appears as its outp>t an arbitrary nunber of tilres.
• (ii) Assune that for sane h, Occur(n,h) for n~k. ~. since k+l should be at the same tiJre an outp>t of T and hence an inp>t of FM, Occur(k+l,h). By mathematical inductioo., for sane h in w, Occur(k,h) (for any k).

(iii) Since Occur(O,l) fran (1), it follows fran (2) that Occur(n,l) for any n in w · SUppose that Occur(k,h) for any k in W and h~m. Since k should be an outp>t of T, k-1 should be an inplt of T, that is, k-1 occtirs in u as many times as k. 'ftlus Occur(k-l,h). Finally Occur(O,h). It follows fran (1) that Occur(O,h+l). 'lberefore there is no case that Occur(k,h+l) does not hold. 'lhis canpletes the inductioo. step of mathematical imuctioo.. Thus Occur(k,m) for any k and for any m.

1. (i) If j·l, the propositioo. holds, since 0 t s · (ii) Assune that Sf(h)+l~h for h~k. Since oo.e of the in~ of FM is Sf(k)+l or O, E(Sf)(k+l)=E(Sf)(k)+l or a. 'ftlus Sf(k+l)+l~(Sf(k)+l)+l_9<+1. 'lhis canpletes the inductioo. step.

By means of fair sequences in wW as oracles, the denota­ ticns of channels can be defined as determinant for each logic programs.

For j·l, ··· ,n, let P ,k(p): W,k(I , (p),d-q,)-> W p in W ) be a oo.e-to~ functi~ audt t:.h4t (for

fort in Wjk(Ij(p),d-qj), where kal, ··· ,h and Ij : w-> W h is a bijectioo. such that any element of I /P) ~· Let Sf -j denote a sequence in w W , qi ven by DEFINITictl 2. Also let

For k-l, ··· ,nj and each ci in Djk such that CattlO(Lj,Djk), we define _ 1 . xi (pl· P jk<sf -j(pl+ll < min { sf ~j(Ord(sf -j(p)) )+1,

IIWjk (Ij (Sf -j(p)+l) ,d-qjl}

if I E(X >I '!Y for sane e such that c is in catt>I(L , )

or if I!Oi.t,I(L . )-a, and

J

Xi(p)-hi otherwise.

PRCPOSITictl 2 For i·l, ··· ,m, there exist asynchronous, continuous functicns F . : ( D 00 )m -> D 00 such that

Proof Since either Ci is in I or ci is in Djk for sane Djk in 2c such that CattJO(Lj,Djk), xi is defined by either a given element in D 00 t:hrouqh Ci or by the above fornula. Since P (S -j(p)+l)-l is a oo.e-to~e functioo. fran w to wjk2fj<lf-j(p)+l),d-qj), ani . the denotatioo. of d-qj is defined by Xe for e such that Ce is in cati>I(Lj), we see xi (p) is a functioo. of Xe[p]. (By Xe[p], the first ·Sequ<!r~Ce of length p in xe is meant.) 'ftlus, we oould p>t

oo m oo Xi-Fi(\, ... ,Xm) for Fi : (D ) ->D · It follows fran d-qr< E(Xj 1 >, ··· ,E(Xjhl ) that Fi are asynchroo.ous. Since Xi[p]-Fi(X 1 [p], ··· ,Xm(p])t Xi·Fi(X 1 , ·· ,Xm)· F . ( t X 1 [p], ··· , t X [p]), l. p P m

• t p Fi(Xl[p], ··· ,Xm[p]) t Fi(Xl, ··· ,Xm). en the other hand, for any pin w, Xi[p]·Fi<x 1 , ... ,xm)[pl t

e

J

Fi<x 1 [p], ··· ,Xm[p]), since Xi(p) is determined by \[p], ··· , X [ p l . 'lberefore m

This completes the proof of the continuity of F .·

This proposition states that the network is reducible to a dataflow by means of fair sequences in W W Finally we have the following proposition:

PROPOSITICN 3

For the network N=({ c 1 , .·. ,C } , { L 1 , ... ,L } ,I,O,Canbi,CanbO) there exists a function F ~ (0 00 )m->(D 'lx, )m such that the (least) fixpoint of FN is i~ Sem(N).

Proof FN is given by (F 1 , ··· ,Fm), where Fi are asynchronous, =ntinua.ls functions. 'lbus there exists a (least) fixpoint of FN [8]. Fi are in accordance with the fornula we have already obtained. Hence X. satisfy the relations as shown in 3.4 (2). Finally the fiiiuint of F is in Sem(N). N

4.3. Operatiooal Semantics of N:LP

In this section, we have an operational semantics of IO:.P based on its fixpoint semantics given in the previous section. In operational semantics, the hiaton hi used in denotational semantics, co=esponds to the states of waiting messages aril/or producing nothing. The denotations of 'Re-c '-atans co=espond to receiving messages and those of 'Se-D e'-atans oo=espond to sending messages. jk

4.3.1. Assumptions

• ( 1) 'lbe messages sent to each channel C should be stored in the unbounded FIFO q . of L . , when c e is in Canbi (L . ) ·
• J J e J ( 2) When a logic program L . wants a longer queue, in order to generate (send) the neft out]OAlt, it must wait for the necessary messages a=iving at its queue.
• Unless a logic program can get something by its oam­ ]OAltations, it never sends any message to channels.

DEFINITICN 4 For a nonempty set A, FairChoice(A) means some b in A is chosen at any tiroe such that the sequence of chosen elements is fair in A W (A sequence is fair in A W if any b in A occurs an arbitrary m.unber of tiroes in the sequence. )

DEFINITICN 5 For a set S of definite clauses, Can]OAlt(S) denotes the set of ground atans, which is the minimal Herbrand model of s.

DEFINITICN 5

Let l'F( .{ c 1 , ··· , Cm , { L 1 , ··· ,Ln} ,I,O,Canbi,CanbO). Let q,=(Hu 00 )#canbi(Lj), that is, a tuple of queues. 'lbe J length of qj is the maximum length among lengths of sequences stored in q. Q. -c means the =ntent of queue of q . , oonneJ J e J cted to the channel C such that C is in Canbi(L.). For pin W, Q.-c (p) denofes the p-th cci.tent it holds. J J e

'lbe procedure f . for L. is given as follows: J J

procedure f . 1 J

~

~

~wait until (the length q/~.Pj1

for each Djk such that CanbO(Lj,Djk) dO

end

end initially defined as empty for

'lbe procedure for N is defined as follows:

5. APPLICM'ICN CF IO:.P

'Ibis section is an overlook of the application of lf:LP to the transformation of sequential logic programs to dataflow networks with fair merge operators. Any sequential logic program denotes an NCLP with fair merge opertors. It follows fran the results of the present paper ariJ. [8] that the denota­ tional semantics of a logic program might be defined as a fixpoint over sequence danains.

Let -> > be a subset of L x L such that (H . ,H.) is in -» (which is denoted by H. -»H . ) iff P. is ~:il to Q. 1 J 1 Jk . for sane 1~J~.n and l~k~nj. NOOn: L-» w is defined by: N<N>(H . )=# { H. I H, -»H . } Let FM(p,q) mean a fair J 1 1 J merge operator with p inp..~t-tuples of q channels and ale ootp..~t-tuple of q channels, which provides a sequence of tuples by interleaving, in a fairly na'ldeterministic way, p inp..~t-tuples of sequences .

For each H. in L, we define 1

where

Let L.=(S(H . ),q, ), where q, is a tuple of queues connected l. 1 l. l. with all the inp..1t channels for S(H. ). 1

the outp..~t-tuple of channels for Next, whenever H, -»H , , l. J S(H, ) is to be connected with sane appropriate inp..~t-tuples for 1 S(H , ), via an FM(N<N>(H , ),m. ). '!be appropriate inp..~tJ J 1 tuple of channels is chosen on the cor>:ii tion that P . is the same as the predicate symbol in the body of a defini~ clause in S(H . ), which has 'Re-'-atoms corresponding to the inp..1t J channels for S(H,). J

'!be total net..:>rk constructed for L in the way mentioned above is denoted by N(L). '!ben N(L) is regarded as an r«:U> with fair merge operators. Let us define the denotational semantics of channels with L. oorresponding to S(H. ) and their operational behavioor as !he same as those of the 'r«:u>-­ N(L), Since each S(H. ) oontains only H. as a definite clause without 'Se- 1 -atoms a.'id 'Re-'-atoms, if 1 we assune fair ncnde­ terminism for choosing the positions of queues in each L. to get messages and provide ootp..~ts, then the outp..~t-tupl~ of sequences from each S(Hi) is an asynchraloo.s, continuoos function of inp..~t-tuples of sequences. FM(p,q) i s an exten­ tion of an ordinary fair merge operator. '!bus N(L) is re­ garded as the net..:>rk presented and discussed by Park [ 8]. 'Ibis means that the semantics of N(L) is well-defined. 'Ibis is a theoretical guarantee from the point of semantics for regarding the OCI!Ip..ltation mechanism of logic programs as dataflows with fair merge operators.

It might be concluded that by using the r«:U>, we can trans­ form any logic program to a net..:>rk of dataflows with fair merge operators. 'Ibis is an interesting and significant aspect of r«:u>.

'!be r«:U> is reduced to a dataflow when fair ncndeterminism is asked for receiving and sending messages. In such a case, there is a (least) fixpoint semantics of a function associated with the r«:u>. As we have seen, this is cne of the denota­ tional semantics defined in Section 3. '!bus, the denota­ tional semantics of r«:U> is well-defined even when it has unl:x:luOOed ncndeterminism.

'!be operational semantics of r«:u> based on its fixpoint semantics was defined in SectiOn 4. '!be implementation of 'FairChoice' can be done by the fair sequences in W W ·

'!be expressiveness of the r«:U> contains interesting aspects ~ with other systans,

It is interesting to extend the r«:U> so that each process can rewrite the contents of its queues.

It was briefly menticned that the r«:U> with fair merge operators can express a CCIIpltation mechanism for sequential logic programs. 'Ibis is a significant aspect of the proposed net..:>rk as well as the ncndeterministic CCIIplting net..:>rk in [8].

First I walld like to thank Professor Park, whOse ..:>rk stinulated the author and inspired the present work during the author's visit to the Department of Catplter Science, University of Warwick. '!be author appreciates the valuable ocmnents of Professor Park concerning this ..:>rk.

'!be author is also heartly grateful to ·Dr. Matthews for his hospitality during the visit.

'!be author is indebted to Professor Doshita for his en­ oouragement during the author's stay in the United Ki.ngdan.