1: \documentclass{tlp} 

2: 

3: \usepackage{epsf}

4: \usepackage{aopmath} 

5: \usepackage{amssymb}

6: \usepackage{proof}

7: \usepackage{euscript}

8: \usepackage{amsfonts}   

9: \usepackage{latexsym} 

10: 

11: 

12: %%%%%%%% macro %%%%%%%

13: 

14: \newenvironment{pf}

15: {\begin{trivlist}\item[]{\bf Proof : }}

16: {\hspace*{\fill}{$\Box$}\end{trivlist}}

17: 

18: %%%%%%%%% Space adjustments

19: 

20: \newcommand{\redspace}{\vspace*{-2.0mm}}

21: \newcommand{\vsp}{\vspace*{0.2cm}}

22: 

23: 

24: %%%%%%% REGOLE

25: 

26: \newcommand{\infrule}[3]{

27: \begin{equation}

28: \label{#1}{#2}\over{#3}

29: \end{equation}}

30: 

31: %%%%%%% CONNETTIVI

32: \def\proimp{ \mbox{:-}}

33: 

34:   %%%%%%%%%%%%%% PAR %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

35: %  \draw package.  Vaughan Pratt  (C) 1993

36: %

37: %       *+,-|.|/012     Table of 81 vectors in [-4,4]x[-4,4]

38: %       3456|7|89:;     Use as parameters to tell \draw how to step along

39: %       <=>?|@|ABCD     \draw zzzzzzz\end draws a straight line 7 steps

40: %       EFGH|I|JKLM        down and to the right

41: %       ----+-+----

42: %       NOPQ|R|STUV     R = (0,0), C = (3,2), * = (-4,-4), r = (-4,4)

43: %       ----+-+----

44: %       WXYZ|[|$$^_     \draw -./9:CMV_gpowvukjaWNE=45\end

45: %       `abc|d|efgh        draws a reasonable circle

46: %       ijkl|m|nopq

47: %       rstu|v|wxyz

48: %

49: \newcount\PLv\newcount\PLw\newcount\PLx\newcount\PLy\newdimen\PLyy\newdimen\PLX

50: \newbox\PLdot \setbox\PLdot\hbox{\tiny.} \def\scl{.08} % resettable scale

51: \def\PLot#1{\PLx`#1\advance\PLx-42\PLy\PLx\PLv\PLx\divide\PLy9\PLw\PLy\multiply

52: \PLw9\advance\PLx-\PLw\advance\PLx-4\PLy-\PLy\advance\PLy4\PLX=\the\PLx pt

53: \advance\PLyy\the\PLy pt\wd\PLdot=\scl\PLX\raise\scl\PLyy\copy\PLdot}

54: \def\draw#1{\ifx#1\end\let\next=\relax\else\PLot#1\let\next=\draw\fi\next}

55: 

56: %  Girard's inverted ampersand.  Usage: \invamp. Draw time @ 10 Mips: .33 sec

57: \def\invamp{\hbox{\PLyy=70pt\draw :::;DMV_gqppyyyyyooooxxxnnwvlutkjaWNE=5-./9%

58: 9:::CCCC:::99/..--544=EENWWaajjjkktttttttNNNVVVVVVVV\end \hskip4pt}}

59: %  \Invamp = Boxed \invamp.  Draw time < .02 sec, but max \ 300 chars/page

60: \newbox\iabox\setbox\iabox\invamp \def\Invamp{\copy\iabox}

61: \newcommand{\seque}{;}

62: \newcommand{\intu}{\Rightarrow}

63: \newcommand{\intui}{\Rightarrow}

64: \newcommand{\into}{\Leftarrow}

65: \newcommand{\with}{\,\&\,}

66: \newcommand{\lolli}{\mathbin{-\hspace{-0.70mm}\circ}}

67: \newcommand{\lollo}{\mathbin{\circ\hspace{-0.70mm}-}}

68: \newcommand{\lollol}{\mathbin{\circ\hspace{-0.70mm}-}\!\!\circ}

69: \newcommand{\metarrow}{\mathbin{\triangleleft\hspace{-0.50mm}-}}

70: \newcommand{\para}{\mathrel{\Invamp}}

71: \newcommand{\tensor}{\otimes}

72: %\newcommand{\ltimes}{\otimes}

73: \newcommand{\anti}{\bot}

74: \newcommand{\all}{\top}

75: \newcommand{\one}{ {\bf 1} }

76: \newcommand{\zero}{ {\bf 0}}

77: \newcommand{\mybang}[1]{\mathbin{!} #1}

78: \newcommand{\rcimpl}{\subset}

79: 

80: 

81: %%%%%%%%%%%%%%%% TYPES

82: \newcommand{\emsg}[1]{\langle\!\langle #1 \rangle\!\rangle}

83: \newcommand{\imsg}[1]{\blangle #1 \brangle}

84: \newcommand{\ra}{\rightarrow}

85: \newcommand{\obj}[1]{[\!\![\,#1\,]\!\!]}

86: \newcommand{\objhead}[1]{{\bf object}(#1)}

87: \newcommand{\objexe}[1]{{\bf frozen}(#1)}

88: \newcommand{\newemsg}[2]{{\bf send}(#1)(#2)}

89: \newcommand{\newimsg}[2]{{\bf call}(#1)(#2)}

90: \newcommand{\new}[1]{{\bf new}#1}

91: \newcommand{\priv}[1]{{\bf private}(#1)}

92: \newcommand{\names}[1]{{\bf names}(#1)}

93: \newcommand{\clone}{{\bf clone}}

94: \newcommand{\merge}{{\bf merge}}

95: \newcommand{\delegate}[3]{{\bf del}(#1)(#2)(#3)}

96: \newcommand{\extend}{{\bf extend}}

97: \newcommand{\override}{{\bf override}}

98: \newcommand{\semsg}[1]{{\bf send}(#1)}

99: \newcommand{\simsg}[1]{{\bf call}(#1)}

100: %%%%%%%%%%%%%%%% LANGUAGE NAMES %%%%%%%%%%%%

101: 

102: \newcommand{\FO}{F\&O}

103: \newcommand{\Lolli}{Lolli}

104: \newcommand{\ACL}{ACL}

105: \newcommand{\ImpLang}{{\em Small}}

106: \newcommand{\mhhf}{${\cal E}_{hhf}$} 

107: \newcommand{\capitalmhhf}{\mhhf}

108: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

109: \newcommand{\statecons}      {\Sigma_{\R}}

110: \newcommand{\stateatoms}     {\Pi_{\statecons}}

111: \newcommand{\bigtensor}      { \bigotimes}

112: \newcommand{\bigpar}         { \para }

113: \newcommand{\range}     [1]  { {i:1.. #1} }

114: \newcommand{\marking}      [1]  { {\bf #1} }

115: \newcommand{\markingdecide}[1]  { \{ #1 \} }

116: \newcommand{\dfrm}{$\D$-formula}

117: \newcommand{\dfrms}{$\D$-formulas}

118: \newcommand{\hfrm}{$\Head$-formula}

119: \newcommand{\hfrms}{$\Head$-formulas}

120: \newcommand{\gfrm}{$\G$-formula}

121: \newcommand{\gfrms}{$\G$-formulas}

122: \newcommand{\balls}{\stackrel{.}{\bullet}}

123: %%%%%%%%%%%

124: \newcommand{\mminus}{\setminus}

125: \newcommand{\munion}{\uplus}

126: \newcommand{\bigmunion}{\biguplus}

127: %%%%%%% SIDE CONDITIONS %%%%%%%%%%%%%%%%%

128: \newcommand{\sidei}{(i)}

129: \newcommand{\sideii}{(ii)}

130: \newcommand{\sideiii}{(iii)}

131: 

132: %%%%%% FORMULE

133: 

134: \newcommand{\labseque}[3]{ {#1\seque...\seque #2}_{(#3)} }

135: \newcommand{\plabseque}[3]{ {#1\seque #2}_{(#3)} }

136: \newcommand{\genlabseque}[2]{ {#1}_{(#2)} }

137: 

138: %%%%%%% MEASURE

139: 

140: \newcommand{\psize}[2]{[#1]_{\scriptscriptstyle #2}}

141: \newcommand{\psizec}[1]{\psize{#1}{c}}

142: 

143: %%%%%%% SEQUENTI

144: 

145: \newcommand{\aclseq}[1]{\vdash{#1}}

146: \newcommand{\gentzen} [2]{#1\longrightarrow #2}

147: \newcommand{\transl}  [2]{( #1 )_{#2}^{\circ}}

148: \newcommand{\forumseq}[4]{#1:#2; #3 \rightarrow #4}

149: \newcommand{\sforumseq}[3]{\forumseq{\Sigma}{#1}{#2}{#3}}

150: \newcommand{\mseq}[4]{ #1;#2\,[#3]\longrightarrow_{\Sigma}#4}

151: \newcommand{\mseqp}[4]{ #1;#2\longrightarrow_{\Sigma}#4}

152: \newcommand{\smseq}[5]{#1;#2\,[#3]\longrightarrow_{#4} #5}

153: \newcommand{\smseqp}[5]{#1;#2\longrightarrow_{#4} #5}

154: \newcommand{\pmseq}[2]{\msmhhseq{\Gamma}{#1}{\Phi}{#2}}

155: \newcommand{\simplyseq}[3]{#1; #2 \rightarrow #3}

156: 

157: %%%%%% RULES MHHF

158: 

159: \newcommand{\rall}{halt}

160: \newcommand{\ranti}{erase}

161: \newcommand{\rpar}{sync}

162: \newcommand{\rwith}{and}

163: \newcommand{\rimpl}{fire}

164: \newcommand{\rintu}{augment}

165: \newcommand{\rforall}{hide}

166: \newcommand{\rres}{bc}

167: \newcommand{\rver}{verify}

168: \newcommand{\rmove}{move}

169: \newcommand{\rfinal}{result}

170: \newcommand{\rempty}{empty}

171: \newcommand{\grndbc}{lollibc}

172: 

173: %%%%%% RULES FORUM

174: 

175: \newcommand{\fall}{\all}

176: \newcommand{\fantiL}{\anti_l}

177: \newcommand{\fantiR}{\anti_r}

178: \newcommand{\fparaR}{\para_r}

179: \newcommand{\fparaL}{\para_l}

180: \newcommand{\flollo}{\lollo}

181: \newcommand{\flolli}{\lolli}

182: \newcommand{\fintui}{\intui}

183: \newcommand{\finto}{\into}

184: \newcommand{\fdecide}{decide}

185: \newcommand{\finitial}{initial}

186: \newcommand{\fwithR}{\with_r}

187: \newcommand{\fwithL}{\with_l}

188: \newcommand{\fforallR}{\forall_r}

189: \newcommand{\fforallL}{\forall_l}

190: 

191: %%%%%% EMBEDDINGS & MAPPINGS

192: 

193: \newcommand{\quant}[1]{#1^\forall}

194: \newcommand{\boundmap}[1]{#1_b}

195: \newcommand{\unboundmap}[1]{#1_u}

196: \newcommand{\mhhftoforum}[1]{(#1)^\circ}

197: \newcommand{\instances}[1]{\langle #1\rangle} 

198: 

199: %%%%% PROVABILITY

200: \newcommand{\llequiv}{\equiv_l}

201: \newcommand{\llprov}{\vdash_l}

202: \newcommand{\mhhfprov}{\vdash_e}

203: \newcommand{\forumprov}{\vdash_f}

204: \newcommand{\resolprov}{\vdash_f^r}

205: \newcommand{\forumproof}[2]{#1\forumprov #2}

206: \newcommand{\resolproof}[2]{#1\resolprov #2}

207: \newcommand{\foprov}{\vdash_{fo}}

208: \newcommand{\mmprov}{\vdash_e^m}

209: \newcommand{\mmproof}[2]{#1\mmprov #2}

210: \newcommand{\bcprov}{\vdash_f^{bc}}

211: \newcommand{\bcproof}[2]{#1\bcprov #2}

212: 

213: \newcommand{\grndprov}{\vdash_f^{l}}

214: \newcommand{\grndproof}[2]{#1\grndprov #2}

215: 

216: \newcommand{\proofhat}[1]{\bar{#1}}

217: 

218: %%%%%%% FO PROOF SYSTEM

219: 

220: % \arrowUpLabel

221: \newcommand{\arrowupdown}[4]{\setbox0=\hbox{$\ {}^{#2}\ $}

222:   \setbox1=\hbox{$\longrightarrow$}

223:   \ifdim\wd0<\wd1\setbox0=\box1\else\relax\fi

224:   {#1}\,\mathop{\hbox to \wd0{\rightarrowfill}}\limits^{#2}_{#3}\,{#4}

225: }

226: 

227: % \arrowBelowLabel

228: \newcommand{\arrowdown}[3]{\setbox0=\hbox{$\ {}_{#2}\ $}

229:   \setbox1=\hbox{$\longrightarrow$}

230:   \ifdim\wd0<\wd1\setbox0=\box1\else\relax\fi

231:   {#1}\,\mathop{\hbox to \wd0{\rightarrowfill}}\limits_{#2}\,{#3}

232: }

233: 

234: 

235: % \Arrow

236: \newcommand\Arrow[3]{\setbox0=\hbox{$\ {}^{#2}\ $}

237:   \setbox1=\hbox{$\Rightarrow$}

238:   \loop\setbox1=\hbox{=\kern-0.3em\unhbox1}\ifdim\wd1<\wd0\repeat

239:   \hbox{${#1}\,\mathop{\box1}\limits^{#2\,}{#3}$}

240: }

241: 

242: % double arrow

243: 

244: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

245: %%%%%%%%%%%%%%%%%% FO SEQUENTS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

246: \newcommand{\blangle}{\langle\!\!\langle}

247: \newcommand{\brangle}{\rangle\!\!\rangle}

248: \newcommand{\rhssep}{\mid\!\mid}

249: \newcommand{\sfoseq}[5]{#2;#3\rightarrow_{#1} #4\,\rhssep\,#5}

250: \newcommand{\foseq}[4]{\sfoseq{\Sigma}{#1}{#2}{#3}{#4}}

251: \newcommand{\unsfos}[5]{#2\,[#3]\rightarrow_{\Sigma} #4\,\rhssep\,#5}

252: \newcommand{\sprfosequent}[2]{\fosequent{\Prog}{\R}{#1}{#2}}

253: \newcommand{\fosequent}[4]{\foseq{#1}{#2}{#3}{#4}}

254: \newcommand{\foresults}[1]{(#1)}

255: \newcommand{\foseqnt}[5]{{#1};{#2}[{#3}]\rightarrow_{\Sigma}{#4\,\rhssep\,#5}}

256: \newcommand{\sfoseqnt}[6]{{#2};{#3}[{#4}]\rightarrow_{#1}{#5\,\rhssep\,#6}}

257: %%%%%%%%%% MULTI-HEADED CLAUSE 

258: 

259: %\newcommand{\multihead}[1]{ #1\left} }

260: 

261: 

262: 

263: %%%%%%%%%%%%% LTS %%%%%%%%%%%%%%%%%%%%%%%%%%

264: 

265: \newcommand{\rewrel}[1]{\leadsto_{#1}}

266: \newcommand{\rewrelclosed}[1]{\leadsto^\star_{#1}}

267: \newcommand{\orule}{\rewrel{o}}

268: \newcommand{\qorel}{\stackrel{\scriptsize\forall}{\leadsto_o}}

269: \newcommand{\qostar}{\stackrel{\scriptsize\forall *}{\leadsto_o}}

270: \newcommand{\spair}[1]{\langle{#1}\rangle}

271: 

272: \newcommand{\orulestar}[2]

273: {{\langle{#1}\rangle}\rewrelclosed{o}{\langle{#2}\rangle}}

274: 

275: \newcommand{\qorule}[2]

276: {{\langle{#1}\rangle}\qorel{\langle{#2}\rangle}}

277: 

278: \newcommand{\qorulestar}[2]

279: {{\langle{#1}\rangle}\qostar{\langle{#2}\rangle}}

280: 

281: \newcommand{\LTSrule}[3]

282: {{\langle{#1}\rangle}\rewrel{#2}{#3}}

283: 

284: \newcommand{\LTSrulestar}[3]

285: {{\langle{#1}\rangle}\rewrelclosed{#2}{#3}}

286: %{\arrowupdown{\langle{#1}\rangle}{\star}{#2}{#3}}

287: 

288: \newcommand{\LTSsrule}[2]

289: {\LTSrule{#1}{s}{\langle{#2}\rangle}}

290: 

291: \newcommand{\LTSerule}[2]

292: {\LTSrule{#1}{e}{#2}}

293: 

294: \newcommand{\LTSdrule}[2]

295: {\LTSrule{#1}{d}{\langle{#2}\rangle}}

296: 

297: \newcommand{\LTSbrule}[2]

298: {\LTSrule{#1}{b}{#2}}

299: 

300: \newcommand{\LTSdrulestar}[2]

301: {\LTSrulestar{#1}{d}{\langle{#2}\rangle}}

302: 

303: \newcommand{\LTSsrulestar}[2]

304: {\LTSrulestar{#1}{s}{\langle{#2}\rangle}}

305: 

306: %%%%%% Small Language

307: 

308: \newcommand{\sskip}{{\bf skip} }

309: \newcommand{\sif}{{\bf if}}

310: \newcommand{\sthen}{{\bf then}}

311: \newcommand{\selse}{{\bf else}}

312: \newcommand{\swhile}{{\bf while}}

313: \newcommand{\sdo}{{\bf do}}

314: \newcommand{\sass}{\hbox{:=}}

315: \newcommand{\sis}{{\bf is}}

316: \newcommand{\sblock}{{\bf in}}

317: \newcommand{\sproc}{{\bf proc}}

318: \newcommand{\svar}{{\bf var}}

319: \newcommand{\splus}{\hbox{+}}

320: \newcommand{\sequal}{\hbox{=}}

321: \newcommand{\sconc}{\hbox{;}}

322: \newcommand{\sprogram}{{\bf program}}

323: 

324: \newcommand{\ptau}{\hbox{\bf $\tau$-rule}}

325: \newcommand{\phalt}{\hbox{\bf halt}}

326: \newcommand{\pfork}{\hbox{\bf fork}}

327: \newcommand{\psync}{\hbox{\bf sync}}

328: \newcommand{\preceive}{\hbox{\bf receive}}

329: \newcommand{\psend}{\hbox{\bf send}}

330: \newcommand{\pwake}{\hbox{\bf wake}}

331: 

332: \newcommand{\sA}     {\mbox{{\sc a}}}

333: \newcommand{\sB}     {\mbox{{\sc b}}}

334: \newcommand{\sC}     {\mbox{{\sc c}}}

335: \newcommand{\sD}     {\mbox{{\sc d}}}

336: \newcommand{\sE}     {\mbox{{\sc e}}}

337: \newcommand{\sF}     {\mbox{{\sc f}}}

338: \newcommand{\sG}     {\mbox{{\sc g}}}

339: \newcommand{\sH}     {\mbox{{\sc h}}}

340: \newcommand{\sI}     {\mbox{{\sc i}}}

341: \newcommand{\sJ}     {\mbox{{\sc j}}}

342: \newcommand{\sK}     {\mbox{{\sc k}}}

343: \newcommand{\sL}     {\mbox{{\sc l}}}

344: \newcommand{\sM}     {\mbox{{\sc m}}}

345: \newcommand{\sN}     {\mbox{{\sc n}}}

346: \newcommand{\sO}     {\mbox{{\sc o}}}

347: \newcommand{\sOpr}   {\mbox{{\sc o'}}}

348: \newcommand{\sP}     {\mbox{{\sc p}}}

349: \newcommand{\sQ}     {\mbox{{\sc q}}}

350: \newcommand{\sR}     {\mbox{{\sc r}}}

351: \newcommand{\sS}     {\mbox{{\sc s}}}

352: \newcommand{\sT}     {\mbox{{\sc t}}}

353: \newcommand{\sU}     {\mbox{{\sc u}}}

354: \newcommand{\sV}     {\mbox{{\sc v}}}

355: \newcommand{\sZ}     {\mbox{{\sc z}}}

356: \newcommand{\sW}     {\mbox{{\sc w}}}

357: \newcommand{\sX}     {\mbox{{\sc x}}}

358: \newcommand{\sY}     {\mbox{{\sc y}}}

359: \newcommand{\CP}     {\mbox{{\sc cp}}}

360: \newcommand{\TwoP}   {\mbox{{\sc p2d}}}

361: \newcommand{\YP}     {\mbox{{\sc yp}}}

362: \newcommand{\NO}     {\mbox{{\sc no}}}

363: \newcommand{\NP}     {\mbox{{\sc np}}}

364: \newcommand{\COL}    {\mbox{{\sc col}}}

365: 

366: \newcommand{\termap}{^{+}}

367: \newcommand{\formap}{^{\star}}

368: 

369: 

370: % Definitions for Neg

371: 

372: \newcommand{\immm}[1]{^{\circ_{#1}}}

373: \newcommand{\imm}{^\circ}

374: \newcommand{\imtwo}{\immm{2}}

375: \newcommand{\ffth}{\Phi}

376: \newcommand{\bfail}{sfail}

377: \newcommand{\btrue}{strue}

378: 

379: %%%%% sezioni e ambienti %%%%%

380: 

381: \newcommand {\sectionl} [2] {\section {#1} \label {#2}}

382: \newcommand {\subsectionl} [2] {\subsection {#1} \label {#2}}

383: \newcommand {\captionl} [2] {\caption {#1} \label {#2}}

384: 

385: \newtheorem {es}{Example}

386: 

387: \newenvironment{example}{\begin{es}}{\hspace*{\fill}$\Box$\end{es}}

388: 

389: \newenvironment{proof2}

390: {\begin{trivlist}\item[]{\bf Proof.\ }}

391: {\hspace*{\fill}{$\Box$}\end{trivlist}}

392: 

393: 

394: %%%%% spaziatura %%%%%

395: 

396: \newcommand {\indtw} {\mbox{\ \ }}

397: \newcommand {\nl} {\mbox{}\\}

398: \newcommand {\vs} {\vspace{0.2cm}}

399: 

400: 

401: %%%%% lettere accentate %%%%%

402: 

403: \newcommand {\Aa} {\mbox{\`{a}\ }}

404: \newcommand {\Ae} {\mbox{\`{e}\ }}

405: \newcommand {\Ai} {\mbox{\`{\i}\ }}

406: \newcommand {\Ao} {\mbox{\`{o}\ }}

407: \newcommand {\Au} {\mbox{\`{u}\ }}

408: \newcommand {\aA} {\mbox{\`{A}\ }}

409: \newcommand {\aE} {\mbox{\`{E}\ }}

410: \newcommand {\aI} {\mbox{\`{I}\ }}

411: \newcommand {\aO} {\mbox{\`{O}\ }}

412: \newcommand {\aU} {\mbox{\`{U}\ }}

413: 

414: \newcommand {\che} {\mbox{ch\'{e}\ }}

415: 

416: %%%%% lettere calligrafiche %%%%%

417: 

418: \newcommand {\calA} {\mbox{${\cal A}$}} 

419: \newcommand {\calB} {\mbox{${\cal B}$}}

420: \newcommand {\calC} {\mbox{${\cal C}$}}

421: \newcommand {\calD} {\mbox{${\cal D}$}}

422: \newcommand {\calE} {\mbox{${\cal E}$}}

423: \newcommand {\calF} {\mbox{${\cal F}$}}

424: \newcommand {\calG} {\mbox{${\cal G}$}}

425: \newcommand {\calH} {\mbox{${\cal H}$}}

426: \newcommand {\calI} {\mbox{${\cal I}$}}

427: \newcommand {\calJ} {\mbox{${\cal J}$}}

428: \newcommand {\calK} {\mbox{${\cal K}$}} 

429: \newcommand {\calL} {\mbox{${\cal L}$}}

430: \newcommand {\calM} {\mbox{${\cal M}$}} 

431: \newcommand {\calN} {\mbox{${\cal N}$}}

432: \newcommand {\calO} {\mbox{${\cal O}$}} 

433: \newcommand {\calP} {\mbox{${\cal P}$}} 

434: \newcommand {\calQ} {\mbox{${\cal Q}$}}

435: \newcommand {\calR} {\mbox{${\cal R}$}} 

436: \newcommand {\calS} {\mbox{${\cal S}$}} 

437: \newcommand {\calT} {\mbox{${\cal T}$}} 

438: \newcommand {\calU} {\mbox{${\cal U}$}} 

439: \newcommand {\calV} {\mbox{${\cal V}$}} 

440: \newcommand {\calW} {\mbox{${\cal W}$}} 

441: \newcommand {\calX} {\mbox{${\cal X}$}}

442: \newcommand {\calY} {\mbox{${\cal Y}$}}  

443: \newcommand {\calZ} {\mbox{${\cal Z}$}}

444: 

445: 

446: %%%%% identificatori da usare in formule %%%%%

447: 

448: \newcommand{\off}                  {o\!f\!\!f}

449: \newcommand{\field}                {f\!ield}

450: \newcommand{\If}                   {i\!f}

451: \newcommand{\deferred}             {de\!f\!erred}

452: \newcommand{\deftrlist }           {de\!f\!trlist}

453: \newcommand{\beforelist}           {be\!f\!orelist}

454: \newcommand{\afterlist}            {a\!f\!terlist}

455: \newcommand{\before}               {be\!f\!ore}

456: \newcommand{\after}                {a\!f\!ter}

457: \newcommand{\difflist}             {di\!f\!\!f\!list}

458: \newcommand{\caffe}                {ca\!f\!\!f\!\grave{e}}

459: \newcommand{\lifetime}             {li\!f\!etime}

460: \newcommand{\flatten}              {f\!latten}

461: \newcommand{\lifeExpectancy}       {li\!f\!eExpectancy}

462: \newcommand{\changeLifeExpectancy} {changeLi\!f\!eExpectancy}

463: \newcommand{\EmptyBuffer}          {EmptyBu\!f\!\!f\!er}

464: \newcommand{\FullBuffer}           {F\!ullBu\!f\!\!f\!er}

465: \newcommand{\Left}                 {le\!f\!t}

466: \newcommand{\verify}               {veri\!f\!y}

467: \newcommand{\fire}                 {f\!ire}

468: \newcommand{\fork}                 {f\!ork}

469: \newcommand{\redefine}             {rede\!f\!ine}

470: \newcommand{\redefined}            {rede\!f\!ined}

471: 

472: 

473: %%%%% numeri naturali %%%%%

474: 

475: \newcommand{\Nat}{\mbox{\cal N}}

476: 

477: 

478: %%%%% algebre %%%%%

479: 

480: \newcommand{\segnat}{\mbox{$ \Sigma = (OP,PR) $}}

481: \newcommand{\Algsigma}{\mbox{$ Alg_\Sigma $}}

482: \newcommand{\Tsigma}{\mbox{$ T_{\Sigma} $}}

483: \newcommand{\TsigmaP}{\mbox{$ T_{\Sigma_P} $}}

484: \newcommand{\TsigmaX}{\mbox{$ T_{\Sigma}(X) $}}

485: \newcommand{\evalAv}{\mbox{$ eval^{A,v} $}}

486: 

487: 

488: %%%%% simboli matematici %%%%%

489: 

490: \newcommand{\smallunion}{\cup}

491: \newcommand{\myunion}{\bigcup}

492: \newcommand{\multiunion}{\uplus}

493: \newcommand{\diff}{\setminus}

494: \newcommand{\intersect}{\cap}

495: \newcommand{\equival}{\ \Leftrightarrow\ }

496: \newcommand{\implica}{\ \Rightarrow\ }

497: \newcommand{\compos}{\circ}

498: \newcommand{\tupleo} [1] {\langle {#1} \rangle}

499: \newcommand{\couple} [2] {\langle {#1},{#2} \rangle}

500: \newcommand{\triple} [3] {\langle {#1},{#2},{#3} \rangle}

501: \newcommand{\qparl}{\mbox{$ [ $}}

502: \newcommand{\qparr}{\mbox{$ ] $}}

503: \newcommand{\diam} [1] {{#1}^\diamond}

504: 

505: 

506: %%%%% sistemi deduttivi %%%%%

507: 

508: \newcommand{\ded}{\vdash}

509: \newcommand{\dedo} [1] {\vdash {#1}}

510: \newcommand{\dedtw} [2] {\vdash^{#1}{#2}}

511: \newcommand{\dedt} [3] {{#1}\vdash^{#2}{#3}}

512: \newcommand{\dedD} [1] {\ded^{#1}}

513: \newcommand{\dedchilb} {\ded^H}

514: \newcommand{\dedC} {\vdash_{\calC}}

515: \newcommand{\dedI} {\vdash_{\calI}}

516: \newcommand{\dedM} {\vdash_{\calM}}

517: \newcommand{\dedItw} [2] {{#1} \dedI {#2}}

518: \newcommand{\dedLL}{\vdash_{LL}}

519: \newcommand{\dedLLtw} [2] {{#1} \dedLL {#2}}

520: \newcommand{\dedL}{\vdash_{\calL}}

521: \newcommand{\dedLt} [3] {{#1};{#2} \dedL {#3}}

522: 

523: \newcommand{\dedLO} [2] {{#1}\Rightarrow{#2}}

524: \newcommand{\dedLOo} [2] {{#1}\Rightarrow_\one{#2}}

525: 

526: %%%%% validita' %%%%%

527: 

528: 

529: \newcommand {\valid}{\models}

530: \newcommand {\valido} [1] {\models #1}

531: \newcommand {\validtw} [2] {#1 \models #2}

532: \newcommand {\validt} [3] {#1,#2 \models #3}

533: \newcommand {\nvalid}{\not\models}

534: \newcommand {\nvalido} [1] {\not\models #1}

535: \newcommand {\nvalidtw} [2] {#1 \not\models #2}

536: \newcommand {\nvalidt} [3] {#1,#2 \not\models #3}

537: 

538: 

539: %%%%% sequenti %%%%%

540: 

541: \newcommand{\rarr} {\rightarrow}

542: \newcommand{\rarro} [1] {\rarr {#1}}

543: 

544: \newcommand {\cseq} [2] {{#1}\rightarrow{#2}}

545: \newcommand {\cseqt} [3] {{#1}:{#2}\rightarrow{#3}}

546: \newcommand {\cseqstd} {\cseq{\Gamma}{\Delta}}

547: \renewcommand {\seq} [6] {{#1};{#2}[{#3}]\rightarrow_{#4}{#5\,\rhssep\,#6}}

548: \newcommand {\seqstd} {\seq {\Gamma}{\Delta}{\Phi}{\Sigma}{\Omega}{\Theta}}

549: \newcommand {\seqS} [5] {{#1};{#2}[{#3}]\rightarrow_{\Sigma}{#4\,\rhssep\,#5}}

550: \newcommand {\seqR} [5] {{#1};{#2}\rightarrow_{#3}{#4\,\rhssep\,#5}}

551: \newcommand {\seqRS} [4] {{#1};{#2}\rightarrow_{\Sigma}{#3\,\rhssep\,#4}}

552: \newcommand {\seqT} [5] {{#1};{#2}[{#3}]\rightarrow_{#4}{#5}}

553: \newcommand {\seqST} [4] {{#1};{#2}[{#3}]\rightarrow_{\Sigma}{#4}}

554: \newcommand {\seqRT} [4] {{#1};{#2}\rightarrow_{#3}{#4}}

555: \newcommand {\seqRST} [3] {{#1};{#2}\rightarrow_{\Sigma}{#3}}

556: \newcommand {\seqt} [3] {{#1};{#2} \rightarrow {#3}}

557: \newcommand {\sseq} [2] {\Sigma:{#1}\rightarrow{#2}}

558: \newcommand {\sseqP} [1] {\Sigma:\calP\rightarrow{#1}}

559: \newcommand {\sseqt} [3] {{#1}:{#2}\rightarrow{#3}}

560: \newcommand {\LOseq} [2] {{#1} \rightarrow {#2}}

561: \newcommand {\LOseqo} [1] {\LOseq {\ }{{#1}}}

562: \newcommand {\ACLseq} [2] {{#1} \rightarrow {#2}}

563: \newcommand {\ACLseqo} [1] {\ACLseq {\mybang{\bf P}}{{#1}}}

564: \newcommand {\hypseq} [4] {{#1} \rarr {#2} \Rightarrow {#3} \rarr {#4}}

565: \newcommand {\hypseqtw} [2] {\rarr {#1} \Rightarrow {#2}}

566: \newcommand {\Fseq} [5] {{#1}:{#2};{#3}\rightarrow {#4};{#5}}

567: \newcommand {\FseqS} [4] {\Sigma:{#1};{#2}\rightarrow {#3};{#4}}

568: \newcommand {\FseqU} [4] {{#1}:{#2};{#3}\rightarrow {#4};\Upsilon}

569: \newcommand {\FseqSU} [3] {\Sigma:{#1};{#2}\rightarrow {#3};\Upsilon}

570: \newcommand {\FseqB} [6] {{#1}:{#2};{#3}\stackrel{#4}{\rightarrow} {#5};{#6}}

571: \newcommand {\FseqBS} [5] {\Sigma:{#1};{#2}\stackrel{#3}{\rightarrow} 

572:                            {#4};{#5}}

573: \newcommand {\FseqBU} [5] {{#1}:{#2};{#3}\stackrel{#4}{\rightarrow}

574:                            {#5};\Upsilon}

575: \newcommand {\FseqBSU} [4] {\Sigma:{#1};{#2}\stackrel{#3}{\rightarrow}

576:                             {#4};\Upsilon}

577: 

578: %%%%% prove %%%%%

579: 

580: \newcommand {\Cprova} {{\bf C}-prova}

581: \newcommand {\Iprova} {{\bf I}-prova}

582: \newcommand {\Mprova} {{\bf M}-prova}

583: \newcommand {\Cprove} {{\bf C}-prove}

584: \newcommand {\Iprove} {{\bf I}-prove}

585: \newcommand {\Mprove} {{\bf M}-prove}

586: \newcommand {\Cproof} [2] {\Sigma: {#1} \ded_C {#2}}

587: \newcommand {\Iproof} [2] {\Sigma: {#1} \ded_I {#2}}

588: \newcommand {\Mproof} [2] {\Sigma: {#1} \ded_M {#2}}

589: 

590: 

591: %%%%% sigle di linguaggi %%%%%

592: 

593: \newcommand{\ehhf}{${\cal E}_{hhf}$}

594: \newcommand{\LDL} {$\calL\calD\calL$}

595: \newcommand{\TR} {$\calT\calR$}

596: \newcommand{\CTR} {$\calC\calT\calR$}

597: 

598: 

599: %%%%% linguaggi del primo ordine %%%%%

600: 

601: \newcommand{\Asigma}{\mbox{$ A_{\Sigma} $}}

602: \newcommand{\AsigmaX}{\mbox{$ A_{\Sigma}(X) $}}

603: \newcommand{\AsigmaP}{\mbox{$ A_{\Sigma_P} $}}

604: \newcommand{\FOFsigma}{\mbox{$ FOF_{\Sigma} $}}

605: \newcommand{\FOFsigmaX}{\mbox{$ FOF_{\Sigma}(X) $}}

606: 

607: 

608: %%%%% universo e base di Herbrand %%%%%

609: 

610: \newcommand{\HU}{\calH\calU}

611: \newcommand{\HB}{\calH\calB}

612: 

613: 

614: %%%%% connettivi logica classica %%%%%

615: 

616: \newcommand {\cand}{\wedge}

617: \newcommand {\clor}{\vee}

618: \newcommand {\cimpl}{\supset}

619: \newcommand {\cnot}{\neg}

620: \newcommand {\ctrue}{\top}

621: \newcommand {\cfalse}{\bot}

622: \newcommand {\cequiv}{\equiv}

623: \newcommand {\forallp} {\forall\ \ }

624: \newcommand {\forallt} {\forall_\tau}

625: \newcommand {\existst} {\exists_\tau}

626: \newcommand {\forallc} {\hat{\forall}}

627: \newcommand {\existsc} {\hat{\exists}}

628: 

629: 

630: %%%%%

631: 

632: \newcommand {\eset} {\emptyset}

633: 

634: %%%%% connettivi lineari %%%%%

635: 

636: \newcommand {\lneg} [1] {\mbox {$ #1^\anti $}}

637: 

638: 

639: %%%%% Prolog/lambda-Prolog %%%%%

640: 

641: \newcommand{\ifP}{\mbox{\tt{\,:{\bf -}\,}}}

642: \newcommand{\goalP}{\mbox{\tt{?{\bf -}\,}}}

643: \newcommand{\intuP}{\mbox{\scriptsize{\boldmath $=\!>$}}}

644: \newcommand{\lolliP}{\mbox{\small{\boldmath $-\circ$}}}

645: \newcommand{\andP}{\mbox{\tt{\bf ,}}}

646: \newcommand{\trueP}{\mbox{\tt true}}

647: \newcommand{\intoP}{\mbox{\scriptsize{\boldmath $<\!=$}}}

648: \newcommand{\withP}{\mbox{\tt \&}}

649: \newcommand{\mybangP}{\mbox{\tt bang}}

650: \newcommand{\eraseP}{\mbox{\tt erase}}

651: 

652: 

653: %%%%% LO %%%%%

654: 

655: \newcommand{\elev}{\mbox{}^\wedge}

656: \newcommand{\LOreg} [1] {\qparl {#1} \qparr}

657: 

658: 

659: %%%%% ACL %%%%%

660: 

661: \newcommand{\AP}{\calA_{P}}

662: \newcommand{\APo} [1] {\calA_{P{#1}}}

663: \newcommand{\Am}{\calA_{m}}

664: \newcommand{\GF} [1] {\calG\calF_{{#1}}}

665: \newcommand{\GC} [1] {\calG\calC_{{#1}}}

666: \newcommand{\Pg} [1] {\calP_{{#1}}}

667: \newcommand{\IR} [1] {\calI\calR_{{#1}}}

668: 

669: 

670: %%%%% Lolli %%%%%

671: 

672: \newcommand{\IOc} [3] {{#1} \{ {#2} \} {#3}}

673: 

674: 

675: %%%%% Lygon %%%%%

676: 

677: \newcommand {\mT} [1] {{#1}^T}

678: \newcommand {\mQ} [1] {{\mbox{?`}} {#1}}

679: 

680: \newcommand {\tensorL}{\mbox {\tt \ *\ }}

681: \newcommand {\oplusL} {\mbox {\tt \ @\ }}

682: \newcommand {\oneL}   {\mbox {\tt one}}

683: \newcommand {\withL}  {\mbox {\tt \ \&\ }}

684: \newcommand {\paraL}  {\mbox {\tt \ \#\ }}

685: \newcommand {\allL}   {\mbox {\tt top}}

686: \newcommand {\lolliL} {\mbox{\scriptsize{\boldmath $\ \ -\!\!\!>\ \ $}}}

687: \newcommand {\lolloL} {\mbox{\scriptsize{\boldmath $\ \ <\!\!\!-\ \ $}}}

688: \newcommand {\lnegL} [1] {\mbox {\tt neg {#1}}}

689: \newcommand {\lnegl} [1] {${\tt #1}^\anti$}

690: \newcommand {\antiL}  {\mbox {\tt bot}}

691: 

692: 

693: %%%%% Tp & Tp iterates %%%%%

694: 

695: \newcommand {\tpo} {T_P^\one}

696: \newcommand {\fpo} {F_\one(P)}

697: 

698: \newcommand {\itp} [1] {T_P\!\!\uparrow_{#1}}

699: \newcommand {\itpo} [1] {T_P^\one\!\!\uparrow_{#1}}

700: \newcommand {\isp} [1] {S_P\!\!\uparrow_{#1}}

701: \newcommand {\ispo} [1] {S_P^\one\!\!\uparrow_{#1}}

702: \newcommand {\itt} [1] {T\!\!\uparrow_{#1}}

703: \newcommand {\Un} [2] {\myunion_{{#1}=1}^{#2}}

704: 

705: \renewcommand {\eps} {\epsilon}

706: 

707: \newcommand {\opo} {O_\one(P)}

708: 

709: \newcommand {\deno} [1] {[\![{#1}]\!]_\one}

710: 

711: \newcommand {\preq} {\preccurlyeq}

712: 

713: \newcommand {\STPo} {S_P^\one}

714: 

715: \newcommand {\asato} {\asat_\one}

716: 

717: \newcommand {\msc}[1] {\widehat{#1}}

718: %\newcommand {\msc}[1] {{\cal M}(#1)}

719: 

720: 

721: %%%%% LO %%%%%

722: 

723: \newcommand {\LOone} {LO${}_\one$\,}

724: \newcommand {\LOonet} {LO{\Large ${}_\one$}\,}

725: \newcommand {\LOonews} {LO${}_\one$}

726: 

727: 

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

729: 

730: 

731: %\newcommand{\ms}[1]{{\cal M}(#1)}

732: %\newcommand{\ms}[1]{\ulcorner\!#1\!\urcorner)}

733: %\newcommand{\ms}[1]{\lceil\!#1\!\rceil)}

734: %\newcommand{\ms}[1]{#1^\bullet}

735: \newcommand{\ms}[1]{\widehat{#1}}

736: 

737: %\newcommand{\formula}[1]{\mathbb{#1}}

738: \newcommand{\formula}[1]{{\bf #1}}

739: 

740: 

741: \renewcommand{\vec}[1]{ {\mathbf{#1}} }

742: \newcommand{\ent}{\sqsubseteq}

743: \newcommand{\sat}{\models}

744: \newcommand{\osat}{\sat}

745: 

746: \newcommand {\val} [3] {#1 \sat #2 [#3]}

747: \newcommand {\valo} [3] {#1 \osat #2 [#3]}

748: \newcommand {\symbvalo} [3] {#1 \asat #2 [#3]}

749: 

750: \newcommand{\den}[1]{[\![{#1}]\!]}

751: \newcommand{\tuple}[1]{\langle{#1}\rangle}

752: \newcommand{\sympre}{\mathbf{sym\_pre}}

753: \newcommand{\pre}{pre}

754: \newcommand{\symbef}{\mbox{Symb-Reach}}

755: \newcommand{\leftlolli}{\lollo}

756: \newcommand{\asat}{\Vdash}

757: \newcommand{\STP}{S_P}

758: \newcommand{\mlub}[2]{#1\bullet #2}

759: \newcommand{\Add}{\alpha}

760: \newcommand{\Rem}{\rho}

761: 

762: \newcommand{\linc} {LC_\Sigma}

763: 

764: \newcommand{\tpa} {T_P^{\#}}

765: \newcommand{\TPA} {\tpa}

766: \newcommand{\tpao} [1] {T_P^{\#}\!\!\uparrow_{#1}}

767: 

768: \newcommand{\trad} [1] {\lceil {#1} \rceil}

769: \newcommand{\tradt} [1] {\mid\!{#1}\!\mid}

770: 

771: \newcommand{\cimp} {\leftarrow}

772: 

773: \newcommand{\true} {\mbox {\tt tt}}

774: 

775: \newcommand{\dtp} {T^{dlp}_P}

776: \newcommand{\lotp} {T^{lo}_P}

777: \newcommand{\tpatr} {T^{\#}_{\lceil P\rceil}}

778: \newcommand{\lotpo} [1] {\lotp\!\!\uparrow_{#1}}

779: \newcommand{\lotptr} [1] {T^{lo}_{\lceil P\rceil}}

780: 

781: \newcommand{\dhbp} {DHB_P}

782: \newcommand{\hblo} {HB_P}

783: \newcommand{\dosp} {O^{dlp}_P}

784: \newcommand{\dfs} {F^{dlp}_P}

785: \newcommand{\lofs} {F^{lo}_P}

786: 

787: \newcommand{\lfp} {\mathit {lfp}}

788: \newcommand{\gnd} {\mathit {gnd}}

789: 

790: %%%%%%% fine macro %%%%%%%

791: 

792: 

793: \title[Fixpoint Semantics for  Linear Logic Programs]

794:   {An Effective Fixpoint Semantics for  Linear Logic Programs}

795: \author[M. Bozzano, G. Delzanno and M. Martelli]

796: {MARCO BOZZANO, GIORGIO DELZANNO and MAURIZIO MARTELLI\\

797: Dipartimento di Informatica e Scienze dell'Informazione\\

798: Universit\`a di Genova\\

799: Via Dodecaneso 35, 16146 Genova - Italy \\

800: \email{\{bozzano,giorgio,martelli\}@disi.unige.it}

801: }

802: \pagerange{\pageref{firstpage}--\pageref{lastpage}}

803: \volume{}

804: \jdate{}

805: \setcounter{page}{1}

806: \pubyear{}

807: 

808: \begin{document}

809: \maketitle

810: \label{firstpage}

811: \begin{abstract}

812: In this paper we investigate the theoretical foundation of a new 

813: bottom-up semantics for linear logic programs, and more precisely 

814: for the fragment of LinLog \cite{And92} that

815: consists of the language LO \cite{AP91a}

816: enriched with the constant $\one$.

817: We use {\em constraints} to symbolically and finitely 

818: represent possibly infinite collections  of provable goals.

819: We define a fixpoint semantics based on a new operator in the style

820: of $T_P$ working over constraints.

821: An application of the fixpoint operator can be computed algorithmically.

822: As sufficient conditions for termination, we show that

823: the fixpoint computation is guaranteed to converge for propositional LO.

824: To our knowledge, this is the first attempt to define an effective

825: fixpoint semantics for linear logic programs. 

826: As an application of our framework, we also present a formal investigation

827: of the relations between LO and Disjunctive Logic Programming \cite{MRL91}. 

828: Using an approach based on abstract interpretation, we show that

829: DLP fixpoint semantics can be viewed as an abstraction of our semantics for LO.

830: We prove that the resulting abstraction is {\em correct} and {\em complete}

831: \cite{CC77,GR97b} for an interesting class of LO programs encoding Petri Nets.

832: \end{abstract}

833: \section{Introduction}

834: In recent years a number of fragments of linear logic \cite{Gir87} have been 

835: proposed as a logical foundation for extensions of

836: logic programming\cite{Mil95}.

837: Several new programming languages like {LO} \cite{AP91a}, LinLog \cite{And92},

838: ACL \cite{KY95}, Lolli \cite{HM94}, and Lygon \cite{HP94} have been proposed 

839: with the aim of enriching traditional logic programming languages like Prolog 

840: with a well-founded notion of state and with aspects of concurrency.

841: The operational semantics of this class of languages is given via 

842: a sequent-calculi presentation of the corresponding fragment of linear logic.

843: Special classes of proofs like the {\em focusing} proofs of \cite{And92} 

844: and the {\em uniform} proofs of \cite{Mil96} allow us to restrict 

845: our attention to {\em cut-free}, {\em goal-driven} proof systems that are 

846: complete with respect to provability in linear logic.

847: These presentations of linear logic are the natural counterpart of the traditional 

848: {\em top-down} operational semantics of logic programs.

849: 

850: In this paper we investigate an alternative operational semantics 

851: for the fragment of linear logic underlying the language LO \cite{AP91a}, and

852: its proper extension with the constant $\one$. Both languages can be seen as

853: fragments of LinLog \cite{And92}, which is a presentation of full linear

854: logic. Throughout the paper, we will simply refer to these two fragments as

855: LO and \LOonews.

856: The reason we selected these fragments is that 

857: we were looking for a relatively simple linear logic language 

858: with a uniform-proof presentation, state-based computations and 

859: aspects of concurrency.  

860: Considering both LO and its extension with the constant $\one$ will help us 

861: to formally classify the different expressive power of linear logic connectives

862: like $\para$, $\with$, $\top$, and $\one$ when incorporated into a logic programming setting.

863: In practice, {LO} has been successfully applied to model 

864: concurrent object-oriented languages \cite{AP91a},

865: and multi-agent coordination languages based on the Linda model \cite{And96}.

866: 

867: The operational semantics we propose consists of a {\em goal-independent}

868: {\em bottom-up} evaluation of programs.

869: Specifically, given an {LO} program $P$ our aim is to compute a finite 

870: representation of the set of goals that are provable from $P$.

871: There are several reasons to look at this problem.

872: First of all, as discussed in \cite{HW98}, 

873: the bottom-up evaluation of programs is the key ingredient

874: for all applications where it is difficult or impossible to specify a given 

875: goal in advance. Examples are active (constraint) databases, agent-based 

876: systems and genetic algorithms. 

877: Recent results connecting verification techniques and 

878: semantics of logic programs \cite{DP99} show that bottom-up evaluation can be used 

879: to automatically check  {\em properties} (specified in temporal logic like CTL) 

880: of the original program. 

881: In this paper will go further showing that the {\em provability} relation in 

882: logic programming languages like LO can be used to naturally 

883: express verification problems for Petri Nets-like models of concurrent systems.

884: Finally,  a formal definition of the bottom-up semantics 

885: can be useful for studying equivalence, compositionality and 

886: abstract interpretation, as for traditional logic programs 

887: \cite{BGLM94,GDL95}.

888: 

889: Technically, our contributions are as follows.

890: We first consider a formulation of {LO} with $\para$, $\lolli$, $\with$ and $\all$.

891: Following the semantic framework of (constraint) logic programming 

892: \cite{GDL95,JM94}, we formulate the bottom-up evaluation procedure in two

893: steps. 

894: We first define what one could call a {\em ground} semantics 

895: via a {\em fixpoint} operator $T_P$ defined over an extended notion 

896: of Herbrand interpretation consisting of {\em multisets} of atomic formulas. 

897: This way, we capture the {\em uniformity} of {LO}-provability, according to which 

898: compound goals must be completely decomposed into atomic goals before 

899: program clauses can be applied. 

900: Due to the structure of the LO proof system, 

901: already in the propositional case there 

902: are infinitely many provable  multisets of atomic formulas. 

903: In fact, {LO}-provability enjoys the following property.

904: If a multiset of goals $\Delta$ is provable in $P$, then 

905: any $\Delta'$ such that $\Delta$ is a sub-multiset of

906: $\Delta'$ is provable in $P$.   

907: To circumvent this problem, we order the interpretations according 

908: to the multiset inclusion relation of their elements and we define a

909: new operator $\STP$ that computes only the {\em minimal} (w.r.t. 

910: multiset inclusion) provable multisets. 

911: Dickson's Lemma \cite{Dic13} ensures the termination of the 

912: fixpoint computation based on $\STP$ for propositional {LO} programs.

913: Interestingly, this result is an instance of the general decidability 

914: results for model checking of infinite-state systems given in \cite{ACJT96,FS01}.

915: 

916: The decidability of propositional  provability shows that LO

917: is not as interesting as one could expect from a state-oriented extension 

918: of the logic programming paradigm.

919: Specifically, LO does not provide a natural way to {\em count} resources.

920: This feature can be introduced by 

921: a slight extension of LO in which we add unit clauses defined

922: via the constant $\one$.

923: The resulting language, namely \LOone, can be viewed as a first step

924: towards more complex languages based on linear logic like LinLog

925: \cite{And92}.

926: As we show in this paper, \LOone allows to model more sophisticated models of 

927: concurrent systems than LO, e.g., in \LOone it is possible to model Petri Nets with 

928: {\em transfer arcs}.   

929: Adding the constant $\one$  breaks down the decidability of provability in propositional {LO}.

930: Despite this negative result, it is still possible to define 

931: an effective $\STPo$ operator for \LOone.

932: For this purpose, 

933: as {\em symbolic} representation of potentially infinite sets of contexts, 

934: we choose a special class of {\em linear constraints} defined over 

935: variables that {\em count} resources.

936: This abstract domain generalizes the domain used for LO:

937: the latter can be represented as the subclass of constraints with 

938: no equalities.

939: Though for the new operator we cannot guarantee that the fixpoint can be

940: reached after finitely many steps, this connection allows us to apply

941: techniques developed in model checking for infinite-state systems 

942: (see e.g. \cite{BGP97,DP99,HHW97})

943: and abstract interpretation \cite{CH78} 

944: to compute approximations of the fixpoint of $\STPo$.

945: 

946: In this paper we limit ourselves to the study of the propositional

947: case that, as shown in \cite{APC97}, can be viewed as the target of 

948: a possible abstract interpretation of a first-order program.

949: To our knowledge, this is the first attempt of defining an effective

950: fixpoint semantics for linear logic programs.

951: 

952: Our semantic framework can also be used as a tool to compare the relative

953: strength of different logic programming extensions. 

954: As an application, we shall present a detailed comparison between LO and Disjunctive Logic

955: Programming (DLP).

956: Though DLP has been introduced in order to represent `uncertain' beliefs,

957: a closer look at its formal definition reveals very interesting

958: connections with the paradigm of linear logic programming:

959: both DLP and LO programs extend Horn programs allowing clauses with

960: {\em multiple} heads. 

961: In fact, in DLP we find  clauses of the form 

962: $$

963: p(X)\vee q(X) \leftarrow r(X)\wedge t(X),

964: $$

965: whereas in LO we find clauses of the form 

966: $$

967: p(X)\para q(X) \leftlolli r(X)\with t(X).

968: $$

969: To understand the differences, we must look at the operational 

970: semantics of DLP programs.

971: In DLP, a resolution step is extended so as to work over positive 

972: clauses ({\em sets}/{\em disjunctions} of facts). 

973: Implicit {\em contraction} steps are applied  over the selected clause.

974: On the contrary,

975: being in a sub-structural logic in which contraction is forbidden,

976: we know that LO resolution behaves as {\em multiset} rewriting.

977: Following the bottom-up approach that we pursue in this paper, we will exploit

978: the classical framework of abstract interpretation to formally compare the

979: two languages. Technically, we first specialize our fixpoint semantics to a

980: {\em flat} fragment of propositional

981: LO (i.e., arbitrary nesting of connectives in goals is forbidden) which

982: directly corresponds to DLP as defined in \cite{MRL91}. Then,

983: by using an abstract-interpretation-based approach,

984: we exhibit  a Galois connection between the semantic domains of DLP and LO,

985: and we show that the semantics of DLP programs can be described

986: as an abstraction of the semantics of LO programs.

987: Using the theory of abstract interpretation and 

988: the concept of {\em complete abstraction} \cite{CC77,GR97b} we

989: discuss the quality of the resulting abstraction.

990: This view of DLP as an abstraction of LO is appealing for several reasons.

991: First of all, it opens the possibility of using techniques developed for DLP 

992: for the analysis of LO programs.  

993: Furthermore, it shows that the paradigm of DLP could have unexpected

994: applications

995: as a framework  to reason about properties of Petri Nets, a well-know

996: formalism for concurrent computations \cite{KM69}.

997: In fact, as we will prove formally in the paper, DLP represents a

998: {\em complete} abstract domain for LO programs that encode Petri Nets. 

999: %

1000: \paragraph*{Plan of the paper.}

1001: After introducing some notations in Section \ref{prelim},

1002: in Section \ref{lo} we recall the main features of {LO} \cite{AP91a}.

1003: In Section \ref{ground} we introduce the so-called {\em ground} semantics,

1004: via the $T_P$ operator,

1005: and prove that the least fixpoint of $T_P$ characterizes the operational 

1006: semantics of an LO program.

1007: In Section \ref{nonground} we reformulate LO semantics by means of

1008: the {\em symbolic} $\STP$ operator, and we relate it to $T_P$.

1009: In Section \ref{groundo} we consider an extended fragment of LO

1010: with the constant $\one$,

1011: extending the notion of satisfiability given in Section \ref{ground} and

1012: introducing an operator $\tpo$.

1013: In Section \ref{nongroundo} we introduce a symbolic operator $\STPo$

1014: for the extended fragment, and we discuss its algorithmic implementation

1015: in Section \ref{nongroundo_computing}. As an application of our framework, in

1016: Section \ref{dlplo} and Section \ref{comparison} we investigate the relations 

1017: between LO and DLP, and in Section \ref{petri} we investigate the relations with Petri Nets.

1018: Finally, in Section \ref{related} and Section \ref{conclusions} we discuss

1019: related works and conclusions.

1020: 

1021: This paper is an extended version of the papers \cite{BDM00a,BDM00b}.

1022: \section{Preliminaries}

1023: \label{prelim}

1024: %

1025: In this paper we will extensively use operations on multisets.

1026: We will consider a fixed signature, i.e a finite set of propositional

1027: symbols, $\Sigma=\{a_1,\ldots,a_n\}$. Multisets over $\Sigma$

1028: will be hereafter called {\em facts}, and symbolically

1029: noted as $\calA,\calB,\calC,\ldots$.

1030: A multiset with (possibly duplicated) elements $b_1,\ldots,b_m\in\Sigma$

1031: will be simply indicated as $\{b_1,\ldots,b_m\}$, overloading the usual

1032: notation for sets.

1033: 

1034: A fact $\calA$ is uniquely determined by a finite map 

1035: $Occ:\Sigma\rightarrow\Nat$ such that $Occ_{\cal A}(a_i)$ is the number of occurrences of 

1036: $a_i$ in $\calA$.

1037: Facts are ordered according to the {\em multiset inclusion} 

1038: relation $\preccurlyeq$ defined as follows: $\calA\preccurlyeq\calB$ 

1039: if and only if $Occ_{\cal A}(a_i)\leq Occ_{\cal B}(a_i)$ for $i:1,\ldots,n$.

1040: The {\em empty} multiset is denoted $\eps$ and is such that 

1041: $Occ_\eps(a_i)=0$ for $i:1,\ldots,n$, and $\eps\preccurlyeq\calA$ 

1042: for any $\calA$. 

1043: The {\em multiset union} $\calA,\calB$ (alternatively $\calA+\calB$ when `,' is ambiguous) 

1044: of two facts $\calA$ and $\calB$ is such that 

1045: $Occ_{{\cal A},{\cal B}}(a_i)=Occ_{\cal A}(a_i)+Occ_{\cal B}(a_i)$ for $i:1,\ldots,n$.

1046: The {\em multiset difference}  $\calA\setminus\calB$ is such that

1047: $Occ_{{\cal A}\setminus{\cal B}}(a_i)=max(0,Occ_{\cal A}(a_i)-Occ_{\cal B}(a_i))$ 

1048: for $i:1,\ldots,n$.

1049: We define a special operation $\mlub{}{}$ to compute the {\em least upper 

1050: bound} of two facts with respect to $\preccurlyeq$. Namely,

1051: $\mlub{\calA}{\calB}$ is such that

1052: $Occ_{\mlub{\cal A}{\cal B}}(a_i)=max(Occ_{\cal A}(a_i),Occ_{\cal B}(a_i))$ for 

1053: $i:1,\ldots,n$.

1054: Finally, we will use the notation $\calA^n$, where $n$ is a natural number, to

1055: indicate $\calA+\ldots+\calA$ ($n$ times).

1056: 

1057: In the rest of the paper we will use $\Delta,\Theta,\ldots$ to denote

1058: multisets of possibly compound formulas. Given two multisets 

1059: $\Delta$ and $\Theta$, $\Delta\preccurlyeq\Theta$ indicates multiset inclusion

1060: and 

1061: $\Delta,\Theta$ multiset union,

1062: as before, and $\Delta,\{G\}$ is written simply $\Delta,G$.

1063: In the following, a {\em context} will denote a multiset of goal-formulas

1064: (a {\em fact} is a context in which every formula is atomic).

1065: Given a linear disjunction of atomic formulas $H=a_1\para\ldots\para a_n$,  

1066: we introduce the notation $\ms{H}$ to denote the multiset $a_1,\ldots,a_n$.

1067: 

1068: Finally, let $T:\calI\rightarrow\calI$ be an operator defined over a complete lattice 

1069:  $\tuple{\calI,\sqsubseteq}$.  

1070: We define $\itt{0}=\eset$, where $\eset$ is the

1071: bottom element, $\itt{k+1}=T(\itt{k})$ for all $k\geq 0$, and

1072: $\itt{\omega}=\bigsqcup_{k=0}^{\infty}\itt{k}$, 

1073: where $\bigsqcup$ is the least upper bound w.r.t. $\sqsubseteq$.

1074: Furthermore, we use $\lfp(T)$ to denote the {\em least fixpoint} of $T$. 

1075: %

1076: \section{The Programming Language {LO}}

1077: \label{lo}

1078: %

1079: {LO} \cite{AP91a} is a logic programming language based on linear logic. 

1080: Its mathematical foundations lie on a proof-theoretical presentation of 

1081: a fragment of linear logic defined over the linear connectives 

1082: $\leftlolli$ ({\em linear implication}), $\with$ ({\em additive conjunction}),

1083: $\para$ ({\em multiplicative disjunction}), and the constant $\all$

1084: ({\em additive identity}). 

1085: In the propositional case {LO} consists of the following class of formulas:

1086: 

1087: $$

1088: \begin{array}{l}

1089: \formula{D}\ ::=\ \formula{A}_1\para\ \ldots\para\ \formula{A}_n\ \leftlolli\ \formula{G}\ \ |\ \ \formula{D}\ \with\ 

1090: \formula{D}\\

1091: [\medskipamount]

1092: \formula{G}\ ::=\ \formula{G}\ \para\ \formula{G}\ \ |\ \formula{G}\ \with\ \formula{G}\ \ |\ \ 

1093: \formula{A}\ \ |\ \ \all

1094: \end{array}

1095: $$

1096: Here $\formula{A}_1,\ldots,\formula{A}_n$ and $\formula{A}$ 

1097: range over propositional symbols from a fixed signature $\Sigma$. 

1098: $\formula{G}$-formulas correspond to {\em goals} to be evaluated in a given program. 

1099: $\formula{D}$-formulas correspond to multiple-headed {\em program clauses}. 

1100: An {LO} program is a $\formula{D}$-formula.  

1101: Let $P$ be the program $C_1\with\ldots\with C_n$.

1102: The execution of  a multiset of $\formula{G}$-formulas $G_1,\ldots,G_k$ 

1103: in $P$ corresponds to a goal-driven proof for the two-sided {LO}-sequent 

1104: $$P\Rightarrow G_1,\ldots,G_k.$$

1105: The {LO}-sequent $P\Rightarrow G_1,\ldots,G_k$ is an abbreviation for 

1106: the following two-sided linear logic sequent: 

1107: $$!C_1,\ldots,!C_n\ \rightarrow\   G_1,\ldots,G_k.$$

1108: The formula $!F$ on the left-hand side of a sequent indicates that $F$ can 

1109: be used in a proof an arbitrary number of times.

1110: This implies that an {LO}-Program can be viewed also as a 

1111: {\em set of reusable clauses}.

1112: According to this view,  the operational semantics of {LO} is given via 

1113: the {\em uniform} (goal-driven)  proof system defined in Figure \ref{system_for_LO}. 

1114: In Figure \ref{system_for_LO}, $P$ is a set of implicational clauses,

1115: ${\cal A}$ denotes a multiset of atomic formulas,

1116: whereas $\Delta$ denotes a multiset of $\formula{G}$-formulas.

1117: A sequent is provable if all branches of its proof tree

1118: terminate with instances of the $\all_r$ axiom.

1119: The proof system of Figure \ref{system_for_LO} is a specialization of more general 

1120: uniform proof systems for linear logic like Andreoli's focusing proofs \cite{And92}, 

1121: and Forum \cite{Mil96}. 

1122: %

1123: \begin{figure*}

1124: $$

1125: \begin{array}{c}

1126: \infer[\all_r]

1127: {P\Rightarrow \all,\Delta}

1128: {}

1129: \ \ \ \ 

1130: \infer[\para_r]

1131: {P\Rightarrow G_1\para G_2,\Delta}

1132: {P\Rightarrow G_1,G_2,\Delta}

1133: \ \ \ \ 

1134: \infer[\with_r]

1135: {P\Rightarrow G_1\with G_2,\Delta}

1136: {P\Rightarrow G_1,\Delta &

1137:  P\Rightarrow G_2,\Delta}

1138: \\

1139: \\

1140: \infer[bc\ \ (H\leftlolli G\ \in\ P)]

1141: {P\Rightarrow \ms{H}+{\cal A}}

1142: {P\Rightarrow G,{\cal A} & }

1143: \end{array}

1144: $$

1145: \caption{A proof system for {LO}}

1146: \label{system_for_LO}

1147: \end{figure*}

1148: The rule {\em bc} denotes a backchaining (resolution) step 

1149: ($\ms{H}$ is the multiset consisting of the literals in 

1150: the disjunction $H$, see Section \ref{prelim}).

1151: Note that {\em bc} can be executed only if the right-hand side of 

1152: the current {LO} sequent consists of atomic formulas.

1153: Thus, {LO} clauses behave like {\em multiset} rewriting rules. 

1154: {LO} clauses having the following form

1155: $$a_1\para\ \ldots\para\  a_n\leftlolli \all$$

1156: play the same role as the unit clauses of Horn programs.

1157: In fact, a backchaining step over such a clause 

1158: leads to {\em success} independently of the current context $\calA$,

1159: as shown in the following scheme:

1160: $$ 

1161: \begin{array}{c}

1162: \infer[bc]

1163: {P\Rightarrow a_1,\ldots,a_n,\calA}

1164: {\infer[\all_r]

1165:   {P\Rightarrow \all,\calA}{} 

1166: } 

1167: \medskip\\

1168: provided\ \ \ a_1\para\ \ldots\para \ a_n\leftlolli\all\in P

1169: \end{array}

1170: $$

1171: This observation leads us to the following property (we recall that 

1172: $\preccurlyeq$ is the sub-multiset relation).

1173: \begin{proposition}

1174: \label{monotonicity}

1175: Given an {LO} program $P$ and two contexts $\Delta,\Delta'$ 

1176: such that $\Delta\preccurlyeq\Delta'$, if 

1177: $P\Rightarrow \Delta$ then $P\Rightarrow \Delta'$.

1178: \end{proposition}

1179: \begin{proof}

1180: By simple induction on the structure of LO proofs.

1181: \end{proof}

1182: This property is the key point in our analysis of the operational 

1183: behavior of {LO}. It states that the $weakening$ rule is $admissible$ in LO.

1184: Thus, LO can be viewed as an {\em affine} fragment of linear logic.

1185: Note that weakening and contraction are both admissible on the left hand side 

1186: (i.e. on the program part) of LO sequents.

1187: %

1188: \begin{example}

1189: \label{LOex}

1190: Let $P$ be the {LO} program consisting of the clauses

1191: %

1192: $$\begin{array}{l}

1193:   1.\ \ a\lollo b\para c\\

1194:   2.\ \ b\lollo(d\para e)\with f\\

1195:   3.\ \ c\para d\lollo\all\\

1196:   4.\ \ e\para e\lollo b\para c\\

1197:   5.\ \ c\para f\lollo\all\\

1198: \end{array}$$

1199: %

1200: and consider an initial goal $e,e$. 

1201: A proof for this goal is shown in Figure \ref{LOproof},

1202: where we have denoted by $bc^{(i)}$ the application of the backchaining rule

1203: over clause number $i$ of $P$. The proof proceeds as follows.

1204: Using clause 4., to prove $e,e$ we have to prove

1205: $b\para c$, which, by {LO} $\para_r$ rule, reduces to prove $b,c$.

1206: At this point we can backchain over clause 2., and we get the new goal

1207: $(d\para e)\with f,c$. By applying $\with_r$ rule, we get

1208: two separate goals $d\para e,c$ and $f,c$. The first, after a reduction

1209: via $\para_r$ rule, is provable by means of clause (axiom) 3., while the latter

1210: is provable directly by clause (axiom) 5.

1211: Note that $\all$ succeeds in a non-empty context (i.e. containing $e$) in

1212: the left branch.

1213: A similar proof shows that the goal $a$ is also provable from $P$.

1214: %

1215: \begin{figure*}

1216: \centering

1217: $$

1218:    \infer[bc^{(4)}]{P\Rightarrow e,e}

1219:   {\infer[\para_r]{P\Rightarrow b\para c}

1220:   {\infer[bc^{(2)}]{P\Rightarrow b,c}

1221:   {\infer[\with_r]{P\Rightarrow (d\para e)\with f,c}

1222:   {\infer[\para_r]{P\Rightarrow d\para e,c}

1223:   {\infer[bc^{(3)}]{P\Rightarrow d,e,c}

1224:   {\infer[\all_r]{P\Rightarrow e,\all}{}}}

1225:     &

1226:    \infer[bc^{(5)}]{P\Rightarrow f,c}

1227:   {\infer[\all_r]{P\Rightarrow \all}{}}}

1228:   }}}

1229: $$

1230: \caption{An LO proof for the goal $e,e$ in the program of Example \ref{LOex}}

1231: \label{LOproof}

1232: \end{figure*}

1233: %

1234: By Proposition \ref{monotonicity}, provability of $e,e$ and $a$

1235: implies provability of any multiset of goals $e,e,\Delta$ and $a,\Delta$, for

1236: every context $\Delta$.

1237: \end{example}

1238: %

1239: 

1240: We conclude this Section with the definition

1241: of the following induction measure on LO goals, which we will later

1242: need in proofs.

1243: %

1244: \begin{definition}

1245: \label{inddef}

1246: Given a goal $G$, the induction measure $m(G)$ is defined according to the

1247: following rules: $m(A) = 0$ for every atomic formula $A$;

1248: $m(\all) = 0$; $m(G_1\with G_2) = m(G_1\para G_2) = m(G_1) + m(G_2)$ + 1.

1249: The induction measure extends to contexts by defining

1250: $m(G_1,\ldots,G_n)=m(G_1)+\ldots+m(G_n)$.

1251: \end{definition}

1252: %

1253: \section{A Bottom-up Semantics for {LO}}

1254: \label{ground}

1255: %

1256: The proof-theoretical semantics of {LO} corresponds to the {\em top-down} 

1257: operational semantics based on resolution for traditional logic 

1258: programming languages like Prolog. 

1259: Formally, we define the operational {\em top-down} semantics of an {LO}

1260: program $P$ as follows:

1261: $$ 

1262: O(P)=\{\calA\ |\ \calA\ is\ a\ fact\ and\ \dedLO{P}{\calA}\ is\ provable\}

1263: $$

1264: Note that the information on provable {\em facts} from a given program $P$

1265: is all we need to decide

1266: whether a general goal (with possible nesting of connectives) is provable from

1267: $P$ or not. This is a consequence

1268: of the {\em focusing} property \cite{And92} of LO

1269: provability, which ensures that provability of a compound goal can always be

1270: reduced to provability of a finite set of atomic multisets.

1271: In a similar way, in Prolog 

1272: the standard bottom-up semantics is defined as a set of {\em atoms}, while

1273: in general {\em conjunctions} of atoms are allowed in clause bodies.

1274: 

1275: In this paper we are interested in finding a suitable definition of

1276: {\em bottom-up} 

1277: semantics that can be used as an alternative operational semantics for {LO}.

1278: More precisely, given an {LO} program $P$ we would like to define a procedure

1279: to compute

1280: all goal formulas $G$ such that $G$ is provable from $P$.

1281: This procedure should enjoy the usual properties of classical bottom-up

1282: semantics, in particular its definition should be based on an {\em effective}

1283: fixpoint operator (i.e. at least every single step must

1284: be finitely computable),

1285: and it should be {\em goal-independent}. As usual, goal independence is

1286: achieved by searching for proofs starting from the axioms (the unit clauses of

1287: Section \ref{lo}) and accumulating goals which can be proved by applying

1288: program clauses to the current interpretation.

1289: As for the operational semantics, we can limit ourselves to goal formulas 

1290: consisting of multisets of atomic formulas, without any loss of generality.  

1291: %

1292: In the rest of the paper we will always consider propositional {LO} programs

1293: defined over a {\em finite} set of propositional symbols $\Sigma$.

1294: We give the following definitions.

1295: \begin{definition}[Herbrand base $B_P$]

1296: Given a pro\-positional {LO} program $P$ defined over $\Sigma$,

1297: the Herbrand base of $P$, denoted $B_P$, is given by

1298:   $$ B_P = \{\calA \ |\  \calA\ \hbox{is a multiset (fact) over $\Sigma$}\}.$$

1299: \end{definition}

1300: \begin{definition}[Herbrand interpretation]

1301: We say that $I\subseteq B_P$ is a Herbrand interpretation.

1302: Herbrand interpretations form a complete

1303: lattice $\tuple{\calD,\subseteq}$ with respect to set inclusion,

1304: where $\calD=\calP(B_P)$.

1305: \end{definition}

1306: %

1307: Before introducing the formal definition of the {\em ground} bot\-tom-up semantics, 

1308: we need to define a notion of satisfiability of a context  $\Delta$ in a 

1309: given interpretation $I$.

1310: For this purpose, we introduce the judgment $\val{I}{\Delta}{\calA}$.

1311: The need for this judgment, with respect to the familiar logic programming setting

1312: \cite{GDL95}, is motivated by the arbitrary nesting of connectives in LO

1313: clause bodies,

1314: which is not allowed in traditional presentations of (constraint)

1315: logic programs.

1316: In $\val{I}{\Delta}{\calA}$, $\calA$ should be read as an {\em output} fact

1317: such that 

1318: $\calA+\Delta$ is valid in $I$.

1319: This notion of {\em satisfiability} is modeled according to the right-introduction 

1320: rules of the connectives. The notion of output fact $\calA$ will simplify the 

1321: presentation of the algorithmic version of the judgment which we will present in Section \ref{nonground}.

1322: \begin{definition}[Satisfiability]

1323: Let $I$ be a Herbrand interpretation, then $\sat$ is defined as follows:

1324: $$\begin{array}{l} 

1325:   \val{I}{\all,\Delta}{\calA'}\ \mbox{for\ any\ fact}\ \calA';\\

1326:   [\medskipamount]

1327:   \val{I}\calA{\calA'}\ \mbox{if}\ \calA+\calA' \in I;\\

1328:   [\medskipamount]

1329:    \val{I}{G_1\para G_2,\Delta}{\calA}\ \mbox{if}\ \val{I}{G_1,G_2,\Delta}{\calA};\\

1330:   [\medskipamount]

1331:   \val{I}{G_1\with G_2,\Delta}{\calA}\ \mbox{if}\ \val{I}{G_1,\Delta}{\calA}\ 

1332:   \mbox{and}

1333:     \ \val{I}{G_2,\Delta}{\calA}.

1334: \end{array}$$

1335: \end{definition}

1336: The relation $\models$ satisfies the following properties.

1337: \begin{lemma}

1338: \label{movlemma}\label{satlemma}\label{finitary_lemma}

1339: For any interpretations $I,J$,

1340: context $\Delta$, and fact $\calA$,

1341: \begin{enumerate}

1342: \item[i)] $\val{I}{\Delta}{\calA}\ if\ and\ only\ if\ \val{I}{\Delta,\calA}{\eps}$;

1343: \item[ii)] if $I\subseteq J$ and $\val{I}{\Delta}{\calA}$ then $\val{J}{\Delta}{\calA}$;

1344: \item[iii)]

1345: given a chain of interpretations $I_1\subseteq I_2\subseteq\ldots$, 

1346: if  $\val{\Un{i}{\infty}I_i}{\Delta}{\calA}$ 

1347: then there exists $k$ s.t. $\val{I_k}{\Delta}{\calA}$.

1348: \end{enumerate}

1349: \end{lemma}

1350: \begin{proof}

1351: The proof of $i)$ and $ii)$ is by simple induction.

1352: The proof of $iii)$ is by (complete) induction on $m(\Delta)$ (see Definition

1353: \ref{inddef}).

1354: \begin{itemize}

1355:   \item[-] If $\Delta=\all,\Delta'$, then, no matter which $k$ you choose,

1356:     $\val{I_k}{\all,\Delta'}{\calA}$;

1357:   \item[-] if $\Delta$ is a fact, then 

1358:     $\val{\Un{i}{\infty}I_i}{\Delta}{\calA}$ means

1359:     $\Delta,\calA\in\Un{i}{\infty}I_i$, which in turn implies that there

1360:     exists $k$ such that

1361:     $\Delta,\calA\in I_k$, therefore $\val{I_k}{\Delta}{\calA}$;

1362:   \item[-] if $\Delta=G_1\with G_2,\Delta'$, then by inductive hypothesis

1363:     there exist $k_1$ and $k_2$ s.t. $\val{I_{k_1}}{G_1,\Delta'}{\calA}$ and

1364:     $\val{I_{k_2}}{G_2,\Delta'}{\calA}$. Therefore, if $k=max\{k_1,k_2\}$, by

1365:     $ii)$ we

1366:     have that $\val{I_k}{G_1,\Delta'}{\calA}$

1367:     and $\val{I_k}{G_2,\Delta'}{\calA}$, therefore

1368:     $\val{I_k}{G_1\with G_2,\Delta'}{\calA}$, i.e.

1369:     $\val{I_k}{\Delta}{\calA}$ as required;

1370:   \item[-] the $\para$-case follows by a straightforward

1371:     application of the inductive hypothesis.

1372: \end{itemize}

1373: \end{proof}

1374: %

1375: We now come to the definition of the fixpoint operator $T_P$.

1376: \begin{definition}[Fixpoint operator $T_P$]

1377: Given a program $P$ and an interpretation $I$,

1378: the operator $T_P$ is defined as follows:

1379:   $$ T_P(I)=\{\ms{H}+\calA\ |\ H\lollo G\in P,\ \val{I}{G}{\calA}\}. $$

1380: \end{definition}

1381: The following property holds.

1382: \begin{proposition}\label{montheor}

1383: For every program $P$, $T_p$ is monotonic and continuous over the lattice

1384: $\tuple{\calD,\subseteq}$.

1385: \end{proposition}

1386: \begin{proof}

1387: {\em Monotonicity}. Immediate from $T_P$ definition and 

1388: Lemma \ref{satlemma} $ii)$.\\

1389: {\em Continuity}. We prove that $T_P$ is finitary. 

1390: Namely, given an increasing chain of interpretations $I_1\subseteq I_2\subseteq\ldots$,

1391: $T_P$ is finitary if 

1392: $T_P(\Un{i}{\infty}I_i)\subseteq \Un{i}{\infty}{T_P(I_i)}$.

1393: We simply need to show that if

1394: $\val{T_P(\Un{i}{\infty}I_i)}{\Delta}{\eps}$ then\ there\ exists\ $k$ \ such\ that\ 

1395:          $\val{T_P(I_k)}{\Delta}{\eps})$. 

1396: 	 The proof is by induction on $m(\Delta)$.

1397:     \begin{itemize}

1398:       \item[-] If $\Delta=\all,\Delta'$, then, no matter which $k$ you choose,

1399:         $\val{T_P(I_k)}{\all,\Delta'}{\eps}$;

1400:       \item[-] if $\Delta$ is a fact and $\Delta\in

1401:         T_P(\Un{i}{\infty}I_i)$,

1402:         then, by definition of $T_P$, there exist a fact $\calA$

1403:         and a clause $A_1\para\ldots\para A_n\lollo G\in P$, such that

1404:         $\val{\Un{i}{\infty}I_i}{G}{\calA}$

1405:         and $\Delta=A_1,\ldots,A_n,\calA$.

1406:         Lemma \ref{finitary_lemma} $iii)$ implies that $\exists k. \val{I_k}{G}{\calA}$,

1407:         therefore, again by definition of $T_P$,

1408:         $\val{T_P(I_k)}{A_1,\ldots,A_n,\calA}{\eps}$, i.e.

1409:         $\val{T_P(I_k)}{\Delta}{\eps}$ as required;

1410:       \item[-] if $\Delta=G_1\with G_2,\Delta'$, then by inductive hypothesis,

1411:         there exist $k_1$ and $k_2$ s.t.

1412:         $\val{T_P(I_{k_1})}{G_1,\Delta'}{\eps}$

1413:         and $\val{T_P(I_{k_2})}{G_2,\Delta'}{\eps}$.

1414:         Then, if $k=max\{k_1,k_2\}$,

1415:         by Lemma \ref{satlemma} $ii)$  we have that

1416:         $\val{T_P(I_k)}{G_1,\Delta'}{\eps}$ and

1417:         $\val{T_P(I_k)}{G_2,\Delta'}{\eps}$. This implies

1418:         $\val{T_P(I_k)}{G_1\with G_2,\Delta'}{\eps}$, i.e.

1419:         $\val{T_P(I_k)}{\Delta}{\eps}$ as required;

1420:       \item[-] the $\para$-case follows by a straightforward application of the

1421:         inductive hypothesis.

1422:     \end{itemize}

1423: \end{proof}

1424: %

1425: Monotonicity and continuity of the $T_P$ operator imply, by Tarski's Theorem,

1426: that $\lfp(T_P)=\itp{\omega}$.

1427: 

1428: Following \cite{Llo87}, we define the {\em fixpoint semantics} 

1429: $F(P)$ of an {LO} program $P$  as the least fixpoint of $T_P$, 

1430: namely $F(P)=\lfp(T_P)$. 

1431: Intuitively, $T_P(I)$ is the set of {\em immediate logical consequences} 

1432: of the program $P$ and of the facts in $I$. 

1433: In fact, if we define $P_I$ as the program $\{A\leftlolli\all\ |\ \ms{A}\in I\}$,

1434: the definition of $T_P$ can be viewed as the following instance 

1435: of the {\em cut} rule of linear logic:

1436: $$

1437: \infer[cut]

1438: {!P,!P_I \rightarrow H,\calA}

1439: {

1440: !P,G\rightarrow H & 

1441: !P_I\rightarrow G,\calA

1442: }

1443: $$

1444: Using the notation used for {LO}-sequents we obtain the following rule:

1445: $$

1446: \infer[cut]

1447: {P \cup P_I \Rightarrow H,\calA}

1448: {

1449: P\Rightarrow H\leftlolli G & 

1450: P_I\Rightarrow G,\calA

1451: }

1452: $$

1453: Note that, since  $H\leftlolli G\in P$, the sequent 

1454: $P\Rightarrow H\leftlolli G$ is always provable in linear logic.

1455: According to this view, $F(P)$ characterizes the set of 

1456: {\em logical consequences} of a program $P$.

1457: 

1458: The fixpoint semantics is sound and complete with respect

1459: to the operational semantics as stated in the following theorem.

1460: \begin{theorem}[Soundness and Completeness]

1461: \label{fixpoint_operational}

1462: For every {LO} program $P$, $F(P)=O(P)$.

1463: \end{theorem}

1464: \begin{proof}

1465: \begin{description}

1466:   \item[$i)\ F(P)\subseteq O(P)$.] We prove that for every $k$ and

1467:     context $\Delta$,

1468:     if $\val{\itp{k}}{\Delta}{\eps}$ then $\dedLO{P}{\Delta}$.

1469:     The proof is by (complete) induction on $\bar{m}(\itp{k},\Delta)$, where

1470:     $\bar{m}$ is an induction measure defined by

1471:     $\bar{m}(\itp{k},\Delta)=\langle k,m(\Delta)\rangle$, and

1472:     $\langle k,m\rangle < \langle k',m'\rangle$ if and only if

1473:     ($k<k'$) or ($k=k'$ and $m<m'$) (lexicographic ordering).

1474:     \begin{itemize}

1475:       \item[-] If $\Delta=\all,\Delta'$, the conclusion is immediate;

1476:       \item[-] if $\Delta$ is a fact, then $\Delta\in \itp{k}$, so

1477:         that $\itp{k}\neq\eset$ and $k>0$. By definition of $T_P$ we have

1478:         that there exist a fact $\calA$ and a clause

1479:         $A_1\para\ldots\para A_n\lollo G\in P$, such that

1480:         $\val{\itp{k-1}}{G}{\calA}$ and $\Delta=A_1,\ldots,A_n,\calA$.

1481:         By Lemma \ref{movlemma} $i)$ we have that

1482:         $\val{\itp{k-1}}{G,\calA}{\eps}$, and then, by inductive

1483:         hypothesis, $\dedLO{P}{G,\calA}$, therefore by LO $bc$ rule,

1484:         $\dedLO{P}{A_1,\ldots,A_n,\calA}$, i.e., $\dedLO{P}{\Delta}$;

1485:       \item[-] if $\Delta=G_1\with G_2,\Delta'$ then by inductive hypothesis

1486:         $\dedLO{P}{G_1,\Delta'}$ and $\dedLO{P}{G_2,\Delta'}$, therefore

1487:         $\dedLO{P}{G_1\with G_2,\Delta'}$ by LO $\with_r$ rule;

1488:       \item[-] the $\para$-case follows by a straightforward

1489:         application of the inductive hypothesis.

1490:     \end{itemize}

1491:   \item[$ii)\ O(P)\subseteq F(P)$.] We prove that for every context $\Delta$

1492:     if $\dedLO{P}{\Delta}$ then there exists $k$ such that

1493:     $\val{\itp{k}}{\Delta}{\eps}$

1494:     by induction on the structure of the LO proof.

1495:     \begin{itemize}

1496:       \item[-] If the proof ends with an application of $\all_r$, then the

1497:         conclusion is immediate;

1498:       \item[-] if the proof ends with an application of the $bc$ rule, then

1499:         $\Delta=A_1,\ldots,A_n,\calA$, where $A_1,\ldots,A_n$ are atomic

1500:         formulas, and there exists a clause

1501:         $A_1\para\ldots\para A_n\lollo G\in P$.

1502:         For the uniformity of LO proofs, we can

1503:         suppose $\calA$ to be a fact. By inductive hypothesis,

1504:         we have that there exists $k$ such that

1505:         $\val{\itp{k}}{G,\calA}{\eps}$, then, by Lemma \ref{movlemma} $i)$,

1506:         $\val{\itp{k}}{G}{\calA}$, which, by definition of $T_P$, in turn

1507:         implies that $A_1,\ldots,A_n,\calA\in T_P({\itp{k}})=\itp{k+1}$,

1508:         therefore $\val{\itp{k+1}}{A_1,\ldots,A_n,\calA}{\eps}$,

1509:         i.e., $\val{\itp{k+1}}{\Delta}{\eps}$;

1510:       \item[-] if the proof ends with an application of the $\with_r$ rule,

1511:         then $\Delta=G_1\with G_2,\Delta'$ and, by inductive hypothesis,

1512:         there exist $k_1$ and $k_2$ such that

1513:         $\val{\itp{k_1}}{G_1,\Delta'}{\eps}$ and

1514:         $\val{\itp{k_2}}{G_2,\Delta'}{\eps}$. Then, if $k=max\{k_1,k_2\}$

1515:         we have, by Lemma \ref{satlemma} $ii)$, that

1516:         $\val{\itp{k}}{G_1,\Delta'}{\eps}$ and

1517:         $\val{\itp{k}}{G_2,\Delta'}{\eps}$, therefore

1518:         $\val{\itp{k}}{G_1\with G_2,\Delta'}{\eps}$, i.e.

1519:         $\val{\itp{k}}{\Delta}{\eps}$;

1520:       \item[-] the $\para$-case follows by a straightforward

1521:         application of the inductive hypothesis.

1522:     \end{itemize}

1523: \end{description}

1524: \end{proof}

1525: %

1526: We note that it is also possible to define a {\em model-theoretic} semantics

1527: (as for classical logic programming \cite{GDL95})

1528: based on the notion of {\em least model} with respect to a given

1529: class of models and partial order relation. In our setting, the partial order

1530: relation is simply set inclusion, while models are exactly

1531: Herbrand interpretations which satisfy program clauses, i.e., $I$ is a model

1532: of $P$ if and only if for every clause $H\lollo G\in P$ and for every fact

1533: $\calA$, $$ \val{I}{G}{\calA} \ \hbox{implies}\  \val{I}{H}{\calA}. $$

1534: It turns out that the operational, fixpoint and model-theor\-etic semantics are

1535: all equivalent. We omit details.

1536: Finally, we also note that these semantics can be proved equivalent to the

1537: {\em phase semantics} for LO given in \cite{AP91a}.

1538: 

1539: 

1540: \section{An Effective Semantics for LO}

1541: \label{nonground}

1542: %

1543: The operator $T_P$ defined in the previous section

1544: does not enjoy one of the crucial properties we required for our

1545: bottom-up semantics, namely its definition is {\em not} effective.

1546: As an example, take the program $P$ consisting of the clause $a\leftlolli\all$.

1547: Then, $T_P(\emptyset)$ is the set of all multisets with {\em at least}

1548: one occurrence of $a$, which is an {\em infinite} set. 

1549: In other words, $T_P(\emptyset)=\{\calB\ |\  a\preccurlyeq \calB\ \}$,

1550: where $\preccurlyeq$ is the multiset inclusion relation of Section

1551: \ref{prelim}.

1552: In order to compute {\em effectively} one step of $T_P$, we have to find

1553: a {\em finite} representation of potentially infinite sets of facts 

1554: (in the terminology of \cite{ACJT96}, a {\em constraint system}). 

1555: The previous example suggests us that a provable fact {\em \calA} may be used to 

1556: {\em implicitly} represent the ideal generated by $\calA$, i.e., 

1557: the subset of $B_P$ defined as follows:

1558: $$

1559: \den{\calA}=\{\calB\ |\ \calA\preccurlyeq\calB\}.

1560: $$

1561: We extend the definition of $\den{\cdot}$ to sets of facts as follows: 

1562: $\den{I}=\bigcup_{{\cal A}\in I} \den{\calA}$. 

1563: Based on this idea, we define an {\em abstract} Herbrand base 

1564: where  we handle every single fact $\calA$ as a representative element

1565: for $\den{\calA}$ (note that in the semantics of Section \ref{ground} 

1566: the denotation of a fact $\calA$ is $\calA$ itself!).

1567: %

1568: \begin{definition}[Abstract Herbrand Inter\-pret\-ation]

1569: \label{interpretation_lattice}

1570: The lattice $\tuple{\calI,\sqsubseteq}$ of abstract Herbrand interpretations is

1571: defined as follows:

1572: \begin{itemize} 

1573: \item[-] $\calI=\calP(B_P)/\simeq$ where $I\simeq J$ if and only 

1574: if $\den{I}=\den{J}$;

1575: \item[-] $[I]_\simeq\sqsubseteq [J]_\simeq$ if and only if for all $\calB\in I$ there exists $\calA\in J$ 

1576: such that $\calA\preccurlyeq\calB$;

1577: \item[-] the bottom element is the empty set $\emptyset$,

1578:       the top element is the $\simeq$-equivalence class of the singleton 

1579:  $\{\eps\}$ ($\eps$=empty multiset,

1580:  $\eps\preccurlyeq \calA$ for any $\calA\in B_P$);

1581: \item[-] the least upper bound $I\sqcup J$ is the $\simeq$-equivalence class of $I\cup J$.

1582: \end{itemize} 

1583: \end{definition}

1584: The equivalence $\simeq$ allows us to reason modulo {\em redundancies}. 

1585: For instance, any $\calA$ is redundant in $\{\eps,\calA\}$, which, in fact, is

1586: equivalent to $\{\eps\}$. 

1587: It is important to note that to compare two ideals we 

1588: simply need to compare their generators w.r.t. the multiset inclusion relation

1589: $\preccurlyeq$. 

1590: Thus, given a {\em finite} set of facts we can always remove all redundancies

1591: using a polynomial number of comparisons.

1592: \paragraph*{Notation.}

1593: For the sake of simplicity, in the rest of the paper we will identify an 

1594: interpretation $I$ with its class $[I]_\simeq$.

1595: Furthermore, note that if

1596: $\calA\preccurlyeq\calB$, then $\den{\calB}\subseteq\den{\calA}$. 

1597: In contrast,  if $I$ and $J$ are two interpretations and $I\sqsubseteq J$ 

1598: then $\den{I}\subseteq\den{J}$.

1599: \\

1600: \mbox{}

1601: 

1602: The two relations $\preccurlyeq$ and $\sqsubseteq$ are {\em well-quasi orderings}

1603: \cite{ACJT96,FS01}, as stated in Proposition \ref{dickson} and 

1604: Corollary \ref{termination_lemma} below.

1605: This property is the key point of our idea. 

1606: In fact, it will allow us to prove that the computation of  

1607: the least fixpoint of the {\em symbolic} formulation of the

1608: operator $T_P$ (working on abstract Herbrand interpretations)

1609: is guaranteed to terminate on every input {LO} program. 

1610: \begin{proposition}[Dickson's Lemma \cite{Dic13}]\label{dickson}

1611: Let $A_1 A_2 \ldots$ be an infinite sequence of 

1612: multisets over the finite alphabet $\Sigma$. 

1613: Then there exist two indices $i$ and $j$ such that $i<j$ and 

1614: $A_i\preccurlyeq A_j$.

1615: \end{proposition}

1616: Following \cite{ACJT96}, by definition of $\sqsubseteq$ the following 

1617: Corollary holds.

1618: \begin{corollary}\label{termination_lemma}

1619: There are no infinite sequences of interpretations $I_1 I_2 \ldots I_k\ldots$

1620: such that for all $k$ and for all $j<k$, $I_k\not\sqsubseteq I_j$.

1621: \end{corollary}

1622: Corollary \ref{termination_lemma} ensures that it is not possible 

1623: to generate infinite sequences of interpretations such that each element 

1624: is not {\em subsumed} (using a terminology from constraint logic programming) 

1625: by one of the previous elements in the sequence. 

1626: The problem now is to define a fixpoint operator over 

1627: abstract Herbrand interpretations that is {\em correct} and {\em complete} w.r.t. the ground semantics. 

1628: If we find it, then we can use the corollary to prove that (for any program)

1629: its fixpoint can be reached after finitely many steps. 

1630: For this purpose and using the multiset operations $\setminus$ (difference), 

1631: $\mlub{}{}$ (least upper bound w.r.t. $\preccurlyeq$), 

1632: and $\eps$ (empty multiset) defined in Section \ref{prelim}, 

1633: we first define a new version of the satisfiability relation 

1634: $\models$.

1635: The intuition under the new judgment 

1636: $I\asat \Delta[\calA]$

1637: is that $\calA$ is the {\em minimal} fact (w.r.t. multiset inclusion) 

1638: that should be added to $\Delta$

1639: in order for $\calA+\Delta$ to be satisfiable in $I$.

1640: %

1641: \begin{definition}[Satisfiability]

1642: \label{spsat}

1643: Let  $I\in\calP(B_P)$, then $\asat$ is defined as follows:

1644: $$\begin{array}{l}

1645: I\asat \all,{\Delta}[{\eps}];\\

1646: [\medskipamount]

1647: I\asat {\calA}[{\calB}\setminus{\calA}]\ \hbox{for}\ {\calB}\in I;\\

1648: [\medskipamount]

1649: I\asat G_1\para G_2,\Delta[{\calA}]\ \hbox{if}\ 

1650: I\asat G_1,G_2,\Delta[{\cal A}];\\

1651: [\medskipamount]

1652: I\asat G_1\with G_2,\Delta[\mlub{\calA_1}{\calA_2}]\ \hbox{if}\ 

1653: I\asat G_1,\Delta[{\calA_1}],\ I\asat G_2,\Delta[{\calA_2}].\\

1654: \end{array}

1655: $$

1656: \end{definition}

1657: Given a finite interpretation $I$ and a context $\Delta$, 

1658:  the previous definition gives us an {\em algorithm} to compute 

1659:  all facts $\calA$ such that $I\asat \Delta[\calA]$ holds.

1660: %

1661: \begin{example}

1662: \label{exjudge}

1663: Let us consider clause 2. of Example \ref{LOex}, namely

1664:   $$ b\lollo(d\para e)\with f, $$

1665: and $I=\{\{c,d\},\{c,f\}\}$.

1666: We want to compute the facts $\calA$ for which $I\asat G[\calA]$, where

1667: $G=(d\para e)\with f$ is the body of the clause. From the second rule defining

1668: the judgment $\asat$,

1669: we have that $I\asat \{d,e\}[\{c\}]$, because $\{c,d\}\in I$ and

1670: $\{c,d\}\setminus\{d,e\}=\{c\}$. Therefore we get $I\asat d\para e[\{c\}]$

1671: using the third rule for $\asat$. Similarly, we have that

1672: $I\asat\{f\}[\{c\}]$, because $\{c,f\}\in I$ and

1673: $\{c,f\}\setminus\{f\}=\{c\}$.

1674: By applying the fourth rule for $\asat$, with $G_1=d\para e$, $G_2=f$,

1675: $\calA_1=\{c\}$, $\calA_2=\{c\}$ and $\Delta=\eps$,

1676: we get $I\asat G[\{c\}]$, in fact $\mlub{\{c\}}{\{c\}}=\{c\}$.

1677: There are other ways to apply the rules for

1678: $\asat$. In fact, we can get $I\asat \{d,e\}[\{c,f\}]$,

1679: because $\{c,f\}\in I$ and $\{c,f\}\setminus\{d,e\}=\{c,f\}$.

1680: Similarly, we can get $I\asat\{f\}[\{c,d\}]$.

1681: By considering all combinations, it turns out that

1682: $I\asat G[\calA]$, for every $\calA\in\{\{c\},\{c,f\},\{c,d\},\{c,d,f\}\}$.

1683: The information conveyed by $\{c,f\},\{c,d\},\{c,d,f\}$ is in some sense

1684: {\em redundant}, as we shall see in the following (see Example \ref{example}).

1685: In other words, it is not always true that the output fact of the

1686: judgment $\asat$

1687: is {\em minimal} (in the previous example only the output $\{c\}$ is minimal).

1688: Nevertheless, the important point to be stressed here is that the set of

1689: possible facts satisfying the judgment, given $I$ and $G$, is {\em finite}.

1690: This will be sufficient to ensure effectiveness of the fixpoint operator.

1691: \end{example}

1692: %

1693: The relation $\asat$ satisfies the following properties.

1694: \begin{lemma}\label{abstract_sat_lemma}

1695: For every $I,J\in\calP(B_P)$, context $\Delta$, and fact $\calA$,

1696: \begin{enumerate}

1697: \item[i)]

1698: if $I\asat \Delta[\calA]$, then

1699: $\den{I}\models \Delta[\calA']$ for all $\calA'$ s.t. 

1700: $\calA\preccurlyeq\calA'$;

1701: \item[ii)]

1702: if  $\den{I}\models \Delta[\calA']$, then

1703: there exists $\calA$ such that

1704: $I\asat \Delta[\calA]$ and $\calA\preccurlyeq\calA'$;

1705: \item[iii)]

1706: if $I\asat \Delta[\calA]$ and $I\sqsubseteq J$, then there exists $\calA'$ such

1707: that $J\asat \Delta[\calA']$ and $\calA'\preccurlyeq\calA$;

1708: \item[iv)] given a chain of abstract Herbrand interpretations

1709: $I_1\sqsubseteq I_2\sqsubseteq \ldots$,

1710: if $\den{\bigsqcup_{i=1}^{\infty} I_i}\models \Delta[\calA]$

1711: then there exists $k$ s.t $\den{I_k}\models \Delta[\calA]$.

1712: \end{enumerate}

1713: \end{lemma}

1714: \begin{proof}

1715: \begin{description}

1716: %

1717: \item[$i)$]

1718: By induction on $\Delta$.

1719: \begin{itemize}

1720: \item[-] $I\asat\all,\Delta[\eps]$  and 

1721: $\den{I}\models\all,\Delta[\calA']$ and

1722: $\eps\preccurlyeq \calA'$ for any $\calA'$;

1723: \item[-]

1724: if $I\asat\calA[\calA']$ then 

1725: $\calA'=\calB\setminus\calA$ for $\calB\in I$. 

1726: Since $\calB\preccurlyeq (\calB\setminus\calA)+\calA=\calA'+\calA$,

1727: we have that $(\calB\setminus\calA)+\calA\in\den{I}$, therefore

1728: $\den{I}\models\calA[\calB\setminus\calA]$, so that $\den{I}\models\calA[\calC]$ for

1729: all $C$ s.t. $\calA'=\calB\setminus\calA\preccurlyeq\calC$, because $\den{I}$

1730: is upward closed;

1731: \item[-]

1732: if $I\asat G_1\with G_2,\Delta[\calA]$ then $\calA=\mlub{\calA_1}{\calA_2}$ 

1733: and $I\asat G_1,\Delta[\calA_1]$ and $I\asat G_2,\Delta[\calA_2]$.

1734: By inductive hypothesis, 

1735: $\den{I}\models G_1,\Delta[\calB_1]$ and 

1736: $\den{I}\models G_2,\Delta[\calB_2]$ for any $\calB_1,\calB_2$ s.t.

1737: $\calA_1\preccurlyeq\calB_1$ and $\calA_2\preccurlyeq\calB_2$. 

1738: That is, $\den{I} \models G_i,\Delta[\calC]$ for any 

1739: $\calC\in \den{\mlub{\calA_1}{\calA_2}}$ $i:1,2$. 

1740: It follows that $\den{I} \models G_1\with G_2,\Delta[\calC]$ for all

1741: $\calC\in \den{\mlub{\calA_1}{\calA_2}}$;

1742: \item[-] the $\para$-case follows by a straightforward

1743: application of the inductive hypothesis.

1744: \end{itemize}

1745: %

1746: \item[$ii)$]

1747: By induction on $\Delta$.

1748: \begin{itemize}

1749: \item[-] The $\all$-case follows by definition;

1750: \item[-]

1751: if $\den{I}\models\calA[\calA']$ then 

1752: $\calA'+\calA\in \den{I}$, i.e.,  there exists $\calB\in I$ 

1753: s.t. $\calB\preccurlyeq \calA'+\calA$. 

1754: Since $\calB\setminus \calA\preccurlyeq (\calA'+\calA)\setminus\calA=\calA'$,

1755: it follows that for $\calC=\calB\setminus \calA$, 

1756: $I\asat\calA[\calC]$ and $\calC\preccurlyeq \calA'$;

1757: \item[-]

1758: if $\den{I} \models G_1\with G_2,\Delta[\calA]$

1759: then $\den{I} \models G_i,\Delta[\calA]$ for $i:1,2$. 

1760: By inductive hypothesis, there exists $\calA_i$ such that 

1761: $\calA_i\preccurlyeq\calA$,

1762: $I\asat G_i,\Delta[\calA_i]$ for $i:1,2$, i.e., 

1763: $I\asat G_1\with G_2,\Delta[\mlub{\calA_1}{\calA_2}]$.

1764: The thesis follows noting that $\mlub{\calA_1}{\calA_2}\preccurlyeq\calA$;

1765: \item[-] the $\para$-case follows by a straightforward application of the

1766: inductive hypothesis.

1767: \end{itemize}

1768: %

1769: \item[$iii)$]

1770: If $I\asat \Delta[\calA]$, then by $i)$,

1771:  $\den{I}\models\Delta[\calA]$. 

1772:  Since $\den{I}\subseteq \den{J}$ then, by Lemma \ref{satlemma} $ii)$,

1773:  $\den{J}\models\Delta[\calA]$.

1774:  Thus, by $ii)$,

1775:  there exists $\calA'\preccurlyeq\calA$ s.t. 

1776:  $J\asat\Delta[\calA']$.

1777: %

1778: \item[$iv)$]

1779: By induction on $\Delta$.

1780: \begin{itemize}

1781:   \item[-] If $\Delta=\all,\Delta'$, then, no matter which $k$ you choose,

1782:     $\den{I_k}\models{\all,\Delta'}[{\calA}]$;

1783:   \item[-] if $\Delta$ is a fact, then 

1784:     $\Delta,\calA\in\den{\bigsqcup_{i=1}^{\infty} I_i}$, that is

1785:     there exists $\calB$ s.t. $\calB\in\bigsqcup_{i=1}^{\infty} I_i$ and

1786:     $\calB\preccurlyeq\Delta,\calA$. Therefore there exists $k$ s.t.

1787:     $\calB\in I_k$ and $\calB\preccurlyeq\Delta,\calA$, that is

1788:     $\Delta,\calA\in\den{I_k}$;

1789:   \item[-] if $\Delta=G_1\with G_2,\Delta'$, then by inductive hypothesis

1790:     there exist $k_1$ and $k_2$ s.t. $\val{\den{I_{k_1}}}{G_1,\Delta'}{\calA}$

1791:     and

1792:     $\val{\den{I_{k_2}}}{G_2,\Delta'}{\calA}$.

1793:     Therefore, if $k=max\{k_1,k_2\}$, by

1794:     Lemma \ref{satlemma} $ii)$, we

1795:     have that $\val{\den{I_k}}{G_1,\Delta'}{\calA}$

1796:     and $\val{\den{I_k}}{G_2,\Delta'}{\calA}$, therefore

1797:     $\val{\den{I_k}}{G_1\with G_2,\Delta'}{\calA}$, i.e.

1798:     $\val{\den{I_k}}{\Delta}{\calA}$;

1799:   \item[-] the $\para$-case follows by a straightforward

1800:     application of the inductive hypothesis.

1801: \end{itemize}

1802: \end{description}

1803: \end{proof}

1804: %

1805: We are ready now to define the abstract fixpoint operator 

1806: $\STP:\calI\rightarrow\calI$.

1807: We will proceed in two steps. 

1808: We will first define an operator working over 

1809: elements of $\calP(B_P)$.

1810: With a little bit of overloading, we will call the operator 

1811: with the same name, i.e.,  $S_P$.

1812: As for the $\STP$ operator used in the symbolic semantics of CLP programs 

1813: \cite{JM94}, the operator should satisfy the equation  

1814: $\den{\STP(I)}=T_P(\den{I})$ for any $I,~J\in\calP(B_P)$.

1815: This property ensures the soundness and completeness of the 

1816: {\em symbolic} representation w.r.t. the ground semantics of LO programs.

1817: 

1818: After defining the operator over $\calP(B_P)$, 

1819: we will lift it to our abstract domain $\calI$ consisting 

1820: of the equivalence classes of elements of $\calP(B_P)$ w.r.t. 

1821: the relation $\simeq$ defined in Definition \ref{interpretation_lattice}.

1822: Formally, we first introduce the following definition.

1823: \begin{definition}[Symbolic Fixpoint Operator]\label{fixpoint_operator}

1824: Given an {LO} program $P$, and $I\in\calP(B_P)$,

1825: the operator $\STP$ is defined as follows:

1826: $$

1827: \STP(I)=\{\ms{H}+{\cal A}\ |\ H\leftlolli G\in P,

1828: \ I\asat G[{\cal A}]\}.

1829: $$

1830: \end{definition}

1831: The following property shows that $\STP$ is 

1832: sound and complete w.r.t. $T_P$.

1833: %

1834: \begin{proposition}\label{completeness} 

1835: Let $I\in\calP(B_P)$, then $\den{\STP(I)}=T_P(\den{I})$.

1836: \end{proposition}

1837: \begin{proof}

1838: Let $\calA=\ms{H},\calB\in \STP(I)$ where $H\leftlolli G\in P$

1839: and $I\asat G[\calB]$ then, by Lemma \ref{abstract_sat_lemma} $i)$,

1840: $\den{I}\models G[\calB']$ for any $\calB'$ s.t. $\calB\preccurlyeq\calB'$.

1841: Thus, for any $\calA'=\ms{H},\calB'$ s.t. $\calA\preccurlyeq\calA'$, 

1842: $\calA'\in T_P(\den{I})$.\\

1843: Vice versa,  if $\calA\in T_P(\den{I})$ then 

1844: $\calA=\ms{H},\calB$ where $H\leftlolli G\in P$

1845: and $\den{I}\models G[\calB]$. 

1846: By Lemma \ref{abstract_sat_lemma} $ii)$, 

1847: there exists $\calB'$ s.t. $\calB'\preccurlyeq\calB$ and 

1848: $I\asat G[\calB']$, i.e., $\calA'=\ms{H},\calB'\in \STP(I)$ 

1849: and $\calA'\preccurlyeq\calA$.

1850: \end{proof}

1851: Furthermore, the following corollary holds.

1852: \begin{corollary}\label{cor_well_def}

1853: Given $I,J\in\calP(B_P)$, if $I\simeq J$ then $S_P(I)\simeq S_P(J)$.

1854: \end{corollary}

1855: \begin{proof}

1856: If $I\simeq J$, then, by definition of $\simeq$, it follows that 

1857: $\den{I}=\den{J}$. This implies that $T_P(\den{I})=T_P(\den{J})$.

1858: Thus, by Prop. \ref{completeness} it follows that 

1859: $\den{S_P(I)}=\den{S_P(J)}$, i.e., $S_P(I)\simeq S_P(J)$.

1860: \end{proof}

1861: The previous corollary allows us to safely lift the definition of $S_P$ 

1862: from the lattice $\tuple{\calP(B_P),\subseteq}$ to the lattice 

1863: $\tuple{\calI,\sqsubseteq}$.

1864: Formally, we define the abstract fixpoint operator as follows. 

1865: \begin{definition}[Abstract Fixpoint Operator $\STP$]\label{symbolic_fixpoint}

1866: Given an {LO} program $P$, and an equivalence class $[I]_\simeq$ of $\calI$, 

1867: the operator $\STP$ is defined as follows:

1868: $$

1869: \STP([I]_\simeq)=[\STP(I)]_\simeq

1870: $$

1871: where $\STP(I)$ is defined in Definition \ref{fixpoint_operator}.

1872: \end{definition}

1873: In the following  we will use $I$ to denote its class $[I]_\simeq$. 

1874: The abstract operator $\STP$ satisfies the following property. 

1875: \begin{proposition}

1876: $\STP$ is monotonic and continuous over the lattice

1877: $\tuple{\calI,\sqsubseteq}$.

1878: \end{proposition}

1879: \begin{proof}

1880: \mbox{}\\

1881: {\em Monotonicity}.

1882: For any $\calA=\ms{H},\calB\in \STP(I)$

1883: there exists $H\leftlolli G\in P$ s.t. 

1884: $I\asat G[\calB]$.

1885: Assume now that $I\sqsubseteq J$. 

1886: Then, by Lemma \ref{abstract_sat_lemma} $iii)$, 

1887: we have that $J\asat G[\calB']$

1888: for $\calB'\preccurlyeq\calB$. Thus, there exists 

1889: $\calA'=\ms{H},\calB'\in \STP(J)$ such that 

1890: $\calA'\preccurlyeq\calA$, i.e., $\STP(I)\sqsubseteq \STP(J)$.

1891: \\

1892: {\em Continuity}. We show that $\STP$ is finitary. 

1893: Let $I_1\sqsubseteq I_2\sqsubseteq \ldots$ be an increasing sequence of 

1894: interpretations.

1895: For any $\calA=\ms{H},\calB\in \STP(\bigsqcup_{i=1}^{\infty} I_i)$ 

1896: there exists $H\leftlolli G\in P$ s.t. 

1897: $\bigsqcup_{i=1}^{\infty} I_i\asat G[\calB]$.

1898: By Lemma \ref{abstract_sat_lemma} $i)$,

1899: $\den{\bigsqcup_{i=1}^{\infty} I_i}\models G[\calB]$. 

1900: By Lemma \ref{abstract_sat_lemma} $iv)$, we

1901: get that $\den{I_k}\models G[\calB]$ for some $k$,

1902: and by Lemma \ref{abstract_sat_lemma} $ii)$, 

1903: $I_k\asat G[\calB']$ for $\calB'\preccurlyeq\calB$.

1904: Thus,  $\calA'=\ms{H},\calB'\in \STP(I_k)$, i.e., 

1905: $\calA'\in \bigsqcup_{i=1}^{\infty} \STP(I_i)$, i.e., 

1906: $\STP(\bigsqcup_{i=1}^{\infty} I_i)\sqsubseteq 

1907: \bigsqcup_{i=1}^{\infty} \STP(I_i)$.

1908: \end{proof}

1909: %

1910: \begin{corollary}

1911: \label{fixpoint_equivalence}

1912: $\den{\lfp(\STP)}=\lfp(T_P)$.

1913: \end{corollary}

1914: %

1915: Let $SymbF(P)=\lfp(\STP)$, then we have the following main theorem.

1916: \begin{theorem}[Soundness and Completeness]

1917: \label{main_theorem}

1918: Given an LO program $P$, $O(P)=F(P)=\den{SymbF(P)}$.

1919: Furthermore, there exists $k\in\Nat$ such that 

1920: $SymbF(P)=\bigsqcup_{i=0}^k \isp{k}(\emptyset)$. 

1921: \end{theorem}

1922: \begin{proof}

1923: Theorem \ref{fixpoint_operational} and Corollary \ref{fixpoint_equivalence} 

1924: show that $O(P)=F(P)=\den{SymbF(P)}$. Corollary \ref{termination_lemma} guarantees

1925: that the fixpoint of $\STP$ can always be reached after finitely many steps.

1926: \end{proof}

1927: %

1928: The previous results give us an algorithm to compute the operational and 

1929: fixpoint semantics of a propositional {LO} program via the operator $\STP$.

1930: The algorithm is inspired by the {\em backward reachability} algorithm 

1931: used in \cite{ACJT96,FS01} to compute {\em backwards} the closure of the 

1932: {\em predecessor} operator of a well-structured transition system.

1933: The algorithm in pseudo-code for computing $F(P)$ is shown in Figure \ref{symbef}.

1934: Corollary \ref{termination_lemma} guarantees that the algorithm always 

1935: terminates and returns a {\em symbolic} representation of $O(P)$. 

1936: %

1937: \begin{figure*}

1938: \centering

1939: \centerline{

1940: \small

1941: $

1942: \begin{array}{ll}

1943: {\bf Procedure}\ symbF(P:\hbox{{LO}\ program}){\bf :}\\

1944: \ \ \ {\bf set}\ {New}:=\{\ms{H}\ |\ H\leftlolli \all\in P\}\ \ {\bf and}\ \ \hbox{Old}:=\emptyset;\\

1945: \ \ \ {\bf repeat}\\

1946: \ \ \ \ \ \ \ \hbox{Old}:= {Old}\ \cup\  \hbox{New};\\

1947: \ \ \ \ \ \ \ \hbox{New}:=\STP(\hbox{New});\\

1948: \ \ \ {\bf until}\  \hbox{New}\sqsubseteq  \hbox{Old};\\

1949: \ \ \ {\bf return}\ \  \hbox{Old}.

1950: \end{array}

1951: $}

1952: \caption{Symbolic fixpoint computation}

1953: \label{symbef}

1954: \end{figure*} 

1955: As a corollary of Theorem \ref{main_theorem}, we obtain the following result.

1956: \begin{corollary}

1957: The provability of $P\Rightarrow G$ in propositional {LO} is {\em decidable}.

1958: \end{corollary}

1959: In view of Proposition \ref{monotonicity}, this result can be considered as an

1960: instance of the general decidability result \cite{Kop95} for propositional

1961: {\em affine}

1962: linear logic (i.e., linear logic with {\em weakening}).

1963: \begin{example}

1964: \label{example}

1965: %

1966: We calculate the fixpoint semantics for the program $P$ of Example \ref{LOex},

1967: which is given below.

1968: %

1969: $$\begin{array}{l}

1970:   1.\ \ a\lollo b\para c\\

1971:   2.\ \ b\lollo(d\para e)\with f\\

1972:   3.\ \ c\para d\lollo\all\\

1973:   4.\ \ e\para e\lollo b\para c\\

1974:   5.\ \ c\para f\lollo\all\\

1975: \end{array}$$

1976: %

1977: We start the computation from $\isp{0}=\eset$.

1978: The first step consists in adding the multisets corresponding to program

1979: facts, i.e., clauses 3. and 5., therefore we compute

1980:  $$ \isp{1}=\{\{c,d\},\{c,f\}\}. $$

1981: Now, we can try to apply clauses 1., 2., and 4. to facts in $\isp{1}$.

1982: From the first clause, we have that $\isp{1}\asat\{b,c\}[\{d\}]$ and

1983: $\isp{1}\asat\{b,c\}[\{f\}]$, therefore $\{a,d\}$ and $\{a,f\}$ are elements of

1984: $\isp{2}$. Similarly, for clause 2. we have that $\isp{1}\asat\{d,e\}[\{c\}]$

1985: and $\isp{1}\asat\{f\}[\{c\}]$, therefore we have,

1986: from the rule for $\with$, that $\{b,c\}$ belongs to $\isp{2}$ (we can also

1987: derive other judgments for clause 2., as seen in Example \ref{exjudge},

1988: for instance

1989: $\isp{1}\asat\{d,e\}[\{c,f\}]$,

1990: but it immediately turns out that

1991: all these judgments give rise to {\em redundant} information, i.e., facts

1992: that are subsumed by the already calculated ones).

1993: By clause 4., finally we have that $\isp{1}\asat\{b,c\}[\{d\}]$ and

1994: $\isp{1}\asat\{b,c\}[\{f\}]$, therefore $\{d,e,e\}$ and $\{e,e,f\}$ belong to

1995: $\isp{2}$. We can therefore take the

1996: following equivalence class as representative for $\isp{2}$:

1997: $$ \isp{2}=\{\{c,d\},\{c,f\},\{a,d\},\{a,f\},\{b,c\},\{d,e,e\},\{e,e,f\}\}. $$

1998: We can similarly calculate $\isp{3}$. For clause 1. we immediately have

1999: that $\isp{2}\asat\{b,c\}[\eps]$, so that $\{a\}$ is an element of

2000: $\isp{3}$; this makes the information given by $\{a,d\}$ and

2001: $\{a,f\}$ in $\isp{2}$

2002: redundant. From clause 4. we can get that $\{e,e\}$ is another element of

2003: $\isp{3}$, which implies that the information given by $\{d,e,e\}$ and

2004: $\{e,e,f\}$ is now redundant. No additional (not redundant) elements are

2005: obtained from clause 2.

2006: We therefore can take

2007: $$ \isp{3}=\{\{c,d\},\{c,f\},\{b,c\},\{a\},\{e,e\}\}. $$

2008: The reader can verify that

2009: $ \isp{4}=\isp{3}=SymbF(P) $

2010: so that

2011: $$ O(P)=F(P)=\den{\{\{c,d\},\{c,f\},\{b,c\},\{a\},\{e,e\}\}}. $$

2012: %

2013: We suggest the reader to compare the top-down proof for the goal $e,e$, given

2014: in Figure \ref{LOproof}, and the part of the

2015: bottom-up computation which yields the same

2016: goal. The order in which the backchaining steps are performed is reversed,

2017: as expected. Moreover, the top-down computation requires to solve one

2018: goal, namely $d,e,c$, which is not {\em minimal}, in the sense that its proper

2019: subset $c,d$ is still provable. Using the bottom-up algorithm sketched above,

2020: at every step only the minimal information (in this case $c,d$) is kept at

2021: every step. In general, this strategy has the further advantage of reducing

2022: the amount of non-determinism in the proof search. For instance, let us

2023: consider the goal $b,e,e$ (which is certainly provable because of Proposition

2024: \ref{monotonicity}). This goal has at least two different proofs. The first is

2025: a slight modification of the proof in Figure \ref{LOproof} (just add the

2026: atom $b$ to every sequent). An alternative proof is the following,

2027: obtained by changing the order of applications of the backchaining steps:

2028: 

2029: $$

2030:     \infer[bc^{(2)}]{P\Rightarrow b,e,e}

2031:    {\infer[\with_r]{P\Rightarrow (d\para e)\with f,e,e}

2032:    {\infer[\para_r]{P\Rightarrow d\para e,e,e}

2033:    {\infer[bc^{(4)}]{P\Rightarrow d,e,e,e}

2034:    {\infer[\para_r]{P\Rightarrow d,e,b\para c}

2035:    {\infer[bc^{(3)}]{P\Rightarrow d,e,b,c}

2036:    {\infer[\all_r]{P\Rightarrow e,b,\all}

2037:    {}}}}}

2038:      &

2039:     \infer[bc^{(4)}]{P\Rightarrow f,e,e}

2040:    {\infer[\para_r]{P\Rightarrow f,b\para c}

2041:    {\infer[bc^{(5)}]{P\Rightarrow f,b,c}

2042:    {\infer[\all_r]{P\Rightarrow b,\all}{}}}}

2043:    }}

2044: $$

2045: There are even more complicated proofs (for instance in the left branch I could

2046: rewrite $b$ again by backchaining over clause 2. rather than axiom 3).

2047: The bottom-up computation avoids these complications by keeping only

2048: {\em minimal} information at every step. We would also like to stress that

2049: the bottom-up computation is always guaranteed to terminate, as stated in

2050: Theorem \ref{main_theorem}, while in general the top-down computation can

2051: diverge.

2052: \end{example}

2053: 

2054: 

2055: \section{A Bottom-up Semantics for \LOonet}

2056: \label{one}\label{groundo}

2057: %

2058: As shown in \cite{And92}, the original formulation of the 

2059: language {LO} can be extended in order to take into consideration 

2060: more powerful programming constructs. 

2061: In this paper we will consider an extension of {LO} where goal formulas 

2062: range over the $\formula{G}$-formulas of Section \ref{lo} and over the logical 

2063: constant $\one$. In other words, we extend {LO} with clauses of the following form:

2064: $$A_1\para\ldots\para A_n\leftlolli \one.$$

2065: We name this language \LOonews,

2066: and use the notation $\dedLOo{P}{\Delta}$ for \LOone sequents.

2067: The meaning of the new kind of clauses is given by the 

2068: following inference scheme:

2069: $$

2070:  \infer[bc\ (H\leftlolli \one\ \in\ P)]

2071: {P\Rightarrow_\one \ms{H}}

2072: {\infer[\one_r]{P\Rightarrow_\one \one}{}}

2073: $$

2074: Note that there cannot be other {\em resources} in the right-hand side 

2075: of the lower sequent apart from $a_1,\ldots,a_n$.

2076: Thus, in contrast with $\all$, the constant $\one$ intuitively

2077: introduces the possibility of 

2078: {\em counting} resources.

2079: %

2080: \begin{example}

2081: \label{espetri}

2082: LO programs can be used to encode Petri Nets

2083: (see also the proof of Proposition \ref{undecidable} and Section \ref{petri}).

2084: Let us consider a simple Petri net with three places $a$, $b$ and $c$.

2085: We can represent a marking with a multiset of atoms and a transition with a

2086: clause. For instance,

2087: the clause $a~\para~b~\lollo~c~\para~c$

2088: can be interpreted as the Petri Net transition that removes one token from 

2089: place $a$, one token from place $b$, and adds two tokens to place $c$.

2090: By using the constant $\one$, we can specify an operation $trans$

2091: which transfers

2092: {\em all} tokens in place $a$ to place $b$. The encoding is as follows:

2093: %

2094: $$\begin{array}{l}

2095:   1.\ \ a\para trans\lollo b\para trans\\

2096:   2.\ \ trans\lollo done\with check\\

2097:   3.\ \ check\para b\lollo check\\

2098:   4.\ \ check\para c\lollo check\\

2099:   5.\ \ check\lollo\one\\

2100: \end{array}$$

2101: %

2102: The first clause specifies the transfer of a single token from $a$ to $b$,

2103: and it is supposed to be used as many times as the number of initial tokens in

2104: $a$. The second clause starts an auxiliary branch of the computation which

2105: checks that all tokens have been moved to $b$.

2106: The proof for the initial marking $a,a,c$ is given in Figure \ref{espetrifig}

2107: (where, for simplicity, applications of the $\para_r$ and $\with_r$ rules

2108: have been

2109: incorporated into backchaining steps).

2110: Note that the check cannot succeed if there are any tokens left in $a$. Using

2111: $\one$ in clause 5. is crucial to achieve this goal.

2112: %

2113: \begin{figure*}

2114: $$

2115:    \infer[bc^{(1)}]{P\Rightarrow_\one a,a,c,trans}

2116:   {\infer[bc^{(1)}]{P\Rightarrow_\one b,a,c,trans}

2117:   {\infer[bc^{(2)}]{P\Rightarrow_\one b,b,c,trans}

2118:   {\infer[]{P\Rightarrow_\one b,b,c,done}{\vdots}

2119:     &

2120:    \infer[bc^{(3)}]{P\Rightarrow_\one b,b,c,check}

2121:   {\infer[bc^{(3)}]{P\Rightarrow_\one b,c,check}

2122:   {\infer[bc^{(4)}]{P\Rightarrow_\one c,check}

2123:   {\infer[bc^{(5)}]{P\Rightarrow_\one check}

2124:   {\infer[\one_r]{P\Rightarrow_\one \one}{}

2125:   }}}}}}}

2126: $$

2127: \caption{An \LOone proof for the goal $a,a,c,trans$ in the program of

2128: Example \ref{espetri}}

2129: \label{espetrifig}

2130: \end{figure*}

2131: %

2132: \end{example}

2133: %

2134: Provability in \LOone amounts to provability in the proof system for {LO} 

2135: augmented with the $\one_r$ rule.

2136: As for {LO}, let us define the top-down operational semantics of an 

2137: \LOone program as follows:

2138: 

2139:   $$ \opo = \{\calA\ |\ \calA\ is\ a\ fact\ and\ \dedLOo{P}{\calA}\ is\ provable\}. $$

2140: %

2141: We first note that, in contrast with Proposition \ref{monotonicity}, the weakening rule 

2142: is not admissible in \LOonews. 

2143: This implies that we cannot use the same techniques we used 

2144: for the fragment without $\one$.

2145: So the question is: can we still find a finite representation of $\opo$? 

2146: The following proposition gives us a negative answer.

2147: %

2148: \begin{proposition}

2149: \label{undecidable}

2150: Given an \LOone program $P$, there is no algorithm to compute $\opo$.

2151: \end{proposition}

2152: \begin{proof}

2153: To prove the result we present an encoding of Vector Addition Systems (VAS) 

2154: as \LOone programs. 

2155: A VAS consists of a transition system defined over $n$ variables

2156: $\tuple{x_1,\ldots,x_n}$ ranging over positive integers.

2157: The transition rules have the form 

2158: $x_1'=x_1+\delta_1,\ldots,x_n'=x_n+\delta_n$ where 

2159: $\delta_n$ is an integer constant.

2160: Whenever $\delta_i<0$,  guards of the form $x_i\geq -\delta_i$ 

2161: ensure that the variables assume only positive values.

2162: Following \cite{Cer95}, the encoding of a VAS in \LOone is defined as follows.

2163: We associate a propositional symbol $a_i\in\Sigma$ 

2164: to each variable $x_i$. A VAS-transition now becomes a 

2165: rewriting rule $H\leftlolli B$ where 

2166: $Occ_{\ms{B}}(a_i)=-\delta_i$ if $\delta_i<0$ (tokens removed from place $i$) 

2167: and $Occ_{\ms{H}}(a_i)=\delta_i$  if $\delta_i\geq 0$ 

2168: (tokens added to place $i$).

2169: We encode the set of initial markings

2170: (i.e., assignments for the variables $x_i$'s) $M_1,\ldots,M_k$ using $k$ clauses

2171: as follows. 

2172: The i-$th$ clause  $H_i\leftlolli\one$ is such that 

2173: if $M_i$ is the assignment $\tuple{x_1=c_1,\ldots,x_n=c_n}$ then 

2174: $Occ_{\ms{H_i}}(a_j)=c_j$ for $j:1,\ldots,n$.

2175: Based on this idea, if $P_V$ is the program that encodes the VAS $V$ 

2176: it is easy to check that  $O(P_V)$ corresponds to 

2177: the set of {\em reachable} markings of $V$ (i.e., to the closure 

2178: $post^*$ of the $successor$ operator $post$ w.r.t. $V$ and the initial

2179: markings). From classical results on Petri Nets (see e.g. the survey \cite{EN94}), 

2180: there is no algorithm to compute the set of reachable states 

2181: of a VAS $V$ (=$O(P_V)$). 

2182: If not so, we would be able to solve the {\em marking equivalence} 

2183: problem that is known to be undecidable.

2184: \end{proof}

2185: %

2186: Despite Proposition \ref{undecidable}, it is still possible to define a

2187: {\em symbolic}, effective fixpoint operator for \LOone programs

2188: as we will show in the following section.

2189: Before going into more details,  we first rephrase the semantics 

2190: of Section \ref{ground} for \LOonews.

2191: We omit the proofs, which are analogous to those of Section \ref{ground}.

2192: For the sake of

2193: simplicity, in the rest of the paper we will still

2194: denote the satisfiability judgments for \LOone with $\osat$ and $\asat$.

2195: %

2196: \begin{definition}[Satisfiability in \LOonews]

2197: Let $I$ be a Herbrand interpretation, then $\osat$ is defined as follows:

2198: $$\begin{array}{l} 

2199:   \valo{I}{\one}{\eps};\\

2200:   [\medskipamount]

2201:   \valo{I}{\all,\Delta}{\calA'}\ \hbox{for any fact}\ \calA';\\

2202:   [\medskipamount]

2203:   \valo{I}\calA{\calA'}\ \hbox{if}\ \calA+\calA' \in I;\\

2204:   [\medskipamount]

2205:   \valo{I}{G_1\para G_2,\Delta}{\calA}\ \hbox{if}\ \valo{I}{G_1,G_2,\Delta}{\calA};\\

2206:   [\medskipamount]

2207:   \valo{I}{G_1\with G_2,\Delta}{\calA}\ \hbox{if}\ \valo{I}{G_1,\Delta}{\calA}\ 

2208:     \mbox{and}\ \valo{I}{G_2,\Delta}{\calA}.\\

2209: \end{array}$$

2210: \end{definition}

2211: %

2212: The new satisfiability relation satisfies the following properties.

2213: %

2214: \begin{lemma}

2215: \label{movlemmao}\label{satlemmao}\label{finitary_lemmao}

2216: For any interpretations $I,J$,

2217: context $\Delta$, and fact $\calA$,

2218: \begin{enumerate}

2219: \item[i)] $\valo{I}{\Delta}{\calA}\ if\ and\ only\ if\ \valo{I}{\Delta,\calA}{\eps}$;

2220: \item[ii)] if $I\subseteq J$ and $\valo{I}{\Delta}{\calA}$ then $\valo{J}{\Delta}{\calA}$;

2221: \item[iii)]

2222: given a chain of interpretations $I_1\subseteq I_2\subseteq\ldots$, if  

2223: $\valo{\Un{i}{\infty}I_i}{\Delta}{\calA}$ 

2224: then there exists $k$ s.t. $\valo{I_k}{\Delta}{\calA}$.

2225: \end{enumerate}

2226: \end{lemma}

2227: %

2228: The fixpoint operator $\tpo$ is defined like $T_P$.

2229: \begin{definition}[Fixpoint operator $\tpo$]

2230: Given an {\LOone} program $P$, and an interpretation $I$,

2231: the operator $\tpo$ is defined as follows:

2232:   $$ \tpo(I)=\{\ms{H}+\calA\ |\ H\lollo G\in P,\ \valo{I}{G}{\calA}\}. $$

2233: \end{definition}

2234: The following property holds.

2235: \begin{proposition}\label{montheoro}

2236: $\tpo$ is monotonic and continuous over the lattice

2237: $\tuple{\calD,\subseteq}$.

2238: \end{proposition}

2239: %

2240: The fixpoint semantics is defined as $\fpo=\lfp(\tpo)=\itpo{\omega}$.

2241: It is sound and complete with respect to the operational semantics, 

2242: as stated in the following theorem.

2243: \begin{theorem}[Soundness and Completeness]

2244: \label{fixpoint_operationalo}

2245: For every \LOone program $P$, $\fpo=\opo$.

2246: \end{theorem}

2247: %

2248: \section{Constraint Semantics for \LOonet}

2249: \label{nongroundo}

2250: %

2251: In this section we will define a {\em symbolic} fixpoint operator which relies

2252: on a con\-straint-based representation of provable multisets. 

2253: The application of this operator is effective. 

2254: Proposition \ref{undecidable} shows however that there is no guarantee that its fixpoint 

2255: can be reached after finitely many steps.

2256: According to the encoding of VAS used in the proof of Proposition \ref{undecidable},

2257: let $\vec{x}=\tuple{x_1,\ldots,x_n}$ be a vector of variables, where variable $x_i$ 

2258: denotes the number of

2259: occurrences of $a_i\in\Sigma$ in a given fact. Then we can

2260: immediately recover the semantics of Section \ref{nonground} using a

2261: very simple class of linear constraints over integer variables.

2262: Namely, given a fact $\calA$

2263: we can denote its closure, i.e., the ideal $\den{\calA}$, by the constraint

2264: $$\varphi_{\den{\cal A}}\ \equiv\ \bigwedge_{i=1}^{n}x_i\geq Occ_{\cal A}(a_i).$$

2265: Then all the operations on multisets involved in the definition of

2266: $\STP$ (see Definition \ref{spsat}) can be expressed as operations over

2267: linear constraints. In particular, given the ideals

2268: $\den{\cal A}$ and $\den{\cal B}$, the ideal $\den{\calA\bullet\calB}$

2269: is represented as the constraint

2270:   $$ \varphi_{\den{{\cal A}\bullet{\cal B}}}=

2271:      \varphi_{\den{\cal A}}\wedge\varphi_{\den{\cal B}}, $$ while

2272: $\den{\calB\setminus\calA}$, for a given multiset $\calA$, is represented as

2273: the constraint

2274:   $$ \varphi_{\den{{\cal B}\setminus{\cal A}}}=

2275:      \exists\vec{x'}.(\varphi_{\den{\cal B}}[\vec{x}'/\vec{x}]\wedge 

2276:       \Rem_{\cal A}(\vec{x},\vec{x'})), $$

2277:      where  

2278:   $$\Rem_{\cal A}(\vec{x},\vec{x'})\ \equiv\ 

2279:    \bigwedge_{i=1}^n x_i=x_i'-Occ_{\cal A}(a_i)\ \wedge\ x_i\geq 0.$$

2280: The constraint $\Rem_{\cal A}$ models the removal of the occurrences of the literals 

2281: in ${\calA}$ from all elements of the denotation of ${\calB}$.

2282: Similarly, $\den{\calB+\calA}$, for a given multiset $\calA$, 

2283: is represented as the constraint 

2284:   $$ \varphi_{\den{{\cal B}+{\cal A}}}=\exists \vec{x'}.(\varphi_{\den{\cal B}}[\vec{x}'/\vec{x}]\wedge \Add_{\cal A}(\vec{x},\vec{x'})), $$

2285: where 

2286: $$\Add_{\cal A}(\vec{x},\vec{x'})\ 

2287: \equiv\ \bigwedge_{i=1}^n 

2288: x_i=x_i'+Occ_{\cal A}(a_i).$$

2289: The introduction of the constant $\one$ breaks down Proposition \ref{monotonicity}. 

2290: As a consequence, the abstraction based on ideals is no more precise.

2291: In order to give a semantics for \LOonews, we need to add a class of

2292: constraints for representing collections of multisets which are not 

2293: upward-closed (i.e., which are not ideals). 

2294: We note then that we can represent a multiset ${\cal A}$ as the linear constraint

2295: $$\varphi_{\cal A}\ \equiv\ \bigwedge_{i=1}^{n}x_i=Occ_{\cal A}(a_i).$$

2296: The operations over linear constraints discussed previously extend smoothly

2297: when adding this new class of equality constraints. In particular,

2298: given two constraints $\varphi$ and $\psi$,

2299: their conjunction $\varphi\cand\psi$ still plays the role that the operation

2300: $\bullet$ (least upper bound of multisets) had in Definition \ref{spsat}, while

2301: $\exists\vec{x'}.(\varphi[\vec{x}'/\vec{x}]\wedge \Rem_{\cal A}(\vec{x},\vec{x'}))$, for a given multiset $\calA$, plays the role of multiset difference.

2302: The reader can compare Definition \ref{spsat} with Definition \ref{sposat}. 

2303: Based on these ideas, we can define a bottom-up evaluation procedure for 

2304: \LOone programs via an extension $\STPo$ of the operator $\STP$.

2305: 

2306: In the following we will use the notation $\msc{\vec{c}}$, where

2307: $\vec{c}=\tuple{c_1,\ldots,c_n}$ is

2308: a solution of a constraint $\varphi$ (i.e., an assignment of natural numbers

2309: to the variables $\vec{x}$ which satisfies $\varphi$),

2310: to indicate the multiset over $\Sigma=\{a_1,\ldots,a_n\}$

2311: which contains $c_i$ occurrences of every propositional symbol $a_i$

2312: (i.e., according to the notation introduced above,

2313: $\vec{c}$ is the unique solution of

2314: $\varphi_{\msc{\vec{c}}}$).

2315: We extend this definition to a set $C$ of constraint

2316: solutions by $\msc{C}=\{\msc{\vec{c}}\ |\ \vec{c}\in C\}$.

2317: We then define the denotation of a given constraint

2318: $\varphi$, written $\deno{\varphi}$,

2319: as the set of multisets corresponding to solutions of $\varphi$, i.e.,

2320: $\deno{\varphi}=\{\msc{\vec{c}}\ |\ \vec{x}=\vec{c}\ \hbox{satisfies}\ \varphi\}$.

2321: 

2322: Following \cite{GDL95}, we introduce an equivalence relation $\simeq$ over constraints, given by

2323: $\varphi\simeq\psi$ if and only if $\deno{\varphi}=\deno{\psi}$, i.e.,

2324: we identify constraints with the same set of solutions. For the

2325: sake of simplicity, in the following we will identify a constraint with its

2326: equivalence class, i.e., we will simply write $\varphi$ instead of

2327: $[\varphi]_\simeq$. 

2328: Let $\linc$ be the set of (equivalence classes of) of linear constraints

2329: over the integer variables 

2330: $\vec{x}=\tuple{x_1,\ldots,x_n}$ 

2331: associated to the signature $\Sigma=\{a_1,\ldots,a_n\}$.

2332: The operator $\STPo$ is defined on {\em constraint interpretations} consisting 

2333: of sets (disjunctions) of (equivalence classes of) linear constraints.

2334: For brevity, we will define the semantics directly on the interpretations

2335: consisting of the representative elements of the equivalence classes. 

2336: The denotation $\deno{I}$ of a constraint interpretation $I$ extends the one for

2337: constraints as expected:

2338: $\deno{I}=\{\deno{\varphi}\ |\ \varphi\in I\}$.

2339: Interpretations form a complete lattice with respect to

2340: set inclusion.

2341: \begin{definition}[Constraint Interpretation]

2342: We say that $I\subseteq\linc$ is a constraint interpretation. Constraint

2343: interpretations form a complete lattice $\tuple{\calC,\subseteq}$

2344: with respect to set inclusion, where $\calC=\calP(\linc)$.

2345: \end{definition}

2346: %

2347: We obtain then a new notion of satisfiability using operations over constraints as follows.

2348: In the following definitions we assume that the conditions apply only when 

2349: the constraints are {\bf satisfiable} (e.g. $x=0\wedge x\geq 1$ 

2350: has no solutions thus the following rules cannot be applied to this case).

2351: %

2352: \begin{definition}[Satisfiability in \LOonews]

2353: \label{sposat}

2354: Let $I\in\calC$, then $\asat$ is defined as follows: 

2355: $$\begin{array}{l}

2356: \symbvalo{I}{\one}{\varphi}

2357: \ \hbox{where}\ \varphi\ \equiv\  x_1=0\wedge\ldots\wedge x_n=0;\\

2358: [\medskipamount]

2359: \symbvalo{I}{\all,{\Delta}}{\varphi}\ \hbox{where}\ 

2360: \varphi\ \equiv\  x_1\geq 0\wedge \ldots\wedge x_n\geq 0;\\

2361: [\medskipamount]

2362: \symbvalo{I}{\calA}{\varphi}\ \hbox{where}\ 

2363: \varphi\equiv\exists\vec{x}'.(\psi[\vec{x}'/\vec{x}]\wedge \Rem_{\cal A}(\vec{x},\vec{x'})),

2364: \ \psi\in I;\\

2365: [\medskipamount]

2366: \symbvalo{I}{G_1\para G_2,\Delta}{\varphi}\ \hbox{if}\  

2367: \symbvalo{I}{G_1,G_2,\Delta}{\varphi};\\

2368: [\medskipamount]

2369: \symbvalo{I}{G_1\with G_2,\Delta}{\varphi_1\wedge\varphi_2}\ \hbox{if}\ 

2370: \symbvalo{I}{G_1,\Delta}{\varphi_1},\ 

2371: \symbvalo{I}{G_2,\Delta}{\varphi_2}.

2372: \end{array}

2373: $$

2374: \end{definition}

2375: %

2376: The relation $\asat$ satisfies the following properties.

2377: %

2378: \begin{lemma}

2379: \label{abstract_sat_one_properties}

2380: Given $I,J\in\calC$, 

2381: \begin{enumerate}

2382: \item[i)] if $\symbvalo{I}{\Delta}{\varphi}$, then

2383:          $\valo{\deno{I}}{\Delta}{\calA}$ for every $\calA\in\deno{\varphi}$;

2384: \item[ii)] if $\valo{\deno{I}}{\Delta}{\calA}$, then

2385: there exists $\varphi$ such that $\symbvalo{I}{\Delta}{\varphi}$ and

2386: $\calA\in\deno{\varphi}$;

2387: \item[iii)] if $I\subseteq J$ and $\symbvalo{I}{\Delta}{\varphi}$, 

2388: then $\symbvalo{J}{\Delta}{\varphi}$;

2389: \item[iv)]

2390: given a chain of constraint interpretations 

2391: $I_1\subseteq I_2\subseteq\ldots$, 

2392: if $\bigcup_{i=1}^\infty \symbvalo{I_i}{\Delta}{\varphi}$ 

2393: then there exists $k$ s.t. $\symbvalo{I_k}{\Delta}{\varphi}$.

2394: \end{enumerate}

2395: \end{lemma}

2396: %

2397: \begin{proof}

2398: \begin{description}

2399: \item[$i)$]

2400: By induction on $\Delta$.

2401: \begin{itemize}

2402: \item[-] If $I\asato\all,\Delta[\varphi]$, then every $\vec{c}$ (with $c_i\geq 0$)

2403:   is solution of $\varphi$, and $\valo{\deno{I}}{\all,\Delta}{\calA'}$

2404:   for every fact $\calA'$;

2405: \item[-] if $I\asato\one[\varphi]$, then $\tuple{0,\ldots,0}$ is the only

2406:  solution of $\varphi$, and $\valo{\deno{I}}{\one}{\eps}$;

2407: \item[-] if $I\asato\calA[\varphi]$ then

2408:   there exists $\psi\in I$ s.t. $\varphi\equiv\exists \vec{x'}.

2409:   (\psi[\vec{x}'/\vec{x}]\wedge \rho_{\cal A}(\vec{x},\vec{x'}))$

2410:   is satisfiable.

2411:   Then for every solution $\vec{c}$ of $\varphi$ there exists a vector

2412:   $\vec{c'}$ s.t.

2413:   $\psi[\vec{c'}/\vec{x}]$ is satisfiable and

2414:   $c_1'\geq Occ_{\cal A}(a_1),c_1=c_1'-Occ_{\cal A}(a_1),\ldots,

2415:   c_n'\geq Occ_{\cal A}(a_n),c_n=c_n'-Occ_{\cal A}(a_n)$. From this we get

2416:   that for $i=1,\ldots,n$, $c_i'=c_i+Occ_{\cal A}(a_i)$ is a solution for

2417:   $\psi$, therefore $\msc{\vec{c}}+\calA\in\deno{\psi}

2418:   \subseteq\deno{I}$ so that we

2419:   can conclude

2420:   $\valo{\deno{I}}{\calA}{\msc{\vec{c}}}$;

2421: \item[-] if $I\asato G_1\with G_2,\Delta[\varphi]$ then

2422:   $\varphi\equiv\varphi_1\cand\varphi_2$ and

2423:   $I\asato G_1,\Delta[\varphi_1]$, $I\asato G_2,\Delta[\varphi_2]$. By

2424:   inductive hypothesis, $\valo{\deno{I}}{G_1,\Delta}{\msc{\vec{c_1}}}$

2425:   and $\valo{\deno{I}}{G_2,\Delta}{\msc{\vec{c_2}}}$ for every

2426:   $\vec{c_1}$ and $\vec{c_2}$ solutions of $\varphi_1$ and $\varphi_2$,

2427:   respectively. Thus

2428:   $\valo{\deno{I}}{G_1\with G_2,\Delta}{\msc{\vec{c}}}$ for every

2429:   $\vec{c}$ which is solution of both $\varphi_1$ and $\varphi_2$, i.e.

2430:   for every $\vec{c}$ which is solution of $\varphi_1\cand\varphi_2$;

2431: \item[-] the $\para$-case follows by a straightforward

2432:   application of the inductive hypothesis.

2433: \end{itemize}

2434: %

2435: \item[$ii)$]

2436: By induction on $\Delta$.

2437: \begin{itemize}

2438: \item[-] $\valo{\deno{I}}{\all,\Delta}{\msc{\vec{c}}}$ for every $\vec{c}$,

2439:   and $I\asato\all,\Delta[\varphi]$, where

2440:   $\varphi\equiv x_1\geq 0,\ldots,x_n\geq 0$, and every $\vec{c}$ is solution

2441:   of $\varphi$;

2442: \item[-] if $\valo{\deno{I}}{\one}{\eps}$, $\eps=\msc{\tuple{0,\ldots,0}}$,

2443:   then $I\asato\one[\varphi]$, where

2444:   $\varphi\equiv x_1=0,\ldots,x_n=0$, and $\tuple{0,\ldots,0}$ is solution

2445:   of $\varphi$;

2446: \item[-] if $\valo{\deno{I}}{\calA}{\msc{\vec{c}}}$ then

2447:   $\msc{\vec{c}}+\calA\in\deno{I}$, therefore  there exists

2448:   $\psi\in I$ s.t. $\msc{\vec{c}}+\calA\in\deno{\psi}$. Therefore,

2449:   if $\vec{a}$ is such that $\msc{\vec{a}}=\calA$, we have that

2450:   $\psi[\vec{c}+\vec{a}/x]$ is satisfiable, $\vec{c}$ is solution of

2451:   $\varphi\equiv\exists \vec{x'}.

2452:   (\psi[\vec{x}'/\vec{x}]\cand \rho_{\cal A}(\vec{x},\vec{x'}))$

2453:   and $I\asato\calA[\varphi]$;

2454: \item[-] if $\valo{\deno{I}}{G_1\with G_2,\Delta}{\msc{\vec{c}}}$ then

2455:   $\valo{\deno{I}}{G_1,\Delta}{\msc{\vec{c}}}$ and

2456:   $\valo{\deno{I}}{G_2,\Delta}{\msc{\vec{c}}}$. By inductive hypothesis,

2457:   there exist $\varphi_1$ and $\varphi_2$ such that

2458:   $I\asato G_1,\Delta[\varphi_1]$ and $I\asato G_2,\Delta[\varphi_2]$,

2459:   and $\vec{c}$ is a solution of $\varphi_1$ and $\varphi_2$.

2460:   Therefore $I\asato G_1\with G_2,\Delta[\varphi_1\cand\varphi_2]$

2461:   and $\vec{c}$ is a solution of $\varphi_1\cand\varphi_2$;

2462: \item[-] the $\para$-case follows by a straightforward

2463:   application of the inductive hypothesis.

2464: \end{itemize}

2465: %

2466: \item[$iii)$]

2467: By simple induction on $\Delta$.

2468: %

2469: \item[$iv)$]

2470: By induction on $\Delta$.

2471: \begin{itemize}

2472: \item[-] The $\all$ and $\one$-cases follow by definition;

2473: \item[-] if $\bigcup_{i=1}^\infty I_i\asato\calA[\varphi]$,

2474:   then there exists $\psi\in\bigcup_{i=1}^\infty I_i$ s.t.

2475:   $\varphi\equiv\exists \vec{x'}.

2476:   (\psi[\vec{x}'/\vec{x}]\cand \rho_{\cal A}(\vec{x},\vec{x'}))$

2477:   is satisfiable. Then there exists $k$ s.t. $\psi\in I_k$

2478:   and $I_k\asato\calA[\varphi]$;

2479: \item[-] if $\bigcup_{i=1}^\infty I_i\asato G_1\with G_2,\Delta[\varphi]$,

2480:   then $\varphi\equiv\varphi_1\cand\varphi_2$, and, by inductive hypothesis,

2481:   there exist $k_1$ and $k_2$ s.t. $I_{k_1}\asato G_1,\Delta[\varphi_1]$ and

2482:   $I_{k_2}\asato G_2,\Delta[\varphi_2]$. Then, for $k=max\{k_1,k_2\}$, we

2483:   have, by $iii)$,

2484:   $I_{k}\asato G_1,\Delta[\varphi_1]$ and $I_{k}\asato G_2,\Delta[\varphi_2]$,

2485:   therefore $I_{k}\asato G_1\with G_2,\Delta[\varphi_1\cand\varphi_2]$;

2486: \item[-] the $\para$-case follows by a straightforward

2487:   application of the inductive hypothesis.

2488: \end{itemize}

2489: %

2490: \end{description}

2491: \end{proof}

2492: %

2493: We are now ready to define the extended operator $\STPo$.

2494: \begin{definition}[Symbolic Fixpoint Operator $\STPo$]

2495: \label{symbolic_fixpoint_with_one}

2496: Given an \LOone program $P$, and $I\in\calC$,

2497: the operator $\STPo$ is defined as follows:

2498: $$

2499: \begin{array}{lcl}

2500: \STPo(I)=\{ 

2501: \ \varphi & | 

2502: & H\leftlolli G\in P,\ \symbvalo{I}{G}{\psi},\\

2503: & & \varphi\equiv\exists\vec{x'}.(\psi[\vec{x'}/\vec{x}]\wedge \Add_{\ms{H}}(\vec{x},\vec{x'}))		

2504: \}.

2505: \end{array}

2506: $$ 

2507: \end{definition}

2508: %

2509: The new operator satisfies the following property.

2510: \begin{proposition}

2511: \label{constraints_monotonicity}

2512: \label{constraints_continuity}

2513: The  operator $\STPo$ is monotonic and continuous over the lattice

2514: $\tuple{\calC,\subseteq}$.

2515: \end{proposition}

2516: \begin{proof}

2517: {\em Monotonicity}. Immediate from $\STPo$ definition and Lemma

2518: \ref{abstract_sat_one_properties} $iii)$.\\

2519: {\em Continuity}.

2520: Let $I_1\subseteq I_2\subseteq\ldots$, be

2521: an increasing sequence of interpretations. 

2522: We show that 

2523: $\STPo(\bigcup_{i=1}^\infty I_i)\subseteq 

2524: \bigcup_{i=1}^\infty \STPo(I_i)$.

2525: If $\varphi\in \STPo(\bigcup_{i=1}^\infty I_i)$, 

2526: by definition there exists a clause $H\leftlolli G\in P$ s.t. 

2527: $\bigcup_{i=1}^\infty I_i\asato G[\psi]$

2528: and $\varphi\equiv\exists\vec{x'}.(\psi[\vec{x'}/\vec{x}]

2529: \wedge \alpha_{\ms{H}}(\vec{x},\vec{x'}))$ is satisfiable.

2530: By Lemma \ref{abstract_sat_one_properties} $iv)$, there exists

2531: $k$ s.t. $I_k\asato G[\psi]$. 

2532: This implies that $\varphi\in\STPo(I_k)$, i.e., 

2533: $\varphi\in\bigcup_{i=1}^\infty \STPo(I_i)$.

2534: \end{proof}

2535: %

2536: Furthermore, $\STPo$ is a symbolic version of the ground operator $\tpo$,

2537: as stated below.

2538: \begin{proposition}

2539: Let $I\in\calC$, then $\deno{\STPo(I)}=T_P^\one(\deno{I})$.

2540: \end{proposition}

2541: \begin{proof}

2542: Let $\msc{\vec{c}}\in\deno{\STPo(I)}$,

2543: then there exist $\varphi\in\STPo(I)$ and

2544: a clause $H\lollo G\in P$, s.t.

2545: $\vec{c}$ is solution of $\varphi$,

2546: $\varphi\equiv\exists\vec{x'}.

2547: (\psi[\vec{x}'/\vec{x}]\wedge \alpha_{\cal\ms{H}}(\vec{x},\vec{x'}))$ and

2548: $I\asato G[\psi]$.

2549: Then there exists $\vec{c'}$ solution of $\psi$ s.t.

2550: $\msc{\vec{c}}=\msc{\vec{c'}}+\msc{H}$, and, by Lemma

2551: \ref{abstract_sat_one_properties} $i)$, $\valo{\deno{I}}{G}{\msc{\vec{c'}}}$.

2552: Therefore, by definition of $\tpo$,

2553: $\msc{\vec{c}}=\msc{\vec{c'}}+\msc{H}\in\tpo(\deno{I})$.

2554: Vice versa,

2555: let $\msc{\vec{c}}\in\tpo(\deno{I})$,

2556: then there exists $H\lollo G\in P$ s.t. $\valo{\deno{I}}{G}{\calA}$ and 

2557: $\msc{\vec{c}}=\msc{H}+\calA$.

2558: By Lemma \ref{abstract_sat_one_properties} $ii)$, there exists $\psi$ s.t.

2559: $I\asato G[\psi]$ and $\calA\in\deno{\psi}$. Therefore

2560: $\varphi\equiv\exists\vec{x'}.

2561: (\psi[\vec{x'}/\vec{x}]\cand \alpha_{\ms{H}}(\vec{x},\vec{x'}))\in\STPo(I)$,

2562: and $\msc{\vec{c}}=\msc{H}+\calA\in\deno{\varphi}\subseteq\deno{\STPo(I)}$.

2563: \end{proof}

2564: %

2565: \begin{corollary}

2566: \label{fixpoint_equivalenceo}

2567: $\deno{\lfp(\STPo)}=\lfp(\tpo)$.

2568: \end{corollary}

2569: %

2570: Now, let $SymbF_\one(P)=\lfp(\STPo)$, then we have the following main theorem

2571: that shows that $\STPo$ can be used (without termination guarantee) to compute symbolically the 

2572: set of logical consequences of an {\LOone} program. 

2573: \begin{theorem}[Soundness and completeness]

2574: Given an \LOone program $P$,

2575:  $\opo=\fpo$ $=\deno{SymbF_\one(P)}$.

2576: \end{theorem}

2577: \begin{proof}

2578: By Theorem \ref{fixpoint_operationalo} and Corollary

2579: \ref{fixpoint_equivalenceo}.

2580: \end{proof}

2581: 

2582: 

2583: %

2584: \section{Bottom-up Evaluation for \LOonet}

2585: \label{nongroundo_computing}

2586: %

2587: Using a constraint-based representation for \LOone provable multisets,

2588: we have reduced the problem of computing $O_\one(P)$ to the problem 

2589: of computing the reachable states of a system with {\em integer} variables.

2590: As shown by Proposition \ref{undecidable}, the termination of the algorithm 

2591: is not guaranteed a priori. In this respect, Theorem \ref{main_theorem}

2592: gives us sufficient conditions that ensure its termination.

2593: The symbolic fixpoint operator $\STPo$ of Section \ref{nongroundo}

2594: is defined over the lattice $\tuple{\calP(\linc),\subseteq}$, 

2595: with set inclusion being

2596: the partial order relation and set union the least upper bound operator.

2597: When we come to a concrete implementation of $\STPo$, it is worth considering

2598: a weaker ordering relation between interpretations, namely pointwise

2599: {\em subsumption}. Let $\preq$ be the partial order between (equivalence

2600: classes of) constraints given by $\varphi\preq\psi$ if and only if

2601: $\deno{\psi}\subseteq\deno{\varphi}$. Then we say that an interpretation $I$

2602: is subsumed by an interpretation $J$, written $I\sqsubseteq J$, if and only

2603: if for every $\varphi\in I$ there exists $\psi\in J$ such that

2604: $\psi\preq\varphi$.

2605: 

2606: As we do not need to distinguish between

2607: different interpretations representing the

2608: same set of solutions, we can consider interpretations $I$ and $J$ to be

2609: equivalent

2610: in case both $I\sqsubseteq J$ and $J\sqsubseteq I$ hold.

2611: In this way, we get a lattice of interpretations ordered by $\sqsubseteq$

2612: and such that the least upper bound operator is still set union.

2613: This construction is the natural extension of the one of Section

2614: \ref{nonground}. Actually, when we limit ourselves to considering {LO} programs

2615: (i.e., without the constant $\one$) it turns out that we need only consider

2616: constraints of the form $\vec{x}\geq\vec{c}$, which can be abstracted away

2617: by considering the upward closure of $\msc{\vec{c}}$, as we did in Section

2618: \ref{nonground}. The reader can note that the $\preq$ relation defined above

2619: for constraints is an extension of the multiset inclusion relation we used in

2620: Section \ref{nonground}.

2621: 

2622: The construction based on $\sqsubseteq$

2623: can be directly incorporated into the semantic

2624: framework presented in Section \ref{nongroundo}, where,

2625: for the sake of simplicity, we have adopted an approach based on $\subseteq$.

2626: Of course, relation $\subseteq$ is stronger than $\sqsubseteq$, therefore

2627: a computation based on $\sqsubseteq$ is correct and it terminates every time

2628: a computation based on $\subseteq$ does.

2629: However, the converse does not always hold, and

2630: this is why a concrete algorithm for computing the least fixpoint of

2631: $\STPo$ relies on subsumption. Let us see an example.

2632: 

2633: \begin{example}

2634: \label{symbex}

2635: We calculate the fixpoint semantics for the following \LOone program made

2636: up of six clauses:

2637: %

2638: $$\begin{array}{l}

2639:   1.\ \ a\lollo\one\\

2640:   2.\ \ a\para b\lollo\all\\

2641:   3.\ \ c\para c\lollo\all\\

2642:   4.\ \ b\para b\lollo a\\

2643:   5.\ \ a\lollo b\\

2644:   6.\ \ c\lollo a\with b\\

2645: \end{array}$$

2646: %

2647: %

2648: \begin{figure*}

2649: \centering

2650: $$\begin{array}{l}

2651: \begin{array}{lllllll}

2652:   \isp{1} & = & \{ & x_a=1\cand x_b=0\cand x_c=0,             &

2653:                      x_a\geq 1\cand x_b\geq 1\cand x_c\geq 0, \\

2654:           & &      & x_a\geq 0\cand x_b\geq 0\cand x_c\geq 2  & \} 

2655: \end{array}

2656: \\

2657: [\medskipamount]

2658: \begin{array}{lllllll}

2659:   \isp{2} & = & \{ & x_a=1\cand x_b=0\cand x_c=0,             &

2660:                      x_a\geq 1\cand x_b\geq 1\cand x_c\geq 0, \\

2661:           &   &    & x_a\geq 0\cand x_b\geq 0\cand x_c\geq 2, & 

2662:                      x_a=0\cand x_b=2\cand x_c=0,  \\

2663: 	  &   &    & x_a\geq 0\cand x_b\geq 3\cand x_c\geq 0, &

2664:                      x_a\geq 2\cand x_b\geq 0\cand x_c\geq 0  & \} 

2665: \end{array}

2666: \\

2667: [\medskipamount]

2668: \begin{array}{lllllll}

2669:   \isp{3} & = & \{ & x_a=1\cand x_b=0\cand x_c=0,             &

2670:                      x_a\geq 1\cand x_b\geq 1\cand x_c\geq 0, \\

2671:           &   &    & x_a\geq 0\cand x_b\geq 0\cand x_c\geq 2, &  

2672: 	             x_a=0\cand x_b=2\cand x_c=0,             \\

2673:           &   &    & x_a\geq 0\cand x_b\geq 3\cand x_c\geq 0, &

2674:                      x_a\geq 2\cand x_b\geq 0\cand x_c\geq 0, \\

2675:           &   &    & x_a=0\cand x_b=1\cand x_c=1,             &

2676:                      x_a\geq 0\cand x_b\geq 2\cand x_c\geq 1, \\

2677:           &   &    & x_a\geq 1\cand x_b\geq 0\cand x_c\geq 1  & \} 

2678: \end{array}

2679: \end{array}

2680: $$

2681: \caption{Symbolic fixpoint computation for the program in Example \ref{symbex}}

2682: \label{symbexample}

2683: \end{figure*} 

2684: %

2685: %

2686: Let $\Sigma=\{a,b,c\}$ and consider constraints over the variables

2687: $\vec{x}=\tuple{x_a,x_b,x_c}$.

2688: We have that

2689: $\isp{0}=\eset\asat\one[x_a=0\cand x_b=0\cand x_c=0]$, therefore,

2690: by the first clause, $\varphi\in\isp{1}$, where

2691: $\varphi=\exists\vec{x'}.(x'_a=0\cand x'_b=0\cand x'_c=0\cand x_a=x'_a+1\cand

2692:  x_b=x'_b\cand x_c=x'_c)$, which is equivalent to

2693: $x_a=1\cand x_b=0\cand x_c=0$. From now on, we leave to the reader the details

2694: concerning equivalence of constraints.

2695: By reasoning in a similar way, using clauses 2. and 3. we calculate $\isp{1}$

2696: (see Figure \ref{symbexample}).

2697: 

2698: We now compute $\isp{2}$.

2699: By 4., as $\isp{1}\asat a[x_a=0\cand x_b=0\cand x_c=0]$, we get

2700: $x_a=0\cand x_b=2\cand x_c=0$, and,

2701: similarly, we get $x_a\geq 0\cand x_b\geq 3\cand x_c\geq 0$.

2702: By 5., we have $x_a\geq 2\cand x_b\geq 0\cand x_c\geq 0$,

2703: while clause 6. is not (yet) applicable. Therefore, modulo redundant

2704: constraints (i.e., constraints {\em subsumed} by the already calculated ones)

2705: the value of $\isp{2}$ is given in Figure \ref{symbexample}.

2706: 

2707: Now, we can compute $\isp{3}$.

2708: By 4. and $x_a\geq 2\cand x_b\geq 0\cand x_c\geq 0\in\isp{2}$ we get

2709: $x_a\geq 1\cand x_b\geq 2\cand x_c\geq 0$, which is subsumed by

2710: $x_a\geq 1\cand x_b\geq 1\cand x_c\geq 0$. By 5. and

2711: $x_a=0\cand x_b=2\cand x_c=0$, we get

2712: $x_a=1\cand x_b=1\cand x_c=0$, subsumed by

2713: $x_a\geq 1\cand x_b\geq 1\cand x_c\geq 0$. Similarly, by 5. and

2714: $x_a\geq 0\cand x_b\geq 3\cand x_c\geq 0$ we get redundant information.

2715: By 6., from

2716: $x_a\geq 1\cand x_b\geq 1\cand x_c\geq 0$ and

2717: $x_a=0\cand x_b=2\cand x_c=0$ we get

2718: $x_a=0\cand x_b=1\cand x_c=1$, from

2719: $x_a\geq 1\cand x_b\geq 1\cand x_c\geq 0$ and

2720: $x_a\geq 0\cand x_b\geq 3\cand x_c\geq 0$ we get

2721: $x_a\geq 0\cand x_b\geq 2\cand x_c\geq 1$, and finally from

2722: $x_a\geq 2\cand x_b\geq 0\cand x_c\geq 0$ and

2723: $x_a\geq 1\cand x_b\geq 1\cand x_c\geq 0$ we have

2724: $x_a\geq 1\cand x_b\geq 0\cand x_c\geq 1$.

2725: The reader can verify that no additional provable multisets can be obtained.

2726: It is somewhat tedious, but in no

2727: way difficult, to verify that clause 6. yields only redundant information

2728: when applied to every possible couple of constraints in $\isp{3}$.

2729: We have then

2730: $\isp{4}=\isp{3}=SymbF_\one(P)$, so that in this particular case we achieve

2731: termination. We can reformulate the operational semantics of $P$ using the

2732: more suggestive multiset notation (we recall that

2733: $\den{\calA}=\{\calB\ |\ \calA\preq\calB\}$, where $\preq$ is multiset

2734: inclusion):

2735: $$\begin{array}{c}

2736: \fpo=\{\{a\},\{b,b\},\{b,c\}\}\ \cup

2737: \den{\{a,b\},\{c,c\},\{b,b,b\},\{a,a\},\{b,b,c\},\{a,c\}}.

2738: \end{array}$$

2739: \end{example}

2740: 

2741: It is often not the case that the symbolic computation of \LOone

2742: program semantics can be carried out in a finite number of steps. 

2743: Nevertheless,

2744: it is important to remark that viewing the bottom-up evaluation of

2745: \LOone programs

2746: as a least fixpoint computation over infinite-state {\em integer} systems

2747: allows us to apply techniques and tools developed in {\em infinite-state}

2748: model checking 

2749: (see e.g. \cite{ACJT96,BGP97,DP99,FS01,HHW97}) and program analysis \cite{CH78}

2750: to compute approximations of the least fixpoint of $\STPo$.

2751: 

2752: In the next section we will

2753: present an interesting application of the semantical framework we have

2754: presented so far. Namely, we shall make a detailed comparison between LO

2755: and Disjunctive Logic Programming. This will help us in clarifying the

2756: relations and the relative strength of the languages. After recalling the basic

2757: definitions of DLP in Section \ref{dlplo}, we will present our view of

2758: DLP as an abstraction of LO in Section \ref{comparison}. Finally,

2759: in Section \ref{petri} we will

2760: give a few hints on how to employ this framework to

2761: study reachability problems in Petri Nets.

2762: %

2763: %

2764: \section{An Application of the Semantics: Relation with DLP}

2765: \label{dlplo}

2766: %

2767: As anticipated in the introduction, the paradigms of linear logic programming 

2768: and Disjunctive Logic Programming have in common the use of {\em multi-headed} clauses.

2769: However, the operational interpretation of the extended notion of clause 

2770: is quite different in the two paradigms.

2771: In fact, as shown in \cite{BDM00b}, from a proof-theoretical perspective it is

2772: possible to view LO as a {\em sub-structural} fragment of DLP in which the

2773:  rule of {\em contraction} is forbidden on the right-hand side of sequents. 

2774: 

2775: While proof theory allows one to compare the {\em top-down}

2776: semantics of the two languages, abstract interpretation \cite{CC77} can be

2777: used to relate the fixpoint, bottom-up evaluation of programs. 

2778: In the following we will focus on the latter approach, exploiting our semantics of LO 

2779: and the bottom-up semantics of DLP given in \cite{MRL91}.

2780: For the sake of clarity, we will use superscripts in order to distinguish between 

2781: the fixpoint operators for LO and DLP, which will be

2782: denoted by $\lotp$ and $\dtp$, respectively. 

2783: First of all, we recall some definitions concerning Disjunctive Logic

2784: Programming.

2785: 

2786: A {\em disjunctive logic program} as defined in \cite{MRL91} is a 

2787: finite set of clauses  

2788: %

2789: $$A_1\clor\ldots\clor A_n\cimp B_1\cand\ldots\cand B_m,$$ 

2790: %

2791: where $n\geq 1$, $m\geq 0$, and $A_i$ and $B_i$ are atomic formulas.

2792: A {\em disjunctive goal} is of the form $\cimp C_1,\ldots,C_n$, where 

2793: $C_i$ is a {\em positive clause} (i.e., a disjunction of atomic formulas) 

2794: for $i:1,\ldots,n$.

2795: To make the language symmetric, in this paper we will consider 

2796: extended clauses of the form

2797: $$A_1\clor\ldots\clor A_n\cimp C_1\cand\ldots\cand C_m$$ 

2798: containing positive clauses in the body.

2799: Following \cite{MRL91},

2800: we will identify positive clauses with sets of atoms.

2801: In order to define the operational and denotational semantics of DLP, 

2802: we need the following notions.

2803: %

2804: \begin{definition}[Disjunctive Herbrand Base]

2805: The {\em disjunctive Herbrand base} of a program $P$, for short $\dhbp$, 

2806: is the set of 

2807: all positive clauses formed by an arbitrary number of atoms. 

2808: \end{definition}

2809: %

2810: \begin{definition}[Disjunctive Interpretation]

2811: A subset $I$ of the disjunctive Her\-brand base $\dhbp$ 

2812: is called a disjunctive Herbrand interpretation. 

2813: \end{definition}

2814: %

2815: \begin{definition} [Ground SLO-derivation]\label{slo-derivation}

2816: Let $P$ be a DLP program. An SLO-derivation of a ground goal $G$ from $P$ 

2817: consists of a sequence of goals $G_0=G,G_1,\ldots$ such that for 

2818: all $i\geq 0$, $G_{i+1}$ is obtained

2819: from $G_i=\leftarrow (C_1,\ldots,C_m,\ldots,C_k)$ as follows:

2820: \begin{itemize}

2821: \item[-] $C\cimp D_1\cand\ldots\cand D_q$ is a ground instance of a clause in $P$ such that

2822: $C$ is contained in $C_m$ (the selected clause);

2823: \item[-]  $G_{i+1}$ is the goal

2824:  $\leftarrow (C_1,\ldots,C_{m-1},D_1\clor C_m,\ldots,D_q\clor C_m,C_{m+1},\ldots,C_k)$.

2825: \end{itemize}

2826: \end{definition}

2827: %

2828: \begin{definition} [SLO-refutation]

2829: Let $P$ be a DLP program. An SLO-refutation of a ground goal $G$ from $P$ 

2830: is an SLO-derivation $G_0,G_1,\ldots,G_k$ s.t. $G_k$ consists of the empty clause only.

2831: \end{definition}

2832: %

2833: As SLD-resolution for Horn programs, SLO-resolution gives us a procedural interpretation 

2834: of DLP programs.

2835: The operational semantics is defined then as follows:

2836: $$\dosp=\{ C \ |\ C\in\dhbp,\ \leftarrow C\ \mbox{has\ an\ SLO-refutation}\}.$$

2837: As for Horn programs, it is possible to define a fixpoint semantics via the following operator (where $\gnd(P)$ denotes the set of ground instances of clauses

2838: in $P$).

2839: %

2840: \begin{definition} [The $\dtp$ Operator]

2841: Given a DLP program $P$ and $I\subseteq \dhbp$,

2842: $$\begin{array}{lll}

2843: \dtp(I) & = & \{\ C\in \dhbp\ |\ C'\cimp D_1,\ldots,D_n\in\gnd(P),\\

2844:         &   & \ \ D_i\clor C_i\in I,\ i:1,\ldots,n\ \\

2845:         &    & \ \ C=C'\clor C_1\clor\ldots\clor C_n\ \}.\\

2846: \end{array}$$

2847: \end{definition}

2848: %

2849: The operator $\dtp$ is monotonic and continuous on the lattice of 

2850: interpretations ordered w.r.t. set inclusion.

2851: Based on this property, the fixpoint semantics is defined as

2852: $\dfs=\lfp(\dtp)=\dtp\!\!\uparrow_\omega$. 

2853: As shown in \cite{MRL91},  

2854: for all $C\in\dosp$ there exists $C'\in\dfs$ s.t. $C'$ implies $C$. 

2855: Note that for two ground clauses $C$ and $C'$, 

2856: $C$ implies $C'$ if and only if $C\subseteq C'$.

2857: This suggests that interpretations can also be ordered w.r.t. subset inclusion 

2858: for their elements, i.e., $I\sqsubseteq J$ if and only if for all $A\in I$ 

2859: there exists $B\in J$ such that $B\subseteq A$ ($B$ implies $A$).

2860: In the rest of the paper we will consider this latter ordering. 

2861: %

2862: \begin{example}

2863: Consider the disjunctive program $P=\{r(a),\ p(X)\vee q(X)\leftarrow r(X)\}$

2864: and the auxiliary predicate $t$. 

2865: Then, $\dhbp=\{r(a),p(a),q(a),t(a),p(a)\vee r(a),p(a)\vee q(a),p(a)\vee q(a)\vee r(a),\ldots\}$.

2866: Furthermore, the goal  

2867: $G_0=\leftarrow (p(a)\vee q(a)\vee t(a))$ has the refutation

2868: $G_0,G_1=\leftarrow  (p(a)\vee q(a)\vee t(a)\vee r(a)),G_2$

2869: where

2870: $G_2$ consists of the empty clause only.

2871: The fixpoint semantics of $P$ is as follows $\dfs=\{r(a),\ p(a)\vee q(a)\}$.

2872: Note that $p(a)\vee q(a)\vee t(a)$ is implied by  $p(a)\vee q(a)$.

2873: \end{example}

2874: %

2875: We note that the definition of the $\dtp$ operator can be re-formulated in

2876: such a way that its input and output domains contain multisets instead of sets

2877: of atoms (i.e., we can consider interpretations which are sets of multisets of

2878: atoms). In fact, we can always map a multiset to its {\em underlying set},

2879: i.e., the set containing the elements with multiplicity greater than zero,

2880: and, vice versa, a set can be viewed as a multiset in which each element has

2881: multiplicity equal to one.

2882: In the following we will assume that $\dtp$ is

2883: defined on domains containing multisets. As the fixpoint operator for LO

2884: is defined on the same kind of domains, this will

2885: make the comparison between the two operators easier.

2886: Furthermore, without loss of generality, we will make the assumption that in

2887: clauses like 

2888: $A_1\clor\ldots\clor A_n\cimp C_1\cand\ldots\cand C_m$,

2889: the $A_i$'s are all {\em distinct}

2890: and each $C_j$ consist of {\em distinct} atoms.

2891: This will simplify the embedding of DLP clauses into linear logic. 

2892: The previous definitions can be easily adapted.

2893: 

2894: Now, we give a closer look at the formal presentations of DLP and LO.

2895: As said in the Introduction, we only need to consider a fragment of LO in

2896: which connectives can not be arbitrarily nested in goals, like in DLP.

2897: This fragment can be described by the following grammar:

2898: 

2899: $$

2900: \begin{array}{l}

2901: \formula{H}\ ::=\ \formula{A}_1\para\ \ldots\para\ \formula{A}_n\\

2902: [\medskipamount]

2903: \formula{D}\ ::=\ \formula{H}\ \leftlolli\ \formula{G}\ \ |\ \ \formula{D}\ \with\ \formula{D}\\

2904: [\medskipamount]

2905: \formula{G}\ ::=\ \formula{H}_1\with\ \ldots\with\ \formula{H}_n\ \ \ |\ \ \ \all

2906: \end{array}

2907: $$

2908: 

2909: where $\formula{A}_i$ is an atomic formula.

2910: The comparison between the two languages is based on the idea that, to some

2911: extent, linear connectives, i.e., additive conjunction $\with$ and

2912: multiplicative disjunction $\para$, should behave like classical conjunction

2913: $\cand$ and classical disjunction $\clor$. Actually, classical connectives

2914: give rise to a fixpoint semantics for DLP which is a proper abstraction of

2915: the semantics for LO. The translation between linear and classical connectives

2916: is given via the following mapping $\trad{\cdot}$:

2917: %

2918: $$

2919: \trad{F\clor G}=\trad{F}\para\trad{G},\

2920: \trad{F\cand G}=\trad{F}\with\trad{G},\

2921: \trad{F\cimp G}=\trad{F}\lollo\trad{G},\

2922: \trad{\true}=\all.

2923: $$

2924: %

2925: In order to make the comparison between DLP and LO more direct,

2926: it is possible to present DLP by means of the following grammar:

2927: $$

2928: \begin{array}{l}

2929: \formula{H}\ ::=\ \formula{A}_1\clor\ \ldots\clor\ \formula{A}_n\\

2930: [\medskipamount]

2931: \formula{D}\ ::=\ \formula{H}\ \cimp\ \formula{G}\ \ |\ \ \formula{D}\ \cand\ \formula{D}\\

2932: [\medskipamount]

2933: \formula{G}\ ::=\ \formula{H}_1\cand\ \ldots\cand\ \formula{H}_n\ \ \ |\ \ \ \true

2934: \end{array}

2935: $$

2936: where $\formula{A}_i$ is an atomic formula.

2937: A DLP program $P$ is now a $\formula{D}$-clause, whereas DLP goals

2938: are represented (modulo `$\leftarrow$') as $\formula{G}$-formulas.

2939: Here, we have introduced an explicit constant $\true$ for $true$ and we

2940: have written {\em unit clauses} (i.e., with empty body) with the syntax

2941: $ A_1\clor\ldots\clor A_n\cimp\true$. With these conventions, the grammars

2942: for LO and DLP given above are exactly the same modulo the translation

2943: $\trad{\cdot}$.

2944: The definitions concerning the operational and fixpoint semantics for DLP

2945: given previously can be adapted in a straightforward manner. 

2946: The reader can also note that by definition of DLP program, the image of

2947: $\trad{\cdot}$ returns a class of LO programs 

2948: where both the head and the disjuncts in the body have no repeated occurrences

2949: of the same atom.

2950: 

2951: We conclude this section by specializing our fixpoint semantics for LO,

2952: given in Section \ref{nonground}, to the simpler fragment presented above.

2953: We give the following definition for the $\lotp$ operator:

2954: %

2955: \begin{definition}[$\lotp$ operator]

2956: Given an LO program $P$ and an interpretation $I$,

2957: the operator $\lotp$ is defined as follows:

2958: {\small $$\begin{array}{lll}

2959:   \lotp(I) & = & \{\ms{H}+({\cal C}_1\bullet\ldots\bullet

2960:   {\cal C}_n)\ |\ H\leftlolli D_1\with\ldots\with D_n\in P,

2961:   \ \forall i=1,\ldots,n,\ \ms{D_i}+{\cal C}_i\in I\}\\

2962:   & & \ \ \ \ \ \smallunion\ \ \ \ \ \{\ms{H}\ |\ H\lollo\all\in P\}

2963: \end{array}$$}

2964: \end{definition}

2965: %

2966: The operator $\lotp$ is monotonic and continuous over the lattice of Herbrand 

2967: interpretations (ordered w.r.t. $\sqsubseteq$).

2968: Thus, the fixpoint semantics of an LO-program $P$ is defined

2969: as 

2970: $$\lofs=\bigsqcup_{i=0}^\omega \lotp\!\!\uparrow_i.$$

2971: A completeness result similar to that of Section \ref{nonground},

2972: stating the equivalence between the operational and fixpoint semantics,

2973: obviously holds for the fragment of LO considered here.

2974: 

2975: 

2976: \section{DLP as Abstraction of LO}

2977: \label{comparison}

2978: %

2979: The fixpoint semantics of LO allows us to investigate in more depth 

2980: the relationships between LO and DLP.

2981: For this purpose, we can employ the mathematical tools provided 

2982: by {\em abstract interpretation} \cite{CC77}, and in particular the notion 

2983: of {\em completeness} \cite{CC77,GR97b} that qualifies the precision of an abstraction.

2984: Informally, the comparison between LO and DLP fixpoint semantics is based

2985: on the abstraction that maps multisets into sets 

2986: of atomic formulas (positive clauses). 

2987: This abstraction induces a Galois connection between the semantic domains 

2988: of DLP and LO. 

2989: We prove that the fixpoint semantics of the

2990: translation of 

2991: an LO program in DLP is a correct abstraction of the fixpoint semantics of the

2992: original LO program.

2993: Furthermore, we show that this abstraction is not {\em fully complete}

2994: with respect to LO semantics.

2995: In a {\em fully complete} abstraction the result of interleaving 

2996: the application of the abstract fixpoint operator with the abstraction

2997: $\alpha$

2998: coincides with the abstraction of the concrete fixpoint operator. 

2999: For a {\em complete} abstraction, a similar relation holds for fixpoints, i.e., the fixpoint

3000: of the abstract operator coincides with the abstraction of the fixpoint of the

3001: concrete one.

3002: We isolate an interesting class of LO programs 

3003: for which we show that the property of completeness holds. In particular,

3004: completeness holds if we forbid conjunctions in the body of

3005: clauses. The resulting class of LO programs

3006: is still very interesting, as it can be used to encode Petri Nets.

3007: 

3008: {\em Abstract Interpretation} \cite{CC77,CC79} is a classical framework for

3009: semantics approximation which is used for the construction of semantics-based

3010: program analysis algorithms. Given a semantics and an abstraction of the

3011: language constructors and standard data, abstract interpretation determines an

3012: abstract representation of the language which is, by construction, sound with

3013: respect to the standard semantics. This new representation enables the

3014: calculation of the abstract semantics in finite time, although it implies

3015: some loss of precision. We recall here some key concepts in abstract

3016: interpretation, which the reader can find in \cite{CC77, CC79, GR97b}.

3017: 

3018: Given a concrete semantics $\tuple{C,T_P}$, specified by a

3019: {\em concrete domain} (complete lattice) $C$

3020: and a (monotone) fixpoint operator $T_P:C\rightarrow C$, the abstract

3021: semantics can be specified by an {\em abstract domain} $A$ and an abstract

3022: fixpoint operator $\TPA$. In this context, program semantics is given by

3023: $\lfp(T_P)$, and its abstraction is $\lfp(\TPA)$. The concrete and abstract

3024: semantics $S=\tuple{C,T_P}$ and $S^\#=\tuple{A,\TPA}$ are related by a Galois

3025: connection $\tuple{\alpha,C,A,\gamma}$, where $\alpha:C\rightarrow A$ and

3026: $\gamma:A\rightarrow C$ are called {\em abstraction} and {\em concretization}

3027: functions, respectively.

3028: $S^\#$ is called a {\em sound} abstraction of $S$ if for all $P$,

3029: $\alpha(\lfp(T_P))\leq_A \lfp(\TPA)$. This condition is implied by the

3030: strongest property of {\em full soundness}, which requires that

3031: $\alpha\compos T_P\leq_A\TPA\compos\alpha$. The notions of {\em completeness}

3032: and {\em full completeness} are dual with respect to those of soundness.

3033: Namely, $S^\#$ is a (fully) {\em complete} abstraction of $S$ if for all $P$,

3034: ($\TPA\compos\alpha\leq_A\alpha\compos T_P$)

3035: $\lfp(\TPA)\leq_A\alpha(\lfp(T_P))$. Often, the notion of completeness is

3036: assumed to include soundness (i.e., we impose '=' in the previous

3037: equations).

3038: It is well-known \cite{CC79} that the abstract domain $A$ induces a {\em best}

3039: correct approximation of $T_P$, which is given by

3040: $\alpha\compos T_P\compos\gamma$, and that it is possible to define a (fully)

3041: complete abstract operator $\TPA$ if and only if the best correct

3042: approximation is (fully) complete. It can be proved that for a fixed

3043: concrete semantics, (full) completeness of an abstract interpretation only

3044: depends on the choice of the abstract domain.

3045: The problem of achieving a (fully) complete abstract interpretation starting

3046: from a correct one, by either refining or simplifying the abstract domain,

3047: is studied in \cite{GR97b}.

3048: We conclude by observing that an equivalent presentation of abstract

3049: interpretation is based on {\em closure operators} \cite{CC79}, i.e.

3050: functions from a concrete domain $C$ to itself which are {\em monotone},

3051: {\em idempotent} and {\em extensive}. This approach provides

3052: independence from specific representations of abstract domain's objects

3053: (the abstract domain is given by the image, i.e., the set of fixpoints, of

3054: the closure operator).

3055: 

3056: We are now in the position of  connecting the LO (concrete) semantics 

3057: with the DLP (abstract) semantics.

3058: We define the abstract interpretation as a closure operator on the 

3059: lattice $\calI$, the domain of LO interpretations of Definition \ref{interpretation_lattice}. 

3060: In fact, as mentioned before, we can consider disjunctive interpretations as a subclass of $\calI$ 

3061: (i.e., all sets in $\calI$).

3062: We recall  that in $\calI$ the ordering of interpretations is defined as

3063: follows: 

3064: $I\sqsubseteq J$ iff for all $B\in I$ there exists $A\in J$ such that $A$ is a sub-multiset 

3065: of $B$ (i.e., for disjunctive interpretations, $A\subseteq B$).

3066: We give the following definitions.

3067: %

3068: \begin{definition} [Abstract Interpretation from LO to DLP]

3069: The abstract interpretation is defined by the closure operator

3070: $\alpha:\calI\rightarrow\calI$ such that

3071: for every $I\in\calI$, $\alpha(I)=\{\alpha(\cal A)\ |\ \cal A\in I\}$, where

3072: for a given multiset $\cal A$, $\alpha(\cal A)$ is the multiset such that

3073: for every $i=1,\ldots,n$, $Occ_{\alpha(\cal A)}(a_i)=0$ if

3074: $Occ_{\cal A}(a_i)=0$, $Occ_{\alpha(\cal A)}(a_i)=1$ otherwise (i.e., we

3075: abstract a multiset with the corresponding set).

3076: \end{definition}

3077: %

3078: \begin{definition}[Abstract semantics]

3079: The abstract fixpoint semantics is given by $\lfp(\tpa)$, where the abstract

3080: fixpoint operator $\tpa$ is defined as $(\alpha\compos\lotp)$.

3081: \end{definition}

3082: %

3083: According to \cite{CC79}, $\alpha\compos\lotp$ is the best correct

3084: approximation of the concrete fixpoint operator $\lotp$, for the fixed

3085: abstraction $\alpha$. The abstraction $\alpha$, as said before, transforms

3086: multisets into sets by forgetting multiple occurrences of atoms. 

3087: It is not difficult to convince ourselves that $\tpa$ is indeed the $\dtp$

3088: operator for disjunctive logic programs, provided that, as discussed

3089: in Section \ref{dlplo}, we consider $\dtp$ defined over domains

3090: containing multisets instead of sets (actually, we are identifying $\dtp$

3091: input domain with the abstract domain which is given by the set of

3092: fixpoints, i.e., the image, of the closure operator $\alpha$).

3093: The operations $\bullet$ ({\em least upper bound} of multisets) and $+$

3094: (multiset union) used in the definition of $\lotp$ are interchangeable

3095: (because of the subsequent application of the operator $\alpha$)

3096: and correspond to set (multiset) union in the definition of $\dtp$.

3097: We have the following results.

3098: %

3099: \begin{proposition}[DLP is an abstraction of LO]

3100: For every  DLP program $P$ and {\em disjunctive} (hence LO) interpretation $I$,

3101: $\dtp(I)=\tpatr(I)$. 

3102: \end{proposition}

3103: \begin{proof}

3104: By definitions.

3105: \end{proof}

3106: %

3107: \begin{proposition}[DLP is a correct abstraction of LO]

3108: For every LO program $P$,

3109: the abstract semantics is a fully sound abstraction of the concrete semantics,

3110: that is, for every interpretation $I$,

3111: $\alpha(\lotp(I))\sqsubseteq\tpa(\alpha(I)).$

3112: \end{proposition}

3113: \begin{proof}

3114: As $\tpa=\alpha\compos\lotp$ and $I\sqsubseteq\alpha(I)$, the proposition follows

3115: by monotonicity of $\tpa$.

3116: \end{proof}

3117: %

3118: The previous result implies {\em soundness}, i.e.

3119: $\alpha(\lfp(\lotp))\sqsubseteq \lfp(\tpa)$.

3120: %

3121: The strong property of {\em full completeness} does not hold for the

3122: abstraction. To see why, take as a counterexample the single clause

3123: $a\leftlolli b$ and the interpretation 

3124: $I$ with the single multiset $\{b,b\}$.

3125: Then, $\alpha(\lotp(I))=\{\{a,b\}\}$, $\tpa(\alpha(I))=\{\{a\}\}$,

3126: and $\tpa(\alpha(I))\not\sqsubseteq \alpha(\lotp(I))$.

3127: 

3128: We conclude this section showing that the abstraction is complete

3129: for the subclass of LO programs whose clauses contain 

3130: {\em at most} one conjunct in the body. We will address some applications

3131: of this result in Section \ref{petri}.

3132: 

3133: (Note: the abstraction not being fully complete has a counterpart in 

3134: the fact that in general $h>1$ in the following lemma, i.e., 

3135: more than one step of $\lotp$ is necessary to simulate one step of $\tpa)$.)

3136: %

3137: \begin{lemma}

3138: \label{complemma}

3139: Let $P$ be an LO  program in which every clause has at most one conjunct in the

3140: body (i.e., conjunction is forbidden), and $I,J$ two interpretations.

3141: If $I\sqsubseteq\alpha(J)$ then there exists a natural number $h$ such

3142: that $\alpha(\lotp(I))\sqsubseteq\alpha(\lotpo{h}(J))$.

3143: \end{lemma}

3144: \begin{proof}

3145: Suppose $I\sqsubseteq\alpha(J)$ and $\calA\in\alpha(\lotp(I))$. Then

3146: there exists $\calA'\in\lotp(I)$ s.t. $\calA=\alpha(\calA')$.

3147: By definition of $\lotp$, there exists a clause $H\lollo D\in P$ (the case for

3148: unit clauses is trivial)

3149: s.t. $\ms{D}+\calC\in I$ and $\calA'=\ms{H}+\calC$. As

3150: $I\sqsubseteq\alpha(J)$, we also have $\ms{D}+\calC\in\alpha(J)$,

3151: which implies that there exists $\calK\in J$ s.t.

3152: $\ms{D}+\calC=\alpha(\calK)$. Let

3153: $p=min\{n\ |\ \calK\preccurlyeq(\ms{D}+\calC)^n\}$ (it is immediate to prove

3154: that such a $p$ exists), and let $\calM=(\ms{D}+\calC)^p$.

3155: We have that $\calK\preccurlyeq\calM$, therefore $\calM\in J$ (because

3156: $\calK\in J$ and $J$ is upward-closed).

3157: Now, $\calM=\ms{D}+(\calC+(\ms{D}+\calC)^{p-1})\in J$, and,

3158: by definition of $\lotp$ ($H\lollo D\in P$),

3159: $\ms{H}+\calC+(\ms{D}+\calC)^{p-1}\in\lotp(J)$. By repeatedly applying $\lotp$

3160: (the proof is by induction on $p$) we get

3161: $(\ms{H}+\calC)^p\in\lotpo{p}(J)$. Therefore

3162: $\calA=\alpha(\ms{H}+\calC)=\alpha((\ms{H}+\calC)^p)\in\alpha(\lotpo{p}(J))$.

3163: \end{proof}

3164: %

3165: \begin{proposition}

3166: Let $P$ be an LO  program in which every clause has at most one conjunct in the

3167: body. Then $\alpha(\lfp(\lotp))=\lfp(\tpa)$.

3168: \end{proposition}

3169: \begin{proof}

3170: By a simple induction, using Lemma \ref{complemma}, we have that for every $k$

3171: there exists $h$ s.t.

3172: $\tpao{k}\sqsubseteq\alpha(\lotpo{h})$. Therefore

3173: $\lfp(\tpa)\sqsubseteq\alpha(\lfp(\lotp))$.

3174: \end{proof}

3175: %

3176: The class of LO programs with one conjunct in the body is still very

3177: interesting. Below, we show how this result could be exploited to study

3178: reachability problems in Petri Nets.

3179: %

3180: \section{Other Applications: Relation with Petri Nets}

3181: \label{petri}

3182: %

3183: As shown in the proof of Proposition \ref{undecidable}, the class of propositional 

3184: LO programs with one conjunct in the body is equivalent to VAS, i.e., to Petri Nets. 

3185: Intuitively, a multiset rewriting rule can be used to describe the effect of firing 

3186: a Petri Net transition.

3187: For instance, the clause $a~\para~b~\para~b~\lollo~c~\para~c$

3188: can be interpreted as the Petri Net transition that removes one token from 

3189: place $a$, two tokens from place $b$, and adds two tokens to place $c$.  

3190: As a consequence, a (possibly infinite) execution (sequence of goals $G_0,G_1,\ldots$) 

3191: of a restricted LO program denotes an execution of the corresponding Petri Net. 

3192: The initial goal $G_0$ can be viewed as the initial marking of the Petri Net.

3193: Consider now the fact $F~\equiv~c\leftlolli\all$, and let $G_0$ be the goal $a\para a\para b$.

3194: Then, the sequent $P\cup F\Rightarrow G_0$ is provable in LO

3195: if and only if there exists a reachable marking having {\em at least} 

3196: one token in place $c$.

3197: In other words, the fact $F$ can be used to implicitly represent an infinite set of 

3198: markings (its upward closure) of the corresponding Petri Net. 

3199: Our bottom-up semantics can be use to effectively compute the set $Pre^*(F)$ 

3200: (using the terminology of \cite{ACJT96}) of markings that can reach a marking in 

3201: the denotation of $F$.

3202: 

3203: This idea can be used to verify {\em safety properties} of concurrent systems.

3204: A safety property $S$ can be viewed as a set of {\em good} states (markings) of a given concurrent 

3205: system (Petri Net).

3206: The system satisfies the property if the set of states that are reachable from the initial 

3207: state $G_0$ are all contained in $S$.

3208: Symmetrically, the set $\neg S$ represents the set of {\em bad} states. 

3209: Thus, the systems can  be proved correct by showing that $Pre^*(\neg S)$ does not contain 

3210: the initial state $G_0$, i.e., by applying the bottom-up algorithm starting from 

3211: a fact denoting $\neg S$.

3212: It is interesting to note that in many real examples $\neg S$ is indeed an upward closed set 

3213: of states (e.g.  the set of states where there are 

3214: {\em at least two processes in the critical section} are the the typical bad states of 

3215: a mutual exclusion algorithm).

3216: In general, the complexity of computing $Pre^*(F)$, for some $F$, can be very high.

3217: However, the results of Section \ref{comparison} show that the fixpoint semantics of DLP can 

3218: be used to approximate the set $Pre^*(F)$.

3219: Completeness implies that all properties that are preserved by the abstraction 

3220: can be checked equivalently over the concrete and the abstract domain.

3221: In our setting the kind of properties that satisfy this requirement can be informally 

3222: characterized as `at least one'-properties (e.g. {\em  is there at least one token in 

3223: place P in a reachable marking?}).

3224: This kind of properties can be used to check `mutual exclusion' for a concurrent system 

3225: represented via a Petri Net.

3226: Suppose we want to prove that a system ensures mutual exclusion 

3227: for two processes represented via a Petri Net. Process $p_i$ is in the critical section 

3228: whenever a token is in a special place $cs_i$ for $i:1,2$. 

3229: Violations of mutual exclusion are expressed as the set of states with {\em at least} one token in place 

3230: $cs_1$ and one token in state $cs_2$.

3231: Thus, the fixpoint semantics of the DLP program obtained as translation 

3232: of the Petri Net (LO program) union the fact $cs_1\vee cs_2$ is an abstraction 

3233: of the set of backward reachable states. 

3234: We obtain a full-test for mutual exclusion properties, whenever the initial states 

3235: can be expressed again as {\em at least one} properties (i.e., whenever membership of the 

3236: initial states in the set of abstract reachable states can be determined exactly).

3237: %

3238: \section{Related Works}

3239: \label{related}

3240: %

3241: Our work is inspired to the general decidability results for infinite-state systems

3242: based on the theory of well-quasi orderings given in \cite{ACJT96,FS01}. 

3243: In fact, the construction of the least fixpoint of $\STP$ and $\STPo$ can be viewed 

3244: as an instance of the {\em backward reachability} algorithm for transition systems 

3245: presented in \cite{ACJT96}.

3246: Differently from \cite{ACJT96,FS01},  we need to add special rules 

3247: (via the satisfiability relation $\asat$) to handle formulas with the connectives 

3248: $\with$, $\all$ and $\one$. 

3249: 

3250: Other sources of inspiration come from linear logic programming.

3251: In \cite{HW98}, the authors present an abstract deductive system

3252: for the bottom-up evaluation of linear logic programs. 

3253: The {\em left introduction} rules plus {\em weakening} and {\em cut} are used to compute 

3254: the logical consequences of a given formula.

3255: The satisfiability relations we use in the definition of the fixpoint 

3256: operators correspond to top-down steps within their bottom-up evaluation 

3257: scheme.

3258: The framework is given for a more general fragment than {LO}. 

3259: However, they do not provide an {\em effective} 

3260: fixpoint operator as we did in the case of {LO} and \LOonews, and

3261: they do not discuss computability issues for the resulting 

3262: derivability relation.  

3263: 

3264: In \cite{APC97}, Andreoli, Pareschi and Castagnetti present a partial 

3265: evaluation scheme for propositional {LO} (i.e without $\one$).

3266: Given an initial goal $G$, they use a construction similar to Karp and Miller's

3267: {\em coverability tree} \cite{KM69} for Petri Nets to build a finite representation 

3268: of a proof tree for $G$. 

3269: During the {\em top-down} construction of the graph for $G$,

3270: they apply in fact a {\em generalization step} that works as follows.

3271: If a goal, say $\calB$, that has to be proved is subsumed by a node already visited, 

3272: say $\calA$, (i.e., $\calB=\calA+\calA'$), then the part of proof tree between the two 

3273: goals is replaced by a proof tree for $\calA+(\calA')^*$;

3274: $\calA+(\calA')^*$ is a finite representation of the union of $\calA$ with 

3275: the closure of $\calA'$.

3276: They use Dickson's Lemma to show that the construction always terminates.

3277: In the case of {LO}, the main difference with our approach is that we give 

3278: a goal independent {\em bottom-up} algorithm.

3279: Technically, another difference is that in our fixpoint semantics we do not 

3280: need any {\em generalization} step. In fact, in our setting the 

3281: computation starts directly from (a representation of) {\em upward-closed} sets of contexts. 

3282: This simplifies the computation as shown in Example \ref{example} 

3283: (we only need to test $\preccurlyeq$).

3284: Finally,  differently from \cite{APC97}, in this paper we have given also a formal 

3285: semantics for the extension of {LO} with the constant $\one$.

3286: 

3287: The partial evaluation scheme of \cite{APC97} is aimed at com\-pile-time

3288: optimizations of abstractions of {\em LinLog} programs.

3289: Another example of analysis of concurrent languages based on linear logic 

3290: is given in \cite{KNY95}, where the authors present a type inference

3291: procedure that returns an approximation of the number of messages 

3292: exchanged by HACL processes.

3293: 

3294: In \cite{Cer95} Cervesato shows how to encode Petri Nets in {LO}, 

3295: Lolli and Forum by exploiting the different features of these languages.  

3296: We used some of these ideas to prove Proposition \ref{undecidable}.

3297: 

3298: Finally, we have discussed the similarities between our semantics and

3299: the bottom-up semantics for 

3300: Disjunctive Logic Programming of Minker, Rajasekar and Lobo \cite{MRL91}.

3301: In a disjunctive logic program, the head of a clause is a disjunction

3302: of atomic

3303: formulas, whereas the body is a conjunction of atomic formulas.

3304: In the semantics of \cite{MRL91} interpretations are collections of

3305: {\em sets} (disjunctions)

3306: of atomic formulas. Only minimal (w.r.t. set inclusion) sets are kept at each

3307: fixpoint iteration.

3308: In contrast, in our setting we need to consider collections of {\em multisets}

3309: of formulas.

3310: Therefore, in the propositional case in order to prove the 

3311: convergence of the fixpoint iteration, we need an argument (Dickson's lemma) 

3312: stronger than the finiteness of the {\em extended} Herbrand base of

3313: \cite{MRL91} (collection of all minimal sets).

3314: %

3315: \section{Conclusions and Future Work}

3316: \label{conclusions}

3317: %

3318: In this paper we have defined a bottom-up semantics for the fragment 

3319: of LinLog \cite{And92} consisting of  the language {LO} \cite{AP91a} 

3320: enriched with the constant $\one$.

3321: In the propositional case, we have shown that without $\one$ 

3322: the fixpoint semantics is finitely computable. 

3323: Our fixpoint operator is defined over constraints and gives us an effective 

3324: way to evaluate bottom-up (abstractions of) linear logic programs. 

3325: To conclude, let us discuss the directions of research that we find more promising.

3326: \smallskip\\

3327: {\em Linear Logic Programming.}

3328: It would be interesting to extend the techniques we presented in this paper 

3329: to larger fragments of linear logic. 

3330: In particular, it would be interesting to define a  bottom-up evaluation 

3331: for languages like Lolli \cite{HM94} and

3332: Lygon \cite{HP94}, and to study techniques for first-order 

3333: formulation for all these languages.

3334: An extension of the present framework to the first-order case should also

3335: take into account the so-called {\em S-semantics}

3336:  \cite{FLMP93,BGLM94}, in order to model

3337: observables like {\em computed answer substitutions} and to cope with issues

3338: like {\em compositional} semantics. Concerning LO, we would also like to

3339: look at the connection with the so-called Chemical Abstract Machine

3340: metaphor \cite{ALPT93}.

3341: \smallskip\\

3342: {\em Verification.}

3343: In \cite{DP99}, the authors show that properties of

3344: concurrent systems expressed in {\em temporal logic} can be defined in terms 

3345: of fixpoint semantics of a logic program  that encodes the transition system 

3346: of a concurrent  system.

3347: In \cite{DP99}, synchronization between processes is achieved via 

3348: {\em shared variables}, whereas in linear logic synchronization can be expressed 

3349: via multiple headed clauses. 

3350: Thus, our semantics might be a first step towards the extension of 

3351: the metaphor of \cite{DP99} to concurrent systems in which  synchronization 

3352: is expressed at the logical level (see Section \ref{petri}).

3353: The other way round, through the connection between semantics and verification,

3354: techniques  used for infinite-state systems with integer variables 

3355: (see e.g. \cite{DP99,BGP97,HHW97}) can be re-used in order to  compute a 

3356: static analysis of linear logic programs.

3357: \smallskip\\

3358: {\em Proof Theory.}

3359: The connection we establish in this paper indicates a potential connection

3360: between the general decidability results for infinite-state systems of \cite{ACJT96,FS01} 

3361: and provability in {\em sub-structural} logics like {LO} and {\em affine} linear logic

3362: \cite{Kop95}.

3363: Viewing the provability relation as a transition relation, it might be possible to find

3364: a notion of {\em well-structured} proof system (paraphrasing the notion of 

3365: {\em well-structured} transition systems of \cite{ACJT96,FS01}), i.e., 

3366: a general notion of provability that ensures the termination of the bottom-up

3367: generation of valid formulas.

3368: \smallskip\\

3369: {\em Relations between DLP and LO.}

3370: We hope that our study will give rise to new ideas for the analysis of

3371: LO programs.

3372: As an example, it could be interesting to study weak notions

3373: of negation for LO that are based on the  negation of DLP.

3374: Moreover, we can use DLP operational and fixpoint semantics to analyze

3375: Petri Nets,

3376: given that the abstraction is complete in this case.

3377: Finally, there are still some open questions concerning the relation 

3378: between DLP and LO in the setting of abstract interpretation.

3379: In particular, we would like to study the notion of completeness for the

3380: general class of LO programs (we remark that the example in \cite{BDM00b}

3381: showing incompleteness was wrong). We would also like to analyze in more detail

3382: the connection between the notion of (full) completeness of the

3383: abstraction and proof-theoretic properties of provability in

3384: sub-structural logics, which has been only partly addressed in

3385: \cite{BDM00b}.

3386: 

3387: \section*{Acknowledgments}

3388: The authors would like to thank Maurizio Gabbrielli for his support, 

3389: Jean-Marc Andreoli for useful comments on the use of LO, 

3390: and the anonymous reviewers for  providing us suggestions and references

3391: that helped us to improve the presentation of the paper.

3392: 

3393: \bibliographystyle{tlp}

3394: \bibliography{biblio}

3395: 

3396: \end{document}

3397: