1: \documentclass{tlp}

2: \usepackage{aopmath}

3: 

4: \newtheorem{definition}{Definition}[section]

5: \newtheorem{example}{Example}[section]

6: \newtheorem{remark}{Remark}[section]

7: \usepackage{amssymb}

8: \usepackage{alltt}

9: \usepackage[arrow,matrix,frame,curve,cmtip]{xy}\CompileMatrices

10: \usepackage[english]{babel}

11: \usepackage{mathrsfs}

12: \usepackage{pslatex}

13: \usepackage{url}

14: 

15: \let\from\colon

16: \let\pto\rightharpoonup

17: \let\emptyset\varnothing

18: \let\setminus\smallsetminus

19: 

20: \newcommand{\cell}[4]{#1\raisebox{-.8ex}{\mbox{$\stackrel%

21: {\textstyle\stackrel{#2}{\longrightarrow}}{\scriptstyle #3}$}}#4}

22: \newcommand{\trans}[3]{#1\stackrel{#2}{\longrightarrow}#3}

23: \newcommand{\nat}{\mathbb{N}}

24: \def\abs#1{\left|#1\right|}

25: \newcommand{\sbtn}[2]{{#1}/{#2}}

26: \newcommand{\irule}[2]{\frac{\textstyle\rule[-1.3ex]{0cm}{3ex}#1}%

27: {\textstyle\rule[-.5ex]{0cm}{3ex}#2}}

28: \newcommand{\dfun}[3]{#1 \from #2 \to #3}

29: \newcommand{\eg}{e.g.}

30: \newcommand{\ie}{i.e.}

31: \newcommand{\wrt}{w.r.t.}

32: \newcommand{\cf}{cf.}

33: \newcommand{\vvdash}{\xymatrix@C=.3pc{{ } \ar@{||-}[r] & { } }}

34: 

35: \newcommand{\Set}{\mathbf{Set}}

36: 

37: \begin{document}

38: \bibliographystyle{tlp}

39: 

40: \title[Interactive Semantics]

41:       {An Interactive Semantics of Logic Programming}

42: \author[R. Bruni, U. Montanari and F. Rossi]

43:        {ROBERTO BRUNI, UGO MONTANARI\\

44:         Dipartimento di Informatica, Universit\`a di Pisa,\\

45:         Corso Italia 40, 56125 Pisa, Italia. \\

46:         \{\texttt{bruni,ugo}\}\texttt{@di.unipi.it}

47:        \and

48:         FRANCESCA ROSSI\\

49:         Dipartimento di Matematica, Universit\`a di Padova,\\

50:         Via Belzoni 7, 35131 Padova, Italia. \\

51:         \texttt{frossi@math.unipd.it}}

52: 

53: \maketitle

54: 

55: \begin{abstract}

56:  We apply to \emph{logic programming} some recently emerging ideas

57:  from the field of reduction-based communicating

58:  systems, with the aim

59:  of giving evidence of the hidden interactions and the coordination

60:  mechanisms that rule the operational machinery of such a programming

61:  paradigm.  The semantic framework we have chosen for presenting our

62:  results is \emph{tile logic}, which has the advantage of allowing a

63:  uniform treatment of goals and observations and of applying abstract

64:  categorical tools for proving the results. As main contributions, we

65:  mention the finitary presentation of abstract unification, and a

66:  concurrent and coordinated abstract semantics consistent with the

67:  most common semantics of logic programming. Moreover, the

68:  compositionality of the tile semantics is guaranteed by standard

69:  results, as it reduces to check that the tile systems associated to

70:  logic programs enjoy the \emph{tile decomposition property}.

71:  An extension of the approach for handling constraint

72:  systems is also discussed.

73: \end{abstract}

74: 

75: \section*{Introduction}

76: 

77:  Logic programming \cite{Llo:FLP} is a foundational research field

78:  that has been extensively investigated throughout the last 25

79:  years. It can be said that, in logic programming, theory and practice

80:  meet together since its very beginning, as each innovation on one

81:  side contributes many insights to the other side thanks to

82:  the basic principle of logic programming, which is `writing

83:  programs by expressing their properties.'

84:  This symbiosis has also facilitated the study and the prototyping

85:  of interdisciplinary applications that either extend the `kernel' of

86:  the framework with additional features or transfer helpful techniques

87:  from a large variety of paradigms. A typical example is the embedding

88:  of constraints within logic programming

89:  \cite{MS:PCI,JM:CLPS}, which retains the declarative and clean semantics of

90:  logic programming, as well as its typical problem solving features,

91:  while extending its applicability to many practical

92:  domains; in fact, constraint logic programming (\textsc{clp}) is now

93:  considered as a major programming paradigm.

94: 

95:  More interestingly, very often these flows of ideas have been

96:  profitably bidirectional and continuous, thus allowing one to

97:  establish strong connections between different areas (bringing useful

98:  analogies) and also to bridge gaps between different formalisms.

99: 

100: \subsubsection*{Interaction via contextualization and instantiation}

101: 

102:  In this paper, inspired by recent progress in the fields of

103:  communicating systems and calculi for concurrency, we want to focus

104:  on an \emph{interactive} view of logic programming. The idea is to

105:  understand logical predicates as (possibly open) interacting agents whose

106:  local evolutions are coordinated by the unification engine. In fact,

107:  the amount of interaction arises from the unification mechanism of

108:  resolution, as subgoals can share variables and therefore

109:  `local' progress of a component can influence other components by further

110:  instantiating such shared variables.

111:  One central aspect of this view is to understand what kind of

112:  information we should observe to characterize interaction and how far

113:  the approach can be extended to deal with different semantic

114:  interpretations of logic programs.  For example, one interesting

115:  issue is \emph{compositionality}.  Having a compositional

116:  semantic framework is indeed very convenient for formal reasoning

117:  on program properties and can facilitate the development of

118:  modular programs \cite{BGLM:CSLP,BLM:CMTS,GS:FACS,MP:ALP}.

119: 

120:  We sketch here the main ideas concerning the role played by

121:  `contexts' in reduction systems, but for a more precise overview we

122:  invite the interested reader to join us in the little detour, from

123:  the logic programming world to the process description calculi

124:  area, inserted in the last part of this introductory

125:  section (with links to related literature).

126: 

127:  Generally speaking, the issue we focus on is that of equipping a

128:  reduction system with an interactive semantics. In fact, although

129:  reduction semantics are often very convenient because of a friendly

130:  presentation, they are not compositional `in principle.'  The problem

131:  is that they are designed having in mind a progressive reduction of

132:  the initial state to a suitable normal form, \ie, one focuses

133:  on a completely specified system that can be studied in

134:  isolation from all the rest. In logic programming, this would

135:  correspond to studying the refutation of ground goals only and to

136:  develop an \emph{ad-hoc} system to this aim.  Then, if one wants to

137:  study the semantics of partially specified components the framework

138:  is no longer adequate and some extensions become necessary. For

139:  example, in process description calculi, a partially specified

140:  component can be a process term (called \emph{open process} or

141:  \emph{context}) that contains suitable process variables representing

142:  generic subprocesses. However, also a closed term (\ie, without free

143:  process variables) can be considered an open system when it evolves

144:  as part of a broader system, by

145:  interacting with the environment.  In logic

146:  programming we can distinguish two main kinds of openness and

147:  interaction. A first kind is due to goals with variables (rather than

148:  ground) that can obviously be regarded as partially specified

149:  systems. A second kind consists of regarding an atomic

150:  goal as part of a larger conjoined goal with which it must interact.

151: 

152:  The obvious way to deal with partially specified components is to

153:  transform the problem into the reduction case, which we know how to

154:  solve. This means that (1) the variables of open

155:  processes will be instantiated in all possible ways to obtain closed

156:  systems that can be studied; (2) in order to study the semantics of

157:  closed subprocesses we will insert them in all possible

158:  contexts and then study their reductions.  Moreover, the

159:  operations of contextual and instantiation closure can be rendered

160:  dynamically, provided that one defines a \emph{labeled transition

161:  system} (\textsc{lts}) whose labels record the information on the

162:  performed closure, and this has originated the idea of observing

163:  contexts and instantiations (sometimes called \emph{external} and

164:  \emph{internal} contexts, respectively).

165: 

166:  Even if these views can look semantically adequate, it can

167:  be noted, as their main drawback, that they are not applicable in

168:  practice, because all considered closures are infinitary.

169:  The situation can be improved if one is able to identify a small

170:  finite set of contexts and/or instances that contains all useful

171:  information, since this can make the approach operationally

172:  satisfactory. While a general methodology for accomplishing this task

173:  in  communicating and mobile calculi is difficult to find

174:  (see \eg, \cite{LM:DBCRS}), we think that logic programming

175:  represents the perfect situation where it is possible to fully develop

176:  the closure approach.

177: 

178:  When dealing with the interactive view of logic programs, the idea is

179:  that unification is the basic action taking place during

180:  computation, and therefore the observed information must rely on such

181:  an action. We have seen that two kinds of closure can be

182:  distinguished that are dual to each other, namely

183:  \emph{contextualization} and \emph{instantiation}. The former can be

184:  used to embed components in a larger environment, while the latter

185:  serves to specialize an open system to some particular instance.

186: 

187:  We shall concentrate our efforts on \emph{pure} logic

188:  programming (\ie, classical Horn clauses, without any additional

189:  `gadgets'). Hence contextualization corresponds to putting the goal

190:  in conjunction with other goals,\footnote{In pure logic programming,

191:  contextualization does not provide any

192:  additional information on the possible reductions, as the head

193:  of each clause consists of only one predicate. The situation

194:  would be different if generalized multi-head Horn clauses were

195:  considered, a topic that will be discussed in the conclusions, or

196:  if second order logic were considered (other predicate contexts

197:  should be considered beside conjunction).}

198:  \ie, given a goal $G$ we should

199:  put it in the context $\_\wedge G'$ for all possible $G'$.

200:  With respect to instantiation, our proposal is to regard the computed

201:  substitutions for the variables in the (sub)goals as observable

202:  internal contexts, which further instantiate the system

203:  components. Thus, given a goal $G$, we can apply the

204:  substitution $\sigma$ to the free variables of $G$ and study the

205:  consequent changes in the semantics.

206: 

207:  The analogy and distinction between internal and external contexts

208:  become clear if we look at the term algebra over a signature

209:  $\Sigma$ from a categorical perspective: the objects of the category

210:  are underlined natural numbers, an $n$-tuple of terms over $m$

211:  variables corresponds to an arrow from $\underline{m}$ to

212:  $\underline{n}$, and composition of arrows $t_1\from \underline{m}

213:  \to \underline{k}$ and $t_2 \from \underline{k} \to \underline{n}$

214:  is given by substituting the $k$ variables in $t_2$ by the corresponding

215:  terms in the tuple $t_1$. Then, composing to the right means

216:  inserting in a context, while composing to the left means providing

217:  an internal context (\eg, $t_2$ above is external to $t_1$, while

218:  $t_1$ is internal to $t_2$).

219: 

220: \subsubsection*{Tile logic as a semantic framework}

221: 

222:  For pursuing this research programme, we have chosen to rely on

223:  \emph{tile logic} \cite{GM:RRCCS,GM:TM} that can provide a convenient

224:  abstract computational model for logic programming, where many of the

225:  discussed aspects can be suitably represented and managed.

226: 

227:  The tile framework takes inspiration from and bears many analogies

228:  with various \textsc{sos} formats

229:  \cite{Plo:SAOS,DeS:HLSD,BIM:BCBT,GV:SOSBC,Ber:CTSOS},

230:  \emph{context systems} \cite{LX:CTOSC},

231:  \emph{structured transition systems} \cite{CM:ASSTS},

232:  and \emph{rewriting logic} \cite{Mes:CRL}. It allows to define models

233:  that are compositional both in `space' (\ie, according to the

234:  structure of the system) and in `time' (\ie, according to the

235:  computation flow). In particular, tile logic extends rewriting logic

236:  with a built-in mechanism, based on observable effects, for

237:  coordinating local rewrites. The effects are in some sense the

238:  counterparts of labels in \textsc{lts} operational semantics.

239:  However, since tiles

240:  are designed for dealing with open states (as opposed to the ordinary

241:  `ground' view of \textsc{lts}'s generated from \textsc{sos} rules),

242:  they seem more apt for many

243:  applications. The idea is to employ a set of rules (called

244:  \emph{tiles}) to define the behavior of partially specified

245:  components (\ie, components that can contain variables), called

246:  \emph{configurations}, only in terms of the possible interactions

247:  with the internal/external environment.

248:  In this way, the behavior of a system must be

249:  described as a coordinated evolution of its local

250:  subconfigurations. The name `tile' is due to the graphical appearance

251:  of such rules, which have the form in Figure~\ref{atilefig}, also

252:  written $\alpha:\cell{t}{u}{v}{s}$, stating that the \emph{initial

253:  configuration} $t$ evolves to the \emph{final configuration} $s$ via

254:  the tile $\alpha$, producing the \emph{effect} $v$, which can be

255:  observed by the rest of the system, but such a step is allowed only

256:  if the subcomponents of $t$ (\ie, the arguments to which $t$ is

257:  connected via its input interface) evolve to the subcomponents of

258:  $s$, producing the effect $u$, which acts as the \emph{trigger} for

259:  the application of $\alpha$. Triggers and effects are called

260:  \emph{observations} and tile vertices are called

261:  \emph{interfaces}. The arrows $t$, $u$, $v$ and $s$ form the

262:  \emph{border} of $\alpha$.

263: 

264: \begin{figure}[t]

265: \begin{center}

266: $\xymatrix@C=6pc@R+1pc{

267:  *[o]=<.5pc>{\ }\drop\cir{}

268:  \ar[r]^{t}

269:  \ar[d]_{u}

270:  \ar@{}[rd]|{\alpha}

271:  \ar@<2.5pc>@{}[r]|{\mathrm{initial}}

272:  \ar@<1.5pc>@{}[r]|{\mathrm{configuration}}

273:  \ar@<-2.5pc>@{}[d]|{\mbox{trigger}}

274:  \POS[]+<-2pc,2.5pc>\drop{\mathit{initial}}

275:  \POS[]+<-2pc,1.5pc>\drop{\mathit{input}}

276:  \POS[]+<-2pc,.5pc>\drop{\mathit{interface}}

277:  &

278:  *[o]=<.5pc>{\ }\drop\cir{}

279:  \ar[d]^{v}

280:  \ar@<2.5pc>@{}[d]|{\mbox{effect}}

281:  \POS[]+<2pc,2.5pc>\drop{\mathit{initial}}

282:  \POS[]+<2pc,1.5pc>\drop{\mathit{output}}

283:  \POS[]+<2pc,.5pc>\drop{\mathit{interface}}

284:  \\

285:  *[o]=<.5pc>{\ }\drop\cir{}

286:  \ar[r]_{s}

287:  \ar@<-1.5pc>@{}[r]|{\mathrm{final}}

288:  \ar@<-2.5pc>@{}[r]|{\mathrm{configuration}}

289:  \POS[]-<2pc,.5pc>\drop{\mathit{final}}

290:  \POS[]-<2pc,1.5pc>\drop{\mathit{input}}

291:  \POS[]-<2pc,2.5pc>\drop{\mathit{interface}}

292:  &

293:  *[o]=<.5pc>{\ }\drop\cir{}

294:  \POS[]+<2pc,-.5pc>\drop{\mathit{final}}

295:  \POS[]+<2pc,-1.5pc>\drop{\mathit{output}}

296:  \POS[]+<2pc,-2.5pc>\drop{\mathit{interface}}

297: }$

298: \end{center}

299: \caption{A tile.}

300: \protect\label{atilefig}

301: \end{figure}

302: 

303: 

304:  Tiles can be composed horizontally, vertically, and in parallel

305:  to generate larger steps. The three compositions are

306:  illustrated in Figure~\ref{threecomptile}. Horizontal composition

307:  yields rewriting synchronization (\eg, between the evolution of

308:  an argument via $\alpha$ and the evolution of its

309:  environment via $\beta$, as the effect of $\alpha$

310:  provides the trigger for $\beta$). Vertical

311:  composition models the sequential

312:  composition of computations.  The operation of parallel composition

313:  corresponds to building concurrent steps, where two (or more)

314:  disjoint configurations can concurrently evolve. Of course, the

315:  border of a concurrent step is the parallel composition of the

316:  borders of each component of the step.

317: 

318:  Given a set of basic tiles, the associated \emph{tile logic} is

319:  obtained by adding some canonical `auxiliary' tiles and then closing

320:  by (the three kinds of) composition both

321:  auxiliary and basic tiles. As an example, auxiliary tiles may be

322:  introduced that accommodate isomorphic transformations of interfaces,

323:  yielding consistent rearrangements of configurations and observations

324:  \cite{BMM:PTTL,Bru:TL}.

325: 

326: \begin{figure}[t]

327: \begin{center}

328: $\vcenter{\xymatrix@R-1pc@C+1pc{

329:  {\circ} \ar[r] \ar[d] \ar@{}[rd]|{\alpha} &

330:  {\circ} \ar[r] \ar[d] \ar@{}[rd]|{\beta} &

331:  {\circ} \ar[d] \\

332:  {\circ} \ar[r] &

333:  {\circ} \ar[r] &

334:  {\circ} }}$

335: \hfill $\vcenter{\xymatrix@R-1pc@C+1pc{

336:  {\circ} \ar[r] \ar[d] \ar@{}[rd]|{\alpha} &

337:  {\circ} \ar[d] \\

338:  {\circ} \ar[r] \ar[d] \ar@{}[rd]|{\beta} &

339:  {\circ} \ar[d] \\

340:  {\circ} \ar[r] &

341:  {\circ} }}$

342: \hfill $\vcenter{\xymatrix@R-2pc@C-1pc{

343:  & {\circ} \ar[rr] \ar[dd] & &

344:  {\circ} \ar[dd] \\

345:  {\circ} \ar[rr] \ar[dd] & &

346:  {\circ} \ar[dd] \ar@{}[ru]|{\beta} \\ &

347:  {\circ} \ar[rr] & & {\circ} \\

348:  {\circ} \ar[rr] \ar@{}[ru]|{\alpha} &

349:  {\ } &

350:  {\circ} }}$

351: \end{center}

352: \caption{Horizontal, vertical and parallel tile

353: compositions.} \protect\label{threecomptile}

354: \end{figure}

355: 

356:  Tile logic deals with algebraic structures on configurations that can

357:  be different from the ordinary, tree-like presentation of terms

358:  employed in most \textsc{lts}'s. All these structures, ranging from

359:  graphs and term graphs to partitions and relations, give rise to

360:  monoidal categories and, therefore, possess the two basic operations

361:  needed by tile configurations. This is very convenient, as the models

362:  of the logic can be formulated in terms of \emph{monoidal double

363:  categories}. In this paper, we assume the reader to be familiar with

364:  the basic concepts of category theory, though we shall not push their

365:  usage too far (employing categories in a mild way) and shall give

366:  informal explanations of most categorical constructs introduced.

367: 

368:  Likewise context systems \cite{LX:CTOSC} and \emph{conditional

369:  transition systems} \cite{Ren:BOT}, tile logic allows one to reason

370:  about terms with variables \cite{BFMM:BC}. This means, \eg, that

371:  trace semantics and bisimilarity can be extended straightforwardly to

372:  open terms by taking as observation the pair $\langle

373:  \mathit{trigger}, \mathit{effect}\rangle$, whereas ordinary

374:  \textsc{lts}'s deal with transitions from closed terms to closed

375:  terms for which triggers are trivial identities. The compositionality

376:  of abstract semantics (either based on traces or on bisimilarity) can

377:  then be guaranteed by algebraic properties of the tile system or by

378:  suitable specification formats \cite{BFMM:BC}. In particular, we

379:  shall see that the \emph{decomposition property} \cite{GM:TM} yields

380:  a very simple proof of the compositionality of the tile logic

381:  associated to a logic program.

382: 

383: \subsubsection*{The tile approach to logic programming}

384: 

385:  A well-known fact (\cf\ the discussion in Section~\ref{RVPsec}

386:  and \cite{BR:CUA,CM:ASSTS}) that is exploited in the construction we

387:  propose is that in categorical terms the construction of the

388:  \emph{most general unifier} (mgu) between a subgoal and the head

389:  of a clause can be expressed as a \emph{pullback} in the

390:  syntactic category associated to the signature under

391:  consideration. One of the contributions of this paper is in fact

392:  to provide a constructive, modular way of building the pullback

393:  construction. It is similar to the ordinary unification mechanism

394:  but formulated in a completely abstract way by means of

395:  coordination rules. This translates immediately in terms of tile

396:  logic, completing the first part of our research programme, that

397:  is, understanding the extent of interaction we shall observe,

398:  and expressing it in a formal system.

399: 

400:  For the rest, we define a transformation from logic programs to

401:  tile systems by associating a basic tile to each Horn clause in the

402:  program.  Then, the resulting tile models are shown to provide a

403:  computational and semantic framework where the program and its

404:  tile representation yield exactly the same set of computed answer

405:  substitutions for any goal. It is remarkable that all

406:  aspects concerning the control flow are now automatically

407:  handled by tiles (e.g. generation of fresh variables, unification,

408:  construction of resolvents).

409: 

410:  One of the advantages of tile logic is to make evident the duality

411:  between contextualization and instantiation, still being able to deal

412:  in a uniform way with both perspectives. The same thing can be said

413:  for the uniform treatment of configurations and observations that

414:  facilitates the use of contexts as labels, providing many insights on

415:  the way the basic pieces can be put together to form a whole

416:  computation.

417: 

418:  The tile presentation of a program allows us not only to

419:  transfer to logic programming abstract semantic equivalences

420:  based on traces and bisimilarity, but also to show that

421:  these equivalences are compositional (\ie, they are

422:  \emph{congruences}) via an abstract proof based on the

423:  decomposition property of the underlying tile system. More

424:  concretely, denoting by $\sim$ any of the two equivalences (on

425:  goals) mentioned above, we have almost for free that if

426:  $G_1\mathrel{\sim} G_2$, then: (1) $\sigma(G_1) \mathrel{\sim}

427:  \sigma(G_2)$ for any substitution $\sigma$, and (2) $G_1\wedge G

428:  \mathrel{\sim} G_2 \wedge G$ for any goal $G$.

429:  (This lifts also to the case where the simpler `success' semantics

430:  is considered.)

431: 

432:  The application of our `tile' techniques to logic programming can

433:  serve as a basis for establishing useful connections and studying

434:  analogies with the process calculi paradigm. For example,

435:  it comes out that there is a strong resemblance between the

436:  parallel operator of many process calculi and the conjunction

437:  operator on goals. As another example, it would be interesting to

438:  transfer to logic programming concepts like `explicit substitution'

439:  and `term graph', which play important roles in the implementation

440:  of distributed systems.

441: 

442: \subsubsection*{A digression: Sources of inspiration}

443: 

444:  Before illustrating the organization of the material, we want to

445:  explain more precisely the intuition that motivated our research on

446:  interactive semantics for reduction systems and its application to

447:  logic programming.

448:  As already pointed out, our sources of inspiration mostly come

449:  from contributions in the theory of communicating systems.  The

450:  first fact to note is that there are two well recognized and

451:  widely studied schools of thought for giving semantics to

452:  process description calculi, namely via \emph{reduction} rules (especially

453:  popular after Berry and Boudol's \textsc{cham} \cite{BB:CAM})

454:  and via \textsc{lts}'s.

455: 

456:  The first approach relies on the assumption that it is possible to

457:  observe and manipulate the global state of a complex system. In particular,

458:  the current state can be inspected for finding a

459:  \emph{redex}, \ie, a candidate for the application of a reduction step. The

460:  redexes usually coordinate the activity of several logically distinct

461:  components of the system, and therefore, to some extent, the

462:  reduction step synchronizes their local activities into a global

463:  atomic move. For dealing with compositionality, one would

464:  be interested in deriving the semantics of a whole entity in terms of

465:  the semantics of its very basic component parts, which can become a

466:  hard task when reductions are global actions.  The

467:  problem is that a redex may lie in between a component and the

468:  external environment, and therefore to understand the behavior of a

469:  component as a stand alone entity, we have to consider its

470:  interactions with all possible environments, in the style of

471:  \emph{testing semantics} \cite{dNH:TEP}.

472: 

473:  Instead, the point of view of observational equivalences based on

474:  \textsc{lts} semantics is to use \emph{observations} (transition labels)

475:  to derive observational equivalences on processes,

476:  as \eg, \emph{bisimilarity} \cite{Par:CAIS,Mil:CCS}. Moreover, the

477:  formats for specifying \textsc{lts} operational semantics can exploit

478:  inductively the structure of a complex state to define its semantics

479:  in terms of the actions that can be accomplished by

480:  subcomponents, guaranteeing compositionality properties

481:  like `bisimilarity is a congruence.'

482: 

483:  One emerging idea to provide reduction semantics with an

484:  interactive, observational view is that of `observing contexts'

485:  \cite{Mil:PPC,MS:DCPB,Mil:CFI,Ber:CTSOS,Sew:RRBC,LM:DBCRS,CLM:CECAG}.

486:  Basically, starting from a reduction system, one has to define

487:  the semantics of a local component by embedding it in all

488:  possible contexts and by considering those contexts as

489:  observations. Then, when several components are assembled

490:  together, it is possible to predict the semantics of the result

491:  simply by inspecting the behaviors of each component in the

492:  environment contributed by all the remaining components.  This

493:  approach gives rise to a special kind of bisimulation, called

494:  \emph{dynamic bisimilarity} \cite{MS:DCPB}, which is the

495:  coarsest congruence that is also an ordinary bisimulation.

496:  This approach

497:  corresponds to some extent to give the possibility to

498:  dynamically reconfigure the system and has also some

499:  applications to open ended systems \cite{BMS:OES}.

500:  Though theoretically sound, this solution

501:  leaves open many operational questions, because the semantics

502:  must take into account all possible contexts.

503: 

504:  Many people attempt to define a general and clever

505:  methodology for passing from reduction semantics to

506:  (compositional) \textsc{lts} semantics

507:  \cite{Sew:RRBC,LM:DBCRS,CLM:CECAG}. In particular, Leifer and

508:  Milner show in \cite{LM:DBCRS} that a minimal set of contexts

509:  is definable whenever sufficiently many \emph{relative pushouts}

510:  exist in the category of configurations. Roughly speaking, it

511:  must be the case that for any configuration $t$ and any reduction

512:  rule with which $t$ can react in a suitable

513:  environment $C$, then there exists a minimal observable context

514:  $C'$ that makes such reduction possible.

515: 

516:  Dual to the problem of `contextualization' is the problem of

517:  `instantiation.' It arises when one wants to extend the

518:  compositionality from ground processes to open processes.

519:  In fact, the equivalence on open terms is usually defined

520:  via the equivalence on closed terms, by saying that two

521:  contexts are equivalent if their closures

522:  under all possible ground instantiations are so. Again, it is

523:  preferable to avoid the instantiation closure and find a more compact

524:  way to enforce the modularity of the framework. This issue has been

525:  pursued in two recent works \cite{Ren:BOT,BFMM:BC} for providing

526:  general specification formats that guarantee the compositionality of

527:  open systems. They are based on the idea of recording in the

528:  transition labels not only the effects of each move, but also the

529:  triggers provided by the subcomponents for applying the transition to

530:  the global state. Consequently, in the `dynamic' version, instantiation

531:  becomes a sort of `internal contextualization' and

532:  substitutions can be used as labels (in the trigger part).

533: 

534:  In the case of logic programming, many of the above concepts find a

535:  natural meaning. Thus, \eg, goal instantiation

536:  is a relevant internal contextualization that can

537:  modify the semantics of the goal (\eg, by making impossible the

538:  unification with the head of a clause which can otherwise be

539:  applicable), while external contextualization is given by conjunction with

540:  other goals (it can be relevant when multi-headed

541:  clauses are allowed).

542: 

543: \subsubsection*{Structure of the paper}

544: 

545:  We fix the notation and recall the necessary

546:  background in Section~\ref{Bsec}. Due to the heterogeneity of the

547:  material, its presentation is separated in four

548:  parts: Section~\ref{Nsec} summarizes a few elementary

549:  definitions about signatures, substitutions and Horn clauses;

550:  Section~\ref{OSsec} recalls the operational machinery of logic

551:  programming; Section~\ref{TLsec} presents the tile notation and

552:  the categorical models based on double categories;

553:  Section~\ref{ATsec} presents the concepts of Section~\ref{Nsec}

554:  under a different light (exploiting Lawvere's pioneering work

555:  \cite{Law:FSAT}), which will offer a more convenient notation

556:  for representing logic programs in tile logic. While the

557:  contents of Sections~\ref{Nsec} and~\ref{OSsec} are standard,

558:  the notions recalled in Sections~\ref{TLsec} and~\ref{ATsec}

559:  might be not so familiar to the logic programming community.

560: 

561:  In Section~\ref{RVPsec} we recall the ways in which

562:  most general unifiers, equalizers and pullbacks intertwine.

563:  This should provide the

564:  reader with the formal knowledge for understanding the technical

565:  details of the correspondence between unification in logic

566:  programming and coordination via pullback tiles, which is

567:  explained in Section~\ref{DCPsec}. In particular, we think that

568:  the results in Section~\ref{FPPsec} are the key to the

569:  application of tiles to logic programming.

570: 

571:  Section~\ref{TSLPsec} exploits the notation and results from

572:  Section~\ref{DCPsec} to establish the connection between logic

573:  programming and tile logic. The transformation is described in

574:  Section~\ref{FLPTLTsec}, together with a simple example that

575:  illustrates the correspondence between the two views. The main

576:  advantages of the tile approach are examined separately in

577:  Section~\ref{FCTTsec} (connections with ongoing research on process

578:  calculi), Section~\ref{ROSsec} (formal correspondence with ordinary

579:  semantics), Section~\ref{GCsec} (goal compositionality via abstract

580:  congruences), Section~\ref{THREEsec} (comparison between

581:  goal equivalences obtained by considering different instantiation

582:  closures), and in Section~\ref{DTsec} (insights on concurrency and

583:  coordination). The compositionality of the resulting framework

584:  strongly depends on the representation results of

585:  Section~\ref{FPPsec}, that allow one to decompose a complex

586:  coordination along its basic bits.

587: 

588:  While the paper focuses on pure logic programs, we think that the

589:  approach can be extended to take into account many variants of logic

590:  programming. Some of these extensions are discussed in

591:  Section~\ref{CLPsec} (devoted to constraint logic programming)

592:  and in the concluding section.

593: 

594: \section{Background}\label{Bsec}

595: 

596: \subsection{Notation}\label{Nsec}

597: 

598:  Let $\Sigma$ be a two sorted signature over the set of sorts

599:  $\{\mathsf{t},\mathsf{p}\}$. Provided that

600:  the sort $\mathsf{p}$ does not appear in the arity of any

601:  operator, we call $\Sigma$ a \emph{logic

602:  program signature} and we denote by $\Sigma_\Phi =

603:  \bigcup_n\Sigma^n_\Phi$ and $\Sigma_\Pi = \bigcup_n\Sigma^n_\Pi$

604:  the ranked sets of \emph{function symbols} $\dfun

605:  f{\mathsf{t}^n}{\mathsf{t}}$ and of \emph{predicate symbols}

606:  $\dfun p{\mathsf{t}^n}{\mathsf{p}}$, respectively.

607: 

608:  As usual, given a set $X$ of (term) variables, we denote with

609:  $\mathbb{T}_\Sigma(X)$ the free $\Sigma$-algebra generated by $X$.  A {\em

610:  term over} $X$ is an element of $\mathbb{T}_{\Sigma_\Phi}(X)$. The set of all

611:  \emph{ground terms} (\ie, terms without variables) is called the {\em

612:  Herbrand universe for} $\Sigma$. An \emph{atomic formula over} $X$ has

613:  the form $p(t_1,\ldots,t_n)$ where $p\in\Sigma^n_\Pi$ and

614:  $t_1,\ldots,t_n$ are terms over $X$. A \emph{conjunctive formula} is

615:  just a tuple of atomic formulas. The set of all ground atomic

616:  formulas is called the \emph{Herbrand base} for $\Sigma$.

617: 

618:  If $X = \{x_1,\ldots,x_n\}$ and $Y$ are sets of variables, a {\em

619:  substitution from $Y$ to $X$} is a function

620:  $\dfun\sigma{X}{\mathbb{T}_{\Sigma_\Phi}(Y)}$, usually denoted by

621:  $[\sbtn{\sigma(x_1)}{x_1},\ldots,\sbtn{\sigma(x_n)}{x_n}]$.  If $t$

622:  is a term over $X$ and $\sigma$ is a substitution from $Y$

623:  to $X$ then the term over $Y$ obtained by {\em

624:  simultaneously} substituting in $t$ all the occurrences of the

625:  variables in $X$ with their images through $\sigma$ is called the {\em

626:  application of $\sigma$ to $t$} and written $\sigma;t$.

627: 

628:  If $\sigma$ is a substitution from $Y$ to $X$ and $\sigma'$ is a

629:  substitution from $Z$ to $Y$, their \emph{composition} is the

630:  substitution $\sigma';\sigma$ from $Z$ to $X$ defined by applying

631:  $\sigma'$ to each image of the variables in $X$ through $\sigma$.  A

632:  substitution $\sigma$ is said to be \emph{more general} than $\sigma'$

633:  if there exists a substitution $\theta$ such that $\sigma' = \theta;\sigma$.

634:  It is worth noticing that since substitution composition is

635:  associative with the identity substitutions

636:  $[\sbtn{x_1}{x_1},\ldots,\sbtn{x_n}{x_n}]$ as neutral elements, then

637:  substitutions form the arrows of a category having finite sets of

638:  variables as objects.

639: 

640:  Two terms (also atomic formulas) $t$ and $s$ \emph{unify} if there

641:  exists a substitution $\theta$ such that $\theta;t = \theta;s$. In

642:  this case $\theta$ is called a \emph{unifier} of $t$ and $s$. If $t$

643:  and $s$ unify there exists also a \emph{most general unifier} (unique

644:  up to variable renaming), \emph{mgu} for short.

645: 

646:  The mgu can be computed by employing, \eg, the following

647:  (nondeterministic) algorithm that operates on a set of equations (at

648:  the beginning the set is the singleton $\{t=s\}$).

649: 

650: {\em

651: \begin{itemize}

652: \item

653:  Apply one of the following steps until stability is reached:

654:  \begin{enumerate}

655:  \item

656:   eliminate the equation $x=x$ from the set for some variable $x$;

657:  \item

658:   eliminate the equation $f(t_1,\ldots,t_n) = f(s_1,\ldots,s_n)$ from

659:   the set and insert the equations $t_1=s_1$,\ldots,$t_n=s_n$ in it;

660:  \item

661:   if the equation $x=t$ with $x$ a variable not appearing in $t$ is

662:   contained in the current set, apply the substitution $[\sbtn{t}{x}]$

663:   to all the other equations (but do not remove $x=t$).

664:   \end{enumerate}

665: \end{itemize}

666: }

667: 

668:  The algorithm always terminates. It terminates with success if

669:  the resulting set of equations has the form $\{x_1 =

670:  t_1,\ldots,x_n=t_n\}$ with $x_i$ not appearing in $t_j$ for all

671:  $i,j\in [1,n]$. The algorithm can be efficiently computed if it

672:  cyclically executes the sequence of steps

673:  1, 3 (with $x=y$), 2, 3 (with $x=t$).

674: 

675: 

676: \subsection{Syntax and operational semantics of logic programs}\label{OSsec}

677: 

678:  In this section we briefly recall the basics of the operational

679:  semantics of logic programs. We refer to \cite{Llo:FLP} for a more

680:  detailed introduction to the subject.

681: 

682:  A \emph{definite Horn clause} $c$ is an expression of the form

683: 

684: \[H \mathrel{:-} B_1,\ldots,B_n\]

685: 

686: \noindent

687:  with $n\geq 0$, where $H$ is an atomic formula called

688:  the \emph{head} of $c$ and $\langle B_1,\ldots,B_n\rangle$ is a

689:  (conjunctive) formula called the \emph{body} of $c$.

690:  A logic program $\mathcal{P}$ is a finite collection of clauses

691:  $\{c_1,\ldots,c_m\}$.

692: 

693:  A \emph{goal} is an expression of the form

694: 

695: \[\mathrel{?-} A_1,\ldots,A_k\]

696: 

697: \noindent

698:  with $k\geq 0$, where $G \mathrel{\equiv} \langle

699:  A_1,\ldots,A_k\rangle$ is a (conjunctive) formula and the $A_i$'s are

700:  the \emph{atomic subgoals} of $G$. If $k=0$, then $G$ is called the

701:  \emph{empty goal} and is denoted by `$\Box$.'

702: 

703:  Given a goal $G \mathrel{\equiv} \langle A_1,\ldots,A_k\rangle$ and a

704:  clause $c\equiv H \mathrel{:-} B_1,\ldots,B_n$ (with all variables in the

705:  latter possibly renamed to avoid confusion with those in $G$) an

706:  \emph{(SLD)-resolution step} involves the selection of an atomic goal

707:  $A_i$ such that $H$ and $A_i$ unify and the construction of their mgu

708:  $\theta$. The step leads to a new goal

709: 

710: \begin{eqnarray*}

711:  G'

712:  & \mathrel{\equiv} &

713:  \theta;\langle A_1,\ldots,A_{i-1},

714:                 B_1,\ldots,B_n,

715:                 A_{i+1},\ldots,A_k\rangle \\

716:  & \mathrel{\equiv} &

717:                 \theta;A_1,\ldots,\theta;A_{i-1},

718:                 \theta;B_1,\ldots,\theta;B_n,

719:                 \theta;A_{i+1},\ldots,\theta;A_k

720: \end{eqnarray*}

721: 

722: \noindent

723:  which is called the \emph{resolvent} of $G$ and $c$. In this case we

724:  say that $G'$ is \emph{derived from $G$ and $c$ via $\theta$} and we

725:  write $G\Rightarrow_{c,\theta} G'$ or simply $G\Rightarrow_{\theta}

726:  G'$.

727: 

728:  Given a logic program $\mathcal{P} = \{c_1,\ldots,c_m\}$ and a goal

729:  $G_0$, an {\em (SLD-)derivation} of $G_0$ in $\mathcal{P}$ is a

730:  (finite or infinite) sequence $G^0,G^1,G^2,\ldots$ of goals, a

731:  sequence $c_{i_1},c_{i_2},\ldots$ of (renamed) clauses and a sequence

732:  $\theta_1,\theta_2,\ldots$ of mgu's such that $G^{i+1}$ is derived

733:  from $G^i$ and $c_{j_i}$ via $\theta_{i}$.  An

734:  \emph{(SLD-)refutation} of $G_0$ is a finite derivation of $G_0$

735:  ending with the empty goal. In this case the substitution $\theta =

736:  (\theta_l;\cdots;\theta_1)_{\mid Var(G)}$ is called a {\em computed

737:  answer substitution} for $G$, written $G\Rightarrow^*_\theta

738:  \Box$. The `small-step' operational semantics is formalized in

739:  Table~\ref{smcasruletab} (but in the rule for atomic goal we must be

740:  certain that $\rho$ renames the variables in the clause by globally

741:  fresh names).

742: 

743: \begin{table}

744: \caption{Operational rules for SLD-resolution (small step

745: semantics).} \protect\label{smcasruletab}

746: \begin{tabular}{ccl}

747: \hline \hline

748:  $\irule{}

749:         {\mathcal{P}\vvdash \Box,G\Rightarrow_{id} G}\ \ \

750:   \irule{}

751:         {\mathcal{P}\vvdash G,\Box\Rightarrow_{id} G}$ & & empty goal \\

752: \\

753:  $\irule{(H \mathrel{:-} F) \in \mathcal{P}\ \

754:          \sigma = \mathrm{mgu}(A,\rho;H)}

755:         {\mathcal{P}\vvdash A\Rightarrow_{\sigma}

756:                             \sigma;\rho;F}$ & & atomic goal \\

757: \\

758:  $\irule{\mathcal{P}\vvdash G\Rightarrow_{\sigma}F}

759:         {\mathcal{P}\vvdash G,G'\Rightarrow_{\sigma}

760:                             F,(\sigma;G')}\ \ \

761:   \irule{\mathcal{P}\vvdash G\Rightarrow_{\sigma}F}

762:         {\mathcal{P}\vvdash G',G\Rightarrow_{\sigma}

763:                             (\sigma;G'),F}$ & & conjunctive goal \\

764: \hline \hline

765: \end{tabular}

766: \end{table}

767: 

768:  The inductive definition of computed answer substitution and

769:  refutation in the `big-step' style is given by the rules in

770:  Table~\ref{casruletab}. The notation $\mathcal{P}\vdash_{\theta} G$

771:  means that $\mathcal{P}\vvdash G \Rightarrow^*_\theta \Box$, \ie,

772:  that the goal $G$ can be refuted by using clauses in the program

773:  $\mathcal{P}$. The first rule says that the empty goal can always be

774:  refuted with the empty computed answer substitution $\epsilon$. The

775:  second clause says that an atomic goal can be refuted provided that

776:  it can be unified with the head $H$ of a clause (suitably renamed by

777:  $\rho$ to avoid name conflicts with $A$) in the program $\mathcal{P}$

778:  via the mgu $\sigma$ and that the goal obtained by applying $\sigma$

779:  to the (renamed) body $F$ of the clause can be refuted with $\theta$.

780:  The third rule says that a conjunctive goal can be refuted provided

781:  that its leftmost subgoal can be refuted first with $\sigma$, and

782:  then the goal obtained by applying $\sigma$ to the other subgoals can

783:  be refuted with $\theta$. Although imposing a sequentialization in

784:  the resolution process can appear as an arbitrary choice, the fact

785:  that refutation involves finite derivations and the well known

786:  switching lemma guarantee the completeness of the formal system.

787: 

788: \begin{table}

789: \caption{Operational rules for SLD-resolution (big step

790: semantics).} \protect\label{casruletab}

791: \begin{tabular}{rcl}

792: \hline \hline

793:  $\irule{}{\mathcal{P}\vdash_{\epsilon} \Box}$ & & empty goal \\

794: \\

795:  $\irule{(H \mathrel{:-} F) \in \mathcal{P}\ \

796:          \sigma = \mathrm{mgu}(A,\rho;H)\ \

797:          \mathcal{P}\vdash_{\theta} \sigma;\rho;F}

798:         {\mathcal{P}\vdash_{\theta;\sigma} A}$ & & atomic goal \\

799: \\

800:  $\irule{\mathcal{P}\vdash_{\sigma} A\ \

801:          \mathcal{P}\vdash_{\theta} \sigma;F}

802:         {\mathcal{P}\vdash_{\theta;\sigma} A,F}$ & & conjunctive goal \\

803: \hline \hline

804: \end{tabular}

805: \end{table}

806: 

807: \subsection{Double categories and tile logic}\label{TLsec}

808: 

809:  The point of view of tile logic \cite{GM:TM,Bru:TL} is that the

810:  dynamics of a complex system can be better understood if we reason in

811:  terms of its basic components and of the interactions between

812:  them. Therefore, reductions must carry observable information about

813:  the triggers and the effects of the local step. This extends the

814:  point of view of rewriting logic, where reductions can be freely

815:  nested inside any context (and also freely instantiated): In tile

816:  logic, contextualization and instantiation are subordinated to the

817:  synchronization of the arguments with the environment, \ie, the

818:  effect of the tile defining the evolution of the former must provide

819:  the trigger for the evolution of the second. When the coordination is

820:  not possible, then the step cannot be performed.

821: 

822:  An abstract account of the connections between states and

823:  dynamics can be given via (monoidal) \emph{double

824:  categories}, by exploiting their two-fold representation: one

825:  dimension is for composing states and the second dimension is

826:  for composing computations. In fact, the models of tile logic are

827:  suitable double categories \cite{GM:TM,BMM:SMCDC}, and the basic

828:  tiles of a tile system provide a finitary presentation ---

829:  which is more convenient to work with --- of the initial model.

830: 

831:  Since we do not want to introduce unnecessary complexity overhead to

832:  readers not acquainted with double categories, we will present a

833:  gentle introduction to the subject. For more details we refer to

834:  \cite{Ehr:CS,Ehr:CS2,MM:TLRL,BMM:PTTL,BMM:SMCDC}.

835: 

836:  A double category contains two categorical structures, called

837:  \emph{horizontal} and \emph{vertical} respectively, defined over the

838:  same set of cells. More precisely, double categories admit the

839:  following na\"\i ve definition.

840: 

841: \begin{figure}[t]

842: \begin{center}

843: $\xymatrix{

844:  {o_0} \ar [r]^{h_0} \ar @{} [dr]|{A} \ar [d]_{v_0} &

845:  {o_1} \ar [d]^{v_1} \\

846:  {o_2} \ar [r]_{h_1} &

847:  {o_3} }$

848: \end{center}

849: \caption{Graphical representation of a cell.}

850: \protect\label{defcell}

851: \end{figure}

852: 

853: 

854: \begin{definition}[Double Category]\label{doubcat}

855:  A \emph{double category} $\mathcal{D}$ consists of a collection

856:  $o,o_0,o',\ldots$ of \emph{objects}, a collection $h,h_0,h',\ldots$

857:  of \emph{horizontal arrows}, a collection $v,v_0,v',\ldots$ of

858:  \emph{vertical arrows} and a collection $A,B,C,\ldots$ of

859:  \emph{double cells} (also called \emph{cells}, for short).

860: 

861: \begin{itemize}

862: \item

863:  Objects and horizontal arrows form the \emph{horizontal 1-category}

864:  $\mathcal{H}$, with identity $id_o$ for each object $o$, and

865:  composition $\_*\_$.

866: 

867: \item

868:  Objects and vertical arrows form also a category, called the

869:  \emph{vertical 1-category} $\mathcal{V}$, with identity $id_o$ for

870:  each object $o$, and composition $\_\cdot\_$.

871: 

872: \item

873:  Cells are assigned \emph{horizontal source} and \emph{target} (which

874:  are vertical arrows) and \emph{vertical source} and \emph{target}

875:  (which are horizontal arrows); furthermore sources and targets must

876:  be \emph{compatible}, in the sense that they must satisfy the

877:  equalities on source and target objects graphically represented by

878:  the square-shaped diagram in Figure~\ref{defcell}, for which we use

879:  the notation $A:\cell{h_0}{v_0}{v_1}{h_1}$.

880: 

881: \item

882:  Cells can be composed both horizontally ($\_*\_$) and vertically

883:  ($\_\cdot\_$) as follows: given $A:\cell{h_0}{v_0}{v_1}{h_1}$,

884:  $B:\cell{h_2}{v_1}{v_2}{h_3}$, and

885:  $C:\cell{h_1}{v_3}{v_4}{h_4}$, then $A *

886:  B:\cell{h_0*h_2}{v_0}{v_2}{h_1*h_3}$, and $A\cdot

887:  C:\cell{h_0}{v_0\cdot v_3}{v_1\cdot v_4}{h_4}$ are cells.

888:  Moreover, given a fourth cell $D:\cell{h_3}{v_4}{v_5}{h_5}$,

889:  horizontal and vertical compositions satisfy the following

890:  \emph{exchange law} (see Figure~\ref{exchlawfig}):

891: 

892: \[

893:  (A\cdot C) * (B\cdot D) = (A * B)\cdot(C * D)

894: \]

895: 

896: \noindent

897:  Under these rules, cells form both a horizontal category ${\cal D}^*$

898:  and a vertical category ${\cal D}^{\cdot}$, with identities

899:  $1_{v}:\cell{id_o}{v}{v}{id_{o'}}$ and

900:  $1^{h}:\cell{h}{id_o}{id_{o'}}{h}$, respectively, with $1^{h_0*h_1} =

901:  1^{h_0} * 1^{h_1}$ and $1_{v_0\cdot v_1} = 1_{v_0} \cdot 1_{v_1}$.

902: 

903: \item

904:  Furthermore, horizontal and vertical identities of identities

905:  coincide, \ie, $1_{id_o} = 1^{id_o}$ and the cell is simply denoted

906:  by $1_o$.

907: \end{itemize}

908: \end{definition}

909: 

910: \begin{figure}

911: \begin{center}

912: $\xymatrix@+1pc{

913:  {\cdot} \ar[r]^{h_0} \ar[d]_{v_0} \ar@{}[rd]|{A} &

914:  {\cdot} \ar[r]^{h_2} \ar[d]|{v_1} \ar@{}[rd]|{B} &

915:  {\cdot} \ar[d]^{v_2} \\

916:  {\cdot} \ar[r]|{h_1} \ar[d]_{v_3} \ar@{}[rd]|{C} &

917:  {\cdot} \ar[r]|{h_3} \ar[d]|{v_4} \ar@{}[rd]|{D} &

918:  {\cdot} \ar[d]^{v_5} \\

919:  {\cdot} \ar[r]_{h_4} &

920:  {\cdot} \ar[r]_{h_5} &

921:  {\cdot} }$

922: \end{center}

923: \caption{Exchange law of double categories.}

924: \protect\label{exchlawfig}

925: \end{figure}

926: 

927:  We shall use monoidal categories (see \eg, \cite{Mac:CWM} for

928:  basic definitions) for horizontal and vertical 1-categories.

929:  As a matter of notation,

930:  sequential composition and monoidal tensor product on 1-categories are denoted

931:  by $\_;\_$ and $\_\otimes\_$, respectively. A \emph{monoidal double

932:  category} is a double category together with an associative

933:  tensor product $\_\otimes\_$ and a unit element $e$.

934: 

935:  Tile logic gives a computational interpretation of (monoidal) double

936:  categories, where (see Figure~\ref{atilefig} for terminology):

937: 

938: \begin{itemize}

939: \item

940:  the objects represent the (initial/final, input/output) interfaces

941:  through which system components can be connected;

942: 

943: \item

944:  the arrows of $\mathcal{H}$ describe (initial/final) configurations,

945:  sources and targets corresponding to input and output interfaces;

946: 

947: \item

948:  the arrows of $\mathcal{V}$ are the observations (trigger/effect),

949:  sources and targets corresponding to initial and final interfaces;

950: 

951: \item

952:  the cells represent the possible transformations (tiles) that can be

953:  performed by the system.

954: \end{itemize}

955: 

956:  Thus, a cell $\cell{h_0}{v_0}{v_1}{h_1}$ says that the state

957:  $h_0$ can evolve to $h_1$ via an action triggered by $v_0$ and

958:  with effect $v_1$. The way in which observations and

959:  configurations of a cell are connected via their interfaces

960:  expresses the locality of actions, \ie, the places where triggers

961:  are applied to and effects are produced by.

962: 

963:  A basic distinction concerns whether one is interested in the

964:  cells or just in their borders. The second alternative has a

965:  more abstract flavor, in  line with behavioral equivalences, and

966:  corresponds to the so called \emph{flat tile logic} \cite{Bru:TL}.

967:  In this paper we shall concentrate on flat tiles only.

968: 

969:  Tile logic gives also the possibility of presenting in a constructive

970:  way the double category of interest. This is in some sense analogous

971:  to presenting a term algebra by giving only the signature: A standard

972:  set of rules tells how to build all the elements starting from the

973:  basic ones. For tile logic, the basic elements consist of: (i) the

974:  category $\mathcal{H}$ of configurations; (ii) the category

975:  $\mathcal{V}$ of observations; and (iii) the set of basic tiles (\ie,

976:  cells on $\mathcal{H}$ and $\mathcal{V}$). Starting from basic

977:  tiles, more complex tiles can be constructed by means of horizontal,

978:  vertical and parallel composition.  Moreover, the horizontal and

979:  vertical identities are always added and composed together with the

980:  basic tiles. All this is illustrated by the rules in

981:  Figure~\ref{comptilefig}, where tiles are seen as logic sequents. As

982:  explained in the Introduction, each operation has a precise

983:  computational meaning: horizontal composition coordinates the

984:  evolution of a context with that of its arguments; parallel

985:  composition models concurrent activities; vertical composition

986:  appends steps to computations. For both terms and tiles, the

987:  operation of building all the elements starting from the basic ones

988:  can be represented by a universal construction corresponding to a

989:  left adjoint.

990: 

991: \begin{figure}[t]

992: \begin{center}

993:  $\irule{\cell{t_0}{u}{v}{s_0}\ \ \cell{t_1}{v}{w}{s_1}}

994:         {\cell{t_0;t_1}{u}{w}{s_0;s_1}}$

995: \hfill

996:  $\irule{\cell{t}{u_0}{v_0}{s}\ \ \cell{s}{u_1}{v_1}{r}}

997:         {\cell{t}{u_0;u_1}{v_0;v_1}{r}}$

998: \hfill

999:  $\irule{\cell{t_0}{u_0}{v_0}{s_0}\ \ \cell{t_1}{u_1}{v_1}{s_1}}

1000:         {\cell{t_0\otimes t_1}{u_0\otimes u_1}{v_0\otimes v_1}{s_0\otimes s_1}}$

1001: \hfill $\irule{t\from o_0\to o_1\in \mathcal{H}}

1002:         {\cell{t}{o_0}{o_1}{t}}$

1003: \hfill $\irule{u\from o_0\to o_1\in \mathcal{V}}

1004:         {\cell{o_0}{u}{u}{o_1}}$

1005: \end{center}

1006: \caption{Composition and identity rules for tile logic.}

1007: \protect\label{comptilefig}

1008: \end{figure}

1009: 

1010: \begin{definition}[Tile system]

1011:  A \emph{tile system} is a tuple $\mathcal{R} =

1012:  (\mathcal{H},\mathcal{V},N,R)$ where $\mathcal{H}$ and

1013:  $\mathcal{V}$ are monoidal categories with the same set of

1014:  objects $\mathbf{O}_{\mathcal{H}} = \mathbf{O}_{\mathcal{V}}$,

1015:  $N$ is the set of rule names and $R\from N \to

1016:  \mathbf{A}_{\mathcal{H}} \times \mathbf{A}_{\mathcal{V}} \times

1017:  \mathbf{A}_{\mathcal{V}} \times \mathbf{A}_{\mathcal{H}}$ is a

1018:  function such that for all $\alpha\in N$, if $R(\alpha)=\langle

1019:  t,u,v,s\rangle$ then $t\from o_0\to o_1$, $u\from o_0\to o_2$, $v\from

1020:  o_1\to o_3$, and $s\from o_2\to o_3$ for suitable objects $o_0$, $o_1$, $o_2$

1021:  and $o_3$ (see Figure~\ref{gentilefig}).  We will denote such rule

1022:  by writing $\alpha\from \cell{t}{u}{v}{s}$.

1023: \end{definition}

1024: 

1025: \begin{figure}[t]

1026: \begin{center}

1027: $\xymatrix@R-1pc@C+1pc{

1028:  {o_0} \ar[r]^{t} \ar[d]_{u} \ar@{}[rd]|{\alpha} &

1029:  {o_1} \ar[d]^{v} \\

1030:  {o_2} \ar[r]_{s} &

1031:  {o_3} }$

1032: \end{center}

1033: \caption{A generic tile $\alpha$.}

1034: \protect\label{gentilefig}

1035: \end{figure}

1036: 

1037:  Depending on the chosen tile format, $\mathcal{H}$ and

1038:  $\mathcal{V}$ can be specialized (\eg, to cartesian categories)

1039:  and suitable \emph{auxiliary tiles} are added and composed with

1040:  basic tiles and identities in all the possible ways. The set of

1041:  resulting sequents (\emph{flat tiles}) define the \emph{flat

1042:  tile logic} associated to $\mathcal{R}$. We say that

1043:  $\cell{t}{u}{v}{s}$ is \emph{entailed} by the logic, written

1044:  $\mathcal{R}\vdash\cell{t}{u}{v}{s}$, if the sequent

1045:  $\cell{t}{u}{v}{s}$ can be expressed as the composition of basic

1046:  and auxiliary tiles. Flat tiles form the cells of a suitable

1047:  double category, which is freely generated by the tile system.

1048: 

1049:  Being interested in tile systems where configurations and

1050:  observations are freely generated by suitable horizontal and

1051:  vertical signatures, in what follows we shall present tile systems as

1052:  tuples of the form $\mathcal{R}=(\Sigma,\Lambda,N,R)$. In particular,

1053:  we shall employ categories of substitutions on $\Sigma$ and $\Lambda$

1054:  as horizontal and vertical 1-categories. In the literature several

1055:  tile formats have been considered

1056:  \cite{GM:TM,FM:TFLMS,BMM:ETS,BM:CCDC,BFMM:BC}. They are all based on

1057:  the idea of having as underlying categories of configurations and

1058:  effects two categories that are freely generated starting from

1059:  suitable (hyper)signatures whose operators model the basic components

1060:  and observations, respectively.

1061:  Varying the algebraic structure of configurations and observations,

1062:  tiles can model many different aspects of dynamic systems,

1063:  ranging \eg

1064:  from synchronization of Petri net transitions \cite{BM:ZSNCCI}, to causal

1065:  dependencies for located calculi and finitely branching approaches

1066:  for name-passing calculi \cite{FM:TFLMS}, to actor systems

1067:  \cite{MT:APA}, names abstraction and creation and higher order

1068:  structures \cite{BM:CCDC}.

1069:  A comparison between the

1070:  various formats is out of the scope of this presentation and can be

1071:  found in \cite{BFMM:BC}.

1072: 

1073:  Ordinary trace semantics and bisimilarity semantics can be

1074:  extended to tiles by considering the transition system whose

1075:  states are (possibly open) configurations and whose transitions

1076:  are the entailed tile sequents: a tile $\cell{t}{u}{v}{s}$

1077:  defines a transition from $t$ to $s$ with label $(u,v)$. An

1078:  interesting question concerns suitable conditions under which

1079:  such abstract equivalences yield congruences (\wrt\ the

1080:  operations of the underlying horizontal structure). \emph{Tile

1081:  decomposition} is one such condition that has a completely

1082:  abstract formulation applicable to all tile systems.

1083: 

1084: \begin{definition}

1085:   A tile system $\mathcal{R} = (\mathcal{H},\mathcal{V},N,R)$

1086:   enjoys the \emph{decomposition property} if for all arrows

1087:   $t \in \mathcal{H}$ and for all sequents

1088:   $\cell{t}{u}{v}{s}$ entailed by~$\mathcal{R}$, then:

1089:   (1)

1090:   if $t = t_1;t_2$ then $\exists w\in\mathcal{V}$,

1091:   $s_1,s_2\in\mathcal{H}$ such that $\mathcal{R}\vdash

1092:   \cell{t_1}{u}{w}{s_1}$, $\mathcal{R}\vdash

1093:   \cell{t_2}{w}{v}{s_2}$ and $s=s_1;s_2$;

1094:   (2) if $t = t_1\otimes t_2$ then

1095:   $\exists u_1,u_2,v_1,v_2\in\mathcal{V}$, $s_1,s_2\in\mathcal{H}$ such

1096:   that $\mathcal{R}\vdash \cell{t_1}{u_1}{v_1}{s_1}$,

1097:   $\mathcal{R}\vdash \cell{t_2}{u_2}{v_2}{s_2}$, $u=u_1\otimes

1098:   u_2$, $v=v_1\otimes v_2$ and $s=s_1\otimes s_2$.

1099: \end{definition}

1100: 

1101:  Condition (1) is called \emph{sequential decomposition} and condition

1102:  (2) is called \emph{parallel decomposition}.  The decomposition property

1103:  characterizes compositionality: It amounts to saying that if a system

1104:  $t$ can undergo a transition $\alpha$, then for every subsystem $t_1$

1105:  of $t$ there exists some transition $\alpha'$, such that $\alpha$ can

1106:  be obtained by composing $\alpha'$ with a transition of the rest.

1107: 

1108: \begin{proposition}[cf.~\cite{GM:TM}]\label{decascongprop}

1109:   If $\mathcal{R}$ enjoys the decomposition property, then tile

1110:   bisimilarity (and also tile trace equivalence) are congruences.

1111: \end{proposition}

1112: 

1113:  When only instantiation/contextualization are considered as

1114:  meaningful operations of the system, then sequential decomposition is

1115:  enough for guaranteeing the congruence of tile bisimilarity and tile

1116:  trace equivalence \wrt\ these closure operations.

1117: 

1118: \subsection{Algebraic theories}\label{ATsec}

1119: 

1120:  An alternative presentation of the category of substitutions

1121:  discussed in Section~\ref{Nsec} can be obtained resorting to

1122:  \emph{algebraic theories} \cite{Law:FSAT}.

1123: 

1124: \begin{remark}

1125:  For simplicity we illustrate here the constructions for one-sorted

1126:  signatures. This can be extended to many sorted signatures by

1127:  considering the free strict monoid on the set of sorts (\eg, strings

1128:  of sorts) in place of underlined natural numbers.

1129: \end{remark}

1130: 

1131: \begin{definition}[Algebraic theory]

1132:  The free algebraic theory associated to a signature $\Sigma$ is the

1133:  category $\textbf{Th}[\Sigma]$ defined below:

1134: \begin{itemize}

1135: \item

1136:  its objects are `underlined' natural numbers;

1137: \item

1138:  the arrows from $\underline{m}$ to $\underline{n}$ are $n$-tuples of

1139:  terms in the free $\Sigma$-algebra with (at most) $m$ canonical

1140:  variables, and composition of arrows is term substitution. The arrows

1141:  of $\textbf{Th}[\Sigma]$ are generated from $\Sigma$ by the inference

1142:  rules in Figure~\ref{ThSigmafig}, modulo the axioms in

1143:  Table~\ref{ThSigmatab}.

1144: \end{itemize}

1145: \end{definition}

1146: 

1147:  The category $\textbf{Th}[\Sigma]$ is isomorphic to the

1148:  category of finite substitutions on $\Sigma$ (with canonical sets of

1149:  variables), and the arrows from $\underline{0}$ to

1150:  $\underline{1}$ are in bijective correspondence with the closed terms

1151:  over $\Sigma$.

1152: 

1153:  An object $\underline{n}$ (interface) can be thought of as

1154:  representing the $n$ (ordered) canonical variables

1155:  $x_1,\ldots,x_n$. This allows us to denote

1156:  $[\sbtn{t_1}{x_1},\ldots,\sbtn{t_n}{x_n}]$ just by the tuple $\langle

1157:  t_1,\ldots,t_n\rangle$, since a standard naming of substituted

1158:  variables can be assumed. We omit angle brackets if no confusion can

1159:  arise.

1160: 

1161: \begin{remark}

1162:  To avoid confusion, it must be clear that the canonical variables are

1163:  just placeholders, \ie, their scope is only local. For example in

1164:  $[\sbtn{f(x_1)}{x_1}]$ the two $x_1$ are different, while in

1165:  $[\sbtn{f(x_1)}{x_1},\sbtn{g(x_1)}{x_2}]$ only the two occurrences of

1166:  $x_1$ in $f(x_1)$ and $g(x_1)$ refer to the same placeholder. Note that

1167:  $[\sbtn{f(x_1)}{x_1},\sbtn{g(x_2)}{x_1}]$ is inconsistent (because

1168:  $x_1$ is assigned twice) and in fact cannot be expressed in the

1169:  language.

1170: \end{remark}

1171: 

1172:  The rule $\mathtt{op}$ defines basic substitutions

1173:  $[\sbtn{f(x_1,\ldots,x_n)}{x_1}] = f(x_1,\ldots,x_n)$ for all

1174:  $f\in\Sigma_n$.  The rule $\mathtt{id}$ yields identity substitutions

1175:  $\langle x_1,\ldots,x_n\rangle$. The rule $\mathtt{seq}$ represents

1176:  application of $\alpha$ to $\beta$. The rule $\mathtt{mon}$ composes

1177:  substitutions in parallel (in $\alpha\otimes\beta$, $\alpha$ goes

1178:  from $x_1,\ldots,x_n$ to $x_1,\ldots,x_m$, while $\beta$ goes from

1179:  $x_{n+1},\ldots,x_{n+k}$ to $x_{m+1},\ldots,x_{m+l}$).  Three

1180:  `auxiliary' operators (\ie, not dependent on $\Sigma$) are introduced

1181:  that recover the cartesian structure (rules $\mathtt{sym}$,

1182:  $\mathtt{dup}$ and $\mathtt{dis}$). The \emph{symmetry}

1183:  $\gamma_{\underline{n},\underline{m}}$ is the permutation $\langle

1184:  x_{n+1},\ldots,x_{n+m}, x_1,\ldots,x_n\rangle$. The \emph{duplicator}

1185:  $\nabla_{\underline{n}} = \langle x_1,\ldots,x_n,x_1,\ldots,x_n

1186:  \rangle$ introduces sharing and hence nonlinear substitutions.  The

1187:  \emph{discharger} $!_{\underline{n}}$ is the empty substitution on

1188:  $x_1,\ldots,x_n$, recovering cartesian projections.

1189: 

1190: \begin{figure}[t]

1191: \begin{center}

1192: $\mathtt{op}\ \

1193:   \irule{f\in\Sigma_n}

1194:         {f \from \underline{n} \to \underline{1}}

1195: \hfill

1196:   \mathtt{id}\ \

1197:   \irule{n\in\nat}

1198:         {id_{\underline{n}}\from \underline{n} \to \underline{n}}

1199: \hfill

1200:   \mathtt{seq}\ \

1201:   \irule{\alpha \from \underline{n} \to \underline{m}\ \ \

1202:          \beta \from \underline{m} \to \underline{k}}

1203:         {\alpha;\beta \from \underline{n} \to \underline{k}}

1204: \hfill

1205:   \mathtt{mon}\ \

1206:   \irule{\alpha \from \underline{n} \to \underline{m}\ \ \

1207:          \beta \from \underline{k} \to \underline{l}}

1208:         {\alpha\otimes\beta \from \underline{n+k} \to \underline{m+l}}$

1209: \end{center}

1210: \begin{center}

1211: $\mathtt{sym}\ \

1212:   \irule{n,m\in\nat}

1213:         {\gamma_{\underline{n},\underline{m}}\from \underline{n+m} \to

1214: \underline{m+n}}

1215: \hfill

1216:   \mathtt{dup}\ \

1217:   \irule{n\in\nat}

1218:         {\nabla_{\underline{n}}\from \underline{n} \to \underline{n+n}}

1219: \hfill

1220:   \mathtt{dis}\ \

1221:   \irule{n\in\nat}

1222:         {!_{\underline{n}}\from \underline{n} \to \underline{0}}$

1223: \end{center}

1224: \caption{The inference rules for the generation of $\textbf{Th}[\Sigma]$.}

1225: \protect\label{ThSigmafig}

1226: \end{figure}

1227: 

1228:  Let us briefly comment on the axiomatization in

1229:  Table~\ref{ThSigmatab}. The first two rows say that

1230:  $\textbf{Th}[\Sigma]$ is a strict monoidal category, with tensor

1231:  product $\otimes$ and neutral element $id_{\underline{0}}$. The third

1232:  row and the naturality axiom for symmetries (first axiom of the last

1233:  row) say that $\textbf{Th}[\Sigma]$ is also symmetric. In particular,

1234:  the axioms in the third row state the coherence of symmetries

1235:  $\gamma_{\underline{n},\underline{m}}$, namely that all the

1236:  equivalent ways of swapping the first $n$ variables with the

1237:  following $m$ variables built out of the basic symmetry

1238:  $\gamma_{\underline{1},\underline{1}}$ (that swaps two adjacent

1239:  variables) are identified. The axioms in the fourth row accomplish a

1240:  similar task for duplicators, and those in the fifth row for

1241:  dischargers. The naturality of duplicators and dischargers (second

1242:  and third axioms of the last row) makes $\textbf{Th}[\Sigma]$

1243:  cartesian.

1244: 

1245: \begin{table}[t]

1246: \begin{center}

1247: \caption{Axiomatization of $\textbf{Th}[\Sigma]$.}

1248: \protect\label{ThSigmatab}

1249: \footnotesize

1250: \begin{tabular}{llcr}

1251: \hline

1252: \hline

1253:   category &

1254:   $\alpha;(\beta;\delta) = (\alpha;\beta);\delta$ & &

1255:   $\alpha;id_{\underline{m}} = \alpha = id_{\underline{n}};\alpha$ \\

1256: \\

1257:   tensor &

1258:   $(\alpha;\alpha')\otimes(\beta;\beta') =

1259:    (\alpha\otimes\beta);(\alpha'\otimes\beta')$ & &

1260:   $id_{\underline{n+m}} = id_{\underline{n}}\otimes id_{\underline{m}}$ \\

1261:   product &

1262:   $\alpha\otimes(\beta\otimes\delta) = (\alpha\otimes\beta)\otimes\delta$ & &

1263:   $\alpha\otimes id_{\underline{0}} = \alpha =

1264:    id_{\underline{0}}\otimes\alpha$ \\

1265: \\

1266:   symmetries &

1267:   $\gamma_{\underline{n},\underline{m+k}} =

1268:     (\gamma_{\underline{n},\underline{m}}\otimes

1269:     id_{\underline{k}});(id_{\underline{m}}\otimes

1270:     \gamma_{\underline{n},\underline{k}})$ &

1271:   $\gamma_{\underline{n},\underline{0}} = id_{\underline{n}}$ &

1272:   $\gamma_{\underline{n},\underline{m}};

1273:    \gamma_{\underline{m},\underline{n}} = id_{\underline{n+m}}$ \\

1274: \\

1275:   duplicators &

1276:   $\nabla_{\underline{n+m}} = (\nabla_{\underline{n}}\otimes

1277:    \nabla_{\underline{m}});(id_{\underline{n}}\otimes

1278:    \gamma_{\underline{n},\underline{m}} \otimes id_{\underline{m}})$ & &

1279:   $\nabla_{\underline{0}} = id_{\underline{0}}$ \\

1280:   & $\nabla_{\underline{n}};(id_{\underline{n}}\otimes\nabla_{\underline{n}})

1281:     = \nabla_{\underline{n}};(\nabla_{\underline{n}}\otimes

1282:     id_{\underline{n}})$ & &

1283:   $\nabla_{\underline{n}};\gamma_{\underline{n},\underline{n}} =

1284: \nabla_{\underline{n}}$ \\

1285: \\

1286:   discharger &

1287:   $!_{\underline{n+m}} = !_{\underline{n}} \otimes !_{\underline{m}}$ &

1288:   $!_{\underline{0}} = id_{\underline{0}}$ &

1289:   $\nabla_{\underline{n}};(id_{\underline{n}}\otimes

1290:    !_{\underline{n}}) = id_{\underline{n}}$ \\

1291: \\

1292:   naturality &

1293:   $(\alpha\otimes\beta);\gamma_{\underline{m},\underline{l}} =

1294:    \gamma_{\underline{n},\underline{k}};(\beta\otimes\alpha)$ &

1295:   $\alpha;\nabla_{\underline{m}} =

1296:    \nabla_{\underline{n}};(\alpha\otimes\alpha)$ &

1297:   $\alpha;!_{\underline{m}} = !_{\underline{n}}$ \\

1298: \hline

1299: \hline

1300: \end{tabular}

1301: \end{center}

1302: \end{table}

1303: 

1304:  This presentation shows that all the auxiliary structure can be

1305:  generated by composing together three basic constructors

1306:  ($\gamma_{\underline{1},\underline{1}}$, $\nabla_{\underline{1}}$ and

1307:  $!_{\underline{1}}$), \ie, it admits a finitary specification.

1308:  Moreover, we think that this construction nicely separates the

1309:  syntactic structure of the signature from the additional auxiliary

1310:  structure common to all cartesian models.

1311: 

1312:  The axiomatization of $\textbf{Th}[\Sigma]$ has been exploited in

1313:  \cite{BFMM:BC} for defining a

1314:  taxonomy of tile formats as certain axioms or operators are omitted

1315:  from the configuration and observation categories. In particular the

1316:  auxiliary tiles needed in all such formats can be characterized as

1317:  the bidimensional counterparts of symmetries, duplicators and

1318:  dischargers. For example, let us mention that the auxiliary tiles of

1319:  \emph{term tile logic} \cite{BMM:PTTL} (where the categories of

1320:  configurations and observations are freely generated cartesian

1321:  categories $\textbf{Th}[\Sigma]$ and $\textbf{Th}[\Lambda]$) are the

1322:  commuting squares of the category $\textbf{Th}[\emptyset]$ generated

1323:  by the empty signature.

1324: 

1325: \section{Resolution via pullbacks}\label{RVPsec}

1326: 

1327:  As we have briefly recalled in the Introduction, the construction

1328:  of the mgu has a clear mathematical meaning: It can be

1329:  formulated in the terminology of category theory as a well-known

1330:  universal construction called pullback (taken in a suitable category).

1331: 

1332:  Universal constructions play a fundamental role in category

1333:  theory, as they express the best way to accomplish a certain

1334:  task. They usually involve a diagram that imposes certain

1335:  constraints on the construction and then require the existence

1336:  and uniqueness in the category of certain arrows satisfying such

1337:  constraints, \ie, representing a possible solution to the

1338:  problem. Among these solutions, one is of course interested in

1339:  the optimal one (if it exists), \eg, the least upper

1340:  bound. Categorically speaking, this is

1341:  achieved by taking the solution that uniquely factorizes all the

1342:  other solutions. Note that since many such optimal solutions can

1343:  exist, any of them is completely equivalent to all the others

1344:  (they are indeed pairwise isomorphic). Universal constructions

1345:  allow one to recast ordinary set-theoretic constructions (\eg,

1346:  cartesian product, disjoint sum) in a more general, abstract

1347:  formulation that can serve as a uniform guide for catching

1348:  analogies and pursuing comparisons between different frameworks.

1349: 

1350: \begin{definition}[Pullback]

1351:  Given a category $\mathcal{C}$ and two arrows $h\from o_0 \to o_2$

1352:  and $g\from o_1 \to o_2$ in $\mathcal{C}$, the \emph{pullback} of $h$ and $g$ in

1353:  $\mathcal{C}$ is an object $o$ together with two projections

1354:  $p_0 \from o \to o_0$ and $p_1 \from o \to o_1$ such that

1355:  \begin{enumerate}

1356:  \item $p_0;h = p_1;g$, and

1357:  \item for any object $o'$ and arrows $q_0 \from o' \to o_0$ and $q_1 \from o' \to

1358:  o_1$ such that $q_0;h = q_1;g$, then there must exist a unique arrow

1359:  $q\from o'\to o$ such that $q;p_0 = q_0$ and $q;p_1 = q_1$.

1360:  \end{enumerate}

1361: \end{definition}

1362: 

1363:  The two arrows $h$ and $g$ encode the instance of the problem,

1364:  posing constraints on the admissible solutions. The first condition

1365:  says that $o$, $p_0$ and $p_1$ yield a solution (called a \emph{cone}

1366:  in category theory). The second condition states that $o$, $p_0$ and

1367:  $p_1$ form the best solution among those contained in $\mathcal{C}$.

1368:  The commuting diagram in Figure~\ref{pullbackfig} illustrates the

1369:  definition (as usual in category theory, universal arrows are dotted).

1370: 

1371: \begin{figure}[t]

1372: \begin{center}

1373: $\xymatrix{

1374:  {o'} \ar@{.>}[rd]^{q} \ar@/^/[rrd]^{q_0} \ar@/_/[rdd]_{q_1} \\

1375:  & {o} \ar[r]^{p_0} \ar[d]_{p_1} &

1376:  {o_0} \ar[d]^{h} \\

1377:  & {o_1} \ar[r]_{g} &

1378:  {o_2} }$

1379: \end{center}

1380: \caption{The pullback of $h$ and $g$.} \protect\label{pullbackfig}

1381: \end{figure}

1382: 

1383: \begin{example}[Pullbacks in $\Set$]

1384:  The category $\Set$ has sets as objects and functions as arrows.

1385:  Given $h\from X \to Z$ and $g\from Y \to Z$, then their pullback is

1386:  the set $U = \{(x,y)\in X\times Y \mid h(x)=g(y)\}$ with the

1387:  obvious projections on the first and second components of each

1388:  pair in $U$.

1389: \end{example}

1390: 

1391:  The category we are interested in is the category of substitutions on

1392:  the signature $\Sigma$. It is well known that the mgu of a set of

1393:  equations is an equalizer in the category of substitutions (see \eg,

1394:  \cite{BR:CUA,Gog:WIU}, though there the authors work with the opposite

1395:  category $\mathbf{Th}[\Sigma]^{\mathrm{op}}$ of

1396:  $\mathbf{Th}[\Sigma]$, and therefore the mgu's are given by

1397:  coequalizers).

1398: 

1399: \begin{definition}[Equalizer]

1400:  Given a category $\mathcal{C}$ and two arrows $h\from o_1 \to o_2$

1401:  and $g\from o_1 \to o_2$, the \emph{equalizer} of $h$ and $g$ in

1402:  $\mathcal{C}$ is an object $o$ together with a projection

1403:  $p \from o \to o_1$ such that

1404:  \begin{enumerate}

1405:  \item $p;h = p;g$, and

1406:  \item for any object $o'$ and arrow $q \from o' \to o_1$

1407:  such that $q;h = q;g$, then there must exist a unique arrow

1408:  $q'\from o'\to o$ such that $q';p = q$.

1409:  \end{enumerate}

1410: \end{definition}

1411: 

1412: \begin{figure}[t]

1413: \begin{center}

1414: \begin{tabular}{ccc}

1415: $\vcenter{\xymatrix{

1416:  {o} \ar[r]^{p} &

1417:  {o_1} \ar@/^/[r]^{h} \ar@/_/[r]_{g} &

1418:  {o_2} \\

1419:  {o'} \ar@{.>}[u]^{q'} \ar[ru]_{q} }}$ & &

1420: $\vcenter{\xymatrix{

1421:  {o} \ar@{.>}[rd]^{r} \ar@/^/[rrd]^{p} \ar@/_/[rdd]_{p} \\

1422:  & {o'_1} \ar[r]^{p_1} \ar[d]_{p'_1} &

1423:  {o_1} \ar[d]^{h} \\

1424:  & {o_1} \ar[r]_{g} &

1425:  {o_2} }}$ \\

1426:  (a) & & (b)

1427: \end{tabular}

1428: \end{center}

1429: \caption{The equalizer (a)  and the pullback of $h$ and $g$

1430:  in the same homset (b).}

1431: \protect\label{equalizerfig}

1432: \end{figure}

1433: 

1434:  The diagram summarizing the equalizer construction is given in

1435:  Figure~\ref{equalizerfig}(a).

1436: 

1437: \begin{example}[Equalizers in $\Set$]

1438:  Given $h\from X \to Z$ and $g\from X \to Z$, then their equalizer is

1439:  the subset $U = \{x\in X \mid h(x)=g(x)\}$ of $X$ with the obvious

1440:  inclusion $U\hookrightarrow X$ as projection.

1441: \end{example}

1442: 

1443:  Note that, in general, for $h,g\from o_1 \to o_2$ the pullback

1444:  of $h$ and $g$ is not

1445:  isomorphic to their equalizer. Moreover, when both exist, the

1446:  cone $(o,p,p)$ (obtained by taking twice the projection of the

1447:  equalizer) uniquely factorizes through the pullback

1448:  $(o'_1,p_1,p'_1)$ (see Figure~\ref{equalizerfig}(b)).

1449: 

1450:  For a given set of equations $\{t_1 = s_1, t_2 = s_2, \ldots, t_n=

1451:  s_n\}$, we can consider the substitutions $\sigma =

1452:  [\sbtn{t_1}{z_1},\sbtn{t_2}{z_2},\cdots,\sbtn{t_n}{z_n}]$ and $\sigma' =

1453:  [\sbtn{s_1}{z_1},\sbtn{s_2}{z_2},\cdots,\sbtn{s_n}{z_n}]$, where the

1454:  $z_i$'s are fresh variables not appearing in the $t_i$'s and

1455:  $s_i$'s. The substitutions $\sigma$ and $\sigma'$ can be seen as

1456:  arrows going from the set of variables appearing in the $t_i$'s and

1457:  $s_i$'s to the set $Z = \{z_1,z_2,\ldots,z_n\}$.  To see how the

1458:  definition of equalizer matches that of mgu, just observe that (1)

1459:  it requires the existence of a substitution $\theta$ such that

1460:  $\theta;\sigma = \theta;\sigma'$ and (2) the fact that $\theta$

1461:  is the most general such substitution corresponds to the universal

1462:  property of equalizers.

1463: 

1464:  However, in the case of logic programming, we are not really

1465:  interested in finding the mgu of a generic set of equations, because

1466:  we know that the variables in the head of the selected clause have

1467:  been renamed on purpose to be different from those in the selected

1468:  goal, \ie, they are fresh. Thus, we want to find the mgu of a set of

1469:  equations $\{t_1 = s_1, t_2 = s_2, \ldots, t_n= s_n\}$ such that the

1470:  variables appearing in $t_i$ and $s_j$ are disjoint for $i,j\in

1471:  [1,n]$. Then, we can consider the substitutions $\sigma_* =

1472:  [\sbtn{t_1}{z_1},\sbtn{t_2}{z_2},\cdots,\sbtn{t_n}{z_n}]$ and $\sigma'_*

1473:  = [\sbtn{s_1}{z_1},\sbtn{s_2}{z_2},\cdots,\sbtn{s_n}{z_n}]$, where the

1474:  $z_i$'s are fresh variables not appearing in the $t_i$'s and

1475:  $s_i$'s. If we denote by $X$ the set of variables appearing in the

1476:  $t_i$'s, by $Y$ the set of variables used in the $s_i$'s, and by $Z$

1477:  the set $\{z_1,z_2,\ldots,z_n\}$, then we can write $\sigma_*\from X \to

1478:  Z$ and $\sigma'_*\from Y\to Z$. Their pullback (when it exists) is

1479:  thus given by a pair of substitutions $\psi_*\from U_*\to X$ and

1480:  $\psi'_*\from U_*\to Y$ such that

1481: \begin{itemize}

1482:  \item $\psi_*;\sigma_* = \psi'_*;\sigma'_*$, and

1483:  \item for any substitutions $\rho \from V \to X$ and $\rho' \from V

1484:        \to Y$ such that $\rho;\sigma_* = \rho';\sigma'_*$, then there

1485:        must exist a unique substitution $\phi \from V\to U_*$ such

1486:        that $\phi;\psi_* = \rho$ and $\phi;\psi'_* = \rho'$.

1487: \end{itemize}

1488: 

1489:  Since the fact that the notion of pullback of $\sigma_*$ and

1490:  $\sigma'_*$ coincides with the notion of equalizer of $\sigma$ and

1491:  $\sigma'$ is not completely straightforward, we illustrate below such

1492:  a correspondence.

1493: 

1494: \paragraph{From equalizers to pullbacks.}

1495: 

1496:  Consider the arrows $\sigma\from X\cup Y \to Z$ and

1497:  $\sigma'\from X\cup Y \to Z$ that are defined exactly as $\sigma_*$

1498:  and $\sigma'_*$ but have different domains. Then, we know that their

1499:  mgu is the equalizer $\theta\from U\to X\cup Y$ discussed

1500:  above. Since $\theta$ is a substitution and since $X=\{x_1,\ldots,x_k\}$

1501:  and $Y=\{y_1,\ldots,y_h\}$ are disjoint, then $\theta$ must have

1502:  the form

1503: 

1504: \begin{center}

1505:  $[\sbtn{r_1}{x_1}, \cdots, \sbtn{r_k}{x_k},

1506:   \sbtn{r'_1}{y_1}, \cdots, \sbtn{r'_k}{y_h}]$.

1507: \end{center}

1508: 

1509:  Then, $\theta_X=[\sbtn{r_1}{x_1},\cdots,\sbtn{r_k}{x_k}]\from U \to X$

1510:  and $\theta_Y=[\sbtn{r'_1}{y_1},\cdots,\sbtn{r'_k}{y_h}]\from U\to Y$

1511:  satisfy $\theta_X;\sigma_* = \theta_Y;\sigma'_*$. We want to show

1512:  that $U$, $\theta_X$ and $\theta_Y$ define a pullback of $\sigma_*$

1513:  and $\sigma'_*$. In fact, suppose that there exist $V$ with $\rho

1514:  \from V \to X$ and $\rho' \from V \to Y$ such that $\rho;\sigma_* =

1515:  \rho';\sigma'_*$, then since $X$ and $Y$ are disjoint, $\rho$ and

1516:  $\rho'$ can be combined together in a substitution $\rho_*\from V \to

1517:  X\cup Y$ such that $\rho_*;\sigma = \rho_*;\sigma'$. By definition of

1518:  equalizer, then there exists a unique arrow $\phi \from V \to U$ such

1519:  that $\phi;\theta = \rho_*$. But the last condition is equivalent to

1520:  imposing that $\phi;\theta_X = \rho$ and $\phi;\theta_Y = \rho'$

1521:  concluding the proof. All this is illustrated in

1522:  Figure~\ref{firstpartfig}.

1523: 

1524: \begin{figure}[t]

1525: \begin{center}

1526: \begin{tabular}{ccc}

1527: $\vcenter{\xymatrix{

1528:  {U} \ar[r]^{\theta} &

1529:  {X\cup Y} \ar@/^/[r]^{\sigma} \ar@/_/[r]_{\sigma'} &

1530:  {Z} \\

1531:  {V} \ar@{.>}[u]^{\phi} \ar[ru]_{\rho_*} } }$ & &

1532: $\vcenter{\xymatrix{

1533:  & & {X} \ar[rd]^{\sigma_*} \\

1534:  {V} \ar@/^/[rru]^{\rho} \ar@/_/[rrd]_{\rho'} \ar@{.>}[r]^{\phi} &

1535:  {U} \ar[ru]^{\theta_X} \ar[rd]_{\theta_Y} & &

1536:  {Z} \\

1537:  & & {Y} \ar[ru]_{\sigma'_*} }}$

1538: \end{tabular}

1539: \end{center}

1540: \caption{From equalizer to pullback.}

1541: \protect\label{firstpartfig}

1542: \end{figure}

1543: 

1544: 

1545: \paragraph{From pullbacks to equalizers.}

1546: 

1547:  It remains to show that to each pullback $(U',\psi_X,\psi_Y)$ of

1548:  $\sigma_*$ and $\sigma'_*$ there corresponds an mgu (\ie, an

1549:  equalizer) of $\sigma$ and $\sigma'$. By arguments similar to those

1550:  employed above, it is evident that $\psi_X$ and $\psi_Y$ can be

1551:  merged to define a substitution $\psi_*\from U'\to X\cup Y$ such that

1552:  $\psi_*;\sigma = \psi_*;\sigma'$. Then, we must show that this

1553:  candidate is indeed an equalizer. Thus, we assume the existence of

1554:  $V$ and $\rho_*\from V\to X\cup Y$ such that $\rho_*;\sigma =

1555:  \rho_*;\sigma'$. As before, we can decompose $\rho_*$ into

1556:  $\rho_X\from V\to X$ and $\rho_Y\from V\to Y$ with $\rho_X;\sigma_* =

1557:  \rho_Y;\sigma'_*$. By definition of pullback, then there exists a

1558:  unique arrow $\phi_*\from V\to U'$ such that $\phi_*;\psi_X = \rho_X$

1559:  and $\phi_*;\psi_Y = \rho_Y$, and the last two conditions are

1560:  equivalent to the constraint $\phi_*;\psi_* = \rho_*$, concluding the

1561:  proof.  All this is illustrated in Figure~\ref{secondpartfig}.

1562: 

1563: \begin{figure}[t]

1564: \begin{center}

1565: \begin{tabular}{ccc}

1566: $\vcenter{\xymatrix{

1567:  & & {X} \ar[rd]^{\sigma_*} \\

1568:  {V} \ar@/^/[rru]^{\rho_X} \ar@/_/[rrd]_{\rho_Y} \ar@{.>}[r]^{\phi_*} &

1569:  {U'} \ar[ru]^{\psi_X} \ar[rd]_{\psi_Y} & &

1570:  {Z} \\

1571:  & & {Y} \ar[ru]_{\sigma'_*} }}$ & &

1572: $\vcenter{\xymatrix{

1573:  {U'} \ar[r]^{\psi_*} &

1574:  {X\cup Y} \ar@/^/[r]^{\sigma} \ar@/_/[r]_{\sigma'} &

1575:  {Z} \\

1576:  {V} \ar@{.>}[u]^{\phi_*} \ar[ru]_{\rho_*} } }$

1577: \end{tabular}

1578: \end{center}

1579: \caption{From pullback to equalizer.}

1580: \protect\label{secondpartfig}

1581: \end{figure}

1582: 

1583: \paragraph{}

1584: 

1585:  Of course, it might well be the case that no such arrows $\psi$

1586:  and $\psi'$ exist, \eg, when one tries to solve the sets $\{f(x)

1587:  = f'(y)\}$ or $\{f(x) = x\}$ for unary operation symbols $f$ and

1588:  $f'$.  There can also exist more solutions than one, and this is

1589:  always the case as the names of the variables in $U$ are not

1590:  important at all.

1591: 

1592:  The different flavors corresponding to the equalizer and the

1593:  pullback views rely on the fact that in the equalizer

1594:  construction we have to work with the full universe $\mathcal{X}$

1595:  of \emph{all} variables, while in the pullback

1596:  construction only the variables of interest for a particular mgu

1597:  creation must be considered. Therefore, the equalizer

1598:  approach is completely centralized, while the pullback

1599:  construction is as much distributed as possible.

1600:  Nevertheless, the result above proves that the two views

1601:  are equivalent.

1602: 

1603: 

1604: \section{The double category of pullbacks}\label{DCPsec}

1605: 

1606:  In this section we show that the construction of pullbacks in the

1607:  category of substitutions can be presented in a modular way, by

1608:  composing together a finite set of basic pullbacks.  We start by

1609:  showing that the pullback squares in a category $\mathcal{C}$ form a

1610:  double category. To see this, let us remind a few classical results.

1611: 

1612: \begin{proposition}\label{proppbcompdef}

1613:  Given a category $\mathcal{C}$ and three arrows $h\from o_0\to o_3$,

1614:  $g_1\from o_1 \to o_2$ and $g_2\from o_2 \to o_3$, let $(o,p_0,p_2)$

1615:  be the pullback of $h$ and $g_2$, and let $(o',q_0,q_1)$ be the

1616:  pullback of $p_2$ and $g_1$ (see Figure~\ref{pbcompfig}). Then,

1617:  $(o',q_0;p_0,q_1)$ is a pullback of $h$ and $g_1;g_2$.

1618: \end{proposition}

1619: 

1620: \begin{proposition}

1621:  Given a category $\mathcal{C}$ and three arrows $h\from o_0\to o_3$,

1622:  $g_1\from o_1 \to o_2$ and $g_2\from o_2 \to o_3$, let $(o,p_0,p_2)$ be the

1623:  pullback of $h$ and $g_2$, and let $(o',q_0;p_0,q_1)$ be the pullback

1624:  of $h$ and $g_1;g_2$. Then, $(o',q_0,q_1)$

1625:  is a pullback of $p_2$ and $g_1$.

1626: \end{proposition}

1627: 

1628: \begin{proposition}

1629:  The pullback of $h\from o_0 \to o_1$ and $id_{o_1}\from o_1\to o_1$

1630:  exists in any category. Moreover, $(o_0,id_{o_0},h)$ is a pullback

1631:  of $h$ and $id_{o_1}$.

1632: \end{proposition}

1633: 

1634: \begin{definition}[Double category of pullbacks]

1635:  Given a category $\mathcal{C}$, the double category of pullbacks in

1636:  $\mathcal{C}$, denoted by $\mathscr{P}(\mathcal{C})$, is defined as

1637:  follows:

1638: \begin{itemize}

1639: \item

1640:  its objects are the objects of $\mathcal{C}$;

1641: \item

1642:  its horizontal 1-category is $\mathcal{C}$;

1643: \item

1644:  its vertical 1-category is $\mathcal{C}$;

1645: \item

1646:  the cells are the squares $(p_0,p_1,h,g)$ (see

1647:  Figure~\ref{pbsqfig}) such that $p_0$ and $p_1$ define a pullback

1648:  of $h$ and $g$;

1649: \item

1650:  given two cells $(q,q',p',g_1)$ and $(p,p',h,g_2)$ their

1651:  horizontal composition is the cell $(q;p,q',h,g_1;g_2)$;

1652: \item

1653:  given two cells $(q,q',h_1,p)$ and $(p,p',h_2,g)$ their

1654:  vertical composition is the cell $(q,q';p',h_1;h_2,g)$.

1655: \end{itemize}

1656: \end{definition}

1657: 

1658: \begin{figure}

1659: \begin{center}

1660: $\xymatrix{

1661:  {o'} \ar[r]^{q_0} \ar[d]_{q_1} &

1662:  {o} \ar[r]^{p_0} \ar[d]|{p_2} &

1663:  {o_0} \ar[d]^{h} \\

1664:  {o_1} \ar[r]_{g_1} &

1665:  {o_2} \ar[r]_{g_2} &

1666:  {o_3}

1667: }$

1668: \end{center}

1669: \caption{Composition of pullbacks.}

1670: \protect\label{pbcompfig}

1671: \end{figure}

1672: 

1673: \begin{figure}[t]

1674: \begin{center}

1675: $\xymatrix{

1676:  {o} \ar[r]^{p_0} \ar[d]_{p_1} &

1677:  {o_0} \ar[d]^{h} \\

1678:  {o_1} \ar[r]_{g} &

1679:  {o_2} }$

1680: \end{center}

1681: \caption{Pullback square as double cell.}

1682: \protect\label{pbsqfig}

1683: \end{figure}

1684: 

1685:  To see that $\mathscr{P}(\mathcal{C})$ is indeed a double category,

1686:  observe that both horizontal and vertical compositions of

1687:  cells return pullback squares (Proposition~\ref{proppbcompdef}).

1688:  Moreover, the trivial pullback squares $(id_{o_0},p,p,id_{o_1})$ and

1689:  $(p,id_{o_0},id_{o_1},p)$ behave as identities \wrt\ the horizontal and

1690:  vertical composition, respectively. The exchange law of double

1691:  categories holds trivially, as the cells are completely identified by

1692:  their borders.

1693: 

1694:  For the arguments presented in the previous section, it follows that

1695:  pullbacks are a fundamental ingredient in the operational semantics,

1696:  as they provide a characterization of the mgu construction, which

1697:  clearly separates the goal dimension (horizontal) from the

1698:  resolution mechanism (the vertical dimension) focusing on their

1699:  interaction (the substitutions yielding the pullback).

1700: 

1701:  However, dealing with all this machinery at the computational level

1702:  is too heavy, as there are infinitely many pullbacks. Therefore, a

1703:  finitary presentation of $\mathscr{P}(\mathcal{C})$ is a main issue.

1704: 

1705: \subsection{Finitary presentation of pullbacks}\label{FPPsec}

1706: 

1707:  Our first contribution consists of recovering in a finitary way the

1708:  double category $\mathscr{P}(\textbf{Th}[\Sigma])$. We start by

1709:  focusing on the small set of commuting squares depicted in

1710:  Figure~\ref{basicpbkfig}. We want to show that any pullback can then

1711:  be obtained by composing these basic squares (and horizontal and

1712:  vertical identity pullbacks), \ie\ that the basic squares

1713:  in Figure~\ref{basicpbkfig} form a basis for the

1714:  generation of arbitrary pullbacks.

1715: 

1716: \begin{figure}[t]

1717: \begin{center}

1718: $\vcenter{\xymatrix{

1719:  {\underline{1}} \ar@{}[rd]|{R_f} &

1720:  {\underline{n}} \ar[l]_{f} \\

1721:  {\underline{n}} \ar[u]^{f} &

1722:  {\underline{n}} \ar[l]^{id_{\underline{n}}} \ar[u]_{id_{\underline{n}}} }}$

1723: \hfill

1724:  $\vcenter{\xymatrix{

1725:  {\underline{2}} \ar@{}[rdd]|{D_f} &

1726:  {\underline{n+1}} \ar[l]_{f\otimes id_{\underline{1}}} \\

1727:  & {\underline{2n}} \ar[u]_{id_{\underline{n}}\otimes f} \\

1728:  {\underline{1}} \ar[uu]^{\nabla_{\underline{1}}} &

1729:  {\underline{n}} \ar[l]^{f} \ar[u]_{\nabla_{\underline{n}}} }}$

1730: \hfill $\vcenter{\xymatrix{

1731:  {\underline{2}} \ar@{}[rrd]|{\hat{D}_f} & &

1732:  {\underline{1}} \ar[ll]_{\nabla_{\underline{1}}} \\

1733:  {\underline{n+1}} \ar[u]^{f\otimes id_{\underline{1}}} &

1734:  {\underline{2n}} \ar[l]^{id_{\underline{n}} \otimes f} &

1735:  {\underline{n}} \ar[l]^{\nabla_{\underline{n}}} \ar[u]_{f} }}$

1736: \hfill (for all $f\in\Sigma^n$)

1737: \end{center}

1738: \begin{center}

1739: $\vcenter{\xymatrix{

1740:  {\underline{2}} \ar@{}[rd]|{R_\nabla} &

1741:  {\underline{1}} \ar[l]_{\nabla_{\underline{1}}} \\

1742:  {\underline{1}} \ar[u]^{\nabla_{\underline{1}}} &

1743:  {\underline{1}} \ar[l]^{id_{\underline{1}}} \ar[u]_{id_{\underline{1}}} }} $

1744: \hfill $\vcenter{\xymatrix{

1745:  {\underline{2}} \ar@{}[rd]|{R_\gamma} &

1746:  {\underline{2}} \ar[l]_{\gamma_{\underline{1},\underline{1}}} \\

1747:  {\underline{2}} \ar[u]^{\gamma_{\underline{1},\underline{1}}} &

1748:  {\underline{2}} \ar[l]^{id_{\underline{2}}} \ar[u]_{id_{\underline{2}}} }}$

1749: \hfill $\vcenter{\xymatrix{

1750:  {\underline{3}} \ar@{}[rd]|{D_\nabla} &

1751:  {\underline{2}} \ar[l]_{\nabla_{\underline{1}}\otimes id_{\underline{1}}} \\

1752:  {\underline{2}} \ar[u]^{id_{\underline{1}}\otimes \nabla_{\underline{1}}} &

1753:  {\underline{1}} \ar[l]^{\nabla_{\underline{1}}}

1754:                  \ar[u]_{\nabla_{\underline{1}}} }}$

1755: \end{center}

1756: \caption{The basic pullbacks.}

1757: \protect\label{basicpbkfig}

1758: \end{figure}

1759: 

1760:  There are a few points for which some explanation is worth. First of

1761:  all, note that we have depicted the pullback cells with the direction

1762:  of the arrows reversed with respect to the usual presentation. The

1763:  reason for this will become much clearer in Section~\ref{TSLPsec},

1764:  where we will show that this representation matches the intuitive

1765:  direction of computation flow (from up to down) and also of

1766:  internal contextualizations, which now compose to the right of the current state.

1767:  From the point of view of the notation this is not problematic in tile logic,

1768:  as we can assume to work with opposite categories of configuration

1769:  and observations. As a matter of notation, the tiles in

1770:  Figure~\ref{basicpbkfig} can be written as the sequents

1771:  \begin{itemize}

1772:  \item

1773:  $R_f\from

1774:  \cell{f}{f}{id_{\underline{n}}}{id_{\underline{n}}}$,

1775:  \item

1776:  $D_f\from

1777:  \cell{f\otimes id_{\underline{1}}}{\nabla_{\underline{1}}}

1778:       {\nabla_{\underline{n}};(id_{\underline{n}}\otimes f)}{f}$,

1779:  \item

1780:  $\hat{D}_f\from

1781:  \cell{\nabla_{\underline{1}}}{f\otimes id_{\underline{1}}}

1782:       {f}{\nabla_{\underline{n}};(id_{\underline{n}}\otimes f)}$,

1783:  \item

1784:  $R_\nabla\from

1785:  \cell{\nabla_{\underline{1}}}{\nabla_{\underline{1}}}

1786:       {id_{\underline{1}}}{id_{\underline{1}}}$,

1787:  \item

1788:  $R_\gamma\from

1789:  \cell{\gamma_{\underline{1},\underline{1}}}

1790:       {\gamma_{\underline{1},\underline{1}}}

1791:       {id_{\underline{2}}}{id_{\underline{2}}}$, and

1792:  \item

1793:  $D_\nabla\from

1794:  \cell{\nabla_{\underline{1}} \otimes id_{\underline{1}}}

1795:       {id_{\underline{1}} \otimes \nabla_{\underline{1}}}

1796:       {\nabla_{\underline{1}}}{\nabla_{\underline{1}}}$.

1797:  \end{itemize}

1798: 

1799:  The second point to notice is that the cells $R_\nabla$, $R_\gamma$, and

1800:  $D_\nabla$ do not depend on $\Sigma$, \ie, they form in some sense

1801:  the intrinsic auxiliary structure of the pullback construction.

1802: 

1803: \begin{definition}

1804:  We let $\mathcal{B} = \{R_\nabla, R_\gamma, D_\nabla\}$ be

1805:  the \emph{signature-independent pullback basis}, and let

1806:  $\mathcal{B}(f) = \{R_f ,D_f, \hat{D}_f\}$ be the \emph{pullback

1807:  basis for the operator $f$}. Given a signature $\Sigma$,

1808:  we call $\mathcal{B}(\Sigma) = \mathcal{B} \cup

1809:  \bigcup_{f\in\Sigma} \mathcal{B}(f)$ the \emph{pullback

1810:  basis for $\Sigma$}. We say that the cell

1811:  $\cell{s}{u}{v}{t}$ is \emph{generated} by

1812:  $\mathcal{B}(\Sigma)$, if it can be expressed as the

1813:  parallel and sequential composition of cells in

1814:  $\mathcal{B}(\Sigma)$ and identity cells.

1815: \end{definition}

1816: 

1817: \begin{figure}[t]

1818: \begin{center}

1819: $\vcenter{\xymatrix{

1820:  {\underline{0}} \ar@{}[rd]|{R_!} &

1821:  {\underline{1}} \ar[l]_{!_{\underline{1}}} \\

1822:  {\underline{1}} \ar[u]^{!_{\underline{1}}} &

1823:  {\underline{1}} \ar[l]^{id_{\underline{1}}} \ar[u]_{id_{\underline{1}}} }}$

1824: \hfill $\vcenter{\xymatrix{

1825:  {\underline{3}} \ar@{}[rd]|{\hat{D}_\nabla} &

1826:  {\underline{2}} \ar[l]_{id_{\underline{1}} \otimes \nabla_{\underline{1}}} \\

1827:  {\underline{2}} \ar[u]^{\nabla_{\underline{1}} \otimes id_{\underline{1}}} &

1828:  {\underline{1}} \ar[l]^{\nabla_{\underline{1}}} \ar[u]_{\nabla_{\underline{1}}} }}$

1829: \hfill $\vcenter{\xymatrix{

1830:  {\underline{2}} \ar@{}[rrd]|{\hat{D}'_f} & &

1831:  {\underline{1}} \ar[ll]_{\nabla_{\underline{1}}} \\

1832:  {\underline{1+n}} \ar[u]^{id_{\underline{1}}\otimes f} &

1833:  {\underline{2n}} \ar[l]^{f \otimes id_{\underline{n}}} &

1834:  {\underline{n}} \ar[l]^{\nabla_{\underline{n}}} \ar[u]_{f} }}$

1835: \end{center}

1836: \caption{\textbf{Q}: Are these three basic cells missing?

1837: \textbf{A}:No.}

1838: \protect\label{misstilesfig}

1839: \end{figure}

1840: 

1841:  There are some cells that one might expect to see

1842:  in Figure~\ref{basicpbkfig} but are instead missing. Trying to

1843:  guess the intuition of the reader, we have listed some of them in

1844:  Figure~\ref{misstilesfig}.

1845: 

1846:  The first cell we consider is $R_!$. Its absence might be surprising,

1847:  because there are analogous cells for all the other basic

1848:  constructors (operators $f\in\Sigma$, symmetries and duplicators).

1849:  But $R_!$ is not a pullback. In fact the pullback of

1850:  $!_{\underline{1}}$ and $!_{\underline{1}}$ is

1851:  $(\underline{2},id_{\underline{1}} \otimes !_{\underline{1}},

1852:  !_{\underline{1}}\otimes id_{\underline{1}})$, yielding a cell that

1853:  can in fact be obtained by composing in parallel the horizontal and

1854:  vertical identities of $!_{\underline{1}}$ (\ie, by putting

1855:  $\cell{id_{\underline{0}}}

1856:        {!_{\underline{1}}}

1857:        {!_{\underline{1}}}

1858:        {id_{\underline{1}}}$ in parallel with

1859:  $\cell{!_{\underline{1}}}

1860:        {id_{\underline{0}}}

1861:        {id_{\underline{1}}}

1862:        {!_{\underline{1}}}$).

1863: 

1864: 

1865: \begin{figure}[t]

1866: \begin{center}

1867: $\xymatrix@C=+2cm{

1868:  {\underline{3}} \ar@{}[rd]|{A_1} &

1869:  {\underline{3}} \ar[l]_{(\gamma_{\underline{1},\underline{1}}\otimes id_{\underline{1}});

1870:                          \gamma_{\underline{2},\underline{1}}}

1871:                  \ar@{}[rd]|{A_2} &

1872:  {\underline{3}} \ar[l]_{\gamma_{\underline{1},\underline{1}}\otimes id_{\underline{1}}}

1873:                  \ar@{}[rrd]|{A_3} &

1874:  {\underline{3}} \ar[l]_{\gamma_{\underline{1},\underline{2}}} &

1875:  {\underline{2}} \ar[l]_{id_{\underline{1}}\otimes \nabla_{\underline{1}}} \\

1876:  {\underline{3}} \ar[u]^{(id_{\underline{1}}\otimes\gamma_{\underline{1},\underline{1}});

1877:                          \gamma_{\underline{1},\underline{2}}}

1878:                  \ar@{}[rd]|{A_4} &

1879:  {\underline{3}} \ar[l]|{id_{\underline{3}}} \ar[u]|{id_{\underline{3}}}

1880:                  \ar@{}[rrdd]|{A_5} &

1881:  {\underline{3}} \ar[l]|{\gamma_{\underline{1},\underline{1}}\otimes id_{\underline{1}}}

1882:                  \ar[u]|{id_{\underline{3}}} &

1883:  {\underline{2}} \ar[l]|{\nabla_{\underline{1}}\otimes id_{\underline{1}}}

1884:                  \ar@{}[rd]|{A_6} &

1885:  {\underline{2}} \ar[l]|{\gamma_{\underline{1},\underline{1}}} \ar[u]_{id_{\underline{2}}} \\

1886:  {\underline{3}} \ar[u]^{id_{\underline{1}}\otimes \gamma_{\underline{1},\underline{1}}}

1887:                  \ar@{}[rdd]|{A_7} &

1888:  {\underline{3}} \ar[u]|{id_{\underline{1}}\otimes \gamma_{\underline{1},\underline{1}}}

1889:                  \ar[l]|{id_{\underline{3}}} & &

1890:  {\underline{2}} \ar[u]|{\gamma_{\underline{1},\underline{1}}}

1891:                  \ar@{}[rd]|{A_8} &

1892:  {\underline{2}} \ar[u]_{id_{\underline{2}}} \ar[l]|{id_{\underline{2}}} \\

1893:  {\underline{3}} \ar[u]^{\gamma_{\underline{2},\underline{1}}} &

1894:  {\underline{2}} \ar[u]|{id_{\underline{1}}\otimes \nabla_{\underline{1}}}

1895:                  \ar@{}[rd]|{A_9} &

1896:  {\underline{2}} \ar[l]|{\gamma_{\underline{1},\underline{1}}}

1897:                  \ar@{}[rd]|{A_{10}} &

1898:  {\underline{1}} \ar[l]|{\nabla_{\underline{1}}} \ar[u]|{\nabla_{\underline{1}}}

1899:                  \ar@{}[rd]|{A_{11}} &

1900:  {\underline{1}} \ar[l]|{id_{\underline{1}}} \ar[u]_{\nabla_{\underline{1}}} \\

1901:  {\underline{2}} \ar[u]^{\nabla_{\underline{1}} \otimes id_{\underline{1}}} &

1902:  {\underline{2}} \ar[u]|{\gamma_{\underline{1},\underline{1}}} \ar[l]^{id_{\underline{2}}} &

1903:  {\underline{2}} \ar[u]|{id_{\underline{2}}} \ar[l]^{id_{\underline{2}}} &

1904:  {\underline{1}} \ar[u]|{id_{\underline{1}}} \ar[l]^{\nabla_{\underline{1}}} &

1905:  {\underline{1}} \ar[u]_{id_{\underline{1}}} \ar[l]^{id_{\underline{1}}}

1906: }$

1907: \end{center}

1908: \caption{How to compose the cell $\hat{D}_\nabla$.}

1909: \protect\label{excompfig}

1910: \end{figure}

1911: 

1912:  The second cell $\hat{D}_\nabla$ defines a pullback, but it can be

1913:  obtained by composition of other basic cells and identities, as

1914:  illustrated in Figure~\ref{excompfig}. Let us comment on the

1915:  composition. At the centre of the figure we find the cell $A_5 =

1916:  D_{\nabla}$, in fact we recall that by the coherence axioms for

1917:  duplicators (cf. Table~\ref{ThSigmatab}) we have

1918:  $\nabla_{\underline{1}};\gamma_{\underline{1},\underline{1}} =

1919:  \nabla_{\underline{1}}$, and by functoriality of tensor product we

1920:  have \eg,

1921: \[

1922:  (id_{\underline{1}} \otimes \nabla_{\underline{1}}) ;

1923:  (id_{\underline{1}} \otimes \gamma_{\underline{1},\underline{1}}) =

1924:  (id_{\underline{1}} ; id_{\underline{1}}) \otimes

1925:  (\nabla_{\underline{1}};\gamma_{\underline{1},\underline{1}}) =

1926:  id_{\underline{1}} \otimes \nabla_{\underline{1}}.

1927: \]

1928: \noindent

1929:  On the bottom-right part of the figure, we find the cells $A_8$

1930:  and $A_{10}$ that are the horizontal and vertical identities of

1931:  $\nabla_{\underline{1}}$, while $A_{11}$ is the trivial identity

1932:  for the object $\underline{1}$. Then, note that $A_6 = A_9 =

1933:  R_{\gamma}$. The cell $A_7$ is a horizontal identity, in fact by

1934:  naturality of the symmetries, we have

1935: \[

1936:  \gamma_{\underline{1},\underline{1}} ;

1937:  (id_{\underline{1}} \otimes \nabla_{\underline{1}}) =

1938:  (\nabla_{\underline{1}} \otimes id_{\underline{1}}) ;

1939:  \gamma_{\underline{2},\underline{1}}.

1940: \]

1941: \noindent

1942:  Likewise, the cell $A_3$ is a vertical identity. Also $A_2$ and

1943:  $A_4$ are obvious identities. The tile $A_1$ deserves more

1944:  attention. The first thing to note is that by naturality of

1945:  symmetries we have that

1946: \[

1947:  (\gamma_{\underline{1},\underline{1}}\otimes id_{\underline{1}});

1948:  \gamma_{\underline{2},\underline{1}} =

1949:  \gamma_{\underline{2},\underline{1}};

1950:  (id_{\underline{1}}\otimes\gamma_{\underline{1},\underline{1}})

1951: \]

1952: \noindent

1953:  and then, by coherence of symmetries, we have

1954: \begin{eqnarray*}

1955:  \gamma_{\underline{2},\underline{1}} & = &

1956:  (id_{\underline{1}}\otimes\gamma_{\underline{1},\underline{1}});

1957:  (\gamma_{\underline{1},\underline{1}}\otimes id_{\underline{1}})

1958:  \\

1959:  \gamma_{\underline{1},\underline{2}} & = &

1960:  (\gamma_{\underline{1},\underline{1}}\otimes id_{\underline{1}});

1961:  (id_{\underline{1}}\otimes\gamma_{\underline{1},\underline{1}})

1962: \end{eqnarray*}

1963: \noindent

1964:  and therefore it follows that

1965: \[

1966:  \gamma_{\underline{2},\underline{1}};

1967:  (id_{\underline{1}}\otimes\gamma_{\underline{1},\underline{1}}) =

1968:  (id_{\underline{1}}\otimes\gamma_{\underline{1},\underline{1}});

1969:  (\gamma_{\underline{1},\underline{1}}\otimes id_{\underline{1}});

1970:  (id_{\underline{1}}\otimes\gamma_{\underline{1},\underline{1}}) =

1971:  (id_{\underline{1}}\otimes\gamma_{\underline{1},\underline{1}});

1972:  \gamma_{\underline{1},\underline{2}}.

1973: \]

1974: \noindent

1975:  We can thus construct $A_1$ as illustrated in

1976:  Figure~\ref{exauxfig}, where $A'_2$ is the vertical identity of

1977:  $id_{\underline{1}}\otimes\gamma_{\underline{1},\underline{1}}$

1978:  and $A'_4$ is the horizontal identity of

1979:  $\gamma_{\underline{1},\underline{1}}\otimes id_{\underline{1}}$

1980:  (for simplicity we omit to specify the borders of the

1981:  cells, as they should be evident from the discussion above).

1982:  To conclude that the composition in Figure~\ref{excompfig} yields

1983:  $\hat{D}_\nabla$ we have to check that their borders are equal, and

1984:  in fact observe that

1985: \begin{eqnarray*}

1986:  \gamma_{\underline{1},\underline{2}};

1987:  (\gamma_{\underline{1},\underline{1}} \otimes id_{\underline{1}});

1988:  (\gamma_{\underline{1},\underline{1}} \otimes id_{\underline{1}});

1989:  \gamma_{\underline{2},\underline{1}} & = &

1990:  \gamma_{\underline{1},\underline{2}};

1991:  \gamma_{\underline{2},\underline{1}}  =

1992:  id_{\underline{3}}

1993:  \\

1994:  \gamma_{\underline{2},\underline{1}};

1995:  (id_{\underline{1}} \otimes \gamma_{\underline{1},\underline{1}});

1996:  (id_{\underline{1}} \otimes \gamma_{\underline{1},\underline{1}});

1997:  \gamma_{\underline{1},\underline{2}} & = &

1998:  \gamma_{\underline{2},\underline{1}};

1999:  \gamma_{\underline{1},\underline{2}}  =

2000:  id_{\underline{3}}.

2001: \end{eqnarray*}

2002: 

2003: \begin{figure}[t]

2004: \begin{center}

2005: $\xymatrix@+1pc{

2006:  {\ } \ar@{}[rd]|{A_{11}\otimes R_{\gamma}} &

2007:  {\ } \ar[l] \ar@{}[rd]|{A_2} &

2008:  {\ } \ar[l] \ar@{}[rd]|{A'_2} &

2009:  {\ } \ar[l] \\

2010:  {\ } \ar[u] \ar@{}[rd]|{A'_4} &

2011:  {\ } \ar[u] \ar[l] \ar@{}[rd]|{R_{\gamma}\otimes A_{11}} &

2012:  {\ } \ar[u] \ar[l] \ar@{}[rd]|{A'_2} &

2013:  {\ } \ar[u] \ar[l] \\

2014:  {\ } \ar[u] \ar@{}[rd]|{A_4} &

2015:  {\ } \ar[u] \ar[l] \ar@{}[rd]|{A_4} &

2016:  {\ } \ar[u] \ar[l] \ar@{}[rd]|{A_{11}\otimes R_{\gamma}} &

2017:  {\ } \ar[u] \ar[l] \\

2018:  {\ } \ar[u] &

2019:  {\ } \ar[u] \ar[l] &

2020:  {\ } \ar[u] \ar[l] &

2021:  {\ } \ar[u] \ar[l]

2022: }$

2023: \end{center}

2024: \caption{How to obtain the cell $A_1$ in Figure~\ref{excompfig}.}

2025: \protect\label{exauxfig}

2026: \end{figure}

2027: 

2028:  The third cell $\hat{D}'_f$ illustrated in

2029:  Figure~\ref{misstilesfig} is a pullback, but it can be composed

2030:  starting from $\hat{D}_f$ as shown in Figure~\ref{exffig}, where

2031:  unnamed cells are obvious (horizontal or vertical) identities. In

2032:  writing the border of $\hat{D}_f$ we have exploited the coherence

2033:  axiom

2034: \[

2035:  \nabla_{\underline{n}};\gamma_{\underline{n},\underline{n}} =

2036:  \nabla_{\underline{n}}.

2037: \]

2038: \noindent

2039:  The cells $B_3$ and $B_2$ are identities that exploit the

2040:  naturality of symmetries. Finally, the cell $B_1$ is obtained by

2041:  a construction analogous to that of $A_1$, employing $R_\gamma$

2042:  as a building block.

2043: 

2044: \begin{figure}[t]

2045: \begin{center}

2046: $\xymatrix@C=+2cm{

2047:  {\underline{2}} \ar@{}[rd]|{R_\gamma} &

2048:  {\underline{2}} \ar[l]_{\gamma_{\underline{1},\underline{1}}} &

2049:  {\underline{2}} \ar[l]_{\gamma_{\underline{1},\underline{1}}} & &

2050:  {\underline{1}} \ar[ll]_{\nabla_{\underline{1}}} \\

2051:  {\underline{2}} \ar[u]^{\gamma_{\underline{1},\underline{1}}}

2052:                  \ar@{}[rddd]|{B_3} &

2053:  {\underline{2}} \ar[u]|{id_{\underline{2}}} \ar[l]|{id_{\underline{2}}}

2054:                  \ar@{}[rrrd]|{\hat{D}_f} &

2055:  {\underline{2}} \ar[u]|{id_{\underline{2}}} \ar[l]|{\gamma_{\underline{1},\underline{1}}} & &

2056:  {\underline{1}} \ar[u]_{id_{\underline{1}}} \ar[ll]|{\nabla_{\underline{1}}} \\

2057:  {\underline{2}} \ar[u]^{\gamma_{\underline{1},\underline{1}}} &

2058:  {\underline{n+1}} \ar[u]|{f\otimes id_{\underline{1}}}

2059:                    \ar@{}[rrd]|{B_2} &

2060:  {\underline{2n}} \ar[l]|{id_{\underline{n}}\otimes f} &

2061:  {\underline{2n}} \ar[l]|{\gamma_{\underline{n},\underline{n}}} &

2062:  {\underline{n}} \ar[u]_{f} \ar[l]|{\nabla_{\underline{n}}} \\

2063:  & {\underline{n+1}} \ar[u]|{id_{\underline{n+1}}}

2064:                      \ar@{}[rd]|{B_1} &

2065:  {\underline{1+n}} \ar[l]|{\gamma_{\underline{1},\underline{n}}} &

2066:  {\underline{2n}} \ar[l]|{f\otimes id_{\underline{n}}} \ar[u]|{id_{\underline{2n}}} &

2067:  {\underline{n}} \ar[l]|{\nabla_{\underline{n}}} \ar[u]|{id_{\underline{n}}} \\

2068:  {\underline{1+n}} \ar[uu]^{id_{\underline{1}}\otimes f} &

2069:  {\underline{1+n}} \ar[u]|{\gamma_{\underline{1},\underline{n}}} \ar[l]^{id_{\underline{1+n}}} &

2070:  {\underline{1+n}} \ar[u]|{id_{\underline{1+n}}} \ar[l]^{id_{\underline{1+n}}}&

2071:  {\underline{2n}} \ar[u]|{id_{\underline{2n}}} \ar[l]^{f\otimes id_{\underline{n}}} &

2072:  {\underline{n}} \ar[u]|{id_{\underline{n}}}\ar[l]|{\nabla_{\underline{n}}}

2073: }$

2074: \end{center}

2075: \caption{How to compose the cell $\hat{D}'_f$.}

2076: \protect\label{exffig}

2077: \end{figure}

2078: 

2079:  We hope that the few examples above can help the reader in

2080:  understanding the compositional mechanism of basic cells, as it will

2081:  be especially useful in Section~\ref{TSLPsec}.

2082: 

2083:  For instance, we can state a few technical lemmata that can be proved

2084:  by tile pastings similar to the cell compositions discussed above. As

2085:  a shorthand, for any two cells

2086:  $A\from\cell{t}{u}{id_{\underline{n}}}{id_{\underline{n}}}$ and

2087:  $B\from\cell{s}{v}{id_{\underline{m}}}{id_{\underline{m}}}$ with $s,v\from

2088:  \underline{n} \to \underline{m}$, we denote by $A\lhd B$ the

2089:  composition $(A*1^s)\cdot B = (A\cdot 1_v)*B$.

2090: 

2091: 

2092: \begin{lemma}\label{lemma1}

2093:  Given any arrow $t\from\underline{n}\to\underline{m}\in

2094:  \mathbf{Th}[\Sigma]$ that can be obtained without using dischargers,

2095:  the cell $\cell{t}{t}{id_{\underline{n}}}{id_{\underline{n}}}$ can be

2096:  generated by $\mathcal{B}(\Sigma)$.

2097: \end{lemma}

2098: 

2099: \begin{proof}

2100:  By hypothesis, the arrow $t$ can be expressed as the parallel and

2101:  sequential composition of arrows in $\Sigma \cup

2102:  \{\gamma_{\underline{1},\underline{1}}, \nabla_{\underline{1}},

2103:  id_{\underline{1}}\}$; therefore, by functoriality of tensor product,

2104:  $t$ can be finitely decomposed as

2105:  $\sigma_1;\sigma_2;\cdots;\sigma_l$ where $\sigma_i =

2106:  id_{\underline{k_i}} \otimes t_i \otimes id_{\underline{m_i}}$, with

2107:  $t_i\in \Sigma \cup \{\gamma_{\underline{1},\underline{1}},

2108:  \nabla_{\underline{1}}, id_{\underline{1}}\}$. Then, the cell

2109:  $\cell{t}{t}{id_{\underline{n}}}{id_{\underline{n}}}$ is just the

2110:  (diagonal) composition $A_1\lhd A_2 \lhd \ldots \lhd A_l$, with $A_i

2111:  = 1_{\underline{k_i}} \otimes R_{t_i} \otimes 1_{\underline{m_i}}$.

2112: \end{proof}

2113: 

2114:  Note that by adding the cells $R_f$ just for the operators of the

2115:  signature, then we are able to construct the analogous cells for

2116:  generic contexts $t$.

2117: 

2118: \begin{lemma}

2119:  Given any arrows $t\from\underline{h}\to\underline{k}$ and

2120:  $s\from\underline{m}\to\underline{n}$ in $\mathbf{Th}[\Sigma]$, the

2121:  cells

2122:  $\cell{t\otimes s}{\gamma_{\underline{n},\underline{k}}}

2123:        {\gamma_{\underline{m},\underline{h}}}{s\otimes t}$

2124:  and

2125:  $\cell{\gamma_{\underline{n},\underline{k}}}{t\otimes

2126:  s}{s\otimes t}{\gamma_{\underline{m},\underline{h}}}$

2127:  can be generated by $\mathcal{B}(\Sigma)$.

2128: \end{lemma}

2129: \begin{proof}

2130:  By Lemma \ref{lemma1}, we know that the cells

2131:  $A=\cell{\gamma_{\underline{n},\underline{k}}}

2132:  {\gamma_{\underline{n},\underline{k}}}

2133:  {id_{\underline{n+k}}}

2134:  {id_{\underline{n+k}}}$ and

2135:  $B=\cell{\gamma_{\underline{h},\underline{m}}}

2136:  {\gamma_{\underline{h},\underline{m}}}

2137:  {id_{\underline{h+m}}}

2138:  {id_{\underline{h+m}}}$

2139:  are generated by the basis $\mathcal{B}$.

2140:  By vertically composing $B$ with the horizontal identity

2141:  of $\gamma_{\underline{m},\underline{h}}$, we get the cell

2142:  $C = B\cdot 1_{\gamma_{\underline{m},\underline{h}}}

2143:  \from \cell

2144:  {\gamma_{\underline{h},\underline{m}}}

2145:  {id_{\underline{m+h}}}

2146:  {\gamma_{\underline{m},\underline{h}}}

2147:  {id_{\underline{m+h}}}$. Then, the

2148:  cell  $\cell{t\otimes s}{\gamma_{\underline{n},\underline{k}}}

2149:        {\gamma_{\underline{m},\underline{h}}}{s\otimes t}$

2150:  is obtained as the composition $A*1^{s\otimes t}*C$,

2151:  because $\gamma_{\underline{h},\underline{m}};(s\otimes

2152:  t);\gamma_{\underline{n},\underline{k}} = t\otimes s$.

2153:  The cell $\cell{\gamma_{\underline{n},\underline{k}}}{t\otimes

2154:  s}{s\otimes t}{\gamma_{\underline{m},\underline{h}}}$

2155:  can be generated by a similar construction.

2156: \end{proof}

2157: 

2158:  The second part of the previous lemma is an instance of a

2159:  more general result.

2160: 

2161: \begin{lemma}\label{pbduallemma}

2162:  If the cell $\cell{s}{u}{v}{t}$ is generated by the basis

2163:  $\mathcal{B}(\Sigma)$, then also the cell $\cell{u}{s}{t}{v}$

2164:  does.

2165: \end{lemma}

2166: \begin{proof}

2167:  Obvious, by observing that the property holds for all cells in

2168:  $\mathcal{B}(\Sigma)$ except $D_\nabla$, for which however

2169:  we have shown how to generate its counterpart

2170:  $\hat{D}_\nabla$.

2171: \end{proof}

2172: 

2173: \begin{lemma}\label{lemmanabla}

2174:  Given any arrow $t\from\underline{m}\to\underline{n}\in

2175:  \mathbf{Th}[\Sigma]$ that can be obtained without using dischargers,

2176:  the cells

2177:  $\cell{\nabla_{\underline{n}}}{t\otimes

2178:  t}{t}{\nabla_{\underline{m}}}$ and $\cell{t\otimes

2179:  t}{\nabla_{\underline{n}}}{\nabla_{\underline{m}}}{t}$ can be

2180:  obtained by composition of basic cells.

2181: \end{lemma}

2182: 

2183: 

2184: \begin{theorem}

2185:  The basis $\mathcal{B}(\Sigma)$ generates all and only pullback squares

2186:  of $\mathbf{Th}[\Sigma]$.

2187: \end{theorem}

2188: 

2189: \begin{proof}

2190:  The fact that all composed cells are pullbacks is

2191:  straightforward, as all basic tiles are pullbacks and such a

2192:  property is preserved by the three operations of the tile model

2193:  (horizontal and vertical sequential compositions and parallel

2194:  composition).

2195: 

2196:  The proof that all pullbacks can be obtained in this way is more

2197:  subtle. We exploit the fact that, in the category

2198:  $\mathbf{Th}[\Sigma]$, whenever the pullback of $\sigma$ and $\theta$

2199:  exists and $\sigma$ can be decomposed as $\sigma_1;\sigma_2$, then

2200:  also the pullback of $\sigma_2$ and $\theta$ exists (because

2201:  $\sigma_2$ is less instantiated than $\sigma$). Since each arrow

2202:  $\sigma$ in $\mathbf{Th}[\Sigma]$ can be finitely decomposed as

2203:  $\sigma_1;\sigma_2;\cdots;\sigma_n$ where $\sigma_i =

2204:  id_{\underline{k_i}} \otimes t_i \otimes id_{\underline{m_i}}$, with

2205:  $t_i\in \Sigma \cup \{\gamma_{\underline{1},\underline{1}},

2206:  \nabla_{\underline{1}},!_{\underline{1}}, id_{\underline{1}}\}$, then

2207:  the pullback of $\theta$ and $\sigma$, if it exists, can be computed

2208:  stepwise. In fact, the proof is by induction on the length $n$ of a

2209:  fixed decomposition of $\sigma$. Thus, it reduces to prove that if

2210:  the pullback of $\theta$ and $id_{\underline{k}} \otimes t \otimes

2211:  id_{\underline{m}}$ (with $t\in \Sigma \cup

2212:  \{\gamma_{\underline{1},\underline{1}},

2213:  \nabla_{\underline{1}},!_{\underline{1}}, id_{\underline{1}}\}$)

2214:  exists, then it is generated by $\mathcal{B}(\Sigma)$. We proceed by

2215:  case analysis on $t$ and, for each case, by induction on the length

2216:  of the decomposition of $\theta$, exploiting the besic cells in

2217:  $\mathcal{B}(\Sigma)$ to cover all possible combinations.

2218: \end{proof}

2219: 

2220: 

2221: \subsection{Pullbacks as tiles}\label{PATsec}

2222: 

2223:  The finitary presentation of pullbacks can be straightforwardly used

2224:  to build a tile system that generates the double category of pullbacks.

2225: 

2226: \begin{definition}[Tile system for pullbacks]

2227:  Given a signature $\Sigma$, we define the tile system

2228:  $\mathcal{R}_{\mathit{PB}(\Sigma)}$ such that its horizontal category is

2229:  $\textbf{Th}[\Sigma]^{\mathrm{op}}$, its vertical category is

2230:  $\textbf{Th}[\Sigma]^{\mathrm{op}}$ and the basic cells are those in

2231:  $\mathcal{B}(\Sigma)$ (see Figure~\ref{basicpbkfig} and

2232:  remember that horizontal and vertical

2233:  identity tiles will be freely generated in the model).

2234: \end{definition}

2235: 

2236:  The representation theorem can then be rephrased as below.

2237: 

2238: \begin{theorem}

2239:  A cell $\cell{t}{u}{v}{s}$ is in $\mathscr{P}(\mathcal{C})$ if and

2240:  only if $\mathcal{R}_{\mathit{PB}(\Sigma)} \vdash \cell{t}{u}{v}{s}$.

2241: \end{theorem}

2242: 

2243: \section{Tile systems for logic programs}\label{TSLPsec}

2244: 

2245:  The idea is to transform a logic program into a tile system which is

2246:  able to compute the same computed answer substitutions for each

2247:  goal. To this aim, we will exploit the tiles presented for building

2248:  pullbacks in the category of substitutions, which provide the

2249:  unification mechanism for goal resolution.

2250: 

2251: \subsection{From logic programs to a logic of tiles}\label{FLPTLTsec}

2252: 

2253:  The tile system that we propose can be

2254:  sketched as follows:

2255: 

2256: \begin{definition}[Tile system for logic programming]

2257:  Given a pure logic program $\mathcal{P}$ on the alphabet $\Sigma$, we

2258:  denote by $\mathcal{R}_{\mathcal{P}}$ the tile system specified by

2259:  the following rules:

2260: \begin{itemize}

2261: \item

2262:  There are two basic sorts $\mathsf{t}$ (for terms) and

2263:  $\mathsf{p}$ (for predicates). Correspondingly, the interfaces

2264:  are elements of $\{\mathsf{t},\mathsf{p}\}^*$ (as a matter of

2265:  notation, we let $\epsilon$ denote the empty string of sorts,

2266:  and denote by $\mathsf{t}^n$ the string composed by $n$

2267:  occurrences of $\mathsf{t}$, and similarly for $\mathsf{p}$).

2268: 

2269: \item

2270:  To each functional symbol $f$ with arity $n$ in the alphabet, we

2271:  associate an operator $\dfun{f}{\mathsf{t}^n}{\mathsf{t}}$ in the

2272:  signature of configurations, and to each predicate symbol $p$ (here

2273:  $\Box$ can be viewed as a nullary predicate) with arity $k$ in the

2274:  alphabet, we associate an operator

2275:  $\dfun{p}{\mathsf{t}^k}{\mathsf{p}}$ in the signature of

2276:  configurations. Then, we add the symbol $\_\wedge\_ \from

2277:  \mathsf{p}^2 \to \mathsf{p}$ for modeling conjunction. (We will show

2278:  that, without loss of generality, the conjunction operator can be

2279:  more conveniently defined to be associative and with unit

2280:  $\Box$.) The configurations are the arrows (of the op-category) of the

2281:  free cartesian category generated by the signature of configurations.

2282: 

2283: \item

2284:  To each functional symbol $f$ with arity $n$ in the alphabet, we

2285:  associate an operator $\dfun{f}{\mathsf{t}^n}{\mathsf{t}}$ in the

2286:  signature of observations (note that the symbol $f$ is thus

2287:  overloaded, since it also appears in the horizontal

2288:  dimension;

2289:  however, this will not create any confusion).  Then, the

2290:  observations are the arrows (of the op-category) of the free

2291:  cartesian category generated by the signature of observations.

2292: 

2293: \item

2294:  To each clause

2295: \[

2296:  c \mathrel{\equiv} p(t_1,\ldots,t_k)\ \mathrel{:-}\

2297:                     q_1(\vec{s}_1),\ldots,q_m(\vec{s}_m)

2298: \]

2299: \noindent

2300:  (over $n$ variables $\{x_1,\ldots,x_n\}$) in the logic program we

2301:  associate a basic tile $T_c$ in our system whose initial

2302:  configuration is $\dfun{p}{\mathsf{t}^k}{\mathsf{p}}$ (representing

2303:  the predicate symbol in the head of $c$), whose final

2304:  configuration is $\dfun{ q_1(\vec{s}_1)\wedge\ldots\wedge

2305:  q_m(\vec{s}_m)}{\mathsf{t}^n}{\mathsf{p}}$ (representing the body of

2306:  the clause), whose trigger is the identity

2307:  $\dfun{id_{\mathsf{p}}}{\mathsf{p}}{\mathsf{p}}$ and whose effect is

2308:  the tuple $\dfun{\langle

2309:  t_1,\ldots,t_k\rangle}{\mathsf{t}^n}{\mathsf{t}^k}$ (representing the

2310:  pattern to be matched by the arguments of predicate $p$). Note that

2311:  the body of the clause may contain variables not appearing in the

2312:  head (\ie, some of the $x_i$'s might not appear in the $t_i$'s) and

2313:  consequently some discharger will be used in the effect of the

2314:  tile. Moreover, since the same variable can be used more than once,

2315:  duplicators can also be necessary (this is to remark the difference

2316:  between the tupling

2317:  $\langle t_1,\ldots,t_k\rangle$ and the tensorial product $t_1\otimes

2318:  \cdots\otimes t_k$, as the former involves duplicators for

2319:  expressing variable sharing).

2320:  Since we take the op-categories the direction of all arrows is

2321:  reversed \wrt\ the standard representation (see the tile $T_c$ in

2322:  Figure~\ref{genclausetile}).

2323: 

2324: \item

2325:  Finally, we add the basic tiles contained in

2326:  $\mathcal{R}_{\mathit{PB}(\Sigma)}$ (see Figure~\ref{basicpbkfig}) for

2327:  building pullbacks. We recall that just three of them depend on the alphabet

2328:  under consideration, while the other three are common to all

2329:  programs, \ie, they can be considered auxiliary to the framework.

2330: \end{itemize}

2331: \end{definition}

2332: 

2333: \begin{remark}

2334:  When it is obvious from the context, we shall abuse the notation by

2335:  avoiding to specify the involved sorts in the subscripts of $id$,

2336:  $\nabla$, $\gamma$ and $!$, writing just the numbers of involved

2337:  arguments (\eg, instead of $\gamma_{\mathsf{tp},\mathsf{p}}$ we shall

2338:  write $\gamma_{\underline{2},\underline{1}}\from \mathsf{tpp} \to

2339:  \mathsf{ptp}$).

2340: \end{remark}

2341: 

2342: \begin{figure}[t]

2343: \begin{center}

2344: $\xymatrix@C=2cm{

2345:  {\mathsf{p}} \ar@{}[rd]|{T_c} &

2346:  {\mathsf{t}^k} \ar[l]_{p} \\

2347:  {\mathsf{p}} \ar[u]^{id} &

2348:  {\mathsf{t}^n} \ar[l]^{q_1(\vec{s}_1)\wedge\ldots\wedge q_m(\vec{s}_m)}

2349:                 \ar[u]_{\langle t_1,\ldots,t_k\rangle}

2350: }$

2351: \end{center}

2352: \caption{}

2353: \protect\label{genclausetile}

2354: \end{figure}

2355: 

2356:  We can assume the operator $\wedge$ to be associative and with unit

2357:  $\Box$ because all the basic tiles associated to the clauses have an

2358:  identity as trigger. This, together with the fact that they are the

2359:  only rewrite rules involving predicate symbols, means that rewrites

2360:  are always enabled for predicates nested in conjunctions. For example

2361:  in the expression $q_1(\vec{s}_1)\wedge\ldots\wedge q_m(\vec{s}_m)$

2362:  it is not important the way in which the $q_i$'s are conjoined, as

2363:  their evolutions do not interact with the `tree' of

2364:  conjunctions. Thus, $q_0 \wedge (q_1 \wedge q_2)$ is equivalent to

2365:  $(q_0 \wedge q_1) \wedge q_2$. Moreover,  we make the special symbol $\Box$

2366:  be the unit for $\wedge$. These assumptions do not

2367:  alter the `behavior' of the system, but allow us to simplify the

2368:  notation and the presentation of main results.

2369: 

2370:  The intuition is that for each goal, we can compute a refutation in the

2371:  tile system by starting from the associated configuration and

2372:  constructing a tile whose final configuration is the empty

2373:  goal (possibly in parallel with some dischargers that act

2374:  as placeholders for the free variables in the computed answer

2375:  substitution), \ie, the final configurations must have the

2376:  form $\Box\otimes !_{\underline{n}}$ (without monoidality of

2377:  $\wedge$ we should have considered as final configurations

2378:  for termination any possible finite conjunction of empty

2379:  goals). The effect of such a tile corresponds to the computed answer

2380:  substitution.  The tiles with initial input interface $\mathsf{p}$

2381:  and final configuration $\Box\otimes !_{\underline{n}}$ for $n\in

2382:  \nat$ are called \emph{refutation tiles}.

2383: 

2384:  The following example should illustrate how the tile system can

2385:  simulate logic programming computations.

2386: 

2387: \begin{figure}[t]

2388: \hrule \ \\

2389:  \centerline{Program clauses translation.}

2390: \begin{center}

2391: $\vcenter{\xymatrix@C=2cm{

2392:  {\mathsf{p}} \ar@{}[rd]|{T_{c_1}} &

2393:  {\mathsf{t}^2} \ar[l]_{p} \\

2394:  {\mathsf{p}} \ar[u]^{id} &

2395:  {\mathsf{t}^2} \ar[l]^{(\nabla_{\underline{1}}\otimes

2396:                          id_{\underline{1}});

2397:                         (q \otimes r);\wedge}

2398:                 \ar[u]_{f\otimes id_{\underline{1}}}

2399: }}$

2400: \hfill

2401: $\vcenter{\xymatrix@C=2cm{

2402:  {\mathsf{p}} \ar@{}[rd]|{T_{c_2}} &

2403:  {\mathsf{t}^2} \ar[l]_{r} \\

2404:  {\mathsf{p}} \ar[u]^{id} &

2405:  {\epsilon} \ar[l]^{\Box} \ar[u]_{a\otimes a}

2406: }}$

2407: \hfill

2408: $\vcenter{\xymatrix@C=2cm{

2409:  {\mathsf{p}} \ar@{}[rd]|{T_{c_3}} &

2410:  {\mathsf{t}^1} \ar[l]_{q} \\

2411:  {\mathsf{p}} \ar[u]^{id} &

2412:  {\epsilon} \ar[l]^{\Box} \ar[u]_{b}

2413: }}$

2414: \end{center}

2415: \hrule \ \\ \ \\

2416: \centerline{Auxiliary pullback tiles associated to the signature.}

2417: \begin{center}

2418: $\vcenter{\xymatrix@C-1pc{

2419:  {\mathsf{t}} \ar@{}[rd]|{R_a} &

2420:  {\epsilon} \ar[l]_{a} \\

2421:  {\epsilon} \ar[u]^{a} &

2422:  {\epsilon} \ar[l]^{id_{\underline{0}}} \ar[u]_{id_{\underline{0}}} }}$

2423: \hfill

2424:  $\vcenter{\xymatrix@C-1pc{

2425:  {\mathsf{t}^2} \ar@{}[rd]|{D_a} &

2426:  {\mathsf{t}} \ar[l]_{a\otimes id_{\underline{1}}} \\

2427:  {\mathsf{t}} \ar[u]^{\nabla_{\underline{1}}} &

2428:  {\epsilon} \ar[l]^{a} \ar[u]_{a} }}$

2429: \hfill $\vcenter{\xymatrix@C-1pc{

2430:  {\mathsf{t}^2} \ar@{}[rd]|{\hat{D}_a} &

2431:  {\mathsf{t}} \ar[l]_{\nabla_{\underline{1}}} \\

2432:  {\mathsf{t}} \ar[u]^{a\otimes id_{\underline{1}}} &

2433:  {\epsilon} \ar[l]^{a} \ar[u]_{a} }}$

2434: \hfill

2435: $\vcenter{\xymatrix@C-1pc{

2436:  {\mathsf{t}} \ar@{}[rd]|{R_b} &

2437:  {\mathsf{t}} \ar[l]_{b} \\

2438:  {\mathsf{t}} \ar[u]^{b} &

2439:  {\epsilon} \ar[l]^{id_{\underline{0}}} \ar[u]_{id_{\underline{0}}} }}$

2440: \hfill

2441:  $\vcenter{\xymatrix@C-1pc{

2442:  {\mathsf{t}^2} \ar@{}[rd]|{D_b} &

2443:  {\mathsf{t}} \ar[l]_{b\otimes id_{\underline{1}}} \\

2444:  {\mathsf{t}} \ar[u]^{\nabla_{\underline{1}}} &

2445:  {\epsilon} \ar[l]^{b} \ar[u]_{b} }}$

2446: \hfill

2447: $\vcenter{\xymatrix@C-1pc{

2448:  {\mathsf{t}^2} \ar@{}[rd]|{\hat{D}_b} &

2449:  {\mathsf{t}} \ar[l]_{\nabla_{\underline{1}}} \\

2450:  {\mathsf{t}} \ar[u]^{b\otimes id_{\underline{1}}} &

2451:  {\epsilon} \ar[l]^{b} \ar[u]_{b} }}$

2452: \end{center}

2453: \begin{center}

2454: $\vcenter{\xymatrix{

2455:  {\mathsf{t}} \ar@{}[rd]|{R_f} &

2456:  {\mathsf{t}} \ar[l]_{f} \\

2457:  {\mathsf{t}} \ar[u]^{f} &

2458:  {\mathsf{t}} \ar[l]^{id_{\underline{1}}} \ar[u]_{id_{\underline{1}}} }}$

2459: \hfill

2460:  $\vcenter{\xymatrix{

2461:  {\mathsf{t}^2} \ar@{}[rd]|{D_f} &

2462:  {\mathsf{t}^2} \ar[l]_{f\otimes id_{\underline{1}}} \\

2463:  {\mathsf{t}} \ar[u]^{\nabla_{\underline{1}}} &

2464:  {\mathsf{t}} \ar[l]^{f}

2465:                  \ar[u]_{\nabla_{\underline{1}};

2466:                          (id_{\underline{1}}\otimes f)} }}$

2467: \hfill $\vcenter{\xymatrix@C+1pc{

2468:  {\mathsf{t}^2} \ar@{}[rd]|{\hat{D}_f} &

2469:  {\mathsf{t}} \ar[l]_{\nabla_{\underline{1}}} \\

2470:  {\mathsf{t}^2} \ar[u]^{f\otimes id_{\underline{1}}} &

2471:  {\mathsf{t}} \ar[l]^{\nabla_{\underline{1}};

2472:                          (id_{\underline{1}} \otimes f)}

2473:                  \ar[u]_{f} }}$

2474: \end{center}

2475: \hrule \ \\ \ \\

2476: \centerline{Auxiliary pullback tiles independent of the

2477: signature.}

2478: \begin{center}

2479: $\vcenter{\xymatrix{

2480:  {\mathsf{t}^2} \ar@{}[rd]|{R_\nabla} &

2481:  {\mathsf{t}} \ar[l]_{\nabla_{\underline{1}}} \\

2482:  {\mathsf{t}} \ar[u]^{\nabla_{\underline{1}}} &

2483:  {\mathsf{t}} \ar[l]^{id_{\underline{1}}} \ar[u]_{id_{\underline{1}}} }} $

2484: \hfill $\vcenter{\xymatrix{

2485:  {\mathsf{t}^2} \ar@{}[rd]|{R_\gamma} &

2486:  {\mathsf{t}^2} \ar[l]_{\gamma_{\underline{1},\underline{1}}} \\

2487:  {\mathsf{t}^2} \ar[u]^{\gamma_{\underline{1},\underline{1}}} &

2488:  {\mathsf{t}^2} \ar[l]^{id_{\underline{2}}} \ar[u]_{id_{\underline{2}}} }}$

2489: \hfill $\vcenter{\xymatrix{

2490:  {\mathsf{t}^3} \ar@{}[rd]|{D_\nabla} &

2491:  {\mathsf{t}^2} \ar[l]_{\nabla_{\underline{1}}\otimes id_{\underline{1}}} \\

2492:  {\mathsf{t}^2} \ar[u]^{id_{\underline{1}}\otimes \nabla_{\underline{1}}} &

2493:  {\mathsf{t}} \ar[l]^{\nabla_{\underline{1}}}

2494:                  \ar[u]_{\nabla_{\underline{1}}} }}$

2495: \end{center}

2496: \hrule

2497: \caption{The tile system associated to the logic program

2498: $\mathcal{P}$.} \protect\label{protilefig}

2499: \end{figure}

2500: 

2501: \begin{example}

2502:  Let us consider the simple

2503:  alphabet consisting of constants $a$ and $b$, unary function symbol

2504:  $f$, unary predicate $q$ and binary predicates $p$ and $r$.

2505: 

2506:  Given the logic program $\mathcal{P}$ defined by the three clauses

2507: 

2508: \begin{alltt}

2509:  \(c\sb{1} \equiv\) p(f(X1),X2) :-  q(X1), r(X1,X2).

2510:  \(c\sb{2} \equiv\) r(a,a).

2511:  \(c\sb{3} \equiv\) q(b).

2512: \end{alltt}

2513: 

2514: \noindent

2515:  the corresponding tile system is illustrated in

2516:  Figure~\ref{protilefig}. The tiles in the first row are those

2517:  associated to the three clauses of the program. The tiles in the

2518:  second row are the basic pullbacks associated to the constants $a$, $b$

2519:  of the alphabet, while the tiles in the third row are the basic

2520:  pullbacks associated to the unary function symbol $f$ of the

2521:  alphabet. The tiles in the fourth row are the auxiliary tiles common

2522:  to all representations of logic programs. Note that, once the

2523:  signature of terms is fixed, then all the auxiliary tiles

2524:  are fixed, and the tiles for representing the logic

2525:  program are in bijection with the clauses of the program.

2526: 

2527:  Now suppose one wants to compute the goal

2528:  $\mathrel{?-}\ p(x_1,x_2)$. The idea is to compute all possible tiles

2529:  that have $p\from \mathsf{t}^2 \to \mathsf{p}$ as initial

2530:  configuration and the empty goal as conclusion. The effect

2531:  of such tiles should in fact correspond to the computed answer

2532:  substitutions of the program execution on the given goal. It is easy

2533:  to argue that no such tile exists for the given goal. In fact, the

2534:  only tile having $p$ as initial configuration is $T_{c_1}$ that leads

2535:  to the configuration $(\nabla_{\underline{1}}\otimes

2536:  id_{\underline{1}});(q\otimes r);\wedge$. Then $T_{c_3}$ and

2537:  $T_{c_2}$ can be (concurrently) applied respectively to $q$ and to

2538:  $r$, but the computation cannot be completed, as the coordination of

2539:  the two resolutions is not possible. In fact the pullback of

2540:  $b\otimes a$ and $\nabla_{\underline{1}}$ does not exist, and hence

2541:  also the pullback of $b\otimes a\otimes a$ and

2542:  $(\nabla_{\underline{1}}\otimes id_{\underline{1}})$ does not exist

2543:  as well. The partial computation is illustrated in

2544:  Figure~\ref{partcompfig}.

2545: 

2546:  If the third clause $c_3$ is replaced by $c'_3 \equiv \mathtt{q(a)}$,

2547:  then we can compute the tile refutation illustrated in

2548:  Figure~\ref{compcompfig}, where the tile $\alpha\from

2549:  \cell{\nabla_{\underline{1}}}{a\otimes a}{a}{id_{\underline{0}}}$ can

2550:  be obtained in any of the two ways illustrated in

2551:  Figure~\ref{twowayfig}. The computed

2552:  answer substitution $f(a)\otimes a$ (representing

2553:  $[\sbtn{f(a)}{x_1},\sbtn{a}{x_2}]$) is given by the effect of the

2554:  composed tile. Note that $c'_3$ and $c_2$ can be applied concurrently, \ie,

2555:  the order in which they are applied is not relevant and moreover,

2556:  they can also be performed in parallel, their outputs being

2557:  coordinated by means of the tile $\alpha$. The two ways of building

2558:  $\alpha$ show that the coordination mechanism does not depend on the

2559:  order of execution of $T_{c'_3}$ and $T_{c_2}$, which is in fact

2560:  immaterial.

2561: \end{example}

2562: 

2563: \begin{figure}[t]

2564: \begin{center}

2565: $\vcenter{\xymatrix@C+1pc{

2566:  {\mathsf{p}} \ar@{}[rrrd]|{T_{c_1}} & & &

2567:  {\mathsf{t}^2} \ar[lll]_{p} \\

2568:  {\mathsf{p}} \ar[u]^{id} &

2569:  {\mathsf{p}^2} \ar[l]^{\wedge} &

2570:  {\mathsf{t}^3} \ar[l]^{q \otimes r} &

2571:  {\mathsf{t}^2} \ar[l]^{\nabla_{\underline{1}}\otimes

2572:                          id_{\underline{1}}}

2573:                 \ar[u]_{f\otimes id_{\underline{1}}} \\

2574:  {\mathsf{p}} \ar[u]^{id} &

2575:  {\mathsf{p}^2} \ar[l]^{\wedge} \ar[u]^{id}

2576:                 \ar@{}[ru]|{T_{c_3}\otimes T_{c_2}} &

2577:  {\epsilon} \ar[l]^{\Box \otimes \Box} \ar[u]_{b\otimes a\otimes a}

2578: }}$

2579: \end{center}

2580: \caption{The incomplete derivation for $p$.}

2581: \protect\label{partcompfig}

2582: \end{figure}

2583: 

2584: \begin{figure}[t]

2585: \begin{center}

2586: $\vcenter{\xymatrix@C+2pc{

2587:  {\mathsf{p}} \ar@{}[rrrd]|{T_{c_1}} & & &

2588:  {\mathsf{t}^2} \ar[lll]_{p} \\

2589:  {\mathsf{p}} \ar[u]^{id} &

2590:  {\mathsf{p}^2} \ar[l]^{\wedge} &

2591:  {\mathsf{t}^3} \ar[l]^{q \otimes r} &

2592:  {\mathsf{t}^2} \ar[l]^{(\nabla_{\underline{1}}\otimes

2593:                          id_{\underline{1}})}

2594:                 \ar[u]_{f\otimes id_{\underline{1}}} \\

2595:  {\mathsf{p}} \ar[u]^{id} &

2596:  {\mathsf{p}^2} \ar[l]^{\wedge} \ar[u]^{id}

2597:                 \ar@{}[ru]|{T_{c'_3}\otimes T_{c_2}} &

2598:  {\epsilon} \ar[l]^{\Box \otimes \Box} \ar[u]|{a\otimes a\otimes a}

2599:                 \ar@{}[ru]|{\alpha\otimes 1_a} &

2600:  {\epsilon} \ar[l]^{id_{\underline{0}}} \ar[u]_{a\otimes a}

2601: }}$

2602: \end{center}

2603: \caption{The refutation for $p$.}

2604: \protect\label{compcompfig}

2605: \end{figure}

2606: 

2607: \begin{figure}[t]

2608: \begin{center}

2609: $\vcenter{\xymatrix{

2610:  {\mathsf{t}^2} \ar@{}[rd]|{\hat{D}_a} &

2611:  {\mathsf{t}} \ar[l]_{\nabla_{\underline{1}}} \\

2612:  {\mathsf{t}} \ar[u]^{a\otimes id_{\underline{1}}} &

2613:  {\epsilon} \ar[l]^{a} \ar[u]_{a} \\

2614:  {\epsilon} \ar[u]^{a}

2615:                 \ar@{}[ru]|{R_a} &

2616:  {\epsilon} \ar[l]^{id_{\underline{0}}} \ar[u]_{id_{\underline{0}}}

2617: }}$

2618: \hspace{1cm}

2619: $\vcenter{\xymatrix{

2620:  {\mathsf{t}^2} \ar@{}[rd]|{\hat{D}'_a} &

2621:  {\mathsf{t}} \ar[l]_{\nabla_{\underline{1}}} \\

2622:  {\mathsf{t}} \ar[u]^{id_{\underline{1}}\otimes a} &

2623:  {\epsilon} \ar[l]^{a} \ar[u]_{a} \\

2624:  {\epsilon} \ar[u]^{a}

2625:                 \ar@{}[ru]|{R_a} &

2626:  {\epsilon} \ar[l]^{id_{\underline{0}}} \ar[u]_{id_{\underline{0}}}

2627: }}$

2628: \end{center}

2629: \caption{Two ways for composing the tile $\alpha$ of

2630:  Figure~\protect\ref{compcompfig}.}

2631: \protect\label{twowayfig}

2632: \end{figure}

2633: 

2634:  Notice that the use of tiles, thanks to its abstract flavour,

2635:  completely frees the user from managing fresh variables, taking

2636:  care in an automatic way of all the problems connected to name

2637:  handling via the use of local placeholders.

2638: 

2639: \subsection{From clauses to tiles}\label{FCTTsec}

2640: 

2641:  We try to explain here informally the intuition that lies behind the

2642:  definition of $\mathcal{R}_{\mathcal{P}}$. Basically, it is strictly

2643:  related to the idea of building an \textsc{lts} out of a reduction

2644:  system to study the interactions between composed components. From

2645:  one point of view, it is evident that the reduction system of goal

2646:  resolution summarized in Section~\ref{OSsec} considers the whole goal

2647:  as an atomic entity, whose parts must all be coordinated. From this

2648:  point of view, the clauses define the basic reduction steps that can

2649:  be conveniently instantiated and contextualized. Indeed, the

2650:  reduction perspective of logic programs has been investigated in

2651:  \cite{CM:ASSTS}. However, to accomplish this view, one usually

2652:  assumes to start with a set of variables large enough to contain all

2653:  names that will be needed by all clause instances used in the

2654:  refutation, as their dynamic creation cannot be modeled. This is a

2655:  very strong assumption that somehow clashes against the desirable

2656:  constructive presentation of computation, where fresh

2657:  variables can be introduced by need.

2658: 

2659:  In \cite{Sew:RRBC,LM:DBCRS} it is suggested that instead of studying

2660:  the behavior of a process in all possible contexts, the basic

2661:  reduction rules of the system can be used to catch the least set of

2662:  contexts that should be considered. This is obtained by considering

2663:  all subterms of the sources of reduction rules. For example, if a

2664:  reduction rewrites $f(g(a))$ to $h(b)$, then the essential contexts

2665:  are $f(\_)$ and $f(g(\_))$, but not $h(\_)$, because only by

2666:  embedding a term within these contexts a reduction may happen (unless

2667:  it is already enabled inside the term itself). Unfortunately, this

2668:  task is hard to accomplish in general, as the reduction semantics for

2669:  process calculi usually impose suitable structural axioms on the

2670:  processes. Nevertheless, the presence of sufficiently many

2671:  \emph{relative pushouts} in the category of states is enough for

2672:  guaranteeing that the universal constructions exist \cite{LM:DBCRS}.

2673: 

2674:  For logic programming, the problem of contextualization is reversed

2675:  to the problem of instantiation, and we know in advance what are the

2676:  interesting `internal' contexts, namely the pullback

2677:  projections. This allows us to transform all clauses (seen as

2678:  reduction rules) by moving as much internal context as possible to

2679:  the observational part: We separate the topmost operator of the head

2680:  of the clause (\ie, the

2681:  predicate symbol) from its arguments (that are moved to the observational

2682:  part, \ie, the effect of the tile) and

2683:  then the basic pullbacks allow us to build incrementally all the

2684:  other decompositions (in particular, we are speaking about tiles

2685:  $R_f$, $R_\nabla$ and $R_\gamma$).

2686: 

2687: \begin{proposition}\label{pt1t2prop}

2688:  For each tile $T_c\from \cell{p}{id}{t}{G}$ and all arrows $t_1,t_2$

2689:  such that $t = t_1;t_2$ (with $t_2$ not involving dischargers), then

2690:  the tile $\cell{t_2;p}{id}{t_1}{G}$ is entailed by

2691:  $\mathcal{R}_{\mathcal{P}}$.

2692: \end{proposition}

2693: \begin{proof}

2694:  The proof follows from Lemma~\ref{lemma1}, \ie, from the existence of

2695:  the tile $\cell{t_2}{t_2}{id}{id}$ that can be vertically composed

2696:  with $\cell{id}{t_1}{t_1}{id}$ (the horizontal identity for $t_1$),

2697:  and with $T_c$ being horizontally composed with the result (see

2698:  Figure~\ref{pt1t2fig}).

2699: \end{proof}

2700: 

2701: 

2702: \begin{figure}[t]

2703: \begin{center}

2704: $\xymatrix{

2705:  {\mathsf{p}} \ar@{}[rdd]|{T_c} &

2706:  {\mathsf{t}^k} \ar[l]_{p} &

2707:  {\mathsf{t}^m} \ar[l]_{t_2} \\

2708:  & {\mathsf{t}^m} \ar[u]_{t_2} &

2709:  {\mathsf{t}^m} \ar[l]|{id_{\underline{m}}} \ar[u]_{id_{\underline{m}}} \\

2710:  {\mathsf{p}} \ar[uu]^{id_{\underline{1}}} &

2711:  {\mathsf{t}^n} \ar[l]^{G} \ar[u]_{t_1} &

2712:  {\mathsf{t}^n} \ar[l]^{id_{\underline{n}}} \ar[u]_{t_1} }$

2713: \end{center}

2714: \caption{Graphical proof of Proposition~\protect\ref{pt1t2prop}.}

2715: \protect\label{pt1t2fig}

2716: \end{figure}

2717: 

2718: \begin{example}

2719:  Let us consider the simple program

2720: 

2721: \begin{alltt}

2722:  \(c\sb{1} \equiv\) sum(0,X1,X1).

2723:  \(c\sb{2} \equiv\) sum(s(X1),X2,s(X3)) :- sum(X1,X2,X3).

2724: \end{alltt}

2725: 

2726: \noindent

2727:  over the signature consiting of constant $0$, unary symbol $s$ and

2728:  ternary predicate symbol $\mathit{sum}$. The possible interactive

2729:  decompositions of the heads of the two clauses are:

2730: \begin{itemize}

2731: \item

2732:  for $c_1$: (1) $\mathit{sum}(0,x_1,x_2)$ with observation

2733:  $\nabla_{\underline{1}}$, (2) $\mathit{sum}(x_1,x_2,x_2)$ with

2734:  observation $0\otimes id_{\underline{1}}$, (3)

2735:  $\mathit{sum}(x_1,x_2,x_3)$ with observation

2736:  $0\otimes\nabla_{\underline{1}}$, and (4) $\mathit{sum}(0,x_1,x_1)$

2737:  with observation $id_{\underline{1}}$;

2738: 

2739: \item

2740:  for $c_2$: (1) $\mathit{sum}(s(x_1),x_2,x_3)$ with observation

2741:  $id_{\underline{2}}\otimes s$, (2) $\mathit{sum}(x_1,x_2,s(x_3))$

2742:  with observation $s\otimes id_{\underline{2}}$, (3)

2743:  $\mathit{sum}(x_1,x_2,x_3)$ with observation $s\otimes

2744:  id_{\underline{1}} \otimes s$, and finally (4)

2745:  $\mathit{sum}(s(x_1),x_2,s(x_3))$ with observation

2746:  $id_{\underline{3}}$.

2747: \end{itemize}

2748: 

2749: \noindent

2750:  Although the basic tiles of the tile system associated to the program

2751:  just consider decompositions of kind (3), which are the most

2752:  general, by parallel and sequential composition with (basic)

2753:  pullback tiles, the tile logic associated to the tile system will

2754:  entail all the other decompositions.

2755: \end{example}

2756: 

2757:  Note that tiles allow one to move contexts along states and

2758:  observations in a very natural and uniform way.

2759:  The interactivity of the tile representation relies on the fact that

2760:  the effects of basic tiles associated to the clauses must be accepted

2761:  by the current instantiation of the matched predicate in the goal,

2762:  otherwise the step cannot take place.

2763: 

2764: \begin{theorem}[Correspondence between (SLD-)derivations and tiles]

2765: \label{reptheo}

2766:  Let $\mathcal{P}$ be a logic program and $G$ a goal. Then,

2767: \begin{enumerate}

2768: \item

2769:  if $\mathcal{P}\vvdash G \Rightarrow_{\sigma} G'$, then

2770:  $\mathcal{R}_{\mathcal{P}}\vdash \cell{G}{id}{\theta}{G'}$ with

2771:  $\theta=\sigma_{|\mathit{Var}(G)}$;

2772: 

2773: \item

2774:  if $\mathcal{R}_{\mathcal{P}}\vdash \cell{G}{id}{\theta}{G'}$, then

2775:  there exists $\sigma$ with $\theta=\sigma_{|\mathit{Var}(G)}$ such

2776:  that $\mathcal{P}\vvdash G \Rightarrow^*_{\sigma} G'$.

2777: \end{enumerate}

2778: \end{theorem}

2779: 

2780: \begin{proof}

2781:  The proof of point 1 proceeds by rule induction. For the `empty goal'

2782:  rules we rely on the fact that $\Box$ is the unit for $\wedge$

2783:  and that the vertical identities always exist. For the `atomic goal'

2784:  we rely on the results of Section~\ref{RVPsec} on the correspondence

2785:  between mgu's and pullbacks while applying the tile $T_{H

2786:  \mathrel{:-} F}$ to the goal $A$. For the `conjunctive goal' rules,

2787:  the difficulty is that $G$ and $G'$ might share some variables. In

2788:  fact, by inductive hypothesis we can assume that

2789:  $\mathcal{R}_{\mathcal{P}}\vdash \cell{G}{id}{\sigma}{F}$ and

2790:  therefore we must employ the pullback tiles for propagating $\sigma$

2791:  to $G'$. This can be done by exploiting the tiles $\hat{D}_f$ and

2792:  $D_{\nabla}$.

2793: 

2794:  For proving the point 2, we fix a decomposition of

2795:  $\cell{G}{id}{\theta}{G'}$ in terms of basic tiles of

2796:  $\mathcal{R}_{\mathcal{P}}$ and then we proceed by induction on the

2797:  number of tiles $T_c$ used for building $\cell{G}{id}{\theta}{G'}$.

2798: \end{proof}

2799: 

2800:  Note that a tile can represent in general a whole sequence of derivation

2801:  steps.

2802: 

2803: \begin{corollary}

2804:   Let $\mathcal{P}$ be a logic program and $G$ a goal. Then,

2805: \begin{enumerate}

2806: \item

2807:  if $\mathcal{P}\vdash_\sigma G$, then

2808:  $\mathcal{R}_{\mathcal{P}}\vdash \cell{G}{id}{\theta}{\Box \otimes

2809:  !_{\underline{n}}}$ with $\theta=\sigma_{|\mathit{Var}(G)}$ and $n$

2810:  the number of free variables in $\theta$;

2811: 

2812: \item

2813:  if $\mathcal{R}_{\mathcal{P}}\vdash \cell{G}{id}{\theta}{\Box \otimes

2814:  !_{\underline{n}}}$, then

2815:  there exists $\sigma$ with

2816:  $\theta=\sigma_{|\mathit{Var}(G)}$ such

2817:  that $\mathcal{P}\vdash_\sigma G$.

2818: \end{enumerate}

2819: \end{corollary}

2820: 

2821: \subsection{Recovering ordinary semantics}\label{ROSsec}

2822: 

2823:  From the tile system $\mathcal{R}_{\mathcal{P}}$ we are able to recover

2824:  several well-known semantics for logic programs.

2825: 

2826: \begin{itemize}

2827: \item

2828:  The \emph{least Herbrand model}, which gives the ordinary

2829:  model-theoretic semantics for logic programs \cite{EK:SPLPL}, is

2830:  given by refutation tiles whose initial configuration is a ground

2831:  atomic goal:

2832: 

2833: \[

2834:  \mathrm{Op}_1(\mathcal{P}) =

2835:  \{ A\from \epsilon \to \mathsf{p} \mid

2836:  \mathcal{R}_{\mathcal{P}}\vdash

2837:  \cell{A}

2838:       {id_{\underline{1}}}

2839:       {!_{\underline{n}}}

2840:       {\Box\otimes !_{\underline{n}}} \}.

2841: \]

2842: 

2843: \item

2844:  The \emph{correct answer substitutions} are given by the instances of

2845:  initial configurations of refutation tiles that are (possibly

2846:  non-ground) atomic goals:

2847: 

2848: \[

2849:  \mathrm{Op}_2(\mathcal{P}) =

2850:  \{ A\from \mathsf{t}^k \to \mathsf{p} \mid

2851:  \mathcal{R}_{\mathcal{P}}\vdash

2852:  \cell{A}

2853:       {id_{\underline{1}}}

2854:       {id_{\underline{k}} \otimes !_{\underline{k+n}}}

2855:       {\Box\otimes !_{\underline{n}}} \}.

2856: \]

2857: 

2858: \item

2859:  The \emph{computed answer substitutions}, which define a useful

2860:  semantic framework for addressing compositionality, concrete

2861:  observables and program analysis \cite{FLMP:DMOBLL,BGLM:SSA}, can be

2862:  immediately obtained by considering the refutation tiles with a

2863:  single predicate as initial configuration:

2864: 

2865: \[

2866:  \mathrm{Op}_3(\mathcal{P}) =

2867:  \{ \theta;p\from \mathsf{t}^k \to \mathsf{p} \mid

2868:  p\in\Sigma_{\Pi},\

2869:  \mathcal{R}_{\mathcal{P}}\vdash

2870:  \cell{p}

2871:       {id_{\underline{1}}}

2872:       {\theta\otimes !_{\underline{n}}}

2873:       {\Box\otimes !_{\underline{k+n}}} \}.

2874: \]

2875: 

2876: \item

2877:  The \emph{resolvents} can be obtained by considering also non

2878:  refutation tiles:

2879: 

2880: \[

2881:  \mathrm{Op}_4(\mathcal{P}) =

2882:  \{ (\theta;p,G) \mid

2883:  p\in\Sigma_{\Pi},\

2884:  \mathcal{R}_{\mathcal{P}}\vdash

2885:  \cell{p}

2886:       {id_{\underline{1}}}

2887:       {\theta}

2888:       {G} \}.

2889: \]

2890: \end{itemize}

2891: 

2892:  All the correspondences above follow as easy corollaries to the

2893:  representation Theorem~\ref{reptheo}.

2894: 

2895: \subsection{Goal compositionality}\label{GCsec}

2896: 

2897:  Though compositionality issues for the classical semantics have been

2898:  extensively studied in the literature, we want to focus here on

2899:  compositionality of goals \wrt\ the two main operations discussed in

2900:  the Introduction, namely instantiation and conjunction

2901:  (AND-compositionality). We focus on goal equivalence for a given

2902:  program $\mathcal{P}$; thus,

2903:  the main questions are: (1) When are two goals equivalent? (2) Is

2904:  equivalence a congruence?

2905: 

2906:  Inspired by the connections with the area of process description

2907:  calculi that motivated our approach, and having at hand an

2908:  established theory developed for trace equivalence and bisimilarity

2909:  in the tile setting, the natural step is to try to apply general

2910:  existing techniques to our special case.  Therefore we can answer

2911:  question (1) by defining the two equivalences:

2912: 

2913: \begin{enumerate}

2914: \renewcommand{\theenumi}{\alph{enumi}}

2915: \item

2916:  $G \simeq_{\mathcal{P}} G'$ if $\mathcal{T}_{\mathcal{P}}(G) =

2917:  \mathcal{T}_{\mathcal{P}}(G')$, where $\mathcal{T}_{\mathcal{P}}(G)

2918:  \stackrel{\mathrm{def}}{=}\{\theta \mid

2919:  \mathcal{R}_{\mathcal{P}}\vdash \cell{G}{id_{\underline{1}}}

2920:  {\theta}{\Box\otimes id_{\underline{n}}} \}$.

2921: 

2922: \item

2923:   $G \cong_{\mathcal{P}} G'$ if $G$ and $G'$ are tile bisimilar in

2924:   $\mathcal{R}_{\mathcal{P}}$.

2925: \end{enumerate}

2926: 

2927:  These equivalences are reminiscent of the analogous notions on the

2928:  processes of a fixed process description calculus modeled with

2929:  tiles. The interactive part of the underlying tile system tells what

2930:  can be observed during the computation, and then the equivalences

2931:  arise naturally as behavior-based concepts.

2932: 

2933:  Now, question (2) corresponds to ask whether $G \simeq G'$ implies

2934:  that $G\wedge F \simeq G'\wedge F$ and $\sigma;G \simeq \sigma;G'$

2935:  for all $F$ and $\sigma$ or not (the same for $\cong$).

2936: 

2937:  Though proving directly these properties is not too complicate, we can exploit

2938:  Proposition~\ref{decascongprop} and just prove that the tile system

2939:  $\mathcal{R}_{\mathcal{P}}$ enjoys the decomposition property for any

2940:  logic program $\mathcal{P}$.

2941: 

2942: \begin{proposition}

2943:  For any logic program $\mathcal{P}$, the corresponding tile system

2944:  $\mathcal{R}_{\mathcal{P}}$ enjoys the sequential decomposition

2945:  property.

2946: \end{proposition}

2947: 

2948: \begin{proof}

2949:  We want to prove that for any goal $\sigma;G$ and tile

2950:  $\mathcal{R}_{\mathcal{P}} \vdash

2951:  \cell{\sigma;G}{id_{\underline{1}}}{\theta}{F}$, there exist

2952:  $\theta'$, $\sigma'$ and $F'$ such that $\mathcal{R}_{\mathcal{P}}

2953:  \vdash \cell{G}{id_{\underline{1}}}{\theta'}{F'}$ and

2954:  $\mathcal{R}_{\mathcal{P}} \vdash

2955:  \cell{\sigma}{\theta'}{\theta}{\sigma'}$. Fixed a decomposition of

2956:  $\cell{\sigma;G}{id_{\underline{1}}}{\theta}{F}$ in terms of basic

2957:  tiles, the proof proceeds by induction on the number of tiles

2958:  associated to the clauses that are considered in the decomposition.

2959: \end{proof}

2960: 

2961: \begin{corollary}

2962:  For any logic program $\mathcal{P}$, the equivalences

2963:  $\simeq_{\mathcal{P}}$ and $\cong_{\mathcal{P}}$ are congruences with

2964:  respect to conjunction of goals and instantiation of free variables.

2965: \end{corollary}

2966: 

2967: \subsection{Three goal equivalences via instantiation closures}\label{THREEsec}

2968: 

2969:  One of the main motivations for the research presented in this paper

2970:  concerns the application of logic programming as a convenient

2971:  computational model for interactive systems. In particular, the

2972:  unification mechanism typical of resolution steps is particularly

2973:  interesting because it differs from the ordinary matching procedures

2974:  of reduction semantics \cite{BB:CAM,Mil:CCS,Mes:CRL}. To some extent,

2975:  mgu's characterizes the minimal amount of dynamic interaction

2976:  with the rest of the system that is needed to evolve. In this section

2977:  we compare other operational alternatives, which are commonly used in

2978:  many concurrent systems and calculi, by means of the equivalences

2979:  they induce on goals.  Each alternative is obtained by slightly

2980:  modifying the operational rule for atomic goals.

2981: 

2982:  The first model allows for applying only ground instances of the

2983:  clauses (to ground goals only):

2984: 

2985: \[

2986:  (1) \irule{(H \mathrel{:-} F) \in \mathcal{P}\ \ \

2987:         A = \sigma;H\ \mathrm{ground}\ \ \

2988:         \sigma;F\ \mathrm{ground}} 

2989:         {\mathcal{P}\vvdash A\Rightarrow_{\sigma}

2990:                             \sigma;F}

2991: \]

2992:  

2993: \noindent

2994:  Then, two goals $G_1$ and $G_2$ (not necessarily ground) are

2995:  equivalent, written $G_1 \mathrel{\sim_{(1)}} G_2$ if and only if for

2996:  any ground substitution $\sigma$ on $\mathit{Var}(G_1,G_2)$, whenever

2997:  $\sigma;G_1$ is refuted then also $\sigma;G_2$ is refuted, and vice

2998:  versa. This equivalence is the most widely used for interactive

2999:  systems (closing open systems in all possible ways), since it is the

3000:  coarser ``correct'' equivalence that can be defined according to the

3001:  operational rules. The disadvantage is that to check goal equivalence

3002:  we must instantiate \wrt\ all ground substitutions, \ie, proving goal

3003:  equivalence is in general very expensive.

3004: 

3005:  The second model allows for applying any instance of the

3006:  clause to any matching instance of the goal:

3007: 

3008: \[

3009:  (2) \irule{(H \mathrel{:-} F) \in \mathcal{P}\ \ \

3010:         \sigma;A = \sigma;\rho;H} 

3011:         {\mathcal{P}\vvdash A\Rightarrow_{\sigma}

3012:                             \sigma;\rho;F}

3013: \]

3014:  

3015: \noindent

3016:  In this case, two goals $G_1$ and $G_2$ are equivalent, written $G_1

3017:  \mathrel{\sim_{(2)}} G_2$ if and only if whenever $G_1$ can be

3018:  refuted with $\sigma$, then also $G_2$ can be refuted with $\sigma$,

3019:  and vice versa. This equivalence extends the previous one to a

3020:  uniform treatment of open and ground goals, but of course equivalence

3021:  proofs become even more complicated and inefficient.

3022: 

3023:  The third model is the ordinary one, where the substitution $\sigma$

3024:  in (2) must be the mgu between $A$ and $\rho;H$. Hence, two goals

3025:  $G_1$ and $G_2$ are equivalent, written $G_1 \mathrel{\sim_{(3)}}

3026:  G_2$ if and only if they have the same set of computed answer

3027:  substitutions (\ie, $\mathrel{\sim_{(3)}}$ is the equivalence

3028:  $\mathrel{\simeq_{\mathcal{P}}}$ discussed in Section~\ref{GCsec}).

3029:  This equivalence is very convenient, because it makes the transition

3030:  system finitely branching (as opposed to (1) and (2)) and therefore

3031:  facilitates equivalence proofs.

3032: 

3033:  If we work with an infinite set of function symbols, it can be easily

3034:  verified that $\mathrel{\sim_{(1)}}$ and $\mathrel{\sim_{(2)}}$

3035:  define exactly the same equivalence classes. The inclusion of

3036:  $\mathrel{\sim_{(2)}}$ into $\mathrel{\sim_{(1)}}$ is obvious,

3037:  because ground substitutions are just a particular case of generic

3038:  substitutions. The converse holds because the existence of a

3039:  refutation with ground substitution $\sigma;\psi$, where $\psi$

3040:  contains function symbols not appearing in the program, implies the

3041:  existence of another refutation with non-ground substitution

3042:  $\sigma$. Therefore, the equivalence over ground substitutions

3043:  ($\mathrel{\sim_{(1)}}$) together with the assumption of an infinite

3044:  set of function symbols imply the equivalence over non-ground

3045:  substitutions ($\mathrel{\sim_{(2)}}$).

3046: 

3047:  The equivalence $\mathrel{\sim_{(3)}}$ is instead stricter than the

3048:  other two. Again, the inclusion of $\mathrel{\sim_{(3)}}$ in

3049:  $\mathrel{\sim_{(1)}}$ is obvious, while it is easy to find an

3050:  example of a logic program $\mathcal{P}$ where two goals have

3051:  different sets of computed answer substitutions but have the same

3052:  sets of ground refutations. Just consider a logic program with the

3053:  following three facts:

3054: 

3055: \begin{alltt}

3056:  p(X).

3057:  p(a).

3058:  q(X).

3059: \end{alltt}

3060: 

3061: \noindent

3062:  If we take the goals $p(X)$ and $q(X)$, it is immediate to see that $p(X)

3063:  \mathrel{\sim_{(1)}} q(X)$. However, the set of computed answer

3064:  substitutions of $p(X)$ is $\{\varepsilon, [\sbtn{a}{X}] \}$, while

3065:  for $q(X)$ we just have $\{\varepsilon\}$ (with $\varepsilon$

3066:  denoting the empty substitution).

3067: 

3068: \subsection{Concurrency and causality}\label{DTsec}

3069: 

3070:  If we look at the  system $\mathcal{R}_{\mathcal{P}}$ from a

3071:  concurrent viewpoint then atomic goals can be regarded as distributed

3072:  components that can evolve separately and where variable sharing

3073:  provides the means to exchange information between

3074:  components. According to this perspective,  \eg, for

3075:  backtracking, it is essential to keep

3076:  track of the causal dependencies among components.

3077: 

3078:  To accomplish this view we slightly modify the associated tile system

3079:  for defining more concrete observations on the causal dependencies

3080:  among replaced and inserted goals. To this aim, to each clause

3081: \[

3082:  c \mathrel{\equiv} p(t_1,\ldots,t_k)\ \mathrel{:-}\

3083:                     q_1(\vec{s}_1),\ldots,q_m(\vec{s}_m)

3084: \]

3085: \noindent

3086:  in the logic program, we associate an operator

3087:  $\dfun{c}{\mathsf{p}^m}{\mathsf{p}}$ in the signature of

3088:  observations. Then, since we want to be aware of the components

3089:  distributed in the system, we do not consider the operator $\wedge$

3090:  and associate to each clause $C$ the tile

3091: 

3092: \[

3093:  C_c =

3094:  \cell{p}

3095:       {c}

3096:       {\langle t_1,\ldots,t_k\rangle}

3097:       {\langle q_1(\vec{s}_1),\ldots,q_m(\vec{s}_m)\rangle}.

3098: \]

3099: 

3100: \noindent

3101:  Note that by using the

3102:  trigger $c$ we can now observe that the initial configuration $p$

3103:  generates $m$ new components that causally depends on it.

3104: 

3105:  For the rest, we add as before the pullback tiles that provide the

3106:  coordination mechanism about local instantiations.  In the new

3107:  setting, equivalent computations from the point of view of

3108:  concurrency and coordination are identified, whereas computations

3109:  that return the same computed answer substitution but that employ

3110:  different concurrent reduction strategies are distinguished. This

3111:  also allows one to observe causal dependencies among resolution

3112:  steps, since the triggers of refutation tiles describe the `concurrent

3113:  strategy' employed for achieving the result.

3114: 

3115:  Of course, the notion of refutation tile slightly changes according

3116:  to the above modification: A refutation tile is an entailed tile of

3117:  the form $\cell{G}{s}{\theta}{\Box^m\otimes !_{\underline{n}}}$, \ie,

3118:  empty goals become \emph{nil} processes distributed around system

3119:  locations.

3120: 

3121:  The trigger of the refutation tile for a generic goal is a tuple of

3122:  terms (without shared variables), \ie, it corresponds to an ordered

3123:  forest of (ordered) trees, whose nodes are labeled with clause

3124:  names. We denote by $\sqsubseteq$ the obvious partial order on nodes

3125:  such that $x \sqsubseteq y$ iff $y$ descends from $x$.  Moreover,

3126:  since the tree is ordered, we have an immediate correspondence

3127:  between each clause instance and the subgoal it was applied to. Then,

3128:  we can characterize the concurrency of the framework by means of the

3129:  following theorem.

3130: 

3131: \begin{theorem}

3132:  Let $\cell{G}{s}{\theta}{\Box^m\otimes !_{\underline{n}}}$ be a tile

3133:  refutation for the goal $G$, and let $\sqsubseteq$ be the partial

3134:  order (forest) associated to $s$. Moreover, let $\preceq$ be any

3135:  total order that extends $\sqsubseteq$. Then by applying the clauses

3136:  associated to the nodes of the tree in the order specified by

3137:  $\preceq$ we obtain again the computed answer substitution $\theta$.

3138: \end{theorem}

3139: 

3140:  The proof is based on the compositional properties of pullbacks and

3141:  expresses the `complete concurrency' (from the trigger side, not from

3142:  the effect side) of the framework.

3143: 

3144:  Since application of clauses that do not depend on each other

3145:  (in $\sqsubseteq$) can be executed in any order by choosing suitable

3146:  total orders $\preceq$, it follows that the order in which they are

3147:  executed is not important. Note however that this depends on the

3148:  fact that the coordination mechanism via pullbacks takes care of the

3149:  side-effects of each clause application.

3150: 

3151: \section{Tiles and constraints}\label{CLPsec}

3152: 

3153:  In this section we informally discuss how the tile-based approach can

3154:  be extended to deal with constraint logic programming (\textsc{clp})

3155:  \cite{MS:PCI,JM:CLPS}.  Computational equivalences between the

3156:  ordinary operational semantics of \textsc{clp} and the tile semantics

3157:  we will briefly describe in this section can be established by

3158:  results analogous to Theorem~\ref{reptheo}.  The interest in

3159:  constraint satisfaction problems is centered around a powerful,

3160:  declarative mechanism for knowledge representation, as many

3161:  situations can be conveniently modeled by means of constraints on a

3162:  set of objects or parameters. Therefore, constraint logic programming

3163:  is not a language in itself, but can be more precisely seen as a

3164:  scheme, parametric \wrt\ the kind of constraints that can be

3165:  handled. For example, pure logic programming is to some extent a

3166:  version of \textsc{clp} dealing with term equalities over a Herbrand

3167:  universe. The way in which constraints are combined and simplified is

3168:  delegated to a \emph{constraint solver} for efficiency reasons. Other

3169:  formalisms, like \eg\ \emph{constraint handling rules}

3170:  \cite{Fru:CHR}, allow for modeling solvers by means of suitable

3171:  guarded clauses. Usually, constraint programming languages are

3172:  monotonic (or \emph{non-consuming}), that is constraints are never

3173:  deleted from the constraint store; however, in the literature there

3174:  are some variants which allow for constraint consumption

3175:  \cite{BdBP:POSOS}. Both the monotonic and the consuming behaviors

3176:  can be represented in our framework.

3177: 

3178:  At the abstract level (see \cite{Sar:CC}), a \emph{constraint system}

3179:  can be seen as a pair $\langle D,\vdash\rangle$, where $D$ is a set of

3180:  \emph{primitive constraints} and $\vdash\subseteq \wp(D) \times D$ is

3181:  the \emph{entailment relation}, relating (finite) sets of primitive

3182:  constraints to entailed primitive constraints. Relation $\vdash$ must

3183:  satisfy

3184: 

3185: \begin{itemize}

3186: \item

3187:  $\mathbf{C}\cup\{\mathbf{c}\} \vdash \mathbf{c}$ (reflexivity);

3188: \item

3189:  if $\mathbf{C} \vdash \mathbf{c}$ for all $\mathbf{c}\in

3190:  \mathbf{C'}$, and $\mathbf{C'}\vdash \mathbf{c'}$, then

3191:  $\mathbf{C}\vdash \mathbf{c'}$ (transitivity).

3192: \end{itemize}

3193: 

3194:  The set of subsets of $D$ which are closed under entailment is

3195:  denoted by $\abs{D}$, and a \emph{constraint} is just an element of

3196:  $\abs{D}$. As usual, we assume that a set $\mathit{Con} \subseteq

3197:  \abs{D}$ of \emph{consistent constraints} is given such that:

3198: 

3199: \begin{itemize}

3200: \item

3201:  if $\mathbf{C}\cup \mathbf{C'} \in \mathit{Con}$, then

3202:  $\mathbf{C},\mathbf{C'}\in\mathit{Con}$;

3203: \item

3204:  if $\mathbf{c}\in D$ then $\{\mathbf{c}\}\in\mathit{Con}$;

3205: \item

3206:  if $\mathbf{C}\in\mathit{Con}$ and $\mathbf{C}\vdash \mathbf{c}$, then

3207:  $\mathbf{C}\cup\{\mathbf{c}\}\in \mathit{Con}$.

3208: \end{itemize}

3209: 

3210:  For our representation, a constraint system can be equivalently seen

3211:  as a category $\mathcal{C}$ whose arrows are constraints and whose

3212:  composition is the conjunction of constraints, in such a way that

3213:  $\mathbf{C};\mathbf{c} = \mathbf{C}$ iff $\mathbf{C}\vdash

3214:  \mathbf{c}$. We also assume a distinguished arrow $\mathbf{ff}$

3215:  exists such that $\mathbf{C} = \mathbf{ff}$ iff $\mathbf{C}\not\in

3216:  \mathit{Con}$.

3217: 

3218:  In the presence of constraints, goals become pairs $(G,\mathbf{C})$,

3219:  where $G$ is an ordinary conjunctive formula and $\mathbf{C}$ is a

3220:  constraint, while clauses can have the more general form

3221: 

3222: \[H \mathrel{:-} \mathbf{c_1} | B_1,\ldots,B_n,\mathbf{c_2}\]

3223: 

3224: \noindent

3225:  where $\mathbf{c_1}$ is a \emph{guard} for the application of the

3226:  clause (similar to the $\mathit{ask}$ operation of \emph{concurrent

3227:  constraint programming} (\textsc{ccp}) \cite{Sar:CC}), and

3228:  $\mathbf{c_2}$ is the constraint to be added to the store after the

3229:  application of the clause (similar to the $\mathit{tell}$ operation

3230:  of \textsc{ccp}). In the ordinary interpretation, the meaning is

3231:  that the clause can be applied only if the constraint component of

3232:  the current goal entails $\mathbf{c_1}$ and that, after the

3233:  resolution step, the constraint $\mathbf{c_2}$ is added to the

3234:  current state, provided that the resulting constraint is consistent,

3235:  \ie, the resolution can be applied only if $\mathbf{C}\vdash

3236:  \mathbf{c_1}$ and $\mathbf{C}\cup \{\mathbf{c_2}\} \in \mathit{Con}$.

3237:  Although usually \textsc{clp} languages do not have guards in their

3238:  syntax but just constraints in the bodies of the clauses (which

3239:  correspond to the tell constraint $\mathbf{c_2}$ above), we decide to

3240:  consider this more general kind of clauses in order to model also

3241:  concurrent formalisms such as \textsc{ccp} and constraint rewriting

3242:  formalisms such as \textsc{chr}.

3243: 

3244:  Now, we face several alternatives for describing the interaction

3245:  between ask/tell and the current store, where each alternative

3246:  corresponds to a different set of auxiliary tiles associated with the

3247:  constraint system $\mathcal{C}$.

3248: 

3249:  For example, likewise pure logic programming, we can take the

3250:  pullback squares in $\mathcal{C}$ (if any), or more generally, we can

3251:  consider the \emph{relative pullbacks}, dualizing the approach of

3252:  Leifer and Milner based on relative pushouts \cite{LM:DBCRS}. In this

3253:  case, given a constraint $\mathbf{C}$ (the current constraint store)

3254:  and another constraint $\mathbf{c_2}$ (the tell part of the clause),

3255:  we have coordination tiles of the form

3256:  $\cell{\mathbf{C}}{\mathbf{c_2}}{\mathbf{c}}{\mathbf{C'}}$ (with the

3257:  condition that $\mathbf{c};\mathbf{C} \neq \mathbf{ff}$) expressing

3258:  that $\mathbf{C'}$ is the minimal constraint to be added to

3259:  $\mathbf{c_2}$ for entailing (all constraints in) $\mathbf{C}$, and

3260:  that $\mathbf{c}$ is the minimal constraint to be added to

3261:  $\mathbf{C}$ for entailing $\mathbf{c_2}$. Therefore, tiles of this

3262:  kind check the consistency of $\mathbf{c_2}$ with $\mathbf{C}$ and

3263:  return the additional amount of information gained by joining the two

3264:  constraints, an operation which is suitable for interpreting tell

3265:  constraints. The guard $\mathbf{c_1}$ should be considered as part of

3266:  the initial configuration of the tile associated with the clause, so

3267:  that the clause can be applied only if the current store $\mathbf{C}$

3268:  can be decomposed as $\mathbf{C_1};\mathbf{c_1}$, while

3269:  $\mathbf{c_2}$ is an effect of the tile (to be coordinated with the

3270:  current state). Since the ask and tell operations are not consuming,

3271:  the join of $\mathbf{c_1}$ and $\mathbf{c_2}$ must be inserted also

3272:  in the final configuration. The resulting tile associated with the

3273:  clause is thus

3274:  $\cell{(P,\mathbf{c_1})}{id}{(t,\mathbf{c_2})}{(B_1,\ldots,B_n,\mathbf{c_2};\mathbf{c_1})}$,

3275:  with $P$ the predicate symbol in $H$ and $t;P = H$.

3276: 

3277:  If the category describing the constraint system does not possess the

3278:  pullbacks, we can consider all commuting squares, instead of just

3279:  (relative) pullbacks. This encoding can be applied to a generic

3280:  category $\mathcal{C}$, but usually involves an infinite number of

3281:  possible closures.

3282: 

3283:  Notice that this way of modeling \textsc{clp} clauses via tiles

3284:  synchronizes $P$ and $\mathbf{c_1}$ and therefore centralizes the

3285:  control, unless $\mathbf{c_1}$ is the empty constraint.  An

3286:  alternative, which solves this problem and gives more emphasis to the

3287:  interaction between subgoals and constraints, is to leave the

3288:  consistency check of the tell operation to the metainterpreter (\eg,

3289:  by discarding all computations that reach an inconsistent store), and

3290:  use the guard $\mathbf{c_1}$ as an effect, to abandon the centralized

3291:  view. Now, the auxiliary tiles for constraints have just the task of

3292:  checking the entailment of the guard in the current store, and

3293:  therefore we can take all squares of the form

3294:  $\cell{\mathbf{C}}{\mathbf{c_1}}{id}{\mathbf{C}}$ such that

3295:  $\mathbf{C};\mathbf{c_1}=\mathbf{C}$ (there is exactly one cell for

3296:  any $\mathbf{C},\mathbf{c_1}$ such that $\mathbf{C}\vdash

3297:  \mathbf{c_1}$). Since $\mathbf{C}$ appears in the final

3298:  configuration, there is no need for reasserting $\mathbf{c_1}$, and

3299:  thus the tile associated with the generic clause is

3300:  $\cell{P}{id}{(t,\mathbf{c_1})}{(B_1,\ldots,B_n,\mathbf{c_2})}$. Note

3301:  that if tiles like $\cell{\mathbf{C}}{\mathbf{c_1}}{id}{\mathbf{C'}}$

3302:  with $\mathbf{C'};\mathbf{c_1}=\mathbf{C}$ were considered instead,

3303:  then the constraint $\mathbf{c_1}$ might also be consumed during the

3304:  entailment check, unless it was reintroduced in the final

3305:  configuration.

3306: 

3307:  It is worth to notice that in all these proposals to model

3308:  \textsc{clp} via tiles, the tile approach allows us to clearly

3309:  separate the rules of the program from the coordination mechanism,

3310:  which is dependent just on the category $\mathcal{C}$ of constraints

3311:  under consideration, and on the features we want to model.

3312: 

3313: \section*{Conclusions and future work}

3314: 

3315:  In this paper we have used tile logic to model the coordination and

3316:  interaction features of logic programming.  Our approach differs from

3317:  that of \cite{CM:ASSTS}, based on structured transition systems, by

3318:  taking into account the computed answer substitutions instead of just

3319:  the correct answer substitutions. In fact, in \cite{CM:ASSTS}, the

3320:  clauses are seen as rewrite rules that can be further instantiated in

3321:  all possible ways and the computational model of a program is a

3322:  suitable 2-category (\ie, a special kind of double category, where

3323:  the vertical category is discrete and thus only identities are

3324:  allowed as observations). This means that if there exists a

3325:  refutation for the goal $G$ with computed answer substitution

3326:  $\theta$, then in the 2-category model we can find a refutation for

3327:  $\theta;G$ but not necessarily one for $G$. The main advantages of

3328:  our approach \wrt\ the one in \cite{CM:ASSTS} are a finite branching

3329:  operational semantics and the built-in unification

3330:  mechanism. Moreover, the drawback of using 2-categories instead of

3331:  double categories is that the dynamic creation of fresh variables

3332:  cannot be modeled, \ie, the variables to be used must all be present

3333:  at the beginning of the computation.

3334: 

3335:   As noted in the Introduction, the usage of tiles emphasizes the

3336:  duality of instantiation and contextualization of goals, allowing for

3337:  a uniform treatment of both. In particular, while instantiation plays

3338:  a fundamental role since it can affect the behavior of the goal,

3339:  here contextualization (\ie, conjunction with disjoint goals) does

3340:  not increase the distinguishing power of the semantics, and therefore

3341:  transitions labeled with external contexts can be avoided in the

3342:  model. In fact, each atomic goal can be studied in isolation from

3343:  other goals and the tiles for putting a goal in any possible

3344:  conjunction are not necessary. The reason for this absence is that

3345:  goals cannot be conjoined in Horn clauses' heads, whereas if

3346:  multi-headed clauses were considered, then, in general, abstract

3347:  semantics would not turn out to be a congruence unless transitions

3348:  for external contexts are added.  Indeed, we believe that our

3349:  approach can be extended to other frameworks where multi-head clauses

3350:  are allowed (see for example the \emph{generalized Horn clauses}

3351:  of \cite{FLP:GHC} and the \textsc{chr} formalism

3352:  \cite{Fru:CHR}), giving us the key for dealing with

3353:  contextualization features --- dually to the instantiation via

3354:  pullbacks considered here.

3355: 

3356:  We have also sketched some ideas for extending our approach to handle

3357:  constraints. In this case, the constraint system and the logic

3358:  program are modeled by two separate sets of tiles, and we have shown

3359:  how to handle both ask and tell constraints.

3360: 

3361:  Exploiting the built-in synchronization features of tile logic, we

3362:  are confident that our framework can be naturally extended to deal

3363:  also with sequentialized commits (\ie, goals of the form

3364:  $G_1;G_2;\cdots;G_k$ where the possibly non-atomic subgoals $G_i$ must be

3365:  resolved in the order given by their indices $i$, giving the

3366:  possibility to the user of specifying more efficient resolution

3367:  strategies). Moreover, the higher-order version of tile logic

3368:  presented in \cite{BM:CCDC} may find application to the modeling of

3369:  higher-order logic programming (\eg, \emph{lambda prolog})

3370:  \cite{Mil:LPILL,MN:HOLP}.

3371: 

3372:  Finally, let us mention that the abstractness of the unification via

3373:  pullbacks makes the tile approach suitable for considering

3374:  unification in equational theories rather than in term algebras. For

3375:  example, this would allow to develop a computational model for

3376:  rewriting logic (and hence for reduction systems on processes up to

3377:  structural congruence) based on unification.

3378: 

3379: \section*{Acknowledgements}

3380: 

3381:  We would like to thank Paolo Baldan and Fabio Gadducci for their

3382:  comments on a preliminary version of this paper.  We are also

3383:  grateful to the anonymous referees for their helpful suggestions and

3384:  comments, which allowed us to improve the presentation of the

3385:  material.

3386: 

3387:  This research has been supported by

3388:   CNR Integrated Project

3389:       \emph{Progettazione e Verifica di Sistemi Eterogenei};

3390:   by Esprit WG

3391:       \emph{CONFER2} and \emph{COORDINA};

3392:   and by MURST project

3393:       \emph{TOSCA}.

3394: 

3395: \begin{thebibliography}{}

3396: 

3397: \bibitem[\protect\citename{Bernstein, }1998]{Ber:CTSOS}

3398: Bernstein, K. (1998).

3399: \newblock A congruence theorem for structured operational semantics of

3400:   higher-order languages.

3401: \newblock {\em Pages  153--164 of:} {\em Proceedings of lics'98, 13th annual

3402:   ieee symposium on logic in computer science}.

3403: \newblock IEEE Computer Society Press.

3404: 

3405: \bibitem[\protect\citename{Berry \& Boudol, }1992]{BB:CAM}

3406: Berry, G., \& Boudol, G. (1992).

3407: \newblock The chemical abstract machine.

3408: \newblock {\em Theoret.\ comput.\ sci.}, {\bf 96}(1), 217--248.

3409: 

3410: \bibitem[\protect\citename{Best {\em et~al.}\relax, }1997]{BdBP:POSOS}

3411: Best, E., de~Boer, S., \& Palamidessi, C. (1997).

3412: \newblock Partial order and sos semantics for linear constraint programs.

3413: \newblock {\em Pages  256--273 of:} {\em Proceedings of coordination'97, 2nd

3414:   international conference on coordination languages and models}.

3415: \newblock Lect.\ Notes in Comput.\ Sci., vol. 1282.

3416: \newblock Springer Verlag.

3417: 

3418: \bibitem[\protect\citename{Bloom {\em et~al.}\relax, }1995]{BIM:BCBT}

3419: Bloom, B., Istrail, S., \& Meyer, A.R. (1995).

3420: \newblock Bisimulation can't be traced.

3421: \newblock {\em Journal of the acm}, {\bf 42}(1), 232--268.

3422: 

3423: \bibitem[\protect\citename{Bossi {\em et~al.}\relax, }1994a]{BGLM:CSLP}

3424: Bossi, A., Gabbrielli, M., Levi, G., \& Meo, M.C. (1994a).

3425: \newblock A compositional semantics for logic programs.

3426: \newblock {\em Theoret.\ comput.\ sci.}, {\bf 122}(1-2), 3--47.

3427: 

3428: \bibitem[\protect\citename{Bossi {\em et~al.}\relax, }1994b]{BGLM:SSA}

3429: Bossi, A., Gabbrielli, M., Levi, G., \& Martelli, M. (1994b).

3430: \newblock The s-semantics approach: Theory and applications.

3431: \newblock {\em Journal of logic programming}, {\bf 19/20}, 149--197.

3432: 

3433: \bibitem[\protect\citename{Brogi {\em et~al.}\relax, }1992]{BLM:CMTS}

3434: Brogi, A., Lamma, E., \& Mello, P. (1992).

3435: \newblock Compositional model-theoretic semantics for logic programs.

3436: \newblock {\em New generation computing}, {\bf 11}(1), 1--21.

3437: 

3438: \bibitem[\protect\citename{Bruni, }1999]{Bru:TL}

3439: Bruni, R. (1999).

3440: \newblock {\em Tile logic for synchronized rewriting of concurrent systems}.

3441: \newblock Ph.D. thesis, Computer Science Department, University of Pisa.

3442: 

3443: \bibitem[\protect\citename{Bruni \& Montanari, }1999]{BM:CCDC}

3444: Bruni, R., \& Montanari, U. (1999).

3445: \newblock Cartesian closed double categories, their lambda-notation, and the

3446:   pi-calculus.

3447: \newblock {\em Pages  246--265 of:} {\em Proceedings of lics'99, 14th annual

3448:   ieee symposium on logic in computer science}.

3449: \newblock IEEE Computer Society Press.

3450: 

3451: \bibitem[\protect\citename{Bruni \& Montanari, }2000]{BM:ZSNCCI}

3452: Bruni, R., \& Montanari, U. (2000).

3453: \newblock Zero-safe nets: Comparing the collective and individual token

3454:   approaches.

3455: \newblock {\em Inform.\ and comput.}, {\bf 156}, 46--89.

3456: 

3457: \bibitem[\protect\citename{Bruni {\em et~al.}\relax, }1998]{BMM:PTTL}

3458: Bruni, R., Meseguer, J., \& Montanari, U. (1998).

3459: \newblock {\em Process and term tile logic}.

3460: \newblock Tech. rept. SRI-CSL-98-06. SRI International.

3461: \newblock Also Technical Report TR-98-09, Computer Science Department,

3462:   University of Pisa.

3463: 

3464: \bibitem[\protect\citename{Bruni {\em et~al.}\relax, }1999]{BMM:ETS}

3465: Bruni, R., Meseguer, J., \& Montanari, U. (1999).

3466: \newblock Executable tile specifications for process calculi.

3467: \newblock {\em Pages  60--76 of:} Finance, J.-P. (ed), {\em Proceedings of

3468:   fase'99, fundamental approaches to software engineering}.

3469: \newblock Lect.\ Notes in Comput.\ Sci., vol. 1577.

3470: \newblock Springer Verlag.

3471: 

3472: \bibitem[\protect\citename{Bruni {\em et~al.}\relax, }2000a]{BFMM:BC}

3473: Bruni, R., de~Frutos-Escrig, D., Mart\'\i-Oliet, N., \& Montanari, U. (2000a).

3474: \newblock Bisimilarity congruences for open terms and term graphs via tile

3475:   logic.

3476: \newblock {\em Pages  259--274 of:} Palamidessi, C. (ed), {\em Proceedings of

3477:   concur 2000, 11th international conference on concurrency theory}.

3478: \newblock Lect.\ Notes in Comput.\ Sci., vol. 1877.

3479: \newblock Springer Verlag.

3480: 

3481: \bibitem[\protect\citename{Bruni {\em et~al.}\relax, }2000b]{BMS:OES}

3482: Bruni, R., Montanari, U., \& Sassone, V. (2000b).

3483: \newblock Open ended systems, dynamic bisimulation and tile logic.

3484: \newblock {\em Pages  440--456 of:} van Leeuwen, J., Watanabe, O., Hagiya, M.,

3485:   Mosses, P.D., \& Ito, T. (eds), {\em Proceedings of ifip tcs 2000, ifip int.

3486:   conf. on theoretical computer science}.

3487: \newblock Lect.\ Notes in Comput.\ Sci., vol. 1872.

3488: \newblock Springer Verlag.

3489: 

3490: \bibitem[\protect\citename{Bruni {\em et~al.}\relax, }2001]{BMM:SMCDC}

3491: Bruni, R., Meseguer, J., \& Montanari, U. (2001).

3492: \newblock Symmetric monoidal and cartesian double categories as a semantic

3493:   framework for tile logic.

3494: \newblock {\em Math.\ struct.\ in comput.\ sci.}

3495: \newblock To appear.

3496: 

3497: \bibitem[\protect\citename{Burstall \& Rydeheard, }1985]{BR:CUA}

3498: Burstall, R.M., \& Rydeheard, D.E. (1985).

3499: \newblock A categorical unification algorithm.

3500: \newblock {\em Pages  493--505 of:} Abramsky, S., Pitt, D., Poigne, A., \&

3501:   Rydeheard, D. (eds), {\em Proceedings of workshop on category theory and

3502:   computer programming}.

3503: \newblock Lect.\ Notes in Comput.\ Sci., vol. 240.

3504: \newblock Springer Verlag.

3505: 

3506: \bibitem[\protect\citename{Cattani {\em et~al.}\relax, }2000]{CLM:CECAG}

3507: Cattani, G.L., Leifer, J.J., \& Milner, R. (2000).

3508: \newblock {\em Contexts and embeddings for a class of action graphs}.

3509: \newblock Tech. rept. 496. Computer Laboratory, University of Cambridge.

3510: 

3511: \bibitem[\protect\citename{Corradini \& Montanari, }1992]{CM:ASSTS}

3512: Corradini, A., \& Montanari, U. (1992).

3513: \newblock An algebraic semantics for structured transition systems and its

3514:   application to logic programs.

3515: \newblock {\em Theoret.\ comput.\ sci.}, {\bf 103}, 51--106.

3516: 

3517: \bibitem[\protect\citename{De~Nicola \& Hennessy, }1984]{dNH:TEP}

3518: De~Nicola, R., \& Hennessy, M. (1984).

3519: \newblock Testing equivalences for processes.

3520: \newblock {\em Theoret.\ comput.\ sci.}, {\bf 34}, 83--133.

3521: 

3522: \bibitem[\protect\citename{De~Simone, }1985]{DeS:HLSD}

3523: De~Simone, R. (1985).

3524: \newblock Higher level synchronizing devices in {MEIJE}--{SCCS}.

3525: \newblock {\em Theoret.\ comput.\ sci.}, {\bf 37}, 245--267.

3526: 

3527: \bibitem[\protect\citename{Ehresmann, }1963a]{Ehr:CS}

3528: Ehresmann, E. (1963a).

3529: \newblock Cat\'egories structur\`ees: {I}--{II}.

3530: \newblock {\em Annales \'ecole normal superieur}, {\bf 80}, 349--426.

3531: 

3532: \bibitem[\protect\citename{Ehresmann, }1963b]{Ehr:CS2}

3533: Ehresmann, E. (1963b).

3534: \newblock Cat\'egories structur\`ees: {III}.

3535: \newblock {\em Cahiers de topologie ed g\'eom\'etrie diff\'erentielle}, {\bf

3536:   5}.

3537: 

3538: \bibitem[\protect\citename{Emden \& Kowalski, }1976]{EK:SPLPL}

3539: Emden, M.H.~van, \& Kowalski, R.A. (1976).

3540: \newblock The semantics of predicate logic as a programming language.

3541: \newblock {\em Journal of the acm}, {\bf 23}(4), 733--742.

3542: 

3543: \bibitem[\protect\citename{Falaschi {\em et~al.}\relax, }1984]{FLP:GHC}

3544: Falaschi, M., Levi, G., \& Palamidessi, C. (1984).

3545: \newblock A synchronization logic: Axiomatics and formal semantics of

3546:   generalized horn clauses.

3547: \newblock {\em Information and control}, {\bf 60}(1-3), 36--69.

3548: 

3549: \bibitem[\protect\citename{Falaschi {\em et~al.}\relax, }1989]{FLMP:DMOBLL}

3550: Falaschi, M., Levi, G., Martelli, M., \& Palamidessi, C. (1989).

3551: \newblock Declarative modeling of the operational behavior of logic languages.

3552: \newblock {\em Theoret.\ comput.\ sci.}, {\bf 69}(3), 289--318.

3553: 

3554: \bibitem[\protect\citename{Ferrari \& Montanari, }2000]{FM:TFLMS}

3555: Ferrari, G.L., \& Montanari, U. (2000).

3556: \newblock Tile formats for located and mobile systems.

3557: \newblock {\em Inform.\ and comput.}, {\bf 156}, 173--235.

3558: 

3559: \bibitem[\protect\citename{Fr\"uhwirth, }1995]{Fru:CHR}

3560: Fr\"uhwirth, T.W. (1995).

3561: \newblock Constraint handling rules.

3562: \newblock {\em Pages  90--107 of:} Podelski, A. (ed), {\em Constraint

3563:   {P}rogramming: {B}asics and {T}rends}.

3564: \newblock Lect.\ Notes in Comput.\ Sci., vol. 910.

3565: \newblock Springer Verlag.

3566: 

3567: \bibitem[\protect\citename{Gadducci \& Montanari, }1996]{GM:RRCCS}

3568: Gadducci, F., \& Montanari, U. (1996).

3569: \newblock Rewriting rules and {CCS}.

3570: \newblock  {\em Proceedings of wrla'96, 1st workshop on rewriting logic and its

3571:   applications}.

3572: \newblock Elect.\ Notes in Th.\ Comput.\ Sci., vol. 4.

3573: \newblock Elsevier Science.

3574: 

3575: \bibitem[\protect\citename{Gadducci \& Montanari, }2000]{GM:TM}

3576: Gadducci, F., \& Montanari, U. (2000).

3577: \newblock The tile model.

3578: \newblock  Plotkin, G., Stirling, C., \& Tofte, M. (eds), {\em Proof, language

3579:   and interaction: Essays in honour of {R}obin {M}ilner}.

3580: \newblock MIT Press.

3581: \newblock Also Technical Report TR-27/96, Dipartimento di Informatica,

3582:   Universit\`a di Pisa, 1996.

3583: 

3584: \bibitem[\protect\citename{Gaifman \& Shapiro, }1989]{GS:FACS}

3585: Gaifman, H., \& Shapiro, E. (1989).

3586: \newblock Fully abstract compositional semantics for logic programs.

3587: \newblock {\em Pages  134--142 of:} {\em Proceedings of popl'89}.

3588: \newblock ACM.

3589: 

3590: \bibitem[\protect\citename{Goguen, }1989]{Gog:WIU}

3591: Goguen, J. (1989).

3592: \newblock What is unification? a categorical view of substitution, equation and

3593:   solution.

3594: \newblock {\em Pages  217--261 of:} Nivat, M., \& A{\"{\i}}t-Kaci, H. (eds),

3595:   {\em Resolution of equations in algebraic structures}.

3596: \newblock Academic Press.

3597: 

3598: \bibitem[\protect\citename{Groote \& Vaandrager, }1992]{GV:SOSBC}

3599: Groote, J.F., \& Vaandrager, F. (1992).

3600: \newblock Structured operational semantics and bisimulation as a congruence.

3601: \newblock {\em Inform.\ and comput.}, {\bf 100}, 202--260.

3602: 

3603: \bibitem[\protect\citename{Jaffar \& Maher, }1994]{JM:CLPS}

3604: Jaffar, J., \& Maher, M.J. (1994).

3605: \newblock Constraint logic programming: A survey.

3606: \newblock {\em Journal of logic programming}, {\bf 19/20}, 503--581.

3607: 

3608: \bibitem[\protect\citename{Larsen \& Xinxin, }1990]{LX:CTOSC}

3609: Larsen, K.G., \& Xinxin, L. (1990).

3610: \newblock Compositionality through an operational semantics of contexts.

3611: \newblock {\em Pages  526--539 of:} Paterson, M.S. (ed), {\em Proceedings of

3612:   icalp'90, 17th international colloquium on automata, languages and

3613:   programming}.

3614: \newblock Lect.\ Notes in Comput.\ Sci., vol. 443.

3615: \newblock Springer Verlag.

3616: 

3617: \bibitem[\protect\citename{Lawvere, }1963]{Law:FSAT}

3618: Lawvere, F.W. (1963).

3619: \newblock Functorial semantics of algebraic theories.

3620: \newblock {\em Proc. national academy of science}, {\bf 50}, 869--872.

3621: 

3622: \bibitem[\protect\citename{Leifer \& Milner, }2000]{LM:DBCRS}

3623: Leifer, J.J., \& Milner, R. (2000).

3624: \newblock Deriving bisimulation congruences for reactive systems.

3625: \newblock {\em Pages  243--258 of:} Palamidessi, C. (ed), {\em Proceedings of

3626:   concur 2000, 11th international conference on concurrency theory}.

3627: \newblock Lect.\ Notes in Comput.\ Sci., vol. 1877.

3628: \newblock Springer Verlag.

3629: 

3630: \bibitem[\protect\citename{Lloyd, }1987]{Llo:FLP}

3631: Lloyd, J.W. (1987).

3632: \newblock {\em Foundations of logic programming}.

3633: \newblock Springer Verlag.

3634: 

3635: \bibitem[\protect\citename{MacLane, }1971]{Mac:CWM}

3636: MacLane, S. (1971).

3637: \newblock {\em Categories for the working mathematician}.

3638: \newblock Springer Verlag.

3639: 

3640: \bibitem[\protect\citename{Mancarella \& Pedreschi, }1987]{MP:ALP}

3641: Mancarella, P., \& Pedreschi, D. (1987).

3642: \newblock An algebra of logic programs.

3643: \newblock {\em Pages  1006--1023 of:} R.A., Kowalski, \& A., Bowen~K. (eds),

3644:   {\em Proceedings of iclp'88, 5th international conference on logic

3645:   programming}.

3646: \newblock MIT Press.

3647: 

3648: \bibitem[\protect\citename{Marriott \& Stuckey, }1998]{MS:PCI}

3649: Marriott, K., \& Stuckey, P.J. (1998).

3650: \newblock {\em Programming with constraints: an introduction}.

3651: \newblock MIT Press.

3652: 

3653: \bibitem[\protect\citename{Meseguer, }1992]{Mes:CRL}

3654: Meseguer, J. (1992).

3655: \newblock Conditional rewriting logic as a unified model of concurrency.

3656: \newblock {\em Theoret.\ comput.\ sci.}, {\bf 96}, 73--155.

3657: 

3658: \bibitem[\protect\citename{Meseguer \& Montanari, }1998]{MM:TLRL}

3659: Meseguer, J., \& Montanari, U. (1998).

3660: \newblock Mapping tile logic into rewriting logic.

3661: \newblock {\em Pages  62--91 of:} Parisi-Presicce, F. (ed), {\em Proceedings of

3662:   wadt'97, 12th workshop on recent trends in algebraic development techniques}.

3663: \newblock Lect.\ Notes in Comput.\ Sci., vol. 1376.

3664: \newblock Springer Verlag.

3665: 

3666: \bibitem[\protect\citename{Miller, }1995]{Mil:LPILL}

3667: Miller, D. (1995).

3668: \newblock {\em lambda prolog: An introduction to the language and its logic}.

3669: \newblock Unpublished. Available at

3670:   \url{http://www.cse.psu.edu/~dale/lProlog/docs.html}.

3671: 

3672: \bibitem[\protect\citename{Miller \& Nadathur, }1998]{MN:HOLP}

3673: Miller, D., \& Nadathur, G. (1998).

3674: \newblock Higher-order logic programming.

3675: \newblock {\em Pages  499--590 of:} Gabbay, D.M., Hogger, C.J., \& Robinson,

3676:   J.A. (eds), {\em Handbook of logics for artificial intelligence and logic

3677:   programming},  vol. 5.

3678: \newblock Clarendon Press.

3679: 

3680: \bibitem[\protect\citename{Milner, }1980]{Mil:CCS}

3681: Milner, R. (1980).

3682: \newblock {\em A {C}alculus of {C}ommunicating {S}ystems}.

3683: \newblock Lect.\ Notes in Comput.\ Sci., vol. 92.

3684: \newblock Springer Verlag.

3685: 

3686: \bibitem[\protect\citename{Milner, }1992]{Mil:PPC}

3687: Milner, R. (1992).

3688: \newblock The polyadic pi-calculus (abstract).

3689: \newblock {\em Page ~1 of:} Cleaveland, R. (ed), {\em Proceedings of concur

3690:   '92, 3rd international conference on concurrency theory}.

3691: \newblock Lect.\ Notes in Comput.\ Sci., vol. 630.

3692: \newblock Springer Verlag.

3693: 

3694: \bibitem[\protect\citename{Milner, }1996]{Mil:CFI}

3695: Milner, R. (1996).

3696: \newblock Calculi for interaction.

3697: \newblock {\em Acta inform.}, {\bf 33}(8), 707--737.

3698: 

3699: \bibitem[\protect\citename{Montanari \& Sassone, }1992]{MS:DCPB}

3700: Montanari, U., \& Sassone, V. (1992).

3701: \newblock Dynamic congruence vs. progressing bisimulation for {CCS}.

3702: \newblock {\em Fundamenta informaticae}, {\bf 16}, 171--196.

3703: 

3704: \bibitem[\protect\citename{Montanari \& Talcott, }1998]{MT:APA}

3705: Montanari, U., \& Talcott, C. (1998).

3706: \newblock Can actors and $\pi$-agents live together?

3707: \newblock  {\em Proceedings of hoots'98, 2nd workshop on higher order

3708:   operational techniques in semantics}.

3709: \newblock Elect.\ Notes in Th.\ Comput.\ Sci., vol. 10.

3710: \newblock Elsevier Science.

3711: 

3712: \bibitem[\protect\citename{Park, }1981]{Par:CAIS}

3713: Park, D. (1981).

3714: \newblock Concurrency and automata on infinite sequences.

3715: \newblock {\em Pages  167--183 of:} {\em Proceedings of fifth g-i conference}.

3716: \newblock Lect.\ Notes in Comput.\ Sci., vol. 104.

3717: \newblock Springer Verlag.

3718: 

3719: \bibitem[\protect\citename{Plotkin, }1981]{Plo:SAOS}

3720: Plotkin, G. (1981).

3721: \newblock {\em A structural approach to operational semantics}.

3722: \newblock Tech. rept. DAIMI FN-19. Aarhus University, Computer Science

3723:   Department.

3724: 

3725: \bibitem[\protect\citename{Rensink, }2000]{Ren:BOT}

3726: Rensink, A. (2000).

3727: \newblock Bisimilarity of open terms.

3728: \newblock {\em Inform.\ and comput.}, {\bf 156}, 345--385.

3729: 

3730: \bibitem[\protect\citename{Saraswat, }1989]{Sar:CC}

3731: Saraswat, V.A. (1989).

3732: \newblock {\em Concurrent constraint logic programming}.

3733: \newblock Ph.D. thesis, Carnegie-Mellon University.

3734: 

3735: \bibitem[\protect\citename{Sewell, }1998]{Sew:RRBC}

3736: Sewell, P. (1998).

3737: \newblock From rewrite rules to bisimulation congruences.

3738: \newblock {\em Pages  269--284 of:} Sangiorgi, D., \& de~Simone, R. (eds), {\em

3739:   Proceedings of concur'98}.

3740: \newblock Lect.\ Notes in Comput.\ Sci., vol. 1466.

3741: \newblock Springer Verlag.

3742: 

3743: \end{thebibliography}

3744: 

3745: \end{document}

3746: