1: %% TLP2esam.tex / sample pages for TLP

2: %% release v2.00, 25-sept-2001

3: %% from Y2028 K02364 FPR

4: 

5: \documentclass{tlp}

6: \usepackage{aopmath}

7: \usepackage{epsf}

8: 

9: \newcommand{\Godel}{G\"{o}del}

10: \newcommand{\Staerk}{St\"{a}rk}

11: 

12: \newcommand{\And}{ \& } %jha change 5 Mar 90

13: \newcommand{\Or}{\vee}

14: \newcommand{\Not}{\neg}

15: \newcommand{\Implies}{\supset}

16: \newcommand{\Arrow}{\rightarrow}

17: 

18: \newcommand{\Lg}{\langle}

19: \newcommand{\Rg}{\rangle}

20: 

21: \newcommand{\Iff}{\leftrightarrow}

22: 

23: \newtheorem{defn}[theorem]{Definition}

24: \newtheorem{notation}[theorem]{Notation}

25: \newtheorem{thm}[theorem]{Theorem}

26: \newtheorem{cor}[theorem]{Corollary}

27: \newtheorem{prop}[theorem]{Proposition}

28: 

29: \newcommand{\Proof}{{\bf Proof}}

30: \newcommand{\QED}{$\Box$}

31: 

32: %

33: 

34: \newcommand{\Lang}{{\cal L}}

35: \newcommand{\Dom}{{\cal D}}

36: \newcommand{\Seq}{{\cal S}}

37: \newcommand{\Sseq}{{\cal S}}

38: \newcommand{\Prog}{{\cal P}}

39: \newcommand{\G}[2]{{\ \stackrel{{\rm #1}}{\Rightarrow_{#2}}\ }}

40: \newcommand{\Gstar}[2]{{\ \stackrel{{\rm #1} *}{\Rightarrow_{#2} ~}\ }}

41: \newcommand{\Sep}{\hspace*{5mm}}

42: \newcommand{\Indent}{\hspace*{5mm}}

43: \newcommand{\Arrows}{\leftrightarrow}

44: 

45: \newsavebox{\colondashbox}

46: \savebox{\colondashbox}{{\tt \ :-\ }}

47: \newcommand{\colondash}{\usebox{\colondashbox}}

48: 

49: \newcommand{\Corners}[1]{\lceil #1 \rceil}

50: 

51: \newcommand{\Rw}[1]{\rhd_{#1}}

52: \newcommand{\dfnf}{{\it dfnf}}

53: \newcommand{\Ae}{\"{a}}

54: 

55: \newenvironment{recdef}%

56: {\begin{list}{$\bullet$}{%

57: \setlength{\topsep}{0.5mm}%

58: \setlength{\itemsep}{0pt}%

59: \setlength{\parsep}{0.5mm}}%

60: }%

61: {\end{list}}

62: 

63: 

64: \newcommand{\Goes}[1]{~\Rightarrow_{#1}~}

65: \newcommand{\Goeslib}{~\stackrel{lb}{\Rightarrow}~}

66: \newcommand{\Goesms}{~\stackrel{ms}{\Rightarrow}~}

67: \newcommand{\Goeswm}{~\stackrel{wm}{\Rightarrow}~}

68: \newcommand{\Goespess}{~\stackrel{ps}{\Rightarrow}~}

69: 

70: % Rule definition command stuff

71: \newlength{\capwidth}

72: \setlength{\capwidth}{2cm}              % You can modify this

73: \newlength{\restwidth}

74: \setlength{\restwidth}{\textwidth}

75: \addtolength{\restwidth}{-\capwidth}

76: \newcommand{\Cap}[1]{\makebox[\capwidth][l]{#1}}

77: \newcommand{\Rule}[4]{{\samepage%

78: \Cap{#1}%

79: \parbox{\restwidth}{\[\frac{#2}{#3}\]}%

80: \\ \Cap{~}\parbox{\restwidth}{#4}}}

81: 

82: 

83: 

84: \sloppy

85: 

86: \begin{document}

87: \bibliographystyle{tlp}

88: 

89: \title{The Witness Properties and the Semantics of the Prolog Cut}

90: \author[James H.\ Andrews]

91: {JAMES H.\ ANDREWS\\

92: Department of Computer Science,

93: University of Western Ontario \\

94: London, Ontario, Canada N6A 5B7}

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

96: \volume{\textbf{10} (3):}

97: \jdate{March 2000}

98: \setcounter{page}{1}

99: \pubyear{2000}

100: 

101: %\maketitle[L]

102: \maketitle

103: \label{firstpage}

104: 

105: \begin{abstract}

106: The semantics of the Prolog ``cut'' construct is explored in the

107: context of some desirable properties of logic programming

108: systems, referred to as the witness properties.  The witness

109: properties concern the operational consistency of responses to

110: queries.  A generalization of Prolog with negation as failure

111: and cut is described, and shown not to have the witness properties.

112: A restriction of the system is then described, which preserves

113: the choice and first-solution behaviour of cut but allows the

114: system to have the witness properties.

115: 

116: The notion of cut in the restricted system is more restricted

117: than the Prolog hard cut, but retains the useful first-solution

118: behaviour of hard cut, not retained by other proposed cuts such

119: as the ``soft cut''.  It is argued that the restricted system

120: achieves a good compromise between the power and utility of the

121: Prolog cut and the need for internal consistency in logic

122: programming systems.  The restricted system is given an abstract

123: semantics, which depends on the witness properties; this

124: semantics suggests that the restricted system has a deeper

125: connection to logic than simply permitting some computations

126: which are logical.

127: 

128: Parts of this paper appeared previously in a different form in

129: the Proceedings of the 1995 International Logic Programming

130: Symposium \cite{andrews-cut-ilps95}.

131: \end{abstract}

132: 

133: \section{Introduction}

134: 

135: Since the first widely-used Prolog implementations of the

136: early 1980s, Prolog programmers have had access to some

137: powerful constructs for controlling the backtracking behaviour

138: of their programs.  The best-known of these is the

139: ``cut'', written ``!'', which appears as a literal in the

140: sequence of literals in a clause body.

141: Cut allows programmers to direct

142: the flow of control in a program by cutting away backtrack

143: points which lead to unwanted execution paths.

144: 

145: Programmers have embraced cut enthusiastically.  Most large

146: Prolog programs now in use contain cuts, or related constructs

147: such as the if-then-else construct ($A$ \verb/->/ $B$ \verb/;/ $C$).

148: Cut is used mainly for choosing between clauses.  However,

149: it has other important uses, such as for obtaining the first

150: solution to a subgoal and discarding others.

151: 

152: Unfortunately, the unrestricted use of cuts produces a program

153: which has no direct logical interpretation.

154: A cut does not even have an effect

155: restricted to the clause in which it

156: appears; rather, it may affect all the clauses of the predicate

157: which its clause is defining.  It is therefore difficult to give

158: a semantics to a program which uses cut, other than an operational

159: semantics.

160: 

161: It seems therefore that the use of cut, and the constructs

162: related to it, must be restricted in order to regain a logical

163: interpretation for Prolog programs.  Various approaches to this

164: have been proposed, including the ``soft cut'' and the mode and

165: determinism restrictions of the Mercury system

166: \cite{mercury-jlp}.  However, neither soft cut nor Mercury allow

167: the behaviour of cut which allows us to choose the first

168: solution to a subgoal and discard other solutions.  This is a

169: fundamental property often used by Prolog programmers, so it

170: would be preferable to preserve it.

171: 

172: Like most logic programming researchers, we believe that

173: Prolog's ``hard cut'' cannot be salvaged from a logical point of

174: view.  However, we do not believe it is necessary to retreat all

175: the way to soft cut.

176: In this paper, we show how the hard cut of Prolog can be

177: restricted to produce a cut, referred to as ``firm cut'', which

178: has important advantages over both soft and hard cut.  Firm cut

179: allows useful behaviours such as first-solution which are

180: disallowed by soft cut.  Modulo a 

181: run-time or compile-time mode restriction, firm cut is

182: operationally identical to the more widely-used hard cut, which

183: soft cut is not.

184: However, firm cut disallows the most non-logical and anti-intuitive

185: behaviours of hard cut, and while (like hard cut) it has no

186: purely logical interpretation, it still satisfies

187: some important consistency properties which hard cut does not.

188: 

189: We refer to the consistency properties which firm cut satisfies

190: as the ``witness properties''.  Because it satisfies these

191: properties, firm cut and the systems incorporating it can be

192: given abstract semantics based on compositional valuation functions

193: (functions from goals to truth values).

194: We demonstrate this by giving such an

195: abstract semantics for the system with firm cut.

196: 

197: Along the way, we also introduce a form of formula, the {\it if}

198: formula, which allows a Prolog program with cuts to be given a

199: ``completed form'' analogous to the Clark completion of a

200: definite clause program.  This form of program may have

201: applications even when dealing with other forms of cut.

202: 

203: \subsection{The Witness Properties}

204: 

205: One of the central properties we like to prove about logic

206: programming systems is the equivalence between the operational

207: and logical semantics.  The well-known equivalence of

208: SLD-resolution and the least model semantics is the most obvious

209: example.  Such properties show that the logic programming

210: system in question achieves some standard of expected behaviour.

211: 

212: But what if the logic programming system has no logical semantics?

213: Is there any standard to which such a system can be held, any

214: middle ground between a system with a full logical semantics and

215: a system indistinguishable from imperative or functional

216: programming systems?

217: We believe that there is, and suggest the {\it witness

218: properties} as a possible standard.

219: 

220: The witness properties are as follows:

221: \begin{enumerate}

222: \item (Success property) If a goal formula $G$ succeeds

223:   (returns an answer substitution), then some ground

224:   instance of $G$ succeeds.

225: \item (Failure property) If a goal formula $G$ fails

226:   (terminates without returning an answer substitution),

227:   then all ground instances of $G$ fail.

228: \end{enumerate}

229: The witness properties accord with our intuitions about the

230: internal consistency of logic programming systems, and about

231: the nature of formulas and the search for satisfying substitutions

232: for them.  They therefore provide a possible standard to which

233: to hold logic programming systems.

234: Their name comes from the notion of witness for

235: an existentially-quantified formula:  the formula $\exists x~G$

236: is true if there is a witness term $t$ such that $G[x:=t]$

237: is true, and false otherwise.  A goal formula such as $p(x)$

238: can be read as asking whether $\exists x~p(x)$ is true.

239: 

240: In the success property, we insist on {\it ground} instances in

241: particular, partly because otherwise it would always be

242: vacuously true: $G$ is an instance of $G$, so if $G$ succeeds,

243: some instance of it succeeds.  We express the failure property

244: in terms of ground terms as well for symmetry.  Another

245: reason for using ground terms in the statement of the properties

246: is that it allows the success and failure of goals with free

247: variables to be characterized in terms of the simpler notion of

248: success and failure of ground goals.  Many variants

249: of these properties are possible and may be valuable for

250: different applications.

251: 

252: Note that the converses of the witness properties are not

253: necessarily enjoyed by logic programming systems.

254: The converse of the success property (if an instance of $G$

255: succeeds, then $G$ succeeds) is not enjoyed by any

256: deterministic definite clause resolution system (like Prolog)

257: using a search rule which selects clauses in order, as the

258: following example shows:

259: \begin{tabbing}

260: \Indent{} \= \kill

261: \>  $p(0) \colondash p(0).$ \\

262: \>  $p(1).$

263: \end{tabbing}

264: The goal $p(y)$ diverges even though its instance $p(1)$

265: succeeds.  The converse of the failure property (if all ground

266: instances of $G$ fail, then $G$ fails) is not enjoyed by

267: any deterministic definite clause resolution system, regardless

268: of search or selection

269: rule, as the following example (based on that of Clark, Andreka

270: and Nemeti) shows:

271: \begin{tabbing}

272: \Indent{} \= \kill

273: \>  $p(f(x)) \colondash p(x).$

274: \end{tabbing}

275: The goal $p(y)$ diverges even though every ground instance

276: of it fails.

277: 

278: The witness properties also have theoretical significance.

279: Generally, we may consider a logic programming system

280: to be unsatisfying from a logical point of view if it can be

281: given only operational semantics, as this leads us to suspect

282: that the operational model is a ``hack'' which is only logical

283: in the sense that it permits some computations which can be

284: viewed as logical.

285: Of course, every operational semantics for an LP language can be

286: converted to a denotational semantics if operational notions

287: such as unification and substitution sequence are suitably

288: ``reified'' (i.e., represented explicitly by mathematical

289: constructs).  However, these semantics should not necessarily

290: boost our confidence that the operational model is logical, any

291: more than the operational semantics did.

292: The existence of semantics which do not reify operational

293: notions suggests that we are dealing with a system which has a

294: deeper connection to logic than simply permitting logical

295: computations.  Evidence from past research and the present paper

296: indicates that the witness properties lead to such semantics.

297: 

298: 

299: \subsection{This Paper}

300: 

301: In this paper, we show how the hard cut of Prolog, as restricted

302: to ``firm cut'', retains the witness properties and can be given

303: an abstract, non-reifying semantics.  We believe that the

304: resulting system is the best compromise yet found between the

305: power and utility of the Prolog cut and the need for internal

306: consistency in logic programming systems.

307: 

308: In section 2, we review background and related work in more

309: detail.  In section 3, we present the notation and syntax we

310: will use for logic

311: programs with cut and a new construct, {\it if}.  In section 4,

312: we present a first operational semantics for the extended

313: programs.  This operational semantics corresponds to Prolog,

314: with its permissive, non-logical view of negation and cut; thus

315: it is referred to as the ``liberal''

316: semantics.  In section 4, we also show that the {\it if}

317: construct allows us to derive a convenient ``completed form''

318: for every program, in which each predicate is defined by exactly

319: one clause.

320: 

321: In section 5, we restrict the liberal operational semantics, and

322: show that the restricted system has the witness properties.

323: The new, restricted system is referred to as the ``conservative'' semantics,

324: and firm cut is defined as the cut associated with it.  In section 6, we

325: define a non-reifying abstract semantics for the system with

326: firm cut, using the witness properties to prove soundness and

327: completeness of the conservative semantics.  Finally, in Section

328: 7 we give some conclusions and suggestions for further research.

329: 

330: 

331: 

332: \section{Background and Related Work}

333: 

334: In this section, we introduce the background of this research

335: and the other research related to it.  We have grouped this

336: material into three sections: one concerning the cut and other

337: choice constructs like the if-then-else, one concerning the

338: semantics of depth-first Prolog and cut, and one concerning the

339: various different notions of termination of a logic program.

340: 

341: \subsection{Cut and Other Choice Constructs}

342: 

343: Cut was introduced in the DECsystem-10/20 Prolog of 1982,

344: written by David Warren, Fernando Pereira, Lawrence Byrd and

345: Luis Pereira.  It was recognized even at the time as a

346: ``meta-theoretic'' control construct, which could at best be

347: read as making meta-level manipulations of the search tree.  Cut

348: was taken into the C-Prolog interpreter \cite{c-prolog}, which

349: became a very widely distributed early version of the language.

350: 

351: Cut operates by cutting away previously-encountered

352: alternatives.  Consider the following program:

353: \begin{tabbing}

354: \Indent{} \= \Indent{} \= \kill

355: \>  $p(a, y).$ \\

356: \>  $p(b, y) \colondash q(y), !, r(y).$ \\

357: \>  $p(x, y).$\vspace{2mm} \\

358: \>  $q(c).$ \\

359: \>  $q(d).$\vspace{2mm} \\

360: \>  $r(d).$ \\

361: \end{tabbing} \vspace{-1ex}

362: ($x$ and $y$ are variables, and $a$-$e$ are constants.)  With

363: respect to this program, calls to the predicate $p$ exhibit the

364: following behaviour.

365: \begin{itemize}

366: \item Goals of the form $p(a, t)$ succeed for any term $t$.

367: \item Goals of the form $p(b, t)$ succeed only if $t$ is $d$, or

368:   if $t$ is not unifiable with either $c$ or $d$; otherwise

369:   they fail.  For instance:

370:   \begin{itemize}

371:   \item The goal $p(b,y)$ fails, because $y$ is unified with $c$

372:     by the first clause for $q$, the last clauses for $p$ and

373:     $q$ are cut away, and $r(c)$ fails.

374:   \item The goal $p(b,d)$ succeeds because $q(d)$ succeeds, only

375:     the last clause for $p$ is cut away, and $r(d)$ succeeds.

376:   \item The goal $p(b,b)$ succeeds because $q(b)$ fails entirely,

377:     and so the third clause for $p$ is used.

378:   \end{itemize}

379: \item Finally, goals of the form $p(s,t)$, where $s$ is anything

380:   other than $a$ and $b$, succeed.

381: \end{itemize}

382: 

383: Cut therefore cuts away not only the later clauses of the same

384: predicate, but also the alternative clauses for subgoals that

385: appear earlier in the clause.  The former behaviour allows us to

386: select clauses, but the latter behaviour allows us to choose the

387: first solution to a subgoal (by stating the subgoal and

388: following it by a cut).  This may be used for various reasons:  to

389: discard solutions that we, the programmers, know to be equivalent

390: to the first; to prevent backtracking because we know there will

391: be no more successes; or simply to select the first solution

392: because we know that is the one we are interested in

393: (for instance, ``$prime(x), x > 100, !$'' for the first prime

394: greater than $100$).

395: 

396: We can see immediately that Prolog with the form of cut

397: described above does not have the failure witness property,

398: since $p(b,y)$ fails but $p(b,d)$ succeeds.  (Examples can be

399: constructed violating the success witness property as well.)

400: The most common way to fix this problem with cut is to allow backtracking

401: into the portion before the cut -- that is, to cut away later

402: clauses to the current clause but not alternative clauses to

403: subgoals before the cut.  This is generally referred to as the

404: ``soft cut'', and the more usual cut is referred to as the

405: ``hard cut'' in order to distinguish it.

406: With soft cut, we can regain a logical interpretation:

407: if ! in the above program is interpreted

408: as soft cut, then the second and third clauses are equivalent to

409: the classical formulas

410: \begin{tabbing}

411: \Indent{} \= \Indent{} \= \kill

412: \>  $p(b, y) \leftarrow q(y) \And r(y).$ \\

413: \>  $p(x, y) \leftarrow (\Not(x=b) \Or (x=b \And \Not q(y))).$

414: \end{tabbing}

415: However, we lose the ability to select the first solution with soft cut.

416: 

417: A construct related to cut is the ``if-then-else'' construct,

418: usually written $(G_1$ \verb/->/ $G_2 ; G_3)$ and read ``if $G_1$ then $G_2$

419: else $G_3$''.  This construct is often syntactic sugar for a

420: hard-cut-like operation; that is, the evaluation of

421: $(G_1$ \verb/->/ $G_2 ; G_3)$ is equivalent to the evaluation of a goal

422: $p(x_1, \ldots, x_n)$ against the program

423: \begin{tabbing}

424: \Indent{} \= \kill

425: \>  $p(x_1, \ldots, x_n) \colondash G_1, !, G_2$ \\

426: \>  $p(x_1, \ldots, x_n) \colondash G_3$ \\

427: \end{tabbing} \vspace{-1ex}

428: where $x_1, \ldots, x_n$ are the free variables in $G_1, G_2, G_3$.

429: 

430: The cut in the if-then-else construct is hard cut in most Prologs.

431: The choice construct of the Mercury language \cite{mercury-jlp}

432: is written in this way and uses soft cut; Mercury has no other

433: choice construct.

434: 

435: \subsection{Semantics of Prolog and Cut}

436: 

437: The least-model semantics \cite{vanE-kow} is traditionally

438: viewed as the standard one for pure logic programming as it was

439: originally conceived.  However, the depth-first search of Prolog

440: and similar systems makes it difficult to fit them into the

441: least-model framework, at least if we want a semantics with

442: respect to which the system is sound and complete.  Evidently

443: some other form of semantics is needed to characterize

444: depth-first logic programming systems precisely, whether taking

445: cut into consideration or not.

446: 

447: The {\it operational} semantics of Prolog with cut was not

448: formally defined in a self-contained system

449: until Billaud's 1990 paper \cite{billaud-cut-tcs}.  In

450: Billaud's semantics, when a predicate is called, the current

451: backtrack stack is stored; the

452: execution of a cut corresponds to discarding the current

453: backtrack stack and replacing it with

454: the one stored by the current predicate.

455: 

456: Various authors have given {\it denotational} semantics for

457: Prolog with cut

458: \cite{prolog-continuation,boerger-opsem,baudinet-jlp},

459: including Billaud in his original paper \cite{billaud-cut-tcs}.

460: Some of these approaches have proven equivalence with an

461: operational semantics.

462: These papers were based on earlier work in operational and

463: denotational semantics of Prolog, including

464: \cite{jones-mycroft,deransart-std-inria,denotationalization,%

465: debray-denotational,nicholson-foo}.

466: 

467: The denotational approaches essentially view a Prolog program as

468: a function from goals to sequences of answer substitutions, and

469: ``reify'' notions like unification and answer substitution

470: sequence by giving abstract mathematical constructs

471: corresponding to them.  Such approaches are able to handle any

472: operational model which transforms a goal into a sequence of

473: substitutions using unification.  This includes models with any

474: conceivable sound or unsound strategy for negation and cut; for

475: instance, sound soft cut, unsound negation as failure, or a

476: negation operator which judges $\Not p(t)$ to be true iff $t$

477: unifies with 42.  Therefore, although a reifying semantics may

478: be very useful for some purposes (for instance, to use as a

479: guide for implementation of a standard computational model), the

480: existence of such a semantics does not by itself suggest that

481: the system thus characterized is any more than an operational

482: superset (or superset of a subset) of pure logic programming.

483: 

484: In contrast, what may be called the ``non-reifying'' semantic

485: tradition

486: \cite{andrews-phd-dd,andrews-lnaf-tcs,staerk-lptp-jlp,elbl-jlp-1999}

487: gives characterizations of the success and failure of Prolog

488: goals not involving reified answer substitutions and

489: unification.  Andrews' earliest characterizations

490: \cite{andrews-phd-dd} took account only of depth-first Prolog

491: without builtins, negation or cut.  Andrews

492: \cite{andrews-lnaf-tcs} and \Staerk{} \cite{staerk-lptp-jlp}

493: then extended this to systems with negation as failure, Andrews

494: by characterizing floundering and \Staerk{} by imposing a mode

495: restriction.  More recently, Elbl \cite{elbl-jlp-1999} has given

496: a semantics for depth-first logic programming which uses more

497: abstract denotations to achieve compositionality, and extends

498: this semantics to take account of negation with a similar mode

499: restriction to \Staerk{}'s.

500: 

501: These more logical approaches draw their power from

502: expressing the semantics of Prolog in a manner which allows

503: them to avoid encoding operational notions such as unification

504: into the semantics.  Without such a property, proofs using

505: \Staerk's proof assistant \cite{staerk-lptp-jlp}, for instance,

506: would have to reason about unification at almost every step.

507: 

508: We should note that even reifying semantics can act as the basis

509: of powerful theorem provers if they are automated.  For example,

510: Lindenstrauss, Sagiv and Serebrenik

511: \cite{lindenstrauss-auto-term-iclp97,lindenstrauss-termilog-cav97}

512: discuss automatic proofs of strong termination based on

513: term rewriting techniques.  However, in proving termination and

514: (especially) correctness properties, it is often necessary to

515: have human intervention, in order to deduce generalizations to

516: be proven by induction or norms for proving termination.

517: 

518: 

519: \subsection{Termination}

520: 

521: We seek an abstract semantics with respect to which some large

522: subset of Prolog with cut is sound {\it and complete}.  The

523: soundness property allows us to argue that any outcome which a

524: Prolog goal does return is consistent with the semantics.  The

525: completeness property, however, allows us to argue that the

526: semantics does not judge a goal to be true (resp.\ false)

527: unless it actually succeeds (resp.\ fails) according to the

528: operational semantics; that is, that we have

529: precisely captured {\it termination} of goals.  We must

530: therefore define exactly what we mean by termination of a goal.

531: In this paper, we study {\it left-to-right} termination, which

532: subsumes the more widely-studied notion of {\it strong} termination.

533: 

534: A Prolog query can have one of several outcomes.

535: It can succeed or fail, or it can diverge (fail to

536: terminate altogether).  If a query succeeds, Prolog typically

537: gives us the option of finding more solutions.  If we keep asking

538: for more solutions, there are three things that may happen:

539: the query may eventually

540: fail back to the top level and report

541: no more solutions; the query may return a finite number of

542: solutions and then diverge; or the query may return

543: an infinite number of solutions.

544: We may label these outcomes as:

545: \begin{enumerate}

546: \item Success:

547:   \begin{enumerate}

548:   \item Finite number of solutions, then failure.

549:   \item Finite number of solutions, then divergence.

550:   \item Infinite number of solutions.

551:   \end{enumerate}

552: \item Failure.

553: \item Divergence.

554: \end{enumerate}

555: 

556: These outcomes correspond to the shape of the resolution

557: search tree for systems with a left-to-right subgoal selection

558: rule, and the placement of solutions within that tree.  (In the

559: following, we assume that the leftmost subgoal is always selected,

560: that the children of each node of the search tree

561: correspond, left to right, to the sequence of clauses defining

562: the selected subgoal's predicate, and that the search rule is

563: also left-to-right.)  If the

564: tree is finite, we get outcome 1(a) or 2.  If it has some infinite

565: path, and there is a finite number of solutions to the left

566: of the leftmost infinite path, we get outcome 1(b) or 3. 

567: Otherwise, there is an infinite number of solutions to the left

568: of the leftmost infinite path (outcome 1(c)), and we can obtain

569: only a finite prefix of the sequence of solutions by

570: backtracking.

571: 

572: The two kinds of termination most often mentioned in the

573: literature are {\it existential termination} and {\it universal

574: termination}.  A query existentially terminates either if it

575: fails, or if there is a solution somewhere in the search tree.

576: Knowing that a query existentially terminates is thus useful

577: primarily if we are studying breadth-first implementations or

578: nondeterministic operational semantics.

579: A query universally terminates if the search tree is finite (i.e.,

580: a search on any path terminates).  Universal termination

581: therefore corresponds only to cases 1(a) and 2 above.

582: 

583: Most of the work on proving termination of Prolog programs (e.g.,

584: \cite{pluemer-lncs,apt-strong-info-comp,bezem-strong-jlp,apt-marchiori,staerk-lptp-jlp}%

585: ) has

586: concentrated on universal termination.  Because of our interest

587: in features of practical logic programming systems such as

588: Prolog, in this paper we continue to study

589: what we refer to as {\it depth-first termination}.  A query

590: depth-first terminates if it returns at least one solution, or

591: if it fails.  Depth-first termination thus encompasses outcomes

592: 1(a)-(c) and 2 above, and thus identifies a larger set of

593: queries as terminating than universal termination.  It also

594: corresponds to one of a Prolog user's intuitive notions of termination

595: of a goal.

596: 

597: Depth-first termination is what we will have to characterize if

598: we want to take account of the behaviour of cut.  Cut cuts

599: away all but the first solution returned from the portion of the

600: clause before the cut, so all that is important to the semantics

601: is that the portion before the cut returns at least one solution

602: or fails.  Note, however, that even in the absence of cut, a

603: goal formula $G$ universally terminates iff the query

604: $(G \And false)$ (in Prolog parlance, {\tt (G, fail)})

605: depth-first terminates.  Depth-first termination is thus

606: strictly more general than universal termination.

607: 

608: 

609: 

610: \section{Notation and Syntax of Extended Programs}

611: 

612: \newcommand{\Bar}{~~|~~}

613: 

614: In this section, we define the syntax of programs that we will

615: use for the rest of the paper.  It is a generalization of the

616: subset of Prolog including cut (!), negation as failure, and

617: defined predicates.  It does not include problematic built-in

618: predicates such as \verb/assert/ and \verb/retract/, \verb/var/,

619: \verb/nonvar/, and \verb/setof/, each of which merits further

620: study but whose inclusion might confuse the issues we study here.

621: 

622: We use the following meta-variables:

623: $B$, $C$, $F$, $G$ and $H$ for formulas,

624: $s$ and $t$ for terms, and

625: $x$, $y$ and $z$ for variables,

626: all possibly primed or subscripted.

627: We use $\vec{x}$, $\vec{t}$, etc.\ generally to stand for

628: sequences of variables, terms, etc.

629: We use $\exists \vec{x}$ as notation to stand for

630: $\exists x_1 \ldots \exists x_n$, where

631: $\vec{x} = (x_1, \ldots, x_n)$.

632: 

633: We define an extended notion of {\it goal formula} (or simply

634: {\it formula}), representing a query or an element of a clause body.

635: The BNF definition of a formula is as follows.\vspace{2mm} \\

636: \begin{tabular}{rrl}

637: $G$ & ::= &

638:       $(t = t)  \Bar  p(t, \ldots, t)  \Bar  G \And G  \Bar  G \Or G$ \\

639:   & $|$ & $\Not G  \Bar  \exists x~G  \Bar  if[\vec{x}](G, G)$ \\

640: \end{tabular} \\

641: All the connectives are standard except the $if$ connective.

642: $if[\vec{x}](B,C)$ is a variable binding construct, which binds

643: all the variables in the list $\vec{x}$.

644: $if[\vec{x}](B, C)$ is computed as follows: if

645: $\exists \vec{x}(B)$ is false, so is

646: $if[\vec{x}](B, C)$; otherwise,

647: $if[\vec{x}](B, C)$ is equivalent to

648: $C\theta$, where $\theta$ is the first substitution

649: for $\vec{x}$ returned by the computation of $B$.

650: This form of formula allows us to express a Prolog

651: program with cuts in a ``completed'' form (see section

652: \ref{completions-section}).

653: 

654: \label{true-false-section}

655: We assume a standard syntax of terms.  We assume that the

656: language of the program contains at least two terms, which we

657: will refer to as $0$ and $1$.  We define the formula $true$ as

658: $0=0$, and the formula $false$ as $0=1$.

659: 

660: Because we will be speaking of clauses with cut, we cannot 

661: use the standard logic-programming definition of clause.

662: The BNF definitions of formula, clause, clause body, and clause

663: body element used in this paper are as follows.\vspace{2mm} \\

664: \begin{tabular}{lll}

665: $clause$ & ::= & $p(t, \ldots, t) \colondash body$ \\

666: $body$ & ::= &

667:       $\epsilon  \Bar  bodyelt, body$ \\

668: $bodyelt$ & ::= &

669:       $G  \Bar  !$ \\

670: \end{tabular} \\

671: ($\epsilon$ is the empty expression.)

672: As in Prolog, we generally write a clause of the form

673: $p(t_1, \ldots, t_n) \colondash \epsilon$

674: as simply $p(t_1, \ldots, t_n)$.

675: Note that we restrict the cut to occurring ``at the top level''

676: in clauses.  In most Prologs it is possible to use cut within a

677: complex formula (for instance, a disjunction), but such cuts are

678: seldom used and their effect is generally said to be

679: undefined\footnote{

680: Billaud's operational semantics of cut \cite{billaud-cut-tcs}

681: defines a behaviour of cuts within complex formulas which is

682: consistent with the operational semantics of some Prolog interpreters.

683: }.

684: 

685: A {\it program} is a sequence of clauses.

686: It is clear that the syntax of programs, as defined here,

687: generalizes the syntax of Prolog programs with only

688: literals and cuts as body elements.

689: For simplicity, we assume that each predicate is defined

690: with a distinct arity in a given program; that is, that at every

691: occurrence of a predicate name, it is given the same number of

692: parameters.  We say that a clause {\it defines} predicate $p$ if

693: the head of the clause has predicate $p$.

694: We use $clauses(p,P)$ to stand for the sequence of

695: clauses defining predicate $p$ in program $P$.

696: 

697: \label{example-section}

698: As an example of a program in the extended syntax, consider the

699: following standard definition of a ``delete'' predicate:

700: \begin{tabbing}

701: \Indent{} \= \kill

702: \>  $d(x, [~], [~])$ \\

703: \>  $d(x, [x|ys], zs) \colondash !, d(x, ys, zs)$ \\

704: \>  $d(x, [y|ys], [y|zs]) \colondash d(x, ys, zs)$

705: \end{tabbing}

706: The goal $d(x, y, z)$ deletes all occurences of the element $x$

707: in the list $y$, resulting in the list $z$.

708: As we will see, the following definition is equivalent:

709: \begin{tabbing}

710: \Indent{} \= $\Or$ \= \kill

711: \>  $d(x, y, z) \colondash$ \\

712: \>  \>  $(y=[~] ~ \And ~ z=[~])$ \\

713: \>  $\Or$ \> $if[ys](y=[x|ys], d(x, ys, z))$ \\

714: \>  $\Or$ \> $(\Not\exists ys(y=[x|ys]) ~ \And$ \\

715: \>        \> \Indent{} $\exists y' \exists ys \exists zs(y=[y'|ys] \And z=[y'|zs] \And d(x, ys, zs)))$

716: \end{tabbing}

717: 

718: 

719: 

720: 

721: \section{The Liberal Operational Semantics}

722: \label{opsem-section}

723: 

724: In order to define precisely the logic programming systems

725: which will be the focus of our study, we must define precisely

726: their operational, or procedural, semantics.

727: In this section, we define two operational semantics

728: (the second simpler than the first) for

729: the extended logic programs defined in the last section.

730: Because they share Prolog's rather lax, non-logical interpretation

731: of negation and cut, they are referred to as ``liberal''

732: operational semantics.  The second of these semantics will be

733: used as the basis of the more ``conservative'' semantics of

734: the next section, which regains the witness properties.

735: 

736: Traditionally,

737: operational semantics of logic programming are given using

738: variants of resolution, in particular SLD-resolution.

739: However, in the presence of such features as depth-first search,

740: negation as failure and cut, SLD-resolution-based operational semantics

741: require an additional superstructure of definitions, for instance

742: to define the order in which branches of the SLD-tree are searched.

743: We therefore follow other researchers

744: \cite{deransart-std-inria,billaud-cut-tcs} in defining operational

745: semantics for our system using the style which has come to be

746: known as SOS, or Structured Operational Semantics \cite{plotkin-opsem}.

747: 

748: The rules in this paper are presented in groups,

749: which (following \cite{abadi-cardelli-objects}) are referred to

750: as ``fragments'', to emphasize that they are only parts

751: of formal systems.  We define various different

752: operational semantics for various different purposes; each semantics will

753: be made up of several of these fragments.

754: 

755: In this section, we first present some basic definitions in section

756: \ref{defns-subsection}.  In section \ref{libgen-subsection},

757: we define the ``liberal general'' operational semantics.

758: This semantics takes its name from its liberal attitude and

759: the fact that it can handle general programs

760: (with multi-clause definitions and cut).

761: 

762: Traditional Prolog multi-clause predicate definitions

763: turn out to be awkward to work with in the presence of cut.

764: Predicates defined with a single clause are more convenient to

765: work with; but is it always possible to transform a program

766: with multi-clause definitions into one with single-clause

767: definitions?  In section \ref{completions-section} we answer this

768: question in the affirmative, defining a ``completed form''

769: for programs and giving an algorithm which transforms a program

770: to completed form.

771: In section

772: \ref{libcomp-subsection}, we give the ``liberal completed''

773: semantics, which is defined only for completed-form programs and is much

774: simpler than the liberal general semantics.  It is this

775: liberal completed semantics that we use as the basis of the

776: safer, ``conservative'' semantics of the rest of the paper.

777: 

778: Finally, in section \ref{inadequate-section}, we show formally

779: that the liberal semantics, like the Prolog systems they

780: characterize, are problematic from a logic programming point of

781: view because they violate not only logic, but also the

782: weaker witness properties.

783: 

784: \subsection{Basic Definitions}

785: \label{defns-subsection}

786: 

787: This section defines some basic notions of the operational

788: semantics, namely goal stacks, results, judgments and

789: computations.

790: 

791: The judgements of the operational semantics contain

792: {\it goal stack elements} and {\it results}.

793: A goal stack element represents a subgoal to solve,

794: possibly with information about how to solve it.  A goal stack

795: element can be one of the following:

796: \begin{itemize}

797: \item a formula;

798: \item an expression of the form $p(t_1, \ldots, t_n) using(\gamma)$,

799:   where $\gamma$ is a sequence of clauses; or

800: \item an expression of the form $body(\eta)$, where $\eta$ is a

801:   clause body (i.e., a possibly empty sequence of body elements).

802: \end{itemize}

803: A goal stack element of the form $p(t_1, \ldots, t_n) using(\gamma)$

804: represents a predicate call along with the sequence of

805: clauses remaining to be used in its processing; a goal stack element

806: of the form $body(\eta)$

807: represents a predicate body, possibly containing cuts.  (We

808: distinguish a predicate body from a regular sequence of formulas

809: in this way because a body with cuts demands some special

810: treatment.)  We define a {\it goal stack} as a sequence of goal

811: stack elements.

812: 

813: In this paper, the {\it result} of a computation in the

814: operational semantics can be one of four things:

815: \begin{itemize}

816: \item A substitution $\theta$, indicating a successful computation

817:   returning $\theta$ as the solution;

818: \item $fail$, indicating failure to find a substitution;

819: \item $flounder$, indicating that a mode restriction

820:   has been violated (see Section \ref{conservative-section}); or

821: \item $diverge$, indicating that the operational semantics

822:   believes the computation to diverge (see Section \ref{sems-section}).

823: \end{itemize}

824: Only the first two results are possible with the semantics in

825: this section, but the others will be possible in later

826: semantics.

827: 

828: A {\it judgement} of an operational semantics is an expression

829: of the form $(\theta: \alpha \Goes{P} \rho)$, where $\theta$ is a

830: (finite representation of a)

831: substitution, $\alpha$ is a goal stack containing no free

832: variables in the domain of $\theta$,

833: $P$ is a program, and $\rho$ is a result.  A judgement indicates

834: that the computation of the goals in $\alpha$, under the current

835: substitution $\theta$ and the program $P$, has the result $\rho$.

836: 

837: A {\it computation} in a given operational semantics

838: is a tree, written root-down, in which each

839: node is a judgement, and where the relationship between each

840: node and its children is defined by the rules in that

841: operational semantics.  Computing the outcome of a Prolog

842: goal $G$ with respect to program $P$ corresponds to finding a

843: result $\rho$ and a

844: computation whose root node is $((): G \Goes{P} \rho)$, where

845: $()$ is the empty substitution.  Generally, we will drop the

846: $P$ subscript where its value is clear.

847: 

848: In the operational semantics, we use $\alpha$ to stand for a

849: goal stack, and $\eta$ to stand for a sequence of

850: body elements.  We use $\gamma$ to stand for a sequence of

851: clauses; to distinguish sequences of clauses more clearly from

852: sequences of goal stack or body elements, we separate clauses

853: in a sequence by semicolons, and goal stack or body elements

854: by commas.

855: 

856: 

857: \subsection{The Liberal General Semantics}

858: \label{libgen-subsection}

859: 

860: \begin{figure}[tp]

861: 

862: \begin{center} %\small

863: \begin{tabular}{ccc}

864: ~

865:   & ~~~ &

866:   $\overline{\theta'': \epsilon \Goes{} \theta''}$ \\

867: ~

868:   & ~~~ &

869:   $\overline{\theta'[x':=a]: z=[~] \Goes{} \theta''}$ \\

870: ~

871:   & ~~~ &

872:   $\overline{\theta'[x':=a]: [~]=[~], z=[~] \Goes{} \theta''}$ \\

873: $\overline{\theta': \epsilon\Goes{} \theta'}$

874:   & ~~~ &

875:   $\overline{\theta': a=x', [~]=[~], z=[~] \Goes{} \theta''}$ \\

876: $\overline{[x:=a,ys:=[~]]: z=zs \Goes{} \theta'}$

877:   & ~~~ &

878:   $\overline{\underline{\theta': d(a,[~],z)using(C_1;C_2;C_3) \Goes{} \theta''}}$ \\

879: $\overline{[x:=a]: [a]=[a|ys], z=zs \Goes{} \theta'}$

880:   & ~~~ &

881:   $\theta': d(a,[~],z) \Goes{} \theta''$ \\

882: $\overline{(): a=x, [a]=[x|ys], z=zs \Goes{} \theta'}$

883:   & ~~~ &

884:   $\overline{\theta': body(d(a,[~],z)) \Goes{} \theta''}$ \\

885: \cline{1-3}

886: \multicolumn{3}{c}{

887:     $(): d(a,[a], z)using(C_2;C_3) \Goes{} \theta''$

888:   } \\

889: \end{tabular}

890: \end{center}

891: 

892: \begin{center} %\small

893: \begin{tabular}{ccc}

894: $\overline{[x:=a]: [a]=[~], z=[~] \Goes{} fail}$

895:   & ~~~ &

896:   (see above) \\

897: $\overline{(): a=x, [a]=[~], z=[~] \Goes{} fail}$

898:   & ~~~ &

899:   $\overline{(): d(a,[a], z)using(C_2;C_3) \Goes{} \theta''}$ \\

900: \cline{1-3}

901: \multicolumn{3}{c}{

902:   $\underline{(): d(a,[a], z)using(C_1;C_2;C_3) \Goes{} \theta''}$

903: } \\

904: \multicolumn{3}{c}{

905:   $(): d(a,[a], z) \Goes{} \theta''$

906: } \\

907: \end{tabular}

908: \end{center}

909: 

910: \caption{An example computation in the liberal general semantics

911:   with respect to the first ``delete'' program of Section 3.

912:   The computation is split into two pieces in order to fit on the page.

913: }

914: \label{libgen-example-fig}

915: \end{figure}

916: 

917: 

918: \begin{figure}[tp]

919: 

920: \noindent

921: \Rule{Unif/succ:}

922:   {\theta\sigma: \alpha\sigma \Goes{} \rho}

923:   {\theta: (s = t), \alpha \Goes{} \rho}

924:   {where $\sigma$ is an mgu of $s$ and $t$}

925: \\ %

926: \Rule{Unif/fail:}

927:   {}

928:   {\theta: (s = t), \alpha \Goes{} fail}

929:   {where $s$ and $t$ are not unifiable}

930: \\ %

931: \Rule{Success:}

932:   {}

933:   {\theta: \epsilon \Goes{} \theta}

934:   {}

935: \\ %

936: \Rule{Conj:}

937:   {\theta: B, C, \alpha \Goes{} \rho}

938:   {\theta: B \And C, \alpha \Goes{} \rho}

939:   {}

940: \\ %

941: \Rule{Disj/nofail:}

942:   {\theta: B, \alpha \Goes{} \rho}

943:   {\theta: B \Or C, \alpha \Goes{} \rho}

944:   {where $\rho$ is not $fail$}

945: \\ %

946: \Rule{Disj/fail:}

947:   {\theta: B, \alpha \Goes{} fail  \Sep

948:    \theta: C, \alpha \Goes{} \rho}

949:   {\theta: B \Or C, \alpha \Goes{} \rho}

950:   {}

951: \\ %

952: \Rule{Exists:}

953:   {\theta: B[x:=x'], \alpha \Goes{} \rho}

954:   {\theta: \exists x(B), \alpha \Goes{} \rho}

955:   {where $x'$ does not occur in the conclusion}

956: 

957: \caption{

958:   [Basic], the operational semantics rules fragment for the

959:   basic logic programming connectives.

960: }

961: \label{basic-rules-fig}

962: \end{figure}

963: 

964: 

965: \begin{figure}[tp]

966: 

967: \noindent

968: \Rule{Not/succ:}

969:   {\theta: B \Goes{} \theta'}

970:   {\theta: \Not B, \alpha \Goes{} fail}

971:   {}

972: \\ %

973: \Rule{Not/fail:}

974:   {\theta: B \Goes{} fail  \Sep  \theta: \alpha \Goes{} \rho}

975:   {\theta: \Not B, \alpha \Goes{} \rho}

976:   {}

977: \\ %

978: \Rule{If/succ:}

979:   {\theta: B[\vec{x}:=\vec{x}'] \Goes{} \theta'  \Sep

980:    \theta': C[\vec{x}:=\vec{x}']\theta', \alpha\theta' \Goes{} \rho}

981:   {\theta: if[\vec{x}](B,C), \alpha \Goes{} \rho}

982:   {where $\vec{x}'$ do not appear in the conclusion}

983: \\ %

984: \Rule{If/fail:}

985:   {\theta: B[\vec{x}:=\vec{x}'] \Goes{} fail}

986:   {\theta: if[\vec{x}](B,C), \alpha \Goes{} fail}

987:   {where $\vec{x}'$ do not appear in the conclusion}

988: 

989: 

990: \caption{

991:   [Liberal Choice], the operational semantics rules fragment for

992:   dealing with ``not'' and ``if'' in a liberal manner.

993: }

994: \label{lib-choice-rules-fig}

995: \end{figure}

996: 

997: 

998: 

999: \begin{figure}[tp]

1000: 

1001: \noindent

1002: \Rule{Pred:}

1003:   {\theta: p(t_1, \ldots, t_n) using (\gamma), \alpha \Goes{} \rho}

1004:   {\theta: p(t_1, \ldots, t_n), \alpha \Goes{} \rho}

1005:   {where $\gamma$ is $clauses(p,P)$, renamed apart from any

1006:    free variables in the conclusion}

1007: \\ %

1008: %\Cap{Using/cut/succ:}\\

1009: %\Rule{}

1010: \Rule{Using/cut/succ:}

1011:   {\theta: s_1=t_1, \ldots, s_n=t_n, \eta_1 \Goes{} \theta'  \Sep

1012:    \theta': body(\eta_2)\theta', \alpha\theta' \Goes{} \rho}

1013:   {\theta: p(s_1, \ldots, s_n) using (C,\gamma), \alpha \Goes{} \rho}

1014:   {where $C$ is of the form $p(t_1, \ldots, t_n) \colondash \eta_1, !, \eta_2$,

1015:    and $\eta_1$ contains no cuts}

1016: \\ %

1017: %\Cap{Using/cut/fail:}\\

1018: %\Rule{}

1019: \Rule{Using/cut/fail:}

1020:   {\theta: s_1=t_1, \ldots, s_n=t_n, \eta_1 \Goes{} fail  \Sep

1021:    \theta: p(s_1, \ldots, s_n) using (\gamma), \alpha \Goes{} \rho}

1022:   {\theta: p(s_1, \ldots, s_n) using (C,\gamma), \alpha \Goes{} \rho}

1023:   {where $C$ is of the form $p(t_1, \ldots, t_n) \colondash \eta_1, !, \eta_2$,

1024:    and $\eta_1$ contains no cuts}

1025: \\ %

1026: %\Cap{Using/nocut/succ:}\\

1027: %\Rule{}

1028: \Rule{Using/nocut/succ:}

1029:   {\theta: s_1=t_1, \ldots, s_n=t_n, \eta, \alpha \Goes{} \theta'}

1030:   {\theta: p(s_1, \ldots, s_n) using (C,\gamma), \alpha \Goes{} \theta'}

1031:   {where $C$ is of the form $p(t_1, \ldots, t_n) \colondash \eta$,

1032:    and $\eta$ contains no cuts}

1033: \\ %

1034: %\Cap{Using/nocut/fail:}\\

1035: %\Rule{}

1036: \Rule{Using/nocut/fail:}

1037:   {\theta: s_1=t_1, \ldots, s_n=t_n, \eta, \alpha \Goes{} fail  \Sep

1038:    \theta: p(s_1, \ldots, s_n) using (\gamma), \alpha \Goes{} \rho}

1039:   {\theta: p(s_1, \ldots, s_n) using (C,\gamma), \alpha \Goes{} \rho}

1040:   {where $C$ is of the form $p(t_1, \ldots, t_n) \colondash \eta$,

1041:    and $\eta$ contains no cuts}

1042: \\ %

1043: \Rule{Using/empty:}

1044:   {}

1045:   {\theta: p(s_1, \ldots, s_n) using (\epsilon), \alpha \Goes{} fail}

1046:   {}

1047: 

1048: %\caption{

1049: %  The first part of [General Predicates], the operational semantics

1050: %  rules fragment for dealing with general (multi-clause) predicate

1051: %  definitions.

1052: %}

1053: %\label{general-pred-rules-figa}

1054: %\end{figure}

1055: %

1056: %

1057: %

1058: %\begin{figure}[tp]

1059: 

1060: \Rule{Body/cut/succ:}

1061:  {\theta: \eta_1 \Goes{} \theta'  \Sep

1062:   \theta': body(\eta_2)\theta', \alpha\theta' \Goes{} \rho}

1063:  {\theta: body(\eta_1, !, \eta_2), \alpha \Goes{} \rho}

1064:  {where $\eta_1$ contains no cuts}

1065: \\ %

1066: \Rule{Body/cut/fail:}

1067:  {\theta: \eta_1 \Goes{} fail}

1068:  {\theta: body(\eta_1, !, \eta_2), \alpha \Goes{} fail}

1069:  {where $\eta_1$ contains no cuts}

1070: \\ %

1071: \Rule{Body/nocut:}

1072:  {\theta: \eta, \alpha \Goes{} \rho}

1073:  {\theta: body(\eta), \alpha \Goes{} \rho}

1074:  {where $\eta$ contains no cuts}

1075: 

1076: \caption{

1077: %  The second part of [General Predicates], the operational semantics

1078: %  rules fragment for dealing with general (multi-clause) predicate

1079: %  definitions.

1080:   [General Predicates], the operational semantics

1081:   rules fragment for dealing with general (multi-clause) predicate

1082:   definitions.

1083: }

1084: \label{general-pred-rules-figb}

1085: \end{figure}

1086: 

1087: The first operational semantics we study, as described

1088: above, is the {\it liberal general} semantics.

1089: It is made up of the fragments

1090: [Basic] (Figure \ref{basic-rules-fig}),

1091: [Liberal Choice] (Figure \ref{lib-choice-rules-fig}), and

1092: %[General Predicates] (Figures \ref{general-pred-rules-figa},

1093: %\ref{general-pred-rules-figb}).

1094: [General Predicates] (Figure

1095: \ref{general-pred-rules-figb}).

1096: The liberal general semantics corresponds

1097: to most common implementations of Prolog, which employ hard cut and

1098: unsound negation as failure.

1099: We begin this section by looking at an example computation,

1100: and then discuss the individual rules of the liberal general

1101: semantics in more detail.

1102: 

1103: \subsubsection{Example Computation}

1104: \label{example-comp-subsection}

1105: 

1106: Figure \ref{libgen-example-fig} shows an example computation in

1107: the liberal general semantics.

1108: (The clauses $C_1, C_2, C_3$ are the clauses for $d$

1109: from the three-clause version defined in Section

1110: \ref{example-section}).

1111: The substitution $\theta'$ is $[x:=a,ys:=[~],zs:=z]$,

1112: and

1113: the substitution $\theta''$ is $[x:=a,ys:=[~],zs:=[~],x':=a,z=[~]]$.)

1114: This computation, like all

1115: computations, gives the result of the computation within the

1116: same judgement as the original goal.  Therefore it may not be

1117: clear how to obtain a result from knowing only the goal we want

1118: to solve.  The example illustrates how we can do so

1119: in a systematic fashion by applying rules bottom-up.

1120: 

1121: We start (at the bottom) with

1122: the goal formula $d(a, [a], z)$ and the empty substitution; our

1123: task is to determine the result expression, to the right of

1124: the $\Goes{}$ symbol.  Since $d(a,[a],z)$ is a predicate

1125: call, we know that the bottommost rule is a Pred rule,

1126: that the substitution in the premise is still empty, and that

1127: the goal stack in the premise is

1128: $d(a,[a], z)using(C_1;C_2;C_3)$.

1129: We therefore apply that rule at the bottom of the computation.

1130: We have now reduced the problem of finding the result of

1131: $((): d(a, [a], z))$ to that of finding the result of

1132: $((): d(a,[a], z)using(C_1;C_2;C_3))$.

1133: 

1134: At this point, we can apply either the Using/nocut/succ or the

1135: Using/nocut/fail rule; we do not know which is applicable.

1136: However, we know that if Using/nocut/succ is applicable,

1137: the substitution in the left-hand premise is the

1138: empty substitution and the goal stack in the left-hand premise is

1139: $(a=x, [a]=[~], z=[~])$; we also know that if Using/nocut/fail

1140: is applicable, then the substitution in the (only) premise

1141: is again empty and the goal stack in the premise is again

1142: $(a=x, [a]=[~], z=[~])$.  If the result of this goal stack is

1143: $fail$, then Using/nocut/fail is applicable; if it is some

1144: substitution $\theta$, then Using/nocut/succ is applicable.

1145: We therefore choose as our next task to find the result of

1146: $((): a=x, [a]=[~], z=[~])$.

1147: 

1148: As it turns out, in two simple steps (a Unif/succ step and

1149: a Unif/fail step) we can determine that

1150: $((): a=x, [a]=[~], z=[~] \Goes{} fail)$.  Therefore

1151: we choose Using/nocut/fail as the rule to apply.  This

1152: choice determines the form of the substitution (again, the

1153: empty substitution) and the goal stack

1154: ($d(a,[a], z)using(C_2;C_3)$) in the right-hand premise.

1155: We can repeat this process of finding results

1156: in order to obtain the result $\theta''$ of

1157: $d(a,[a], z)using(C_2;C_3)$, which is inherited by our

1158: original goal $d(a, [a], z)$ as its result.

1159: $\theta''$ contains the mapping $[z:=[~]]$; thus the

1160: computation has correctly told us that the result of

1161: deleting $a$ from the list $[a]$ is the empty list.

1162: 

1163: In general, whenever we are faced with a choice of two rules,

1164: the above strategy will work.  The form of substitution and goal

1165: stack in one of the premises can be uniquely determined, and the

1166: choice of rule and form of substitution and goal stack in the

1167: other premise (if another is needed) can be uniquely determined

1168: from the result of the

1169: first premise.  Thus, information in a computation

1170: can be seen as ``flowing'' in a clockwise manner around the

1171: perimeter of the computation.

1172: 

1173: \subsubsection{The Rules}

1174: \label{rules-subsection}

1175: 

1176: We now describe the general significance of the rules in the

1177: liberal general semantics in terms of how the different kinds of goal

1178: stack elements are handled.

1179: 

1180: The equality rules in the [Basic] fragment describe the usual

1181: results of unification; if unification fails, the entire goal

1182: stack fails, but if it succeeds, the computation proceeds under

1183: the mgu.

1184: The first order connective rules in [Basic] express the usual

1185: operation of Prolog interpreters.  We solve a conjunction by

1186: solving each of its conjuncts in turn, left to right.  We solve

1187: a disjunction by attempting to solve its left-hand disjunct and

1188: the rest of the subgoals; if this is solvable, we can ignore the

1189: right-hand disjunct, but if not, we attempt to solve that

1190: disjunct with the rest of the subgoals.  Finally, we solve an

1191: existential formula (corresponding to a free variable in a

1192: clause) by renaming its variable apart from the rest of the

1193: variables in the goal.

1194: 

1195: In the [Liberal Choice] rules, we solve a negation by solving

1196: the negated formula, inverting the sense of the result at the end.

1197: This is the usual unsound strategy, which will be corrected

1198: in the system with firm cut.

1199: Similarly, the formula

1200: $if[\vec{x}](B, C)$ is computed by first computing $B$ and

1201: checking the result.  If the result is a successful computation

1202: returning satisfying substitution $\theta$, then $\theta$ is

1203: used to compute $C$; otherwise, the whole formula fails.

1204: This will also be modified in the system with firm cut,

1205: in order to achieve the witness properties.

1206: 

1207: The predicate call and clause selection rules of the

1208: [General Predicates] fragment reflect how Prolog

1209: backtracks over clauses and cuts away alternate solutions.

1210: We ``launch'' the processing of a predicate

1211: call by collecting the clauses in the program defining the predicate

1212: into an initial $using$ expression.

1213: Then, if the first clause contains a cut, we process first only

1214: the part before

1215: the cut.  On success, we retain the substitution returned and

1216: discard the other clauses, but on failure,

1217: we discard that first clause and repeat the procedure.

1218: This characterizes the behaviour of

1219: Prolog clauses with cut.

1220: 

1221: Conversely, if the first clause does not contain

1222: a cut, we process the entire clause body {\it along with the rest

1223: of the subgoals}.  Again, on success of the goal stack we

1224: discard the other clauses, and on failure of the goal stack, the

1225: first clause.

1226: However, because we have included the rest of the subgoals in the

1227: goal stack,

1228: we retain the option of returning to another clause if a

1229: subgoal fails later in the computation.  This characterizes the

1230: behaviour of usual Prolog clauses without cut.

1231: 

1232: Finally, the predicate body rules reflect how cuts in a clause body

1233: after the first cut may prune the search tree.  If a clause body

1234: has cuts, then the portion before the first cut

1235: is processed first; if it returns a solution, we process the rest

1236: of the body with that first solution, and otherwise the entire body fails.

1237: If the body has no cuts, however, it is processed just as a

1238: sequence of formulas.

1239: 

1240: \subsection{Completed Forms of Programs}

1241: \label{completions-section}

1242: 

1243: In this section, we show that it is possible to transform any

1244: program into one in a ``completed'' form, in which every

1245: predicate is defined by a single clause without cuts.  This is

1246: valuable because programs in completed form are much easier to

1247: work with in the proofs we need to do.  We begin by giving the

1248: transformation algorithm, show an example of how it transforms a

1249: program, and then prove the required properties of the

1250: transformation algorithm.

1251: 

1252: We say that a program is {\it in completed form} when each of

1253: the following conditions hold:

1254: \begin{enumerate}

1255: \item The parameters in the clause head are distinct variables;

1256: \item There is only one clause defining each predicate;

1257: \item The body of each clause consists of a single formula; and

1258: \item The free variables in the body are a subset of the parameters

1259:   in the head.

1260: \end{enumerate}

1261: Our transformation of programs into completed forms depends on

1262: the fact that our definition of formula includes the $if$

1263: connective, which allows us to achieve the effect of cuts;

1264: in fact, this is the main reason why $if$ was included in the

1265: syntax and operational semantics of our language.

1266: 

1267: \subsubsection{Transformation Algorithm}

1268: \label{transformation-subsection}

1269: 

1270: Here, we give an algorithm which progressively

1271: transforms a program into completed form, by replacing clauses

1272: with other clauses.  The program, as it is being transformed,

1273: will progressively satisfy each of the following properties.

1274: \begin{itemize}

1275: \item[(A)] The parameters in the clause head are distinct variables.

1276: \item[(B)] Each clause body begins and ends with a formula, and

1277:   alternates formulas and cuts.

1278: \item[(C)] Each clause has at most one cut; that is, each clause

1279:   body consists of either a singleton formula $F$, or a sequence

1280:   $F, !, G$.

1281: \item[(D)] The last clause defining each predicate has a body

1282:   which is a single formula, having no free variables except

1283:   those appearing in the head.

1284: \item[(E)] Each predicate is defined by exactly one clause.

1285: \end{itemize}

1286: 

1287: The algorithm is as follows.

1288: \begin{itemize}

1289: \item[1.] Choose a countable

1290:   sequence of variables not appearing in the program.

1291:   We will refer to these variables as $x_1, x_2, \ldots$

1292:   in the rest of the algorithm.

1293: \item[2.] While there is some clause in the program not of

1294:   the form $(p(x_1, \ldots, x_n) \colondash \eta)$:

1295:   \begin{itemize}

1296:   \item[2.1.] Choose one such clause $C$, of the form \\

1297:     $p(t_1, \ldots, t_{k-1}, t_k, x_{k+1}, \ldots, x_n) \colondash \eta$,

1298:     where $t_k$ is not $x_k$.

1299:   \item[2.2.] If $t_k$ is a variable $y$ distinct from

1300:     $x_1, \ldots, x_n$, then replace $C$ in the program by $C[y:=x_k]$.

1301:   \item[2.3.] Otherwise, replace $C$ by \\

1302:     $p(t_1, \ldots, t_{k-1}, x_k, x_{k+1}, \ldots, x_n) \colondash

1303:     (x_k = t_k), \eta$.

1304:   \end{itemize}

1305:   (After this while loop has been completed,

1306:   we can assume that property (A) above is satisfied.)

1307: \item[3.] While there is some clause of the form

1308:   $p(x_1, \ldots, x_n) \colondash \eta_1, F, G, \eta_2$, where $F$

1309:   and $G$ are formulas:

1310:   choose one such clause and transform it to the

1311:     form $p(x_1, \ldots, x_n) \colondash \eta_1, (F \And G), \eta_2$.

1312: \item[4.] While there is some clause with an empty body:

1313:   choose one such clause and replace the body by the single

1314:   formula $true$ (i.e., $0=0$).

1315: \item[5.] While there is some clause with two consecutive cuts:

1316:   choose one such clause and replace the consecutive cuts by a

1317:   single cut.

1318: \item[6.] While there is some clause beginning with a cut:

1319:   choose one such clause and insert the formula $true$ before

1320:   the first cut.

1321: \item[7.] While there is some clause ending with a cut:

1322:   choose one such clause and insert the formula $true$ after

1323:   the last cut.

1324:   (We can now assume that property (B) above is satisfied.)

1325: \item[8.] While there is some clause of the form

1326:   $p(x_1, \ldots, x_n) \colondash \eta, !, F, !, G$:

1327:   \begin{itemize}

1328:   \item[8.1.] Select one such clause.

1329:   \item[8.2.] Select a predicate name $q$ not appearing in the

1330:     program.

1331:   \item[8.3.] Add a clause to the program of the form

1332:     $q(\vec{y}) \colondash F, !, G$, where

1333:     $\vec{y}$ are all the free variables of $F, G$.

1334:   \item[8.4.] Replace the original selected clause by 

1335:     $p(x_1, \ldots, x_n) \colondash \eta, !, q(\vec{y})$.

1336:   \end{itemize}

1337:   (We can now assume that property (C) above is satisfied.)

1338: \item[9.]

1339:   Repeat until the last clause of all predicates is

1340:   of the form $p(x_1, \ldots, x_n) \colondash G$,

1341:   where all free variables of $G$ appear in the head:

1342:   \begin{itemize}

1343:   \item[9.1.] Choose the last clause of one predicate for which

1344:     this is not the case; let it be of the form

1345:     $p(x_1, \ldots, x_n) \colondash \eta$.

1346:   \item[9.2.] If $\eta$ is some singleton formula $G$, replace the

1347:     clause by \linebreak[4]

1348:     $p(x_1, \ldots, x_n) \colondash \exists \vec{y} (G)$,

1349:     where $\vec{y}$ are all the free variables of $G$ not

1350:     in $x_1, \ldots, x_n$.

1351:   \item[9.3.] Otherwise, $\eta$ is a sequence of the form $F, !, G$.

1352:     Replace the clause by

1353:     $p(x_1, \ldots, x_n) \colondash if[\vec{y}](F, G)$,

1354:     where $\vec{y}$ are all the free variables of $F, G$ not

1355:     in $x_1, \ldots, x_n$.

1356:   \end{itemize}

1357:   (We can now assume that property (D) above is satisfied.)

1358: \item[10.] While there is some predicate which is defined by more

1359:   than one clause:

1360:   \begin{itemize}

1361:   \item[10.1.] Choose one such predicate $p$.  Let the second-last

1362:     clause defining $p$ be

1363:     $p(x_1, \ldots, x_n) \colondash \eta$, and let the last clause

1364:     defining $p$ be

1365:     $p(x_1, \ldots, x_n) \colondash H$.

1366:   \item[10.2.] If $\eta$ is some singleton formula $G$, replace the

1367:     two clauses by the single clause

1368:     $p(x_1, \ldots, x_n) \colondash \exists \vec{y} (G) \Or H$,

1369:     where $\vec{y}$ are all the free variables of $G$ not

1370:     in $x_1, \ldots, x_n$.

1371:   \item[10.3.] Otherwise, $\eta$ is a sequence of the form $F, !, G$.

1372:     Replace the two clauses by the single clause

1373:     $p(x_1, \ldots, x_n) \colondash

1374:        if[\vec{y}](F, G) \Or ((\Not\exists \vec{y} (F)) \And H)$,

1375:     where $\vec{y}$ are all the free variables of $F,G$ not

1376:     in $x_1, \ldots, x_n$.

1377:   \end{itemize}

1378:   (We can now assume that property (E) above is satisfied.)

1379: \end{itemize}

1380: 

1381: The effect of all these steps is that we have arrived at a program

1382: in completed form, i.e.\ in which all predicates are defined by

1383: a single clause of the form $p(x_1, \ldots, x_n) \colondash G$,

1384: where the free variables of $G$ are among $x_1, \ldots, x_n$.

1385: 

1386: Given program $P$, we refer to the program resulting at the end

1387: of the sequence of transformations as the {\it augmented Clark

1388: completion} of $P$, or $acc(P)$.

1389: The augmented Clark completion of $P$ serves

1390: essentially the same purpose as the Clark completion in Clark's

1391: original treatment of negation as failure \cite{clark-negfail};

1392: that is, it gives a closed form of the intended meaning of

1393: each predicate.  We cannot truly consider it to be a logical

1394: completion, however; the $if$ construct, while it can be

1395: given a semantics consistent with the witness properties (as we

1396: will see), cannot be given a logical interpretation.

1397: 

1398: 

1399: \subsubsection{Example}

1400: \label{example-subsection}

1401: 

1402: As an example, consider the first ``delete'' program from Section

1403: \ref{example-section}:

1404: \begin{tabbing}

1405: \Indent{} \= \kill

1406: \>  $d(x, [~], [~])$ \\

1407: \>  $d(x, [x|ys], zs) \colondash !, d(x, ys, zs)$ \\

1408: \>  $d(x, [y|ys], [y|zs]) \colondash d(x, ys, zs)$

1409: \end{tabbing}

1410: Assume that the variables selected in Step 1 are $x_1, x_2, x_3, \ldots$.

1411: The program is transformed, by the end of Step 2, to the form:

1412: \begin{tabbing}

1413: \Indent{} \= \kill

1414: \>  $d(x_1, x_2, x_3) \colondash (x_2=[~]), (x_3=[~])$ \\

1415: \>  $d(x_1, x_2, x_3) \colondash (x_2=[x_1|ys]), !, d(x_1, ys, x_3)$ \\

1416: \>  $d(x_1, x_2, x_3) \colondash (x_2=[y|ys]), (x_3=[y|zs]), d(x_1, ys, zs)$

1417: \end{tabbing}

1418: By the end of step 7, the program has been transformed into:

1419: \begin{tabbing}

1420: \Indent{} \= \kill

1421: \>  $d(x_1, x_2, x_3) \colondash (x_2=[~] ~\And ~ x_3=[~])$ \\

1422: \>  $d(x_1, x_2, x_3) \colondash (x_2=[x_1|ys]), !, d(x_1, ys, x_3)$ \\

1423: \>  $d(x_1, x_2, x_3) \colondash (x_2=[y|ys] ~\And ~ x_3=[y|zs] ~\And ~ d(x_1, ys, zs))$

1424: \end{tabbing}

1425: Step 8 has no effect because there is no clause with more than

1426: one cut (this is the case in most programs).  However, Step 9

1427: scopes the local variables in the last clause, making the whole

1428: program read as follows:

1429: \begin{tabbing}

1430: \Indent{} \= \kill

1431: \>  $d(x_1, x_2, x_3) \colondash (x_2=[~] ~\And ~ x_3=[~])$ \\

1432: \>  $d(x_1, x_2, x_3) \colondash (x_2=[x_1|ys]), !, d(x_1, ys, x_3)$ \\

1433: \>  $d(x_1, x_2, x_3) \colondash \exists y \exists ys \exists zs(x_2=[y|ys] ~\And ~ x_3=[y|zs] ~\And ~ d(x_1, ys, zs))$

1434: \end{tabbing}

1435: Let us refer to this new body of the third clause as $B_3$.

1436: Step 10 first combines the last two clauses into a single clause

1437: with $if$, resulting in a new program as follows:

1438: \begin{tabbing}

1439: \Indent{} \= \Indent{} \= \Indent{} \= \kill

1440: \>  $d(x_1, x_2, x_3) \colondash (x_2=[~] ~\And ~ x_3=[~])$ \\

1441: \>  $d(x_1, x_2, x_3) \colondash$ \\

1442: \>  \> $if[ys](x_2=[x_1|ys], d(x_1, ys, x_3)) \Or

1443:                               (\Not\exists ys(x_2=[x_1|ys]) ~\And ~ B_3)$ \\

1444: \end{tabbing}

1445: Let us refer to this new body of the second clause as $B_2$.  Step

1446: 10 then continues, and transforms the remaining two clauses to the

1447: single clause

1448: \begin{tabbing}

1449: \Indent{} \= \kill

1450: \>  $d(x_1, x_2, x_3) \colondash (x_2=[~] ~\And ~ x_3=[~]) \Or B_2$

1451: \end{tabbing}

1452: The program is now in completed form.

1453: 

1454: \subsubsection{Properties}

1455: \label{properties-subsection}

1456: 

1457: We now prove the properties we want the algorithm to have:

1458: that is, that it terminates, that it produces a program in

1459: completed form, and that the completed-form result program

1460: actually does the same thing as the original program.

1461: 

1462: \begin{thm}[Completion Algorithm Termination]

1463:   The completion algorithm terminates.

1464: \end{thm}

1465: 

1466: \begin{proof}

1467: Each loop in the algorithm continues while there is a

1468: clause in the program with a specified property.  The effect of

1469: each loop, however, is to eliminate all clauses with the

1470: specified property.  Therefore each loop in the algorithm

1471: terminates. 

1472: \end{proof}

1473: 

1474: \begin{thm}[Completed Form Formation]

1475:   The completion algorithm produces a program in completed form.

1476: \end{thm}

1477: 

1478: \begin{proof}

1479: Once the program being transformed achieves each of the

1480: properties (A)-(E), as stated in the algorithm text, it never

1481: loses those properties.  The conjunction of the properties

1482: (A)-(E) is the same as saying that the program is in completed

1483: form.

1484: \end{proof}

1485: 

1486: To prove that the completion algorithm preserves the results of

1487: computations, it is technically necessary to prove by induction

1488: on the structure of computations that each transformation step

1489: preserves result.  For brevity, we will prove this in detail

1490: for only one of the transformations, and then argue more informally

1491: in the main proof.  The following is a lemma and a theorem to do

1492: with the transformation we will prove in detail.  All proofs are

1493: contained in Appendix \ref{proofs-appx}.

1494: 

1495: \begin{lemma}

1496: \label{completed-goal-stack-lemma}

1497:   Let $\alpha$ be a goal stack.

1498:   Let $\alpha'$ be $\alpha$

1499:   with any number of occurrences of a sequence $B, C$ in a goal stack or

1500:   clause body replaced by $B \And C$, where $B$ and $C$ are

1501:   formulas.

1502:   Then $(\theta: \alpha \Goes{P} \rho)$ in the liberal general semantics

1503:   iff  $(\theta: \alpha' \Goes{P} \rho)$ in the liberal general semantics.

1504: \end{lemma}

1505: 

1506: \begin{proof}

1507: See Appendix \ref{proofs-appx}.  

1508: \end{proof}

1509: 

1510: \begin{lemma}

1511: \label{conjoin-lemma}

1512:   Let $P'$ be $P$ with some sequence $B, C$ in a clause body

1513:   replaced by $B \And C$.

1514:   Then $\theta: \alpha \Goes{P} \rho$ in the liberal general semantics

1515:   iff  $\theta: \alpha \Goes{P'} \rho$ in the liberal general semantics.

1516: \end{lemma}

1517: 

1518: \begin{proof}

1519: See Appendix \ref{proofs-appx}.  

1520: \end{proof}

1521: 

1522: The main result preservation theorem is as follows.

1523: 

1524: \begin{thm}[Result Preservation of Completion Algorithm]

1525: \label{result-preservation-thm}

1526:   The completion algorithm preserves result according to

1527:   the liberal general operational semantics.  That is,

1528:   if $P'$ is the completion of $P$, then

1529:   $\theta: \alpha \Goes{P} \rho$ in the liberal general semantics iff

1530:   $\theta: \alpha \Goes{P'} \rho$ in the liberal general semantics.

1531: \end{thm}

1532: 

1533: \begin{proof}

1534: We prove the theorem by proving that each of the

1535: transformations preserves result.  The lemma is used in the

1536: proof of step 3.  The details of the proof can be found in

1537: Appendix \ref{proofs-appx}.  

1538: \end{proof}

1539: 

1540: Now that we know that the completion process

1541: preserves result, we can assume that the programs we deal with

1542: will be in completed form (since if not, we have an automatic

1543: process for transforming them to completed form).  We will

1544: therefore assume this for the rest of this paper.

1545: 

1546: 

1547: \subsection{The Liberal Completed Semantics}

1548: \label{libcomp-subsection}

1549: 

1550: Due to the complex behaviour of the Prolog cut, the liberal

1551: general operational semantics contains nine rules for

1552: predicates.  These rules exist mainly to manipulate the

1553: sequences of body elements that exist in the clauses of a

1554: general program, and to backtrack over multiple clauses defining

1555: a predicate.  Since we now are assuming completed-form programs,

1556: we can discard these rules in favour of one simple rule.  The

1557: resulting operational semantics is referred to as the

1558: {\it liberal completed} semantics.  Its simplicity moves us to

1559: adopt it as the standard presentation of the liberal semantics

1560: for the rest of the paper.

1561: 

1562: \begin{figure}[tp]

1563: 

1564: \noindent

1565: \Rule{Pred:}

1566:   {\theta: B[x_1:=t_1,\ldots,x_n:=t_n], \alpha \Goes{} \rho}

1567:   {\theta: p(t_1, \ldots, t_n),         \alpha \Goes{} \rho}

1568:   {where $p(x_1, \ldots, x_n) \colondash B$ is the clause

1569:    defining $p$ in the completed-form program $P$}

1570: 

1571: \caption{

1572:   The predicate rule for the liberal completed semantics,

1573:   the only rule in the [Completed Predicates] fragment.

1574: }

1575: \label{completed-preds-rule-figure}

1576: \end{figure}

1577: 

1578: The liberal general semantics' nine rules for predicates were

1579: contained in the fragments [General Predicates].  The one rule

1580: replacing them is the rule contained in Figure

1581: \ref{completed-preds-rule-figure}.  We refer to the proof system

1582: fragment containing only this rule as the [Completed Predicates]

1583: fragment.  Thus, the liberal completed semantics consists of the

1584: fragments [Basic], [Liberal Choice], and [Completed Predicates].

1585: 

1586: The following result proves that it is safe to use the

1587: liberal completed semantics when we have a completed program.

1588: 

1589: \begin{thm}[Equivalence of General and Completed Semantics]

1590:   If $P$ is a program in completed form, then the liberal

1591:   general and liberal completed semantics have the same

1592:   result.  That is,

1593:   $\theta: \alpha \Goes{P} \rho$ in the liberal general

1594:   semantics iff

1595:   $\theta: \alpha \Goes{P} \rho$ in the liberal completed

1596:   semantics.

1597: \end{thm}

1598: 

1599: \begin{proof}

1600: The computation in the liberal general semantics may

1601: have portions ending in applications of the Using/nocut/succ and

1602: Pred rules, of the following form.

1603: \begin{center}

1604: \begin{tabular}{c}

1605: $\underline{\theta\xi: G\xi, \alpha\xi \Goes{} \rho}$ \\

1606: $\vdots$ \\

1607: $\overline{\theta: \vec{t} = \vec{x}, G, \alpha \Goes{} \rho}$ \\

1608: $\overline{\underline{\theta: p(\vec{t}) using (p(\vec{x}) \colondash G), \alpha \Goes{} \rho}}$ \\

1609: ${\theta: p(\vec{t}), \alpha \Goes{} \rho}$ \\

1610: \end{tabular}

1611: \end{center}

1612: where $\xi$ is the substitution $[x_1:=t_n, \ldots, x_n:=t_n]$.

1613: (We assume without loss of generality that the free variables

1614: of the clause are distinct from those of the conclusion.)

1615: This portion of the computation in the liberal completed

1616: semantics will have the following form:

1617: \begin{center}

1618: \begin{tabular}{c}

1619: $\theta: G\xi, \alpha \Goes{} \rho'$ \\

1620: $\overline{\theta: p(\vec{t}), \alpha \Goes{} \rho'}$ \\

1621: \end{tabular}

1622: \end{center}

1623: where $\rho'$ differs from $\rho$ only in that it does not contain

1624: substitutions for the renamed variables arising from clauses.

1625: Since the substitution $\xi$ deals only with the $x_i$ variables,

1626: which do not appear in $\alpha$, the uppermost judgements in the

1627: two computations are essentially identical.

1628: 

1629: The computation in the liberal general semantics may also

1630: have portions ending in a sequence of applications of the Using/empty,

1631: Using/nocut/fail and Pred rules, of the following form.

1632: \begin{center}

1633: \begin{tabular}{ccc}

1634: $\theta\xi: G\xi, \alpha\xi \Goes{} fail$ \\

1635: \cline{1-1}

1636: $\vdots$ \\

1637: \cline{1-1} \cline{3-3}

1638: $\theta: \vec{t} = \vec{x}, G, \alpha \Goes{} fail$ & \Sep &

1639: $\theta: p(\vec{t}) using (), \alpha \Goes{} fail$ \\

1640: \cline{1-3}

1641: \multicolumn{3}{c}{

1642:   $\theta: p(\vec{t}) using (p(\vec{x}) \colondash G), \alpha \Goes{} fail$

1643: } \\

1644: \cline{1-3}

1645: \multicolumn{3}{c}{

1646:   $\theta: p(\vec{t}), \alpha \Goes{} fail$

1647: } \\

1648: \end{tabular}

1649: \end{center}

1650: where $\xi$ is the substitution $[x_1:=t_n, \ldots, x_n:=t_n]$.

1651: This portion of the computation in the liberal completed semantics

1652: will have the following form:

1653: \begin{center}

1654: \begin{tabular}{c}

1655: $\theta: G\xi, \alpha \Goes{} fail$ \\

1656: $\overline{\theta: p(\vec{t}), \alpha \Goes{} fail}$ \\

1657: \end{tabular}

1658: \end{center}

1659: Again, the substitution $\xi$ does not affect $\alpha$.

1660: \end{proof}

1661: 

1662: \begin{figure}[tp]

1663: 

1664: \begin{center} %\small

1665: \begin{tabular}{ccc}

1666: %\cline{3-3}

1667: & \Sep &

1668:   $\overline{\underline{\theta'': \epsilon \Goes{} \theta''}}$ \\

1669: & \Sep &

1670:   $[ys:=[~]]: z=[~] \Goes{} \theta''$ \\

1671: & \Sep &

1672:   $\overline{[ys:=[~]]: [~]=[~], z=[~] \Goes{} \theta''}$ \\

1673: & \Sep &

1674:   $\overline{[ys:=[~]]: ([~]=[~] \And z=[~]) \Goes{} \theta''}$ \\

1675: \cline{3-3}

1676: $[ys:=[~]]: \epsilon \Goes{} [ys:=[~]]$

1677: & \Sep &

1678:   $[ys:=[~]]: ([~]=[~] \And z=[~]) \Or B_2 \Or B_3 \Goes{} \theta''$ \\

1679: \cline{1-1} \cline{3-3}

1680: $(): [a]=[a|ys] \Goes{} [ys:=[~]]$

1681:   & \Sep &

1682:   $[ys:=[~]]: d(a, [~], z)) \Goes{} \theta''$ \\

1683: \cline{1-3}

1684: \multicolumn{3}{c}{

1685:   $(): if[ys]([a]=[a|ys], d(a, ys, z)) \Goes{} \theta''$

1686: } \\

1687: \cline{1-3}

1688: \multicolumn{3}{c}{

1689:   $(): if[ys]([a]=[a|ys], d(a, ys, z)) \Or B_3 \Goes{} \theta''$

1690: } \\

1691: \end{tabular}

1692: \end{center}

1693: 

1694: \begin{center} %\small

1695: \begin{tabular}{ccc}

1696: ~

1697:   & \Sep &

1698:   (see above) \\

1699: \cline{1-1} \cline{3-3}

1700: $(): [a]=[~] \And z=[~] \Goes{} fail$

1701:   & \Sep &

1702:   $(): if[ys]([a]=[a|ys], d(a, ys, z)) \Or B_3 \Goes{} \theta''$ \\

1703: \cline{1-3}

1704: \multicolumn{3}{c}{

1705:   $\underline{(): ([a]=[~] \And z=[~]) \Or B_2 \Or B_3 \Goes{} \theta''}$

1706: } \\

1707: \multicolumn{3}{c}{

1708:   $(): d(a,[a], z) \Goes{} \theta''$

1709: } \\

1710: \end{tabular}

1711: \end{center}

1712: 

1713: \caption{A sample computation in the liberal completed semantics.

1714:   $B_1 \Or B_2 \Or B_3$ is the body of the clause defining $d$

1715:   from the second program in Section 3, with parameters

1716:   instantiated.  Not all substitutions are listed in full.

1717: }

1718: \label{delete-example-lc-fig}

1719: \end{figure}

1720: 

1721: Figure \ref{delete-example-lc-fig} shows a sample computation in

1722: the liberal completed semantics, using the second, one-clause

1723: version of the delete program from Section 3.  ($\theta''$ is the

1724: substitution $[ys:=[~],z:=[~]]$.)  Note that

1725: although the number of steps is similar to that of the liberal

1726: general computation, now the elements of a goal stack are simply

1727: formulas.  This will simplify our analysis,

1728: since we can focus on formulas rather than having to

1729: deal with the interaction of formulas and sequences of clauses

1730: with cuts.

1731: 

1732: \subsection{Inadequacy of Liberal Semantics}

1733: \label{inadequate-section}

1734: 

1735: \begin{figure}[tp]

1736: 

1737: \begin{center}

1738: \begin{tabular}{ccc}

1739: \cline{1-1}

1740: $[x:=0]: \epsilon \Goes{} [x:=0]$ \\

1741: \cline{1-1} \cline{3-3}

1742: $(): x=0 \Goes{} [x:=0]$

1743:   & \Sep &

1744:   $[x:=1]: \epsilon \Goes{} [x:=1]$ \\

1745: \cline{1-1} \cline{3-3}

1746: $(): \Not(x=0) \Goes{} fail$

1747:   & \Sep &

1748:   $(): x=1 \Goes{} [x:=1]$ \\

1749: \cline{1-3}

1750: \multicolumn{3}{c}{

1751:   $(): \Not(\Not(x=0)), x=1 \Goes{} [x:=1]$

1752: } \\

1753: \multicolumn{3}{c}{

1754:   $\overline{(): \Not(\Not(x=0)) \And x=1 \Goes{} [x:=1]}$

1755: } \\

1756: \end{tabular}

1757: \end{center}

1758: \vspace{2mm}

1759: 

1760: \begin{center}

1761: \begin{tabular}{ccc}

1762: $\overline{(): \epsilon \Goes{} ()}$ \\

1763: $\overline{(): 0=0 \Goes{} ()}$ \\

1764: \cline{1-1} \cline{3-3}

1765: $(): \Not(0=0) \Goes{} fail$

1766:   & \Sep &

1767:   $(): 0=1 \Goes{} fail$ \\

1768: \cline{1-3}

1769: \multicolumn{3}{c}{

1770:   $(): \Not(\Not(0=0)), 0=1 \Goes{} fail$

1771: } \\

1772: \multicolumn{3}{c}{

1773:   $\overline{(): \Not(\Not(0=0)) \And 0=1 \Goes{} fail}$

1774: } \\

1775: \end{tabular}

1776: \end{center}

1777: \vspace{2mm}

1778: 

1779: \begin{center}

1780: \begin{tabular}{ccc}

1781: \cline{1-1} \cline{3-3}

1782: $(): a=0 \Goes{} fail$

1783:   & \Sep &

1784:   $(): \epsilon \Goes{} ()$ \\

1785: \cline{1-3}

1786: \multicolumn{3}{c}{

1787:   $(): \Not(a=0) \Goes{} ()$

1788: } \\

1789: \multicolumn{3}{c}{

1790:   $\overline{(): \Not(\Not(a=0)), a=1 \Goes{} fail}$

1791: } \\

1792: \multicolumn{3}{c}{

1793:   $\overline{(): \Not(\Not(a=0)) \And a=1 \Goes{} fail}$

1794: } \\

1795: \end{tabular}

1796: \end{center}

1797: 

1798: \caption{Computations showing that the goal 

1799:   $\Not(\Not(x=0)) \And x=1$ violates the success property

1800:   in the liberal completed semantics.

1801:   $a$ is some arbitrary ground term not identical to 0.

1802: }

1803: \label{unsound-examplea-lc-fig}

1804: \end{figure}

1805: 

1806: 

1807: 

1808: \begin{figure}[tp]

1809: 

1810: \begin{center}

1811: \begin{tabular}{c}

1812: \cline{1-1}

1813:   $[x:=0]: \epsilon \Goes{} [x:=0]$ \\

1814: \cline{1-1}

1815:   $(): x=0 \Goes{} [x:=0]$ \\

1816: \cline{1-1}

1817:   $(): \Not(x=0), x=1 \Goes{} fail$ \\

1818: \cline{1-1}

1819:   $(): \Not(x=0) \And x=1 \Goes{} fail$ \\

1820: \end{tabular}

1821: \end{center}

1822: \vspace{2mm}

1823: 

1824: \begin{center}

1825: \begin{tabular}{ccc}

1826: \cline{3-3}

1827: ~

1828:   & \Sep &

1829:   $(): \epsilon \Goes{} ()$ \\

1830: \cline{1-1} \cline{3-3}

1831: $(): 1=0 \Goes{} fail$

1832:   & \Sep &

1833:   $(): 1=1 \Goes{} ()$ \\

1834: \cline{1-3}

1835: \multicolumn{3}{c}{

1836:   $(): \Not(1=0), 1=1 \Goes{} ()$

1837: } \\

1838: \multicolumn{3}{c}{

1839:   $\overline{(): \Not(1=0) \And 1=1 \Goes{} ()}$

1840: } \\

1841: \end{tabular}

1842: \end{center}

1843: 

1844: \caption{Computations showing that the goal 

1845:   $\Not(x=0) \And x=1$ violates the failure property

1846:   in the liberal completed semantics.

1847: }

1848: \label{unsound-exampleb-lc-fig}

1849: \end{figure}

1850: 

1851: 

1852: Because it is intended to capture the behaviour of Prolog

1853: programs with cut, the liberal completed semantics does not

1854: have either of the witness properties.  Figure

1855: \ref{unsound-examplea-lc-fig} shows that the goal formula

1856: $G_1 \equiv \Not(\Not(x=0)) \And x=1$ succeeds in the liberal

1857: completed semantics, even though

1858: $G_1[x:=0]$ fails and $G_1[x:=a]$, where $a$ is any arbitrary

1859: ground term not identical to 0, fails.

1860: Similarly, Figure \ref{unsound-exampleb-lc-fig} shows that the

1861: goal formula $G_2 \equiv \Not(x=0) \And x=1$ fails in the liberal

1862: completed semantics, even though

1863: $G_2[x:=1]$ succeeds.

1864: 

1865: This is consistent with the behaviour of

1866: the usual unsound implementation of negation as failure.  We

1867: can, of course, ban unsound NAF alone with a mode restriction

1868: similar to that of \Staerk{} \cite{staerk-lptp-jlp}; however, if

1869: we retain the general {\it if} construct (corresponding to the hard

1870: cut), we will still permit behaviour which violates the witness

1871: properties.  This suggests that we need some further restriction

1872: to {\it if} analogous to \Staerk{}'s restriction on negation.

1873: 

1874: Note that these counterexamples also show that the liberal

1875: general semantics (a generalization of the liberal completed

1876: semantics) has neither of the witness properties.

1877: 

1878: 

1879: 

1880: \section{The Conservative Operational Semantics}

1881: \label{conservative-section}

1882: 

1883: In the last section, we gave operational semantics for programs

1884: which characterized Prolog computation, but were inadequate from

1885: a logic-programming point of view because they violated

1886: the witness properties.  In this section, we repair the faults

1887: of the liberal semantics by placing simple restrictions on some

1888: of its rules.  The result is the {\it conservative} semantics,

1889: which does enjoy the witness properties.  We refer to the form

1890: of cut embodied in the conservative semantics as {\it firm} cut.

1891: 

1892: In Section \ref{conservative-rules-section}, we present and

1893: describe the rules for the conservative semantics, and in

1894: Section \ref{conservative-properties-section} we prove useful

1895: properties of it, including the witness properties.  Finally, in

1896: \ref{implementation-section} we show that the firm cut still

1897: permits the useful first-solution behaviour of the Prolog cut.

1898: 

1899: 

1900: \subsection{The Conservative Semantics Rules}

1901: \label{conservative-rules-section}

1902: 

1903: \begin{figure}[tp]

1904: 

1905: \noindent

1906: \Rule{Not/succ:}

1907:   {\theta: B \Goes{} \theta'}

1908:   {\theta: \Not B, \alpha \Goes{} fail}

1909:   {where $B$ has no free variables}

1910: \\ %

1911: \Rule{Not/fail:}

1912:   {\theta: B \Goes{} fail  \Sep  \theta: \alpha \Goes{} \rho}

1913:   {\theta: \Not B, \alpha \Goes{} \rho}

1914:   {where $B$ has no free variables}

1915: \\ %

1916: \Rule{Not/flounder:}

1917:   {}

1918:   {\theta: \Not B, \alpha \Goes{} flounder}

1919:   {where $B$ has free variables}

1920: \\ %

1921: \Rule{Not/sub:}

1922:   {\theta: B \Goes{} \rho}

1923:   {\theta: \Not B, \alpha \Goes{} \rho}

1924:   {where $B$ has no free variables, and $\rho$ is $flounder$ or $diverge$}

1925: \\ %

1926: \Rule{If/succ:}

1927:   {\theta: B[\vec{x}:=\vec{x}'] \Goes{} \theta'  \Sep

1928:    \theta': C[\vec{x}:=\vec{x}']\theta', \alpha \Goes{} \rho}

1929:   {\theta: if[\vec{x}](B,C), \alpha \Goes{} \rho}

1930:   {where $\exists \vec{x}(B)$ has no free variables, and

1931:    $\vec{x}'$ do not appear in the conclusion}

1932: \\ %

1933: \Rule{If/fail:}

1934:   {\theta: B[\vec{x}:=\vec{x}'] \Goes{} fail}

1935:   {\theta: if[\vec{x}](B,C), \alpha \Goes{} fail}

1936:   {where $\exists \vec{x}(B)$ has no free variables, and

1937:    $\vec{x}'$ do not appear in the conclusion}

1938: \\ %

1939: \Rule{If/flounder:}

1940:   {}

1941:   {\theta: if[\vec{x}](B,C), \alpha \Goes{} flounder}

1942:   {where $\exists \vec{x}(B)$ has free variables}

1943: \\ %

1944: \Rule{If/sub:}

1945:   {\theta: B[\vec{x}:=\vec{x}'] \Goes{} \rho}

1946:   {\theta: if[\vec{x}](B,C), \alpha \Goes{} \rho}

1947:   {where $\exists \vec{x}(B)$ has no free variables, and

1948:    $\vec{x}'$ do not appear in the conclusion, and $\rho$

1949:    is $flounder$ or $diverge$}

1950: 

1951: \caption{

1952:   The rules of the [Conservative Choice] fragment, for

1953:   computing the choice constructs in a more restricted fashion.

1954: }

1955: \label{conservative-choice-fragment-fig}

1956: \end{figure}

1957: 

1958: \begin{figure}[tp]

1959: 

1960: \begin{center}

1961: \begin{tabular}{c}

1962: \cline{1-1}

1963:   $(): \Not(x=0), x=1 \Goes{} flounder$ \\

1964: \cline{1-1}

1965:   $(): \Not(x=0) \And x=1 \Goes{} flounder$ \\

1966: \end{tabular}

1967: \end{center}

1968: 

1969: \caption{The safe computation of

1970:   $\Not(x=0) \And x=1$ in the conservative semantics.

1971: }

1972: \label{unsound-exampleb-c-fig}

1973: \end{figure}

1974: 

1975: The conservative operational semantics 

1976: restricts the computation of negation and {\it if}.

1977: Whereas the liberal completed semantics is made up of the

1978: rules fragments

1979: [Basic] (Fig.\ \ref{basic-rules-fig}),

1980: [Liberal Choice] (Fig.\ \ref{lib-choice-rules-fig}), and

1981: [Completed Predicates] (Fig.\ \ref{completed-preds-rule-figure}),

1982: the conservative semantics is made up of the rules fragments

1983: [Basic], [Conservative Choice], and [Completed Predicates].

1984: The rules for the new fragment, [Conservative Choice], are in

1985: Figure \ref{conservative-choice-fragment-fig}.

1986: 

1987: Consider the rules Not/succ and Not/fail from [Conservative

1988: Choice].  These rules are the same as those of the [Liberal

1989: Choice] fragment, except that they have the restriction that $B$

1990: (the negated formula) must have no free variables.  When $B$

1991: does have free variables, a new rule, Not/flounder, applies.

1992: Not/flounder states that a goal stack beginning with a negated

1993: formula with free variables immediately returns a new result,

1994: $flounder$, indicating that the computation cannot continue

1995: at this point.

1996: 

1997: Another new rule, Not/sub, defines what happens when $B$ has no

1998: free variables, but the sub-computation itself flounders: the

1999: $flounder$ result is passed on.  Note that the rules in the

2000: [Basic] and [Completed Predicates] fragments are already described in

2001: such a way that they also automatically pass on the new $flounder$

2002: result.  Hence, $flounder$ acts as a kind of run-time exception,

2003: which causes the computation to terminate immediately.\footnote{

2004:   Not/sub also passes on the result $diverge$, which is not

2005:   needed until Section \ref{pessimistic-sec}.

2006: }

2007: 

2008: The conservative rules for the $if$ connective are constructed

2009: from those of the liberal rules in a similar manner, modulo the

2010: bound variables of the $if$.  As an example of a conservative

2011: computation, consider again the goal $\Not(x=0) \And x=1$,

2012: which was a problem for the liberal semantics.  Figure

2013: \ref{unsound-exampleb-c-fig} shows that the conservative

2014: semantics handles it in a sound way, by immediately stating that

2015: it flounders.

2016: 

2017: We should note at this point that there are other approaches

2018: to the problem of handling negation in a sound way.  Loveland and Reed,

2019: for example \cite{loveland-near-horn}, define a resolution

2020: method by which queries against programs with negation

2021: can be evaluated in a sound and complete manner.  Dahl

2022: \cite{dahl-negation} defines an approach which delays the

2023: evaluation of a negated goal until it becomes ground, and

2024: an approach which, within a negated goal's computation,

2025: blocks only the unification of variables which are free

2026: outside the scope of the negation.

2027: Di Pierro et al.\ \cite{IC::PierroMP1995}

2028: define an approach in which an existentially closed negated atom

2029: (a formula of the form $\exists[\Not A]$)

2030: succeeds iff all branches of the SLD-tree of the atom either

2031: fail or instantiate the atom.  Some of these methods

2032: have been implemented in a variety of systems, for instance in

2033: Naish's NU-Prolog \cite{naish-negation-lncs}.  Here we are

2034: motivated by our interest in the features implemented

2035: in the most widely-used Prolog systems.  Most Prolog systems

2036: implement the simple negation as failure characterized by

2037: the liberal semantics and restricted by the conservative

2038: semantics.

2039: 

2040: \subsection{Properties of the Conservative Semantics}

2041: \label{conservative-properties-section}

2042: 

2043: In this section, we prove the properties of the conservative

2044: operational semantics that we wanted to hold.  First, we prove

2045: the correspondence of computations in the liberal and the

2046: conservative semantics.  Then, we prove the witness properties.

2047: 

2048: \subsubsection{Correspondence of Computations}

2049: 

2050: First, we note that successful and failing computations in

2051: the conservative semantics correspond to successful and

2052: failing computations in the liberal completed semantics.

2053: 

2054: \begin{thm}

2055:   If $\theta: \alpha \Goes{} \rho$ in the conservative

2056:   semantics, and $\rho$ is not $flounder$, then

2057:   $\theta: \alpha \Goes{} \rho$ in the liberal completed

2058:   semantics.

2059: \end{thm}

2060: 

2061: \begin{proof}

2062: Any computation in the conservative semantics which

2063: contains applications of the Not/flounder or If/flounder rules

2064: must result in $flounder$, since the $flounder$ outcomes of

2065: these rules descend through all other rules in the [Basic],

2066: [Conservative choice] and [Completed predicates] fragments.

2067: Therefore if a computation in the conservative semantics

2068: does not result in $flounder$, it must not use those rules;

2069: rather, it uses only the

2070: other Not and If rules, which are

2071: restrictions of those in the liberal completed semantics,

2072: and the other rules, which are identical to those in the

2073: liberal completed semantics.

2074: Such a computation is, in fact, a computation in the liberal

2075: completed semantics.  

2076: \end{proof}

2077: 

2078: The converse does not hold, since successful and failing

2079: computations in the liberal completed semantics may flounder

2080: in the conservative semantics.  However, all

2081: computations in the liberal completed semantics do correspond

2082: to some kind of computations in the conservative semantics,

2083: as the next theorem shows.

2084: 

2085: \begin{thm}

2086:   If $\theta: \alpha \Goes{} \rho$ in the liberal completed

2087:   semantics, then there is some $\rho'$ such that

2088:   $\theta: \alpha \Goes{} \rho'$ in the conservative

2089:   semantics, and $\rho'$ is either $\rho$ or $flounder$.

2090: \end{thm}

2091: 

2092: \begin{proof}

2093: By induction on the structure of the liberal completed

2094: computation.  Cases are on the bottommost rule application.

2095: 

2096: All applications of rules with 0 premises correspond to rule

2097: applications in the conservative semantics.

2098: 

2099: If the bottommost rule is Disj/fail:

2100: the bottommost judgement is of the form

2101: $(\theta: B \Or C, \alpha \Goes{} fail)$,

2102: and its left-hand premise judgement

2103: is of the form $(\theta: B, \alpha \Goes{} fail)$.

2104: By the induction hypothesis (IH), either 

2105: $(\theta: B, \alpha \Goes{} fail)$ in the conservative semantics,

2106: or $(\theta: B, \alpha \Goes{} flounder)$ in the conservative semantics.

2107: In the first case, the result follows directly from another

2108: application of the IH;

2109: in the second case, the result follows from one application of the

2110: Disj/nofail rule.

2111: 

2112: The cases for the Not and If rules are similar to that of Disj/fail.

2113: Applications of all other

2114: rules in the liberal completed computation have exactly one

2115: premise, and correspond to applications of the same rules in the

2116: conservative computation. 

2117: \end{proof}

2118: 

2119: Examples of goals whose outcomes differ in the liberal completed

2120: and conservative semantics are as follows:

2121: \begin{itemize}

2122: \item The goal $\Not\Not(x=0)$ succeeds in the liberal

2123:   completed semantics, but flounders in the conservative semantics.

2124: \item The goal $\Not(x=0)$ fails in the liberal

2125:   completed semantics, but flounders in the conservative semantics.

2126: \item The goal $\Not\Not(x=0) \And loop(x)$,

2127:   where the predicate $loop$ is defined with the definition

2128:   $loop(x) \colondash loop(x)$, diverges (does not have any

2129:   finite computation) with respect to the liberal completed

2130:   semantics; however, it flounders in the conservative

2131:   semantics.

2132: \end{itemize}

2133: These examples, along with the witness properties to be proven

2134: next, show that although strictly fewer goals succeed or fail in

2135: the conservative semantics, strictly more goals terminate in the

2136: conservative semantics.

2137: 

2138: \subsubsection{The Witness Properties}

2139: \label{witness-properties-section}

2140: 

2141: Finally, we show the witness properties of the conservative

2142: semantics.  Most proofs are contained in full in Appendix

2143: \ref{proofs-appx}.

2144: 

2145: We begin with some useful definitions.

2146: We say that {\it $\theta$ is a specialization of $\theta'$},

2147: in symbols $\theta \subseteq \theta'$, if there is some

2148: $\theta''$ such that $x\theta \equiv x\theta'\theta''$,

2149: for all variables $x$ in the domain of $\theta'$.

2150: Given a set $V$ of variables and a substitution $\theta$,

2151: we say that a substitution $\xi$ {\it grounds $V$ consistent

2152: with $\theta$} if $\xi \subseteq \theta$ and $x\xi$ is

2153: ground for every $x \in V$.

2154: 

2155: An inductive generalization of the failure property can be

2156: proven directly; the corresponding generalization of the

2157: success property requires a technical lemma.  These three

2158: lemmas are as follows.

2159: 

2160: \begin{lemma}[General Failure Property of Conservative Semantics]

2161:   \label{general-failure-property-lemma}

2162:   Let $\theta, \alpha$ be such that

2163:   $(\theta: \alpha \Goes{} fail)$ in the conservative semantics.

2164:   Then for any $\xi$,

2165:   $(\theta: \alpha\xi \Goes{} fail)$ in the conservative semantics.

2166: \end{lemma}

2167: 

2168: \begin{proof}

2169: See Appendix \ref{proofs-appx}. 

2170: \end{proof}

2171: 

2172: \begin{lemma}[Substitution Monotonicity of Conservative Semantics]

2173:   \label{substitution-monotonicity-lemma}

2174:   Let $\theta, \alpha$ be such that $\alpha\theta \equiv \alpha$ and

2175:   $\theta: \alpha \Goes{} \theta'$ in the conservative semantics.

2176:   Then $\theta' \subseteq \theta$.

2177: \end{lemma}

2178: 

2179: \begin{proof}

2180: See Appendix \ref{proofs-appx}. 

2181: \end{proof}

2182: 

2183: \begin{lemma}[General Success Property of Conservative Semantics]

2184:   \label{general-success-property-lemma}

2185:   Let $\theta, \alpha$ be such that

2186:   $\theta: \alpha \Goes{} \theta'$ in the conservative semantics.

2187:   Let $V$ be a subset of the free variables of $\alpha$.

2188:   Then for any $\xi$ grounding $V$ consistent with $\theta'$,

2189:   $\theta: \alpha\xi \Goes{} \theta'\xi$ in the conservative semantics.

2190: \end{lemma}

2191: 

2192: \begin{proof}

2193: See Appendix \ref{proofs-appx}. 

2194: \end{proof}

2195: 

2196: We can now state and prove the witness properties mentioned in

2197: the Introduction for the conservative semantics.  First, we

2198: define more precisely what we mean by success and failure.

2199: 

2200: We say that a goal $G$ {\it succeeds} (in the conservative semantics)

2201: if there is a computation with a conclusion of the form $(): G \Goes{} \theta'$.

2202: We say that a goal $G$ {\it fails}

2203: if there is a computation with a conclusion of the form $(): G \Goes{} fail$.

2204: 

2205: \begin{thm}[Witness Properties of the Conservative Semantics] ~ \\

2206:   (1) If a goal $G$ succeeds, then some ground instance of $G$ succeeds. \\

2207:   (2) If a goal $G$ fails, then any ground instance of $G$ fails.

2208: \end{thm}

2209: 

2210: \begin{proof}

2211: (1) If $G$ succeeds, this means there is a $\theta'$ such that

2212: $(): G \Goes{} \theta'$.  Let $\sigma$ be the substitution which substitutes

2213: all free variables of $G\theta'$ by 0.  Let $\xi$ be the substitution

2214: which substitutes any variable $x \in FV(G)$ by $x\theta'\sigma$.

2215: Then $\xi$ grounds $FV(G)$ consistent with $\theta'$. By the

2216: General Success Property, we have that $(): G\xi \Goes{} \theta'\xi$.

2217: Thus the ground instance $G\xi$ of $G$ succeeds.

2218: 

2219: (2) If $G$ fails, then $(): G \Goes{} fail$.  By the General Failure

2220: Property, for any $\xi$, including those grounding all variables

2221: in $FV(G)$, we have that $(): G\xi \Goes{} fail$.  Thus all ground

2222: instances of $G$ fail.  

2223: \end{proof}

2224: 

2225: 

2226: \subsection{Implementation Issues}

2227: \label{implementation-section}

2228: 

2229: In this section, we discuss some implementation-related issues.

2230: We show that the conservative semantics retains the

2231: desirable first-solution behaviour of the Prolog hard cut.

2232: We also discuss the possibility of turning the mode restriction

2233: of the conservative semantics into a static rather than a

2234: dynamic one.

2235: 

2236: \subsubsection{First Solution Behaviour}

2237: 

2238: When we have a formula of the form $if[\vec{x}](B, C)$,

2239: the conservative operational semantics allows the $\vec{x}$

2240: variables to pass on to $C$, and allows free variables other

2241: than $\vec{x}$ in $C$; however, only the first successful

2242: substitution for $\vec{x}$ is passed on.  The conservative

2243: semantics therefore still allows the useful ``first

2244: solution'' behaviour which $if$ has inherited from cut.

2245: 

2246: For an example of this behaviour, consider the following

2247: problem.  We define an {\em association list} as a list of terms

2248: of the form $a(k,j)$, where $k$ is a key and $j$ is a value

2249: associated with it.  A problem commonly encountered in symbolic

2250: programming is to extract the first value (and only the first

2251: value) associated with a key in an association list, which is

2252: taken as the ``current'' value of the key.

2253: We can write the standard logic programming ``member'' predicate as

2254: \[ m(x,y) \colondash

2255:    \exists yh \exists yt (y=[yh|yt] \And (x=yh \Or m(x,yt))) \]

2256: and then write a predicate which solves the first-value problem as follows:

2257: \[ v(x, y, z) \colondash if[w](m(a(y,w), x), z=w) \]

2258: The predicate call $v(x, y, z)$, where $x$ is an association

2259: list, $y$ is a key, and $z$ is any term, succeeds iff $z$ is the

2260: first value associated with $y$ in $x$.

2261: 

2262: \begin{figure}

2263: 

2264: \noindent

2265: Computation of $m$ subgoal:

2266: \begin{center}

2267: \begin{tabular}{c}

2268: $\overline{

2269:   [yh:=a(b,0),yt:=[a(b,1)],w:=0]: \epsilon \Goes{} [w:=0]

2270: }$ \\

2271: $\overline{

2272:   [yh:=a(b,0),yt:=[a(b,1)]]: a(b,0)=a(b,w) \Goes{} [w:=0]

2273: }$ \\

2274: $\overline{\underline{

2275:   [yh:=a(b,0),yt:=[a(b,1)]]: a(b,0)=a(b,w) \Or m(a(b,w),[a(b,1)] \Goes{} [w:=0]

2276: }}$ \\

2277: $(): [a(b,0),a(b,1)]=[yh|yt], (yh=a(b,w) \Or m(a(b,w),yt) \Goes{} [w:=0]

2278: $ \\

2279: $\overline{

2280:   (): [a(b,0),a(b,1)]=[yh|yt] \And (yh=a(b,w) \Or m(a(b,w),yt) \Goes{} [w:=0]

2281: }$ \\

2282: $\overline{

2283:   (): \exists yt([a(b,0),a(b,1)]=[yh|yt] \And (yh=a(b,w) \Or m(a(b,w),yt)))

2284:       \Goes{} [w:=0]

2285: }$ \\

2286: $\overline{\underline{

2287:   (): \exists yh \exists yt([a(b,0),a(b,1)]=[yh|yt] \And (yh=a(b,w) \Or m(a(b,w),yt)))

2288:       \Goes{} [w:=0]

2289: }}$ \\

2290: $(): m(a(b,w),[a(b,0),a(b,1)]) \Goes{} [w:=0]$ \\

2291: \end{tabular}

2292: \end{center}

2293: 

2294: \noindent

2295: Successful computation:

2296: \begin{center}

2297: \begin{tabular}{ccc}

2298: \cline{3-3}

2299: (see above) & & $[w:=0,z:=0]: \epsilon \Goes{} [z:=0]$ \\

2300: \cline{1-1} \cline{3-3}

2301: $(): m(a(b,w),[a(b,0),a(b,1)]) \Goes{} [w:=0]$

2302:   & \Sep &  $[w:=0]: z=0 \Goes{} [z:=0]$ \\

2303: \cline{1-3}

2304: \multicolumn{3}{c}{

2305:   $\underline{(): if[w](m(a(b,w),[a(b,0),a(b,1)]), z=w) \Goes{} [z:=0]}$

2306: } \\

2307: \multicolumn{3}{c}{

2308:   $(): v([a(b,0),a(b,1)], b, z) \Goes{} [z:=0]$

2309: } \\

2310: \end{tabular}

2311: \end{center}

2312: 

2313: \noindent

2314: Failing computation:

2315: \begin{center}

2316: \begin{tabular}{ccc}

2317: (see above) \\

2318: \cline{1-1} \cline{3-3}

2319: $(): m(a(b,w),[a(b,0),a(b,1)]) \Goes{} [w:=0]$

2320:   & \Sep &  $[w:=0]: 1=0 \Goes{} fail$ \\

2321: \cline{1-3}

2322: \multicolumn{3}{c}{

2323:   $\underline{(): if[w](m(a(b,w),[a(b,0),a(b,1)]), 1=w) \Goes{} fail}$

2324: } \\

2325: \multicolumn{3}{c}{

2326:   $(): v([a(b,0),a(b,1)], b, 1) \Goes{} fail$

2327: } \\

2328: \end{tabular}

2329: \end{center}

2330: 

2331: \caption{

2332:   Examples showing first-solution behaviour of conservative

2333:   semantics.  (Some substitutions are simplified for clarity.)

2334:   Top: a computation returning the first solution to a call to the

2335:   membership predicate.  Middle:  a computation

2336:   showing that the first solution is selected by $if$.

2337:   Bottom: a computation showing that subsequent solutions are not

2338:   selected by $if$.

2339: }

2340: \label{alist-example-revised-fig}

2341: \end{figure}

2342: 

2343: The query $v([a(b,0),a(b,1)], b, z)$ to this program should

2344: result in the binding $[z:=0]$, since this is the first value

2345: returned by $m$ as associated with the key $b$ in the list.

2346: However, the query $v([a(b,0),a(b,1)], b, 1)$ to this program

2347: should fail; even though the value 1 is associated with $b$

2348: later in the list, $if$ should select only the first solution.

2349: Figure \ref{alist-example-revised-fig} shows that this is indeed

2350: the behaviour of the conservative semantics.

2351: 

2352: We could evidently get closer to the liberal general

2353: semantics by allowing the first subformula of the $if$

2354: to be computed with free variables,

2355: as long as those variables do not get bound in the course of

2356: the computation, as suggested by one of Dahl's negation

2357: strategies \cite{dahl-negation} and Di Pierro et al.\ \cite{IC::PierroMP1995}.

2358: Since this

2359: would complicate the operational semantics and our analysis,

2360: we have decided to stick with the conservative

2361: semantics as given.

2362: 

2363: \subsubsection{Static Analysis}

2364: 

2365: \label{mode-checking-discussion-section}

2366: The conservative operational semantics restricts the behaviour

2367: of the logic programming system by essentially enforcing mode

2368: checks at run time.  However, we do not believe that there is

2369: any obstacle to doing static mode checking (see for example

2370: \cite{barbuti-martelli-1990,apt-marchiori,gabbrielli-etalle-1999})

2371: in order to catch programs at compile time which

2372: could result in floundering goals.  (In \cite{andrews-cut-tr},

2373: a static analysis scheme is proposed which does a

2374: fine-grained analysis in order to reject as few programs as

2375: possible, at the expense of some complexity.)

2376: 

2377: %Because the conservative semantics behaves identically to the

2378: %liberal semantics on non-floundering goals, and because the

2379: %liberal semantics characterizes Prolog, this implies that an

2380: %implementation of firm cut should be achievable simply by

2381: %imposing static mode restrictions on a conventional logic

2382: %programming system.  For the sake of brevity, we do not explore

2383: %this issue further here, but assume in the rest of the paper

2384: %that such a static analysis system is possible.

2385: 

2386: Because the conservative semantics behaves identically to the

2387: liberal semantics on non-floundering goals, and because the

2388: liberal semantics characterizes Prolog, we believe that an

2389: implementation of firm cut is achievable simply by

2390: imposing static mode restrictions on a conventional logic

2391: programming system.  For the sake of brevity, we do not explore

2392: this issue further here, but assume in the rest of the paper

2393: that such a static analysis system is possible.

2394: 

2395: 

2396: 

2397: \section{The Abstract Semantics}

2398: \label{sems-section}

2399: 

2400: In this section, we present an abstract semantics for the

2401: conservative operational semantics.  The abstract semantics does

2402: not reify such notions as substitution sequence and unification;

2403: rather, the central element of the semantics which deals with

2404: free variables is the interpretation of the existential quantifier

2405: by a valuation function of the same form as those of classical

2406: truth theory \cite{kripke,fitting-kripke}.

2407: This suggests that the conservative semantics and firm cut

2408: have a deeper connection to logic than simply permitting some

2409: logical computations.

2410: 

2411: The abstract semantics is in the UNV

2412: (unfolding-normal-form-valuation) style \cite{andrews-lnaf-tcs},

2413: and it depends on the witness properties to achieve soundness

2414: and completeness.  In UNV semantics, we associate a truth value

2415: to a goal; the truth value can be described as the maximally

2416: defined truth value among the valuations of the normal forms of

2417: the unfoldings of the goal.  We doubt that it is possible to

2418: give such a semantics for the liberal semantics and thus for

2419: Prolog with hard cut, due to those systems' failure to achieve

2420: the witness properties.

2421: 

2422: We begin with an overview of UNV semantics in

2423: Section \ref{overview-section}

2424: containing some basic definitions, including that of an

2425: (operational) {\it outcome} of a goal $G$ with respect to a

2426: program $P$, $outcome_P(G)$.  Section \ref{overview-section}

2427: also contains a ``roadmap'' of the series of results that

2428: follow, referred to as the ``raising lemmas''.

2429: %

2430: In Sections \ref{unfoldings-section} through \ref{denotation-section}

2431: we proceed, through the raising lemmas, to systematically raise the

2432: characterizing expression for $outcome_P(G)$ to greater and

2433: greater levels of abstraction, until all operational notions

2434: have been abstracted away.

2435: %Section \ref{unfoldings-section} has to do with the notion of

2436: %unfolding of a goal, and its relationship to a ``pessimistic''

2437: %operational semantics which assumes that all predicates diverge;

2438: %it ends with the first raising lemma, which in some sense abstracts

2439: %away considerations of predicate calls.

2440: %Section \ref{dfnf-section} shows how every goal can be put into

2441: %a ``depth-first'' normal form, which is

2442: %operationally identical to the original goal; it ends with the

2443: %second raising lemma, which shows that we can restrict our attention

2444: %to goals in depth-first normal form.

2445: %Section \ref{valuation-section} gives a compositional valuation

2446: %function for goals in depth-first normal form; it ends with the

2447: %third raising lemma, which proves the equivalence of the

2448: %operational outcome of a goal in this form with its valuation.

2449: 

2450: Finally, in Section \ref{denotation-section}, we link the

2451: previous raising lemmas into a final characterization of outcome

2452: of a general goal with respect to a program, and give an

2453: expression describing the abstract denotation of a program.

2454: We conclude with an example, in Section

2455: \ref{sems-example-section}, and some discussion in Section

2456: \ref{sems-discussion-section}.

2457: 

2458: In this section, whenever we refer to a program $P$ and a goal

2459: $G$, we assume that $G$ does not yield the $flounder$ result.

2460: It may also be possible to characterize the $flounder$ result,

2461: as in, for instance, \cite{andrews-lnaf-tcs}.

2462: However, for simplicity, here we assume that programs will be subject

2463: to a static analysis which excludes those able to generate such

2464: a result, as discussed in Section \ref{mode-checking-discussion-section}.

2465: 

2466: \subsection{UNV Semantics}

2467: \label{overview-section}

2468: 

2469: \begin{figure}[tp]

2470: 

2471: \centerline

2472: {\epsffile{unvsmall.eps}

2473: }\vspace{5mm}

2474: 

2475: \caption{

2476:   Diagram of the basic notions of UNV

2477:   (unfolding-normal-form-valuation) semantics.

2478: }

2479: \label{unv-fig}

2480: \end{figure}

2481: 

2482: Here we give an overview of UNV semantics and some basic

2483: definitions which will be used throughout the section.

2484: We also give a ``roadmap'' of the results which will be

2485: proven.

2486: 

2487: \subsubsection{Overview}

2488: 

2489: The UNV semantics given here is based on six basic notions:

2490: \begin{itemize}

2491: \item The three {\it truth values} $T$, $F$ and $U$, or

2492:   ``true'', ``false'', and ``undefined''.

2493: \item The {\it definedness ordering} on truth values, which ranks

2494:   $T$ and $F$ as being more defined than $U$.

2495: \item The {\it alethic} or {\it truth ordering} on truth values,

2496:   which ranks $U$ as ``more true'' than $F$ and $T$ as ``more

2497:   true'' than $U$.

2498: \item The {\it unfoldings} of a goal, which are the formulas

2499:   obtained from the goal by expanding zero or more predicate

2500:   calls, possibly repeatedly.

2501: \item The {\it depth-first normal form}, or DFNF, of a goal,

2502:   which is a formula closely related to the disjunctive

2503:   normal form (DNF) of the goal.

2504: \item The {\it valuation} $v(G)$ of a goal $G$ in DFNF, which is

2505:   a compositional function from formulas to truth values.

2506: \end{itemize}

2507: The last three of these will be given more precise and detailed

2508: definitions in the course of this section.

2509: 

2510: A schematic diagram of the basic notions of UNV semantics is

2511: contained in Figure \ref{unv-fig}.  Given a goal $G$, we

2512: consider all the (possibly infinitely many) unfoldings

2513: $G_1, G_2, G_3, \ldots, G_n, \ldots$

2514: of the goal.  Then, we find the DFNFs of all the unfoldings,

2515: resulting in the normal-form goals

2516: $G'_1, G'_2, G'_3, \ldots, G'_n, \ldots$.

2517: We apply the valuation function

2518: $v$ to the normal-form goals, getting a set

2519: $V_1, V_2, V_3, \ldots, V_n, \ldots$ of truth values, each of

2520: them equal to either $T$, $F$, or $U$.

2521: (The alethic ordering of truth values is used to compute the

2522: valuation of existentially-quantified goals.)

2523: There will be one unique maximally defined truth value in this

2524: set; this will be taken as the truth value of the original goal $G$.

2525: 

2526: \subsubsection{Outcomes of Goals}

2527: 

2528: When we evaluate a goal in a logic programming system, we expect

2529: to receive a substitution (if one exists) as the result of the

2530: evaluation.  However, when we prove properties of logic programs,

2531: we are more interested in proving whether a general pattern of

2532: goals succeeds or fails; we are less interested in obtaining

2533: substitutions, because there may be a different substitution for

2534: each different instance of the pattern.  Hence, in this paper (as in

2535: \cite{andrews-phd-dd,andrews-lnaf-tcs,staerk-lptp-jlp}) we take

2536: the ``observable'' of interest to be whether a goal succeeds, fails

2537: or diverges, linking these observables to the truth values $T$,

2538: $F$ and $U$ respectively.

2539: 

2540: We therefore define the {\it outcome} of a goal $G$ with

2541: respect to $P$, $outcome_P(G)$, as follows.

2542: \begin{itemize}

2543: \item If there is a $\theta'$ such that $((): G \Goes{P} \theta')$

2544:   in the conservative operational semantics, then $outcome_P(G) = T$.

2545: \item If $((): G \Goes{P} fail)$ in the conservative operational semantics,

2546:   then $outcome_P(G) = F$.

2547: \item Otherwise (i.e., if there is no result $\rho$ such that

2548:   $((): G \Goes{P} \rho)$ in the conservative semantics), then

2549:   $outcome_P(G) = U$.

2550: \end{itemize}

2551: This notion of outcome will be what is characterized by the

2552: abstract, UNV semantics.

2553: 

2554: For use in the raising lemmas, we will also need the

2555: closely-related notion of ``pessimistic outcome''

2556: $outcome^\frown(G)$ of a goal $G$.  This is what the

2557: outcome of $G$ would be, independent of the program, if we were

2558: to pessimistically assume that all predicates in the program

2559: would diverge (result in infinite computations).  This notion

2560: will be defined more precisely below.

2561: 

2562: \subsubsection{Roadmap}

2563: 

2564: Here we present a guide to the characterization results that

2565: follow.  The sequence

2566: of raising lemmas we will prove will be as follows:

2567: \begin{enumerate}

2568: \item The outcome of a goal $G$ with respect to a program $P$

2569:   can be obtained by inspecting all the pessimistic outcomes of

2570:   all the unfoldings of $G$, and taking the maximally defined one.

2571:   ($outcome_P(G) = max_k(\{outcome^\frown(G') ~|~ G'$ is an

2572:   $P$-unfolding of $G\})$.)

2573: \item The pessimistic outcome of a goal $G$ is the same as the

2574:   pessimistic outcome of its depth-first normal form.

2575:   ($outcome^\frown(G) = outcome^\frown(dfnf(G))$.)

2576: \item The pessimistic outcome of a goal $G$ in depth-first normal

2577:   form can be characterized by a compositional valuation function

2578:   (function from goals to truth values), $v$.

2579:   ($outcome^\frown(G) = v(G)$.)

2580: \item Putting the previous three raising lemmas together,

2581:   the outcome of $G$ with respect to $P$, $outcome_P(G)$,

2582:   can be alternatively characterized by the expression

2583:   $max_k(\{v(dfnf(G')) ~|~ G'$ is a $P$-unfolding of $G\})$.

2584: \end{enumerate}

2585: 

2586: This final result gives an abstract view of the meaning of a

2587: program, which allows us to define the program's denotation,

2588: concluding the characterization.

2589: 

2590: \subsection{Unfoldings and the Pessimistic Semantics}

2591: \label{unfoldings-section}

2592: 

2593: In this section, we define the notion of unfolding of a goal,

2594: and also define the pessimistic operational semantics, which treats all

2595: predicates as being divergent.  We then show how the two notions

2596: are related by proving that every terminating goal has some

2597: unfolding which terminates even in the pessimistic semantics.

2598: This property is useful because it allows us to abstract

2599: away (into the notion of unfolding) all consideration

2600: of the program, and concentrate on characterizing outcomes

2601: under the program-independent pessimistic semantics.

2602: 

2603: We then draw upon the standard notion of definedness ordering

2604: of truth values in order to get a succinct characterization

2605: of this relationship.  The section concludes with the first

2606: raising lemma.

2607: 

2608: \subsubsection{Unfoldings}

2609: 

2610: Informally, an unfolding of a goal is the goal after some

2611: predicate calls are replaced by the corresponding predicate

2612: bodies, possibly repeatedly.  The notion comes originally from

2613: Burstall and Darlington's corresponding functional programming

2614: notion \cite{burstall-darlington}, and is analogous to Tamaki

2615: and Sato's notion of unfolding of a program

2616: \cite{tamaki-sato-unfold}.  Unfoldings are also used in the

2617: unfolding semantics of Gabbrieli and Levi \cite{levi-unfold-tcs92},

2618: and in other semantics such as Etalle's for modular general

2619: logic programs \cite{etalle-modular-general}.

2620: 

2621: More formally, given a program $P$ in completed form, a

2622: formula $G'$ is a {\it 1-$P$-unfolding} of $G$ if it is $G$ with

2623: one occurrence of $p(t_1, \ldots, t_n)$ replaced by

2624: $B[x_1:=t_1, \ldots, x_n:=t_n]$, where

2625: $(p(x_1, \ldots, x_n) \colondash B)$ is a definition in $P$.

2626: A formula $G'$ is a {\it $P$-unfolding} of $G$ if it is either $G$

2627: itself, or a $P$-unfolding of a 1-$P$-unfolding of $G$.

2628: We will drop the program name $P$ when it is unimportant or

2629: clear from context.  Clearly, the $P$-unfolding operation, seen

2630: as a rewriting, is confluent.

2631: 

2632: For instance, let the program $P$ consist of the definitions

2633: $(q \colondash r)$ and $(p \colondash q \And p)$.

2634: Then the goal $G = (q \Or p)$ has two 1-$P$-unfoldings, namely

2635: $(r \Or p)$ and $(q \Or (q \And p))$.  $G$ has an infinite number

2636: of $P$-unfoldings, including $G$ itself, its two 1-$P$-unfoldings,

2637: and other unfoldings such as $(r \Or (q \And (r \And p)))$.

2638: 

2639: We define a $P$-unfolding of a {\it sequence} $G_1, \ldots, G_n$

2640: of formulas as any sequence $G'_1, \ldots, G'_n$ of formulae in

2641: which $G'_i$ is a $P$-unfolding of $G_i$, for all $1 \leq i \leq n$.

2642: 

2643: \subsubsection{The Pessimistic Semantics}

2644: \label{pessimistic-sec}

2645: 

2646: If we unfold a succeeding or failing goal enough, we obtain a

2647: goal which succeeds or fails without doing any predicate

2648: expansions.  A divergent goal, however, cannot be unfolded to

2649: a point where it succeeds or fails without predicate expansions.

2650: 

2651: These facts suggest the following analytical framework.

2652: We define an operational semantics, the {\it pessimistic} semantics,

2653: which returns the result $diverge$ on any predicate

2654: call.  We can then characterize a successful goal as one with an

2655: unfolding which succeeds in the pessimistic semantics, a failing

2656: goal as one with an unfolding which fails in the pessimistic

2657: semantics, and a divergent goal as one with no unfolding which

2658: returns anything but $diverge$ in the pessimistic semantics.

2659: 

2660: \begin{figure}[tp]

2661: 

2662: \noindent

2663: \Rule{Pred:}

2664:   {}

2665:   {\theta: p(t_1, \ldots, t_n),         \alpha \Goes{} diverge}

2666:   {}

2667: 

2668: \caption{

2669:   The predicate rule for the pessimistic semantics,

2670:   the only rule in the [Pessimistic Predicates] fragment.

2671: }

2672: \label{pessimistic-preds-rule-fig}

2673: \end{figure}

2674: 

2675: To this end, we define the pessimistic operational semantics

2676: as being made up of the the operational semantics fragments

2677: [Basic], [Conservative Choice], and [Pessimistic Predicates],

2678: where the latter fragment consists of the single rule shown in

2679: Figure \ref{pessimistic-preds-rule-fig}.  Note that the rules

2680: in [Basic] and [Conservative Choice] are described in such a way

2681: that they pass on the $diverge$ outcome.  Thus, as soon as a

2682: predicate call is encountered in the course of computation,

2683: the pessimistic semantics effectively assumes that the

2684: computation will diverge.  This means, for instance, that if there

2685: is a predicate call in a goal $G$ to the left of the first

2686: disjunction in $G$, then $G$ will diverge according to the

2687: pessimistic semantics.

2688: 

2689: We define the {\it pessimistic outcome} of a goal $G$,

2690: $outcome^\frown(G)$, as follows.

2691: \begin{itemize}

2692: \item If there is a $\theta'$ such that $((): G \Goes{} \theta')$

2693:   in the pessimistic operational semantics, then $outcome^\frown(G) = T$.

2694: \item If $((): G \Goes{} fail)$ in the pessimistic operational semantics,

2695:   then $outcome^\frown(G) = F$.

2696: \item Otherwise (i.e., if $((): G \Goes{} diverge)$ in the

2697:   pessimistic semantics), then $outcome^\frown(G) = U$.

2698: \end{itemize}

2699: Note that the program $P$ is irrelevant to the pessimistic

2700: semantics, and that all computations in the pessimistic

2701: semantics are of bounded size because predicate calls are not

2702: expanded.

2703: 

2704: \subsubsection{Results}

2705: 

2706: Here we show the relationship between unfoldings and the

2707: pessimistic semantics.

2708: 

2709: \begin{thm}

2710: \label{cons-unf-thm}

2711:   Let $\theta: \alpha \Goes{P} \rho$ in the conservative semantics.

2712:   Then some $P$-unfolding $\alpha'$ of $\alpha$ is such that

2713:   $\theta: \alpha' \Goes{P} \rho$ in the pessimistic semantics.

2714: \end{thm}

2715: 

2716: \begin{proof}

2717: By induction on the structure of the conservative

2718: computation.  Cases are on the bottommost rule, and all cases follow

2719: trivially from the induction hypothesis except the case in which

2720: the bottommost rule is a Pred rule.  In this case, one additional

2721: predicate unfolding is necessary to obtain $\alpha'$ from the

2722: $\alpha'$ of the induction hypothesis. 

2723: \end{proof}

2724: 

2725: The converse of the above theorem is also the case:

2726: 

2727: \begin{thm}

2728: \label{unf-cons-thm}

2729:   Let some $P$-unfolding $\alpha'$ of $\alpha$ be such that

2730:   $\theta: \alpha' \Goes{P} \rho$ in the pessimistic semantics,

2731:   where $\rho$ is not $diverge$.

2732:   Then $\theta: \alpha \Goes{P} \rho$ in the conservative semantics.

2733: \end{thm}

2734: 

2735: \begin{proof}

2736: By induction on the number of 1-$P$-unfoldings needed

2737: to derive $\alpha'$ from $\alpha$.

2738: The base case (0 unfoldings) is trivial.  For the inductive case

2739: ($n$ unfoldings), let $\alpha''$ be a 1-$P$-unfolding

2740: of $\alpha$ such that $\alpha'$ is a $P$-unfolding of $\alpha''$

2741: after $n-1$ unfoldings.  By the induction hypothesis,

2742: $\theta: \alpha'' \Goes{P} \rho$ in the conservative semantics.

2743: 

2744: It remains to prove that $\theta: \alpha \Goes{P} \rho$ as well.

2745: We do this by induction on the structure of the $\alpha''$

2746: computation.  The cases are on the bottommost rule applied.

2747: In all cases, if $\alpha$ starts with a predicate call and

2748: $\alpha''$ is derived from it by unfolding that call, then

2749: the computation of $\alpha$ can be derived from that of

2750: $\alpha''$ by just adding an application of Pred.  Otherwise,

2751: all cases follow directly from one or more applications of

2752: the induction hypothesis.

2753: \end{proof}

2754: 

2755: This property of predicate unfoldings and the pessimistic

2756: semantics will be useful for the rest of the paper, because it

2757: allows us to abstract away from the unbounded computations of

2758: the non-pessimistic semantics and consider only the simpler,

2759: bounded computations of the pessimistic semantics.

2760: 

2761: \subsubsection{The Definedness Ordering}

2762: 

2763: The following definitions and theorem makes the connections

2764: between unfoldings and the pessimistic semantics more precise

2765: and concise by allowing us to give an expression corresponding

2766: to the outcome of a goal in terms of its pessimistic outcome.

2767: 

2768: \begin{figure}[tp]

2769: 

2770: \centerline{\epsffile{hasse.eps}}

2771: 

2772: \caption{

2773:   Hasse diagrams of the ``definedness'' ordering $<_k$ (left)

2774:   and the ``truth'' ordering $<_t$ (right) of truth values.

2775: }

2776: \label{hasse-fig}

2777: \end{figure}

2778: 

2779: We define the {\it definedness ordering} $<_k$ on truth values

2780: as the least partial order relation such that $U <_k T$ and $U <_k F$

2781: (see Figure \ref{hasse-fig}).  This is a standard ordering for

2782: these three truth values; see for example \cite{belnap-four-valued}.

2783: The expression $max_k(S)$, where $S$ is a set of truth values,

2784: is undefined if $\{T, F\} \subseteq S$, and otherwise

2785: is defined as the unique truth value $V$ such that $W \leq_k V$

2786: for all $W \in S$.

2787: 

2788: Finally, we give the first raising lemma.

2789: 

2790: \begin{lemma}[Raising Lemma 1]

2791: \label{unf-outcome-char-thm}

2792:   For any goal $G$,

2793:   $max_k(\{outcome^\frown(G') ~|~ G'$ is a

2794:   $P$-unfolding of $G\})$

2795:   is well-defined and equal to $outcome_P(G)$.

2796: \end{lemma}

2797: 

2798: \begin{proof}

2799: Let the set $S$ of truth values be

2800: $\{outcome^\frown(G') ~|~ G'$ is a $P$-unfolding of $G\}$.

2801: First assume that $outcome_P(G) = T$.

2802: By Theorem \ref{cons-unf-thm}, $T \in S$;

2803: however, if $F \in S$, then by Theorem \ref{unf-cons-thm},

2804: $outcome_P(G) = F$, a contradiction.  Therefore

2805: $max_k(S)$ is defined and must be $T$.

2806: Similarly, if $outcome_P(G) = F$ then $max_k(S)$ is defined

2807: and equal to $F$.

2808: If $outcome_P(G) = U$, then it cannot be the case that

2809: $T \in S$ or $F \in S$, because otherwise, by Theorem

2810: \ref{unf-cons-thm}, $outcome_P(G) \not= U$.  Therefore

2811: $S = \{U\}$, and $max_k(S)$ is defined and equal to $U$.  

2812: \end{proof}

2813: 

2814: \subsection{Depth-First Normal Form}

2815: \label{dfnf-section}

2816: 

2817: We now turn to the notion of depth-first normal form (DFNF)

2818: in order to increase the level of abstraction of the semantics.  

2819: The DFNF of a formula $G$ is a formula which

2820: is operationally equivalent to $G$ but whose outcome can be

2821: given a compositional characterization.

2822: In this section, we first define a term-rewriting system which

2823: rewrites formulas into formulas.  We then prove that the system

2824: is locally confluent and terminating, and that it transforms

2825: every formula to a unique normal form (which we define as the

2826: DFNF).  We then prove that each of the transformations of the

2827: rewriting system preserves pessimistic outcome.  The conclusion

2828: is that each goal has a unique DFNF which has the same

2829: pessimistic outcome as the original goal.

2830: 

2831: The DFNF by itself does not directly raise the abstraction

2832: level of the semantics; however, it puts a goal in a form which

2833: can be given an abstract characterization, as we will see in the

2834: next section.  The conclusion of this section is therefore referred

2835: to as the second raising lemma.

2836: 

2837: \subsubsection{Term-Rewriting System}

2838: 

2839: The notion of DFNF, which is closely related to the notion

2840: of disjunctive normal form (DNF), was introduced in

2841: \cite{andrews-lnaf-tcs}.  Here we expand the notion to take

2842: account of $if$ formulas.

2843: 

2844: The classes of {\it negated-disjunction} ($N$) and

2845: {\it outer-disjunction} ($O$) formulae

2846: are defined mutually

2847: recursively as follows.  (Informally, an $O$ formula has $\Or$s

2848: directly inside only $\Not$s or other $\Or$s.)

2849: \[ N ~~::=~~

2850:     p(t_1, \ldots, t_n) ~~|~~

2851:     s = t ~~|~~

2852:     N \And N ~~|~~

2853:     \exists x N ~~|~~

2854:     \Not O

2855: \]

2856: \[ O ~~::=~~

2857:     N ~~|~~

2858:     O \Or O

2859: \]

2860: For example, $p \Or (\exists x(q(x)) \And r)$ is an

2861: outer-disjunction formula but not a negated-disjunction formula;

2862: however, $\Not (p \Or (\exists x(q(x)) \And r))$ is a

2863: negated-disjunction formula and thus automatically an

2864: outer-disjunction formula.

2865: 

2866: \begin{figure}[tp]

2867: 

2868:   \begin{itemize}

2869:   \item[R1]

2870:     $(B_1 \Or B_2) \And C ~\Rw{}~ (B_1 \And C) \Or (B_2 \And C)$

2871:   \item[R2]

2872:     $B \And (C_1 \Or C_2) ~\Rw{}~ (B \And C_1) \Or (B \And C_2)$,

2873:     where $B$ is negated-disjunction

2874:   \item[R3]

2875:     $ \exists x (B_1 \Or B_2) ~\Rw{}~

2876:      (\exists x B_1) \Or (\exists x B_2)$

2877:   \item[R4]

2878:     $if[\vec{x}]((B_1 \Or B_2), C) ~\Rw{}~

2879:      if[\vec{x}](B_1, C)

2880:      \Or

2881:      (\Not(\exists \vec{x} B_1)

2882:       \And if[\vec{x}](B_2, C))$

2883:   \item[R5]

2884:     $if[\vec{x}](B, C) ~\Rw{}~

2885:      \exists \vec{x} (B \And C)$,

2886:     where $B$ is negated-disjunction

2887:   \end{itemize}

2888: 

2889: \caption{The rules of the term-rewriting relation $\Rw{}$.}

2890: \label{rw-fig}

2891: \end{figure}

2892: 

2893: The notion of depth-first normal form is based on the five rules

2894: R1-R5 of

2895: the term-rewriting relation $\Rw{}$ (Figure \ref{rw-fig}), which

2896: can be applied anywhere in a formula to rewrite it into another

2897: formula.  Two of the rules refer to the notion of a

2898: negated-disjunction formula.  We define a formula to be

2899: {\it in depth-first normal form} if none of R1-R5 can be applied

2900: anywhere in the formula.

2901: 

2902: For example, the formula

2903: $if[x](x=0, p(x) \Or q(x))$

2904: can be rewritten by one application of R5 to

2905: $\exists x (x=0 \And (p(x) \Or q(x)))$,

2906: and then by one application of R2 to

2907: $\exists x ((x=0 \And p(x)) \Or (x=0 \And q(x)))$.

2908: It can then be rewritten by one application of R3 to

2909: $\exists x (x=0 \And p(x)) \Or \exists x (x=0 \And q(x))$.

2910: None of the rules R1-R5 apply to this latter formula,

2911: so it is in depth-first normal form.

2912: \label{dfnf-example-section}

2913: 

2914: \subsubsection{Local Confluence and Termination}

2915: 

2916: To prove that the rewriting process always leads to a

2917: single formula, we prove local confluence and termination of this

2918: rewriting system.  The proofs are contained in Appendix

2919: \ref{proofs-appx}.

2920: 

2921: \begin{thm}[Local Confluence of Rewriting System]

2922: \label{local-confluence-thm}

2923:   If $A \Rw{} A_1$ and $A \Rw{} A_2$,

2924:   then there is an $A_3$ such that $A_1 \Rw{}^* A_3$ and $A_2 \Rw{}^* A_3$.

2925: \end{thm}

2926: 

2927: \begin{proof}

2928: See Appendix \ref{proofs-appx}.  

2929: \end{proof}

2930: 

2931: In preparation for proving termination of the rewriting system, we

2932: define the {\it depth} $d(G)$ of a formula $G$.  It is the

2933: conventional notion of depth of a formula, expanded to take

2934: account of $if$. \\

2935: \begin{tabular}{l}

2936:   $d(s=t) = d(p(t_1, \ldots, t_n)) = 1$ \\

2937:   $d(B \And C) = d(B \Or C) = max(d(B),d(C)) + 1$ \\

2938:   $d(\Not B) = d(\exists x~B) = d(B) + 1$ \\

2939:   $d(if[x_1,\ldots,x_n](B, C)) = max(d(B),d(C)) + 1$ \\

2940: \end{tabular}

2941: 

2942: We also define the {\it maximum potential depth} $pd(G)$ of a

2943: formula $G$.  This is the depth that the formula might possibly

2944: attain after repeatedly being transformed with R1-R5.  \\

2945: \begin{tabular}{l}

2946:   $pd(s=t) = pd(p(t_1, \ldots, t_n)) = 1$ \\

2947:   $pd(B \And C) = pd(B \Or C) = max(pd(B),pd(C)) + 1$ \\

2948:   $pd(\Not B) = pd(\exists x~B) = pd(B) + 1$ \\

2949:   $pd(if[x_1,\ldots,x_n](B, C)) = n + 2pd(B) + max(pd(B), pd(C))$ \\

2950: \end{tabular} \\

2951: Clearly $1 \leq d(G) \leq pd(G)$ for all formulas $G$.

2952: 

2953: The main lemma we need for termination is to prove that each

2954: application of R1-R5 maintains or decreases potential depth.

2955: 

2956: \begin{lemma}

2957: \label{rule-decreases-pd-lemma}

2958:   If $G \Rw{} G'$, then $pd(G) \geq pd(G')$.

2959: \end{lemma}

2960: 

2961: \begin{proof}

2962: See Appendix \ref{proofs-appx}.  

2963: \end{proof}

2964: 

2965: \begin{thm}[Termination of Rewriting System]

2966: \label{termination-thm}

2967:   For every $G$, there is an integer $j$ such that for

2968:   every sequence of formulas $G = G_0, G_1, G_2, \ldots, G_k$

2969:   such that $G_i \Rw{} G_{i+1}$ for all $1 \leq i < k$,

2970:   we have that $k \leq j$.

2971: \end{thm}

2972: 

2973: \begin{proof}

2974: Each of the rules R1-R5 increase the number of connectives

2975: in the formula, where $if$ is counted as one connective.  However,

2976: the Lemma shows that the depth of the resultant formula is

2977: bounded by $pd(G)$.  Since the formula tree has a bounded depth and

2978: bounded branching factor, there is a limit $j$ to how many nodes

2979: (connectives) it can contain.  The rewriting process must stop

2980: at or before this limit.  

2981: \end{proof}

2982: 

2983: \subsubsection{Unique Normal Form and DFNF}

2984: 

2985: Because of local confluence and termination, we are able to

2986: state the following corollary, which shows that every goal has a

2987: unique normal form under the rewriting rules R1-R5.

2988: 

2989: \begin{cor}[Unique Normal Form]

2990: \label{unique-normal-form-cor}

2991:   For every formula $G$ not in normal form, there is a unique

2992:   formula $G''$ in normal form, such that for all $G'$ such that

2993:   $G \Rw{} G'$, we have that $G' \Rw{}^* G''$.

2994: \end{cor}

2995: 

2996: \begin{proof}

2997: See Appendix \ref{proofs-appx}.  

2998: \end{proof}

2999: 

3000: Because of this corollary, we are justified in

3001: making the following definition.  The {\it depth-first normal

3002: form} of a formula, $dfnf(G)$, is the unique formula

3003: $G'$ such that $G \Rw{}^* G'$ and there is no $G''$ such that

3004: $G' \Rw{} G''$.

3005: (For instance, the depth-first normal form of the example

3006: formula from Section \ref{dfnf-example-section},

3007: $if[x](x=0, p(x) \Or q(x))$, is

3008: $\exists x (x=0 \And p(x)) \Or \exists x (x=0 \And q(x))$.)

3009: Clearly, despite the complexity of the proofs

3010: of confluence and termination, we can obtain $dfnf(G)$ in a

3011: straightforward fashion, by simply applying one of the rules

3012: R1-R5 to any suitable redex (say, the outermost one) until

3013: there are no more redexes.

3014: 

3015: We also note that $dfnf(G)$ is outer-disjunction, a fact which

3016: will be important soon.

3017: 

3018: \begin{theorem}

3019: \label{dfnf-outcome-char-thm}

3020:   For all $G$, $dfnf(G)$ is outer-disjunction.

3021: \end{theorem}

3022: 

3023: \begin{proof}

3024: If $dfnf(G)$ were not outer-disjunction, it would have

3025: some disjunction as an immediate subformula of a conjunction,

3026: existential formula, or $if$ formula.  In all these cases,

3027: one of rules R1-R5 would apply. 

3028: \end{proof}

3029: 

3030: \subsubsection{Outcome Preservation}

3031: 

3032: We now show that the depth-first normal form formation does

3033: not change the outcome of a goal under the pessimistic

3034: semantics.

3035: 

3036: \begin{thm}[General Result Preservation of $dfnf$]

3037: \label{general-result-pres-thm}

3038:   If $\alpha'$ is $\alpha$

3039:   with some formulas transformed by applications of rules R1-R5,

3040:   then $\theta: \alpha \Goes{} \rho$ in the pessimistic semantics iff

3041:   $\theta: \alpha' \Goes{} \rho$ in the pessimistic semantics.

3042: \end{thm}

3043: 

3044: \begin{proof}

3045: See Appendix \ref{proofs-appx}.  

3046: \end{proof}

3047: 

3048: We can now give the second raising lemma, by showing the

3049: specific result that we wanted to obtain.

3050: 

3051: \begin{lemma}[Raising Lemma 2]

3052: \label{outcome-pres-cor}

3053:   $outcome^\frown(G) = outcome^\frown(dfnf(G))$.

3054: \end{lemma}

3055: 

3056: \begin{proof}

3057: By Theorem \ref{general-result-pres-thm},

3058: with respect to the pessimistic semantics,

3059: $((): G \Goes{} \rho)$ iff $((): dfnf(G) \Goes{} \rho)$.

3060: Therefore, with respect to the pessimistic semantics,

3061: $G$ succeeds (fails, diverges) exactly when $dfnf(G)$

3062: succeeds (fails, diverges).

3063: \end{proof}

3064: 

3065: Note that we have come one step closer to an abstract

3066: characterization of outcome, by reducing the problem of

3067: characterizing outcome of a general goal with respect to a

3068: general program to the problem of characterizing the outcome of

3069: an outer-disjunction goal with respect to the pessimistic

3070: semantics.

3071:  

3072: \subsection{The Valuation Function}

3073: \label{valuation-section}

3074: 

3075: Finally we come to the definition of the valuation $v$, which

3076: characterizes the outcomes of outer-disjunction goals (e.g.,

3077: goals in DFNF) with respect to the pessimistic semantics.

3078: This valuation is a compositional function from formulae to

3079: truth values, like valuations in standard theories of truth

3080: \cite{kripke,fitting-kripke}, and interprets the binary connectives

3081: in a manner consistent with the left-to-right search algorithm

3082: of Prolog.  $v$ is based on the similar valuation in

3083: \cite{andrews-lnaf-tcs}.  The valuation in that paper

3084: is on a domain of

3085: four truth values, but we need only three truth values here

3086: because we do not consider the $flounder$ outcome.

3087: 

3088: In this section, we first define the alethic ordering $<_t$ on

3089: truth values, and then the valuation function $v$ which uses it.

3090: Then we show that the valuation of a goal in outer-disjunction

3091: form is the same as its pessimistic outcome.

3092: 

3093: \subsubsection{Alethic Ordering and Valuation Function}

3094: 

3095: We define the {\it alethic ordering} $<_t$ on truth values as

3096: the least partial order relation such that $F <_t U$ and $U <_t T$.

3097: (See Fig. \ref{hasse-fig}.  This is another standard ordering on

3098: these truth values; see for instance \cite{belnap-four-valued}.)

3099: The expression $max_t(S)$, where $S$ is a set of truth values,

3100: is defined as the unique truth value $V$ such that $W \leq_t V$

3101: for all $W \in S$.  The alethic ordering is used in the

3102: valuation function to express the meaning of $\exists x~G$ in

3103: terms of the meaning of the instances of $G$.

3104: 

3105: $v$, a {\it valuation function} mapping ground,

3106: outer-disjunction (O) formulae to truth values in

3107: $\{T, U, F\}$, is defined as follows.

3108: \begin{recdef}

3109: \item $v(t=t) = T$;

3110: \item $v(s=t) = F$, where $s$ is not identical to $t$;

3111: \item $v(p(t_1, \ldots, t_n)) = U$;

3112: \item \parbox{10cm}{

3113:       \( v(B \And C) = \left\{\begin{array}{ll}

3114:                                 v(C) & \mbox{if $v(B)=T$,} \\

3115:                                 v(B) & \mbox{otherwise;}

3116:                                 \end{array}

3117:                          \right. \)

3118:       \hfill{}

3119:       }

3120: \item \parbox{10cm}{

3121:       \( v(B \Or  C) = \left\{\begin{array}{ll}

3122:                                 v(C) & \mbox{if $v(B)=F$,} \\

3123:                                 v(B) & \mbox{otherwise;}

3124:                                 \end{array}

3125:                          \right. \)

3126:       \hfill{}

3127:       }

3128: \item $v(\exists x~B) = max_{t}(\{v(B[x:=t]) ~|~ t \mbox{ ground}\})$;

3129: \item \parbox{10cm}{

3130:       \( v(\Not B) =  \left\{  \begin{array}{ll}

3131:                                 F & \mbox{if $v(B)=T$,} \\

3132:                                 U & \mbox{if $v(B)=U$,} \\

3133:                                 T & \mbox{if $v(B)=F$.}

3134:                                 \end{array}

3135:                        \right. \)

3136:       \hfill{}

3137:       }

3138: \end{recdef}

3139: For instance, recall from Section \ref{true-false-section}

3140: that $true$ is the formula $(0=0)$ and

3141: $false$ is the formula $(0=1)$.  By the definition of $v$,

3142: we have that $v(true)=v(0=0)=T$, and $v(false)=v(0=1)=F$, as

3143: expected.  We also have that $v(\Not true)=F$,

3144: $v(true \And false) = F$, and $v(false \Or true) = T$.

3145: We have that $v(false \Or p(0))$ and $v(true \And p(0))$ are both

3146: $U$, but $v(false \And p(0))=F$ and $v(true \Or p(0))=T$,

3147: consistent with how the pessimistic semantics would execute

3148: the formulas as queries.

3149: 

3150: In fact, while $v(0=0)=T$, we have that $v(s=0)=F$ for any term

3151: $s$ other than $0$.  Therefore the set

3152: $\{v(t=0) ~|~ t \mbox{ ground}\}$ is the set

3153: $\{v(0=0)\} \cup 

3154:  \{v(t=0) ~|~ t \mbox{ ground and } t \neq 0\}$,

3155: i.e.\ $\{T\} \cup \{F\}$, or $\{T, F\}$.

3156: As a consequence,

3157: $v(\exists x (x=0)) =

3158:  \{v(t=0) ~|~ t \mbox{ ground}\} = T$,

3159: since $T$ is the maximally true truth value in the set $\{T, F\}$.

3160: 

3161: \subsubsection{Equivalence of Valuation and Pessimistic Outcome}

3162: 

3163: The valuation function $v$ characterizes precisely the behaviour of

3164: outer-disjunction formulae with respect to the pessimistic

3165: semantics.  In preparation for this result, we state a

3166: proposition which is a weaker form of the converse of the

3167: witness properties, applying only to $N$ formulas.

3168: 

3169: \begin{prop}

3170: \label{reverse-witness-prop}

3171:   Let $\alpha$ be a sequence of negated-disjunction ($N$)

3172:   formulas, such that $\theta: \alpha \Goes{} \rho$ in the

3173:   pessimistic semantics.

3174:   Let $V$ be a subset of the free variables of $\alpha$.

3175:   Then: \\

3176:   (1) If for some substitution $\xi$ grounding $V$ consistent

3177:     with $\theta$, $(\theta: \alpha\xi \Goes{} \theta')$ in the

3178:     pessimistic semantics, then $\rho$ is some $\theta''$. \\

3179:   (2) If for all substitutions $\xi$ grounding $V$ consistent

3180:     with $\theta$, $(\theta: \alpha\xi \Goes{} fail)$ in the

3181:     pessimistic semantics, then $\rho$ is $fail$.

3182: \end{prop}

3183: The fragment of the pessimistic semantics

3184: dealing with negated-disjunction formulas is identical to

3185: the fragment of the semantics of \cite{andrews-lnaf-tcs}

3186: dealing with negated-disjunction formulas with respect to

3187: the empty program.  The proof of this Proposition is thus

3188: a simple adaptation of

3189: the proof of Lemma 4.5 from \cite{andrews-lnaf-tcs}.

3190: Intuitively, the Proposition applies only to $N$

3191: formulas because instantiating an $N$ formula will

3192: either cause it to fail or will not change the outcome

3193: its computation.  In contrast, for example, $B \Or C$

3194: may diverge because $B$ diverges, but $B\theta \Or C\theta$

3195: may succeed because $B\theta$ fails

3196: and $C\theta$ succeeds.  We cannot draw any conclusions about

3197: the behaviour of $B \Or C$ from the behaviour of its instances.

3198: 

3199: We are now in a position to state the third raising lemma,

3200: continuing our process of abstraction.  Note that this lemma

3201: relates an operational notion (pessimistic outcome)

3202: to an entirely abstract one (valuation).

3203: 

3204: \begin{theorem}[Raising Lemma 3]

3205: \label{v-outcome-char-thm}

3206:   If $G$ is ground and

3207:   outer-disjunction, then $v(G) = outcome^\frown(G)$.

3208: \end{theorem}

3209: 

3210: \begin{proof}

3211: By induction on the structure of $G$.  Cases are on the

3212: outermost connective.

3213: We note only the three subcases of the

3214: case in which $G = \exists x~B$.

3215: 

3216: If $outcome^\frown(G) = T$, there must be some

3217: $\theta'$ such that $((): \exists x~B \Goes{} \theta')$ in

3218: the pessimistic semantics.

3219: In this case, we also have that

3220: $((): B[x:=x'] \Goes{} \theta')$, and by the witness properties,

3221: there must be some ground $t$ and $\theta''$ such that

3222: $((): B[x:=x'][x':=t] \Goes{} \theta'')$.

3223: Thus for some $t$, $outcome^\frown(B[x:=t]) = T$.

3224: By the induction hypothesis,

3225: $v(B[x:=t]) = T$; and by the definition of $max_t$, $v(G) = T$.

3226: 

3227: If $outcome^\frown(G) = F$, then

3228: $((): \exists x~B \Goes{} fail)$ in

3229: the pessimistic semantics.

3230: In this case, we also have that

3231: $((): B[x:=x'] \Goes{} fail)$, and by the witness properties,

3232: for all ground $t$,

3233: $((): B[x:=x'][x':=t] \Goes{} fail)$.

3234: Thus for all $t$, $outcome^\frown(B[x:=t]) = F$.

3235: By the induction hypothesis,

3236: $v(B[x:=t]) = F$; and by the definition of $max_t$, $v(G) = F$.

3237: 

3238: Otherwise, $outcome^\frown(G)=U$.

3239: By Prop.\ \ref{reverse-witness-prop}, there cannot be

3240: any $t$ such that $outcome^\frown(B[x:=t]) = T$, because otherwise

3241: $outcome^\frown(G)$ would be $T$; and again

3242: by Prop.\ \ref{reverse-witness-prop}, it cannot be the case that

3243: for all $t$, $outcome^\frown(B[x:=t]) = F$, because otherwise

3244: $outcome^\frown(G)$ would be $F$.  Thus for some $t$,

3245: $outcome^\frown(B[x:=t]) = U$, so the set

3246: $\{v(B[x:=t]) ~|~ t$ is ground $\}$ of truth values is either

3247: $\{U\}$ or $\{U, F\}$.

3248: Thus by the definition of $max_t$, $v(G) = U$.

3249: \end{proof}

3250: 

3251: 

3252: \subsection{The Denotation of a Program}

3253: \label{denotation-section}

3254: 

3255: In this section, we give the final raising lemma which summarizes

3256: the previous ones.  This lemma gives an expression which is an

3257: abstract characterization of the outcome of a goal; we therefore

3258: give a definition of the denotation of a program which uses this

3259: expression.

3260: 

3261: \begin{lemma}[Raising Lemma 4]

3262: \label{v-top-outcome-char-thm}

3263:   For any ground goal $G$, \\

3264:   $outcome_P(G) = max_k(\{v(dfnf(G')) ~|~ G'$ is a

3265:   $P$-unfolding of $G\})$.

3266: \end{lemma}

3267: 

3268: \begin{proof}

3269: By Raising Lemma 1,

3270: $outcome_P(G) = max_k(\{outcome^\frown(G') ~|~ G'$ is a $P$-unfolding of $G\})$.

3271: By Raising Lemma 2, $outcome^\frown(G') = outcome^\frown(dfnf(G'))$ for

3272: any $G'$.  But by Theorem \ref{dfnf-outcome-char-thm},

3273: $dfnf(G')$ is in outer-disjunction form for any $G'$; therefore by Raising

3274: Lemma 3, $outcome^\frown(dfnf(G')) = v(dfnf(G'))$.

3275: Putting this all together, we conclude that

3276: $outcome_P(G) = max_k(\{v(dfnf(G')) ~|~ G'$ is a $P$-unfolding of $G\})$.

3277: \end{proof}

3278: 

3279: We therefore make the following

3280: definition.  The {\it denotation} $v_P$ of a program $P$ is a

3281: valuation function defined by:

3282: \begin{center}

3283:   $v_P(G) = max_k(\{v(\dfnf(G')) ~|~ G'$ is an unfolding of $G\})$.

3284: \end{center}

3285: 

3286: We have the following trivial theorem.

3287: \begin{theorem}[Denotation]

3288:   For any ground goal $G$, $outcome_P(G) = v_P(G)$.

3289: \end{theorem}

3290: 

3291: \begin{proof}

3292: By Raising Lemma 4 and the definition of $v_P$.

3293: \end{proof}

3294: 

3295: Note that the restriction to ground goals does not decrease the

3296: generality of the denotation result, since a goal $G$ with free

3297: variables $\vec{x}$ has the same outcome as the goal

3298: $\exists \vec{x} G$.

3299: 

3300: \subsection{Example}

3301: \label{sems-example-section}

3302: 

3303: As a further example of how the denotation of a program defines the

3304: correct truth value of a goal, we derive the value obtained by

3305: applying the denotation of a program to a goal.

3306: 

3307: Let the program $P$ be the second

3308: ``delete'' program from Section \ref{example-section}:

3309: \begin{tabbing}

3310: \Indent{} \= $\Or$ \= \kill

3311: \>  $d(x, y, z) \colondash$ \\

3312: \>  \>  $(y=[~] ~ \And ~ z=[~])$ \\

3313: \>  $\Or$ \> $if[ys](y=[x|ys], d(x, ys, z))$ \\

3314: \>  $\Or$ \> $(\Not\exists ys(y=[x|ys]) ~ \And$ \\

3315: \>        \> \Indent{} $\exists y' \exists ys \exists zs(y=[y'|ys] \And z=[y'|zs] \And d(x, ys, zs)))$

3316: \end{tabbing}

3317: Consider the goal $G = \exists z ~ d(a, [~], z)$.

3318: This goal asks whether

3319: there is a $z$ which is obtained by deleting $a$ everywhere from

3320: the empty list $[~]$.  It has the outcome

3321: $T$ in the conservative semantics, since there does exist a

3322: $z$, namely the empty list $[~]$ itself, which is obtained that way.

3323: 

3324: We take as our objective to derive the value of $v_P(G)$.

3325: From the definition of $v_P$, we have that

3326: $v_P(G) = max_k(\{v(\dfnf(G')) ~|~ G'$ is an unfolding of $G\})$.

3327: Let $S$ be the set 

3328: $\{v(\dfnf(G')) ~|~ G'$ is an unfolding of $G\}$; then

3329: $v_P(G) = max_k(S)$.  As discussed in the proof of Raising Lemma 1,

3330: if $\{U, T\} \subseteq S$, then $F \not\in S$; so if we can find

3331: one unfolding of $G$ whose DFNF valuation is $U$ and another

3332: whose DFNF valuation is $T$, then we know $S = \{U, T\}$.

3333: 

3334: In fact, we can find such unfoldings.  The subsequent sections

3335: show that $G$ itself is such that $v(dfnf(G)) = U$, and that

3336: the first unfolding $G_1$ of $G$ is such that $v(dfnf(G_1)) = T$.

3337: Hence $v_P(G) = max_k(S) = max_k(\{U, T\}) = T$.

3338: 

3339: First, we show that $v(dfnf(G)) = U$.  Then, we find the expression

3340: for $G_1$ and for $dfnf(G_1)$.  Finally, we show that $v(dfnf(G_1)) = T$.

3341: 

3342: \subsubsection{$v(dfnf(G)) = U$}

3343: 

3344: $G$ is $\exists z ~ d(a, [~], z)$.  This formula contains no

3345: disjunctions or $if$s, so none of the DFNF rewriting rules applies

3346: to it; hence $dfnf(G)$ is $G$ itself.  By the definition of $v$,

3347: $v(dfnf(G)) = v(G) = v(\exists z ~ d(a, [~], z))$, which is the expression

3348: $max_t(\{ d(a, [~], z) ~|~ t$ is a ground term$\})$; that is,

3349: the maximally true truth value amongst the valuations of all

3350: the formulas of the form $d(a, [~], t)$, where $t$ is a ground term.

3351: 

3352: However, by the definition of $v$, the valuation of any

3353: predicate call formula is $U$ (since $v$ correctly characterizes

3354: the pessimistic semantics).  Hence 

3355: $max_t(\{ d(a, [~], z) ~|~ t$ is a ground term$\}) = max_t(\{U\}) = U$.

3356: Since this was the expression for $v(dfnf(G))$, we have that

3357: $v(dfnf(G)) = U$.

3358: 

3359: \subsubsection{First Unfolding and its DFNF}

3360: 

3361: $G$ is $\exists z ~ d(a, [~], z)$.

3362: The first unfolding of $G$, $G_1$, can be obtained by replacing

3363: the predicate call within it by the body of the definition of

3364: the predicate $d$, replacing formal by actual parameters.

3365: Therefore:

3366: \begin{tabbing}

3367: \Indent{} \= $\Or$ \= \kill

3368: \>  $G_1 = \exists z($ \\

3369: \>  \>  $([~]=[~] ~ \And ~ z=[~])$ \\

3370: \>  $\Or$ \> $if[ys]([~]=[a|ys], d(a, ys, z))$ \\

3371: \>  $\Or$ \> $(\Not\exists ys([~]=[a|ys]) ~ \And$ \\

3372: \>        \> \Indent{} $\exists y' \exists ys \exists zs([~]=[y'|ys] \And z=[y'|zs] \And d(a, ys, zs)))$

3373: \end{tabbing}

3374: We abbreviate this formula as

3375: $\exists z(G'_1 \Or G'_2 \Or (G'_3 \And G'_4))$.

3376: 

3377: The DFNF rewriting rule R3 can be applied twice to $G_1$, to

3378: yield the formula 

3379: $(\exists z(G'_1) \Or \exists z(G'_2) \Or \exists z(G'_3 \And G'_4))$.

3380: $G'_2$ is an $if$ formula,

3381: $if[ys]([~]=[a|ys], d(a, ys, z))$, whose first subformula

3382: $([~]=[a|ys])$ is a negated-disjunction formula; hence, the

3383: DFNF rewriting rule R5 can be applied to it, yielding the

3384: subformula $G'_5 = \exists ys([~]=[a|ys] \And d(a, ys, z))$.

3385: At this point, no more of the DFNF rewriting rules can be

3386: applied to the formula, so it is in depth-first normal form.

3387: 

3388: Hence, $dfnf(G_1) = 

3389: (\exists z(G'_1) \Or \exists z(G'_5) \Or \exists z(G'_3 \And G'_4))$,

3390: where:

3391: \begin{itemize}

3392: \item $G'_1 = ([~]=[~] ~ \And ~ z=[~])$;

3393: \item $G'_5 = \exists ys([~]=[a|ys] \And d(a, ys, z))$;

3394: \item $G'_3 = \Not\exists ys([~]=[a|ys])$; and

3395: \item $G'_4 = \exists y' \exists ys

3396:               \exists zs([~]=[y'|ys] \And z=[y'|zs] \And d(a, ys, zs)))$.

3397: \end{itemize}

3398: 

3399: \subsubsection{$v(dfnf(G_1)) = T$}

3400: 

3401: $v(dfnf(G_1)) =

3402:  v(\exists z(G'_1) \Or \exists z(G'_5) \Or \exists z(G'_3 \And G'_4))$.

3403: We can therefore obtain the value of $v(dfnf(G_1))$ by first obtaining

3404: the values of its disjuncts.

3405: By the definition of $v$,

3406: we have that $v(\exists z(G'_1))$ is the value of the expression

3407: $max_t(\{v([~]=[~] ~ \And ~ t=[~]) ~|~ t$ is a ground term$\})$.

3408: The value of $v([~]=[~] ~ \And ~ t=[~])$ is $T$ if the values of both

3409: $v([~]=[~])$ and $v(t=[~])$ are $T$, and it is $F$ otherwise.

3410: However, $v([~]=[~])$ is always $T$; and

3411: $v(t=[~])$ is $T$ if $t$ is $[~]$, and otherwise is $F$.

3412: 

3413: The set

3414: $\{v([~]=[~] ~ \And ~ t=[~]) ~|~ t$ is a ground term$\}$

3415: therefore consists of the two truth values $\{T, F\}$.  The maximally

3416: true member of this set is $T$; hence,

3417: $v(\exists z(G'_1)) = max_t(\{T, F\}) = T$.

3418: Now, $dfnf(G_1)$ is of the form $(\exists z(G'_1) \Or H)$;

3419: so $v(dfnf(G_1)) = v(\exists z(G'_1) \Or H)$.  By the

3420: definition of $v$, and because $v(\exists z(G'_1)) = T$,

3421: $v(\exists z(G'_1) \Or H) = T$; hence $v(dfnf(G_1)) = T$.

3422: 

3423: We conclude the example by reiterating the value of $v_P(G)$.

3424: Because $v(dfnf(G)) = U$ and $v(dfnf(G_1)) = T$, the set

3425: $\{v(\dfnf(G')) ~|~ G'$ is an unfolding of $G\}$ is just

3426: $\{U, T\}$.  Therefore: \vspace{2mm} \\

3427: \begin{tabular}{lll}

3428: $v_P(G)$ & $=$ & $max_k(\{v(\dfnf(G')) ~|~ G'$ is an unfolding of $G\})$ \\

3429:          & $=$ & $max_k(\{U, T\})$ \\

3430:          & $=$ & $T$ \\

3431: \end{tabular} \\

3432: This result accords with the fact that the original goal $G$

3433: did succeed under the conservative semantics.

3434: 

3435: \subsection{Discussion}

3436: \label{sems-discussion-section}

3437: 

3438: Note that the abstract semantics is based on six basic,

3439: relatively simple notions: the notion of truth value,

3440: the two orderings of the truth

3441: values, the notion of predicate unfolding, the notion of

3442: depth-first normal form, and the logical valuation.

3443: The notion of depth-first normal form, in turn, is based on a

3444: rewriting system of five rules.  The predicate unfolding and

3445: normal form constructions essentially do local

3446: meaning-preserving transformations to prepare the goal in

3447: question for characterization, and the valuation actually

3448: performs that characterization.

3449: 

3450: In some sense, the crucial element of the abstract semantics,

3451: the element which allows it not to reify such notions as

3452: substitutions and unification, is the $\exists$ clause of the

3453: definition of $v$.  Rather than view a variable operationally,

3454: as a placeholder in a term which at some future point can be

3455: replaced by another term, the $\exists$ clause allows us to view

3456: it as a true variable ranging over a fixed domain of discourse.

3457: This, in turn, has been enabled by the

3458: witness properties of the conservative semantics.  Without the

3459: witness properties, we would not have been able to prove that

3460: the value of $v(\exists x G)$ could be derived directly from the

3461: consideration of the values of $v(G[x:=t])$, for any ground $t$.

3462: Hence, the witness properties are useful not only from the point

3463: of view of intuitively justifying the behaviour of a logic

3464: programming system, but also on theoretical grounds.

3465: 

3466: 

3467: 

3468: \section{Conclusions}

3469: 

3470: The main contributions of this paper are as follows.

3471: \begin{itemize}

3472: \item We have defined an extension of Prolog with hard cut and

3473:   negation as failure in which programs can provably be put

3474:   in a convenient ``completed'' form.  This completion has

3475:   been achieved by using a variable-binding choice construct, $if$.

3476: \item We have identified the witness properties as important

3477:   properties intermediate between the strict logicalness of pure

3478:   Horn clause programming and the unrestricted freedom of

3479:   typical Prolog implementations.

3480: \item We have defined restrictions on the computation of

3481:   extended programs which allow the resulting system to achieve

3482:   the witness properties.  We have referred to the resulting

3483:   notion of cut as {\it firm cut}, insofar as it is intermediate

3484:   between hard and soft cut.

3485: \item We have defined an abstract semantics for the restricted system

3486:   (taking depth-first termination, rather than universal termination,

3487:   as its observable),

3488:   which uses the witness properties in order to avoid reifying

3489:   the concepts of unification and substitution.

3490: \end{itemize}

3491: 

3492: Long investigations by the author have not resulted in any

3493: semantics for Prolog which allow the full range of behaviour of

3494: hard cut while rising in any meaningful way above the level of

3495: an operational semantics.  We do not believe at this point that

3496: such a semantics is possible.  We believe that the system with

3497: firm cut, as defined in this paper, is the best compromise

3498: yet found between

3499: the power of the hard cut and the logical rigour of the soft

3500: cut.  We believe that the behaviours of hard cut excluded by

3501: firm cut are unlikely to be missed by Prolog programmers, and

3502: that the witness properties achieved by firm cut capture the

3503: core of programmers' desiderata about a logic programming

3504: system, even though they are not in complete harmony with logic.

3505: However, these are merely beliefs.  We invite readers to decide

3506: whether they agree or disagree based on their experience.

3507: 

3508: The more theoretically substantiated conclusions we draw from

3509: this work are as follows.

3510: \begin{itemize}

3511: \item The widely-held view that features such as cut and

3512:   negation as failure entirely destroy the declarative

3513:   interpretation of logic programming systems seems to be too

3514:   strong.  While firm cut cannot be interpreted as a logical

3515:   construct, the abstract semantics developed here suggest that a

3516:   system with firm cut is more declarative than one with hard cut,

3517:   while still retaining behaviour of hard cut which is useful in

3518:   practice.

3519: \item If a logic programming language does not achieve soundness

3520:   with respect to traditional logical interpretations, it might

3521:   still be possible for it to achieve the witness properties.

3522:   Given that practical, widely-used languages often implement

3523:   pragmatic features which depart from well-defined semantics,

3524:   insisting on the witness properties might be an acceptable

3525:   alternative to insisting on soundness with respect to first

3526:   order logic.

3527: \item The Prolog syntax and clause-based operational semantics is

3528:   difficult to work with in an abstract setting when taking cut into

3529:   consideration.  We have found it easier to study semantic issues

3530:   with programs in ``completed'' program form, and the

3531:   structured operational semantics, described in this paper.  The

3532:   syntax of the Mercury language \cite{mercury-jlp} is already

3533:   closer to the completed form described here, since it uses an

3534:   efficient ``if'' formula (though the ``if'' of Mercury

3535:   corresponds to soft cut, not firm cut).

3536: \end{itemize}

3537: 

3538: There are several interesting open questions suggested by

3539: this research.

3540: \begin{itemize}

3541: \item Are other ``non-logical'' features of Prolog able to be

3542:   given a form which allows the witness properties to be preserved?

3543:   Obviously there is no hope for the {\tt var} and

3544:   {\tt nonvar} predicates, which check the instantiation of their

3545:   arguments, but what about {\tt assert}, {\tt retract},

3546:   {\tt bagof}, and so on?

3547: \item What is the largest subset of the liberal general

3548:   semantics with the witness properties?  That is, can we define

3549:   an operational semantics analogous to the conservative

3550:   semantics, but with respect to which all goals with the witness

3551:   properties do not

3552:   flounder?  The answer to this question may lie with different

3553:   strategies for coping with negation.

3554: \item Can a mode {\it inference} system be devised which ensures

3555:   non-floundering of goals?  That is, can we automate the process of

3556:   defining modes for a program that will guarantee that no goal

3557:   consistent with the inferred modes of the program's predicates

3558:   will flounder?

3559: \end{itemize}

3560: 

3561: We have implemented the ideas contained in this paper in an

3562: experimental proof assistant program called SVP (Spreadsheet

3563: Verifier for Prolog), whose user interface has been described

3564: in \cite{andrews-spreadsheet-uitp}.  SVP transforms a Prolog

3565: program with cuts into completed form, and then assists the user

3566: in proving theorems in an assertion language similar to those

3567: defined in \cite{andrews-phd-dd,staerk-lptp-jlp}.  We hope to

3568: report on this work in the future.

3569: 

3570: 

3571: 

3572: \section{Acknowledgements}

3573: 

3574: Thanks to Ver\'{o}nica Dahl and the Logic and Functional

3575: Programming Laboratory at Simon Fraser University for the use of

3576: their facilities in preparing this material.  Thanks also to Kai

3577: Salomaa for clarification on terminology.  Michel Billaud,

3578: Robert \Staerk{}, and Torkel Franzen helped with the original

3579: conference version of this paper, and the anonymous journal

3580: referees contributed valuable comments and corrections.

3581: This research is supported by

3582: an NSERC (Natural Sciences and Engineering Research Council of

3583: Canada) Individual Research Grant.

3584: 

3585: 

3586: 

3587: 

3588: \bibliography{tplp}

3589: 

3590: \setcounter{section}{0}

3591: \appendix

3592: \newpage

3593: 

3594: 

3595: \section{Proofs of Results}

3596: \label{proofs-appx}

3597: 

3598: \subsection{Completion Algorithm Properties}

3599: 

3600: \noindent

3601: {\bf Lemma \ref{completed-goal-stack-lemma}.}

3602: \begin{quote} \it

3603:   Let $\alpha$ be a goal stack.

3604:   Let $\alpha'$ be $\alpha$

3605:   with any number of occurrences of a sequence $B, C$ in a goal stack or

3606:   clause body replaced by $B \And C$, where $B$ and $C$ are

3607:   formulas.

3608:   Then $(\theta: \alpha \Goes{P} \rho)$ in the liberal general semantics

3609:   iff  $(\theta: \alpha' \Goes{P} \rho)$ in the liberal general semantics.

3610: \end{quote}

3611: 

3612: \begin{proof}

3613: By induction on the number of replacements of $B, C$ by

3614: $B \And C$.  The base case (0 replacements) is trivial.  For the

3615: inductive case, it suffices to demonstrate the case where

3616: $\alpha'$ is derived from $\alpha$ by one replacement of $B, C$

3617: by $B \And C$.  This in turn we prove by induction on the

3618: structure of the computation of $\alpha$.

3619: If $\alpha$ begins with $B, C$ and $\alpha'$ begins

3620: with $B \And C$, then the computation of $\alpha'$ can be derived

3621: from that of $\alpha$ with one Conj step.  Otherwise, either the

3622: first formulas in the two goal stacks are identical, or they

3623: have the same top-level connective; in either case, regardless

3624: of the bottommost rule applied, the result

3625: follows straightforwardly from the induction hypothesis.

3626: \end{proof}

3627: 

3628: \noindent

3629: {\bf

3630:   Lemma \ref{conjoin-lemma}.

3631: }

3632: \begin{quote} \it

3633:   Let $P'$ be $P$ with some sequence $B, C$ in a clause body

3634:   replaced by $B \And C$.

3635:   Then $\theta: \alpha \Goes{P} \rho$ in the liberal general semantics

3636:   iff  $\theta: \alpha \Goes{P'} \rho$ in the liberal general semantics.

3637: \end{quote}

3638: 

3639: \begin{proof}

3640: By the Lemma, we can add new rules to the operational

3641: semantics as follows:

3642: \[ (1) \frac{\theta: \alpha' \Goes{P} \rho}

3643: 	{\theta: \alpha \Goes{P} \rho}

3644:    \Sep

3645:    (2) \frac{\theta: \alpha \Goes{P} \rho}

3646: 	{\theta: \alpha' \Goes{P} \rho}

3647: \]

3648: where $\alpha'$ is $\alpha$ with any number of occurrences of a

3649: sequence $B, C$ in a goal stack or clause body replaced by

3650: $B \And C$.  Moreover, by the

3651: Lemma, we can essentially insert applications of these rules anywhere in a

3652: computation and derive a computation of the premise from the

3653: computation of the conclusion.

3654: 

3655: Therefore the ($\rightarrow$)

3656: direction of the theorem can be proven as follows.  Given the

3657: computation of $\theta: \alpha \Goes{P} \rho$, insert an

3658: application of (1) above each Pred rule involving the clause

3659: transformed in $P'$, obtaining the computation of the premise

3660: from the Lemma.

3661: The transformed proof will have sections of the form:

3662: \begin{center}

3663: \begin{tabular}{c}

3664:   $\theta: p(\vec{t})using(\gamma'), \alpha \Goes{P} \rho$ \\

3665:   $\overline{\underline{

3666:     \theta: p(\vec{t})using(\gamma), \alpha \Goes{P} \rho

3667:   }}$ \\

3668:   $\theta: p(\vec{t}), \alpha \Goes{P} \rho$ \\

3669: \end{tabular}

3670: \end{center}

3671: To obtain the computation of $\theta: \alpha \Goes{P'} \rho$,

3672: replace each such section by 

3673: \begin{center}

3674: \begin{tabular}{c}

3675:   $\underline{

3676:     \theta: p(\vec{t})using(\gamma'), \alpha \Goes{P'} \rho

3677:   }$ \\

3678:   % \hline

3679:   $\theta: p(\vec{t}), \alpha \Goes{P'} \rho$ \\

3680: \end{tabular}

3681: \end{center}

3682: and replace $P$ by $P'$ everywhere else.

3683: The other

3684: direction of the theorem can be proven by inverting this operation. 

3685: \end{proof}

3686: 

3687: \noindent

3688: {\bf

3689:   Theorem \ref{result-preservation-thm}.

3690: }

3691: \begin{quote} \it

3692:   The completion algorithm preserves result according to

3693:   the liberal general operational semantics.  That is,

3694:   if $P'$ is the completion of $P$, then

3695:   $\theta: \alpha \Goes{P} \rho$ in the liberal general semantics iff

3696:   $\theta: \alpha \Goes{P'} \rho$ in the liberal general semantics.

3697: \end{quote}

3698: 

3699: \begin{proof}

3700: We prove the theorem by proving that each of the

3701: transformations preserves result.  In what follows, we will

3702: refer to the original program as $P$ and the program after

3703: the single transformation in question as $P'$.

3704: 

3705: Step 2.2:

3706: Clearly the two computations are equivalent up to a renaming

3707: of some of the variables involved in the computations.

3708: 

3709: Step 2.3:

3710: It suffices to show that any application of any of the four

3711: $using$ rules with $P$ correspond to parts of computations with

3712: $P'$.  Consider an application of the Using/nocut/succ rule with

3713: $P$, where the formula being considered is an application of

3714: predicate $p$.  The bottommost portion of the computation is:

3715: \begin{center}

3716: \begin{tabular}{c}

3717:   $\underline{\theta\xi: \eta\xi, \alpha\xi \Goes{} \theta'}$ \\

3718:   $\vdots$ \\

3719:   $\overline{\theta: (s_1=t_1), \ldots, (s_k=t_k),

3720:             \ldots, (s_n=x_n), \eta, \alpha \Goes{} \theta'}$ \\

3721:   $\overline{\theta: p(s_1, \ldots, s_n) using

3722:      (p(t_1, \ldots, t_k, \ldots, x_n) \colondash \eta),

3723:                                       \gamma), \alpha \Goes{} \theta'}$ \\

3724: \end{tabular}

3725: \end{center}

3726: where $\xi$ is the substitution resulting from the unifications.

3727: With $P'$, the bottommost portion of the computation is the following:

3728: \begin{center}

3729: \begin{tabular}{c}

3730:   $\underline{\theta\xi': \eta\xi', \alpha\xi' \Goes{} \theta'}$ \\

3731:   $\vdots$ \\

3732:   $\overline{\theta: (s_1=t_1), \ldots, (s_k=x_k),

3733:            \ldots, (s_n=x_n), (x_k=t_k), \eta, \alpha \Goes{} \theta'}$ \\

3734:   $\overline{\theta: p(s_1, \ldots, s_n) using

3735:      (p(t_1, \ldots, x_k, \ldots, x_n) \colondash (x_k=t_k), \eta),

3736:                                       \gamma), \alpha \Goes{} \theta'}$ \\

3737: \end{tabular}

3738: \end{center}

3739: where $\xi'$ is the substitution resulting from the unifications.

3740: However, by the properties of unification, we can rearrange

3741: the equality formulas in the judgement second from the bottom to read:

3742: $(s_1=t_1), \ldots, (x_k=s_k), (x_k=t_k),

3743: \ldots, (s_n=x_n)$.  This sequence makes it

3744: clear that the result substitution $\xi'$ is identical to $\xi$.

3745: The cases of the other Using rules are proven similarly.

3746: 

3747: Step 3:

3748: See Lemma \ref{conjoin-lemma} just before this theorem.

3749: 

3750: Step 4:  Let $\alpha$ be a goal stack, and let $\alpha'$ be

3751: $\alpha$ with the formula $true$ inserted anywhere in a sequence

3752: of goal stack elements or body elements.  Then

3753: $(\theta: \alpha \Goes{P} \rho)$

3754: iff $(\theta: \alpha' \Goes{P} \rho)$, by a simple structural

3755: induction.  We can then follow the same line of reasoning as in

3756: Lemma \ref{conjoin-lemma} to conclude that inserting $true$ anywhere

3757: in a clause body preserves result.

3758: 

3759: Step 5:

3760: When a clause with two consecutive cuts appears, instances of

3761: the Body/cut/succ rule will arise in which $\eta_1$ is empty;

3762: that is, a portion of some computations will be of the form

3763: \begin{center}

3764: \begin{tabular}{c}

3765:  ${\overline{\theta: \epsilon \Goes{} \theta}  \Sep

3766:   \theta: body(\eta_2), \alpha \Goes{} \rho}$ \\

3767:  \cline{1-1}

3768:  ${\theta: body(!, \eta_2), \alpha \Goes{} \rho}$ \\

3769: \end{tabular}

3770: \end{center}

3771: where the Success rule has been used at the left-hand premise.

3772: When the program is transformed to remove the second cut,

3773: this portion of the computation will be replaced by the single

3774: judgement $(\theta: body(\eta_2), \alpha \Goes{} \rho)$.

3775: 

3776: Step 6:  See Step 4 above.

3777: 

3778: Step 7:  See Step 4 above.

3779: 

3780: Step 8:

3781: The original computation may have applications of

3782: the Body/cut/succ rules of the following form:

3783: \begin{center}

3784: \begin{tabular}{c}

3785:  ${\theta: \eta_1 \Goes{} \theta'  \Sep

3786:   \theta': body(\eta_2)\theta', \alpha\theta' \Goes{} \rho}$ \\

3787:  \cline{1-1}

3788:  ${\theta: body(\eta_1, !, \eta_2), \alpha \Goes{} \rho}$ \\

3789: \end{tabular}

3790: \end{center}

3791: This part of the computation is replaced in the new computation

3792: by the following sequence:

3793: \begin{center}

3794: \begin{tabular}{ccc}

3795: $\theta[\vec{y}:=\vec{y}']: \eta_1 \Goes{} \theta'$ \\

3796: \cline{1-1}

3797: $\vdots$ \\ 

3798: \cline{1-1}

3799: $\theta: \vec{y}=\vec{y}', \eta_1[\vec{y}:=\vec{y}'] \Goes{} \theta'$ & ~~~~~ &

3800:   $\theta': body(\eta_2)\theta', \alpha\theta' \Goes{} \rho$ \\

3801: \cline{1-3}

3802: \multicolumn{3}{c}{

3803:   $\theta: q(\vec{y}) using (q(\vec{y}') \colondash \eta_1[\vec{y}:=\vec{y}'], !, \eta_2[\vec{y}:=\vec{y}']), \alpha \Goes{} \rho$

3804: } \\

3805:   \cline{1-3}

3806:   \multicolumn{3}{c}{

3807:   $\theta: q(\vec{y}), \alpha \Goes{} \rho$} \\

3808:   \multicolumn{3}{c}{

3809:   $\overline{\theta: body(q(\vec{y})), \alpha \Goes{} \rho}$} \\

3810: \end{tabular}

3811: \end{center}

3812: Note that the substitution $[\vec{y}:=\vec{y}']$ has the effect

3813: of restoring $\eta_1, \eta_2$ to their original naming.

3814: We do not show $[\vec{y}:=\vec{y}']$ elsewhere since the

3815: computations are equivalent up to renaming.

3816: 

3817: The original computation may also have applications of

3818: Body/cut/fail, which are transformed similarly.

3819: 

3820: Step 9.2:

3821: In computations with $P$, variables in the clause are renamed

3822: apart at the appropriate applications of the Pred rule.  In

3823: computations with $P'$, the $\vec{y}$ variables are bound and

3824: therefore not renamed apart.  However, they become renamed apart

3825: in Exists rule applications above the application of the Using

3826: or Body rule in which they become part of the goal stack.

3827: 

3828: Step 9.3:

3829: The original computation may have portions ending with applications

3830: of the Using/cut/succ rule, of the form \\

3831: \begin{center}

3832: \begin{tabular}{ccc}

3833: $\theta\xi: F\xi \Goes{} \theta'$ \\

3834: \cline{1-1}

3835: $\vdots$ & \Sep & $\theta': G\theta', \alpha\theta' \Goes{} \rho$ \\

3836: \cline{1-1} \cline{3-3}

3837: $\theta: \vec{t}=\vec{x}, F \Goes{} \theta'$

3838:  & & $\theta': body(G)\theta', \alpha\theta' \Goes{} \rho$ \\

3839: \cline{1-3}

3840: \multicolumn{3}{c}{

3841: $\theta: p(\vec{t}) using (p(\vec{x}) \colondash F, !, G), \alpha \Goes{} \rho$

3842: } \\

3843: \end{tabular}

3844: \end{center}

3845: where $\xi$ is the substitution

3846: resulting from the unification of $\vec{t}$ with $\vec{x}$.

3847: (Without loss of generality, to avoid confusion, we assume that

3848: the free variables of the clause are different from those in

3849: $\vec{t}$ and $\alpha$, and do not require renaming apart.)

3850: The computation with respect to $P'$ will have this portion of

3851: the computation replaced by the following:

3852: \begin{center}

3853: \begin{tabular}{ccc}

3854: $\theta\xi: F\xi \Goes{} \theta'$ & \Sep &

3855: $\theta': G\xi\theta', \alpha\xi \Goes{} \rho$ \\

3856: \cline{1-3}

3857: \multicolumn{3}{c}{

3858:   $\underline{\theta\xi: if[\vec{y}](F, G)\xi, \alpha\xi \Goes{} \rho}$

3859: } \\

3860: \multicolumn{3}{c}{$\vdots$ } \\

3861: \multicolumn{3}{c}{

3862:   $\overline{\theta: \vec{t}=\vec{x}, if[\vec{y}](F, G), \alpha \Goes{} \rho}$

3863: } \\

3864: \cline{1-3}

3865: \multicolumn{3}{c}{

3866:   $\theta: p(\vec{t}) using (p(\vec{x}) \colondash if[\vec{y}](F, G)), \alpha \Goes{} \rho$

3867: } \\

3868: \end{tabular}

3869: \end{center}

3870: However, because the $\vec{x}$ are distinct and different from the

3871: variables in $\alpha$, $\alpha\xi$ is just $\alpha$; and because

3872: $\theta'$ has arisen from $\theta\xi$, $\xi\theta' = \theta'$.  Thus the

3873: two judgements at the top of this portion of this computation

3874: are the same as the two at the top of the portion of the

3875: computation with respect to $P$.

3876: 

3877: The original computation may also have applications of Using/cut/fail,

3878: which are transformed similarly.

3879: 

3880: Step 10.2:

3881: The original computation may have portions ending in

3882: applications of the Using/nocut/succ

3883: rule, of the form

3884: \begin{center}

3885: \begin{tabular}{c}

3886: $\underline{\theta\xi: G\xi, \alpha\xi \Goes{} \rho}$ \\

3887: $\vdots$ \\

3888: $\overline{\theta: \vec{t}=\vec{x}, G, \alpha \Goes{} \rho}$ \\

3889: $\overline{\theta: p(\vec{t}) using (p(\vec{x}) \colondash G; p(\vec{x}) \colondash H), \alpha \Goes{} \rho}$ \\

3890: \end{tabular}

3891: \end{center}

3892: where $\xi$ is the substitution resulting from the unification of

3893: $\vec{t}$ with $\vec{x}$.  (Again, without loss of generality we

3894: assume the free variables of the clauses are different from those

3895: of the conclusion.)

3896: The computation with respect to $P'$ will have this portion of

3897: the computation replaced by the following:

3898: \begin{center}

3899: \begin{tabular}{c}

3900: $\underline{\theta\xi: G\xi, \alpha\xi \Goes{} \rho}$ \\

3901: $\vdots$ \\

3902: $\overline{\theta\xi: \exists\vec{y}(G)\xi, \alpha\xi \Goes{} \rho}$ \\

3903: $\underline{\overline{\theta\xi: \exists\vec{y}(G)\xi \Or H\xi, \alpha\xi \Goes{} \rho}}$ \\

3904: $\vdots$ \\

3905: $\overline{\theta: \vec{t}=\vec{x}, \exists\vec{y}(G) \Or H, \alpha \Goes{} \rho}$ \\

3906: $\overline{\theta: p(\vec{t}) using (p(\vec{x}) \colondash \exists\vec{y}(G) \Or H), \alpha \Goes{} \rho}$ \\

3907: \end{tabular}

3908: \end{center}

3909: The topmost judgements of these portions of the

3910: proof are the same.

3911: 

3912: The original computation may also have applications of Using/nocut/fail,

3913: which are transformed similarly.

3914: 

3915: Step 10.3:

3916: The original computation may have portions ending in

3917: applications of the Using/cut/succ rule, of the form

3918: \begin{center}

3919: \begin{tabular}{ccc}

3920: $\theta\xi: F\xi \Goes{} \theta'$ \\

3921: \cline{1-1}

3922: $\vdots$ & \Sep &

3923: $\theta': G\theta', \alpha\theta' \Goes{} \theta'$ \\

3924: \cline{1-1} \cline{3-3}

3925: $\theta: \vec{t}=\vec{x}, F \Goes{} \theta'$ & \Sep &

3926: $\theta': body(G)\theta', \alpha\theta' \Goes{} \theta'$ \\

3927: \cline{1-3}

3928: \multicolumn{3}{c}{

3929:   $\theta: p(\vec{t}) using (p(\vec{x}) \colondash F, !, G; p(\vec{x}) \colondash H), \alpha \Goes{} \rho$

3930: } \\

3931: \end{tabular}

3932: \end{center}

3933: where $\xi$ is the substitution resulting

3934: from the unification of $\vec{t}$ and $\vec{x}$.

3935: (Throughout, we assume the variables of the clauses are distinct

3936: from the other variables in the computation.)

3937: The computation

3938: with $P'$ will have this portion replaced by the following:

3939: \[\begin{array}{c}

3940: \underline{\theta\xi: F\xi \Goes{} \theta' \Sep 

3941:  \theta': G\xi\theta', \alpha\xi\theta' \Goes{} \rho} \\

3942: {\theta\xi: if[\vec{y}](F,G)\xi, \alpha\xi \Goes{} \rho} \\

3943: \overline{\underline{\theta\xi: if[\vec{y}](F,G)\xi \Or ((\Not\exists\vec{y}(F) \And H)\xi, \alpha\xi \Goes{} \rho}} \\

3944: \vdots \\

3945: \overline{\theta: \vec{t}=\vec{x}, if[\vec{y}](F,G) \Or ((\Not\exists\vec{y}(F) \And H), \alpha \Goes{} \rho} \\

3946: \overline{\theta: p(\vec{t}) using (p(\vec{x}) \colondash if[\vec{y}](F,G) \Or ((\Not\exists\vec{y}(F) \And H)), \alpha \Goes{} \rho} \\

3947: \end{array}\]

3948: As in Step 9.3, because of the way the substitutions were formed, the topmost

3949: judgements in this portion of the $P'$ computation are the same as

3950: those at the top of the portion of the $P$ computation.

3951: 

3952: The original computation may also have portions ending in

3953: applications of the Using/cut/fail rule, of the form

3954: \begin{center}

3955: \begin{tabular}{ccc}

3956: & & $\underline{\theta\xi: H\xi, \alpha\xi \Goes{} \rho}$ \\

3957: $\theta\xi: F\xi \Goes{} fail$ & \Sep &

3958: $\vdots$ \\

3959: \cline{1-1}

3960: $\vdots$ & \Sep &

3961: $\overline{\theta: \vec{t}=\vec{x}, H, \alpha \Goes{} \rho}$ \\

3962: \cline{1-1} \cline{3-3}

3963: $\theta: \vec{t}=\vec{x}, F \Goes{} fail$ & \Sep &

3964: $\theta: p(\vec{t}) using (p(\vec{x}) \colondash H), \alpha \Goes{} \rho$ \\

3965: \cline{1-3}

3966: \multicolumn{3}{c}{

3967:   $\theta: p(\vec{t}) using (p(\vec{x}) \colondash F, !, G; p(\vec{x}) \colondash H), \alpha \Goes{} \rho$

3968: } \\

3969: \end{tabular}

3970: \end{center}

3971: where $\xi$ is the substitution renaming the variables of the

3972: first clause apart, and $\xi'$ is the substitution resulting

3973: from the unification of $\vec{t}$ and $\vec{x}$.  The computation

3974: with $P'$ will have this portion replaced by the following:

3975: \begin{center}

3976: \begin{tabular}{ccccc}

3977: & ~ & 

3978:   $\theta\xi: F\xi \Goes{} fail$ \\

3979: \cline{3-3}

3980: & ~ & 

3981:   $\vdots$ \\

3982: \cline{3-3}

3983: & ~ & 

3984:   $\theta\xi: \exists\vec{y}(F)\xi \Goes{} fail$

3985:   & ~ & 

3986:   $\theta\xi: H\xi, \alpha\xi \Goes{} \rho$ \\

3987: \cline{3-5}

3988: $\theta\xi: F\xi \Goes{} fail$ & ~ & 

3989: \multicolumn{3}{c}{

3990:   $\theta\xi: \Not\exists\vec{y}(F)\xi, H\xi, \alpha\xi \Goes{} \rho$

3991: } \\

3992: \cline{1-1}

3993: $\theta\xi: if[\vec{y}](F,G)\xi, \alpha\xi \Goes{} fail$ & ~ & 

3994: \multicolumn{3}{c}{

3995:   $\overline{\theta\xi: (\Not\exists\vec{y}(F) \And H)\xi, \alpha\xi \Goes{} \rho}$

3996: } \\

3997: \cline{1-5}

3998: \multicolumn{5}{c}{

3999:   $\underline{\theta\xi: if[\vec{y}](F,G)\xi \Or (\Not\exists\vec{y}(F) \And H)\xi, \alpha\xi \Goes{} \rho}$

4000: } \\

4001: \multicolumn{5}{c}{

4002:   $\vdots$

4003: } \\

4004: \multicolumn{5}{c}{

4005:   $\overline{\theta: \vec{t}=\vec{x}, if[\vec{y}](F,G) \Or (\Not\exists\vec{y}(F) \And H), \alpha \Goes{} \rho}$

4006: } \\

4007: \multicolumn{5}{c}{

4008:   $\overline{\theta: p(\vec{t}) using (p(\vec{x}) \colondash if[\vec{y}](F,G) \Or (\Not\exists\vec{y}(F) \And H)), \alpha \Goes{} \rho}$

4009: } \\

4010: \end{tabular}

4011: \end{center}

4012: The three judgements at the top of this $P'$ computation portion

4013: consist of two instances of one of the judgements at the top of the

4014: $P$ portion, and one instance of the other one.

4015: 

4016: Since all the individual transformations preserve result, we

4017: conclude that the entire transformation process preserves result.

4018: \end{proof}

4019: 

4020: \subsection{Witness Properties of Conservative Semantics}

4021: 

4022: \noindent

4023: {\bf

4024:   Lemma \ref{general-failure-property-lemma}.

4025: }

4026: \begin{quote} \it

4027:   Let $\theta, \alpha$ be such that

4028:   $(\theta: \alpha \Goes{} fail)$ in the conservative semantics.

4029:   Then for any $\xi$,

4030:   $(\theta: \alpha\xi \Goes{} fail)$ in the conservative semantics.

4031: \end{quote}

4032: 

4033: \begin{proof}

4034: By induction on the structure of the computation of

4035: $(\theta: \alpha \Goes{} fail)$.

4036: Cases are on the bottommost rule applied.

4037: 

4038: Unif/succ:  Let $\sigma$ be the mgu found in the rule.

4039: If $\xi \subseteq \sigma$, then $s\xi$ and $t\xi$

4040: are identical,

4041: and the result follows from

4042: the induction hypothesis (IH).

4043: Otherwise, if $s\xi$ and $t\xi$ have mgu $\sigma'$, then

4044: since $\sigma$ is an mgu of $s$ and $t$,

4045: there must be some $\xi'$ such that $\xi\sigma' = \sigma\xi'$.

4046: The result then follows from the IH.

4047: Otherwise, $s\xi$ and $t\xi$ do

4048: not unify, and the computation fails with a single Unif/fail step.

4049: 

4050: Unif/fail:  If $s\xi$ and $t\xi$ had a unifier $\sigma$, then $s$

4051: and $t$ would have a unifier $\xi\sigma$.  Since $s$ and $t$ have

4052: no unifier, the computation of $\theta: \alpha\xi \Goes{} fail$

4053: also consists of just one Unif/fail step.

4054: 

4055: Success:  Cannot occur.

4056: 

4057: Conj, Disj/nofail, Disj/fail:  Directly from the IH.

4058: 

4059: Exists:  We have not required that the substitution $\xi$

4060: substitutes a term for $x'$.  Therefore the result follows from

4061: the IH.

4062: 

4063: Not/succ:  $B$ has no free variables, so the computation

4064: $\theta: B\xi \Goes{} fail$ is the same as that for

4065: $\theta: B \Goes{} fail$.

4066: 

4067: Not/fail:  Again, $B$ has no free variables, so the computation

4068: of the left-hand premise is the same. The result then follows from the IH.

4069: 

4070: Not/flounder, Not/sub:  cannot occur.

4071: 

4072: If/succ: We must prove that

4073: $\theta: if[\vec{x}](B, C\xi), \alpha\xi \Goes{} fail$.

4074: ($B$ has no free variables other than $\vec{x}$, and

4075: $if$ binds the variables $\vec{x}$.  We assume without

4076: loss of generality that $dom(\xi) \cap \{\vec{x}\} = \emptyset$.)

4077: For this, it suffices to prove that, for some $\theta'$,

4078: $\theta: B[\vec{x}:=\vec{x}'] \Goes{} \theta'$

4079: (which it does by assumption), and that

4080: $\theta': C\xi[\vec{x}:=\vec{x}']\theta', \alpha\xi \Goes{} fail$.

4081: Because $\vec{x}'$ do not appear in the conclusion,

4082: $C\xi[\vec{x}:=\vec{x}']\theta'$ is the same thing as

4083: $C[\vec{x}:=\vec{x}']\theta'\xi$.

4084: The result therefore follows from the induction hypothesis.

4085: 

4086: If/fail: $B$ has no free variables other than

4087: the $\vec{x}$ variables, so the computation

4088: $\theta: B[\vec{x}:=\vec{x}']\xi \Goes{} fail$ is the same as that for

4089: $\theta: B[\vec{x}:=\vec{x}'] \Goes{} fail$.

4090: By the hypothesis, this computation fails.

4091: 

4092: If/flounder, If/sub:  Cannot occur.

4093: 

4094: Pred:  Directly from the IH. 

4095: \end{proof}

4096: 

4097: \noindent

4098: {\bf

4099:   Lemma \ref{substitution-monotonicity-lemma}.

4100: }

4101: \begin{quote} \it

4102:   Let $\theta, \alpha$ be such that $\alpha\theta \equiv \alpha$ and

4103:   $\theta: \alpha \Goes{} \theta'$ in the conservative semantics.

4104:   Then $\theta' \subseteq \theta$.

4105: \end{quote}

4106: 

4107: \begin{proof}

4108: By induction on the structure of the computation.  The

4109: only rule which modifies the substitution in the judgements is

4110: the Unif/succ rule, which obviously produces a more specific

4111: substitution.  All other cases are straightforward consequences

4112: of the induction hypothesis.  

4113: \end{proof}

4114: 

4115: \noindent

4116: {\bf

4117:   Lemma \ref{general-success-property-lemma}.

4118: }

4119: \begin{quote} \it

4120:   Let $\theta, \alpha$ be such that

4121:   $\theta: \alpha \Goes{} \theta'$ in the conservative semantics.

4122:   Let $V$ be a subset of the free variables of $\alpha$.

4123:   Then for any $\xi$ grounding $V$ consistent with $\theta'$,

4124:   $\theta: \alpha\xi \Goes{} \theta'\xi$ in the conservative semantics.

4125: \end{quote}

4126: 

4127: \begin{proof}

4128: By induction on the structure of the computation.

4129: Cases are on the bottommost rule.

4130: 

4131: Unif/success:  Let $\sigma$ be the mgu found in the

4132: rule.  By substitution monotonicity, any $\xi$ grounding

4133: $V$ consistent with $\theta'$ must also ground $V$ consistent

4134: with $\sigma$.  Thus $\alpha\xi\sigma$ is the same as $\alpha\sigma\xi$,

4135: and the result follows from the induction hypothesis (IH).

4136: 

4137: Unif/fail:  Cannot occur.

4138: 

4139: Success:  Trivial.

4140: 

4141: Conj, Disj/nofail:  Directly from the IH.

4142: 

4143: Disj/fail:

4144: From the General Failure Property, we have that

4145: $\theta: B\xi, \alpha\xi \Goes{} fail$.

4146: From the IH, we have that

4147: $\theta: C\xi, \alpha\xi \Goes{} \theta'\xi$.

4148: The result follows in one Disj/fail step.

4149: 

4150: Exists:  Because $V$ is also a subset of the free variables of

4151: $B[x:=x']$, the result follows from the IH.

4152: 

4153: Not/succ:  Cannot occur.

4154: 

4155: Not/fail:  Because $B$ has no free variables, $B\xi$ is the same as

4156: $B$.  The result follows from the original left-hand premise and

4157: from the IH.

4158: 

4159: Not/flounder, Not/sub:  Cannot occur.

4160: 

4161: If/succ:  We assume without loss of generality that

4162: $dom(\xi) \cap \{\vec{x}\} = \emptyset$.  (We can do this because

4163: the $\vec{x}$ variables are renamed and thus can be prevented from

4164: appearing in $\theta'$.)  We must therefore prove that

4165: $(\theta: if[\vec{x}](B, C\xi), \alpha\xi \Goes{} \theta'\xi)$.

4166: By assumption, $\theta: B[\vec{x}:=\vec{x}'] \Goes{} \theta''$

4167: for some $\theta''$.  By the IH,

4168: $\theta'': C[\vec{x}:=\vec{x}']\theta''\xi, \alpha\xi \Goes{} \theta'\xi$.

4169: By substitution monotonicity, $\xi$ must ground $V$ consistent

4170: with $\theta''$ as well.  Thus

4171: $C[\vec{x}:=\vec{x}']\theta''\xi$ is the same as

4172: $(C\xi)[\vec{x}:=\vec{x}']\theta''$, and the result

4173: follows in one If/succ step.

4174: 

4175: If/fail, If/flounder, If/sub:  Cannot occur.

4176: 

4177: Pred:  Directly from the IH.

4178: \end{proof}

4179: 

4180: \subsection{Depth-First Normal Form Results}

4181: 

4182: \noindent

4183: {\bf

4184:   Theorem \ref{local-confluence-thm}.

4185: }

4186: \begin{quote} \it

4187:   If $A \Rw{} A_1$ and $A \Rw{} A_2$,

4188:   then there is an $A_3$ such that $A_1 \Rw{}^* A_3$ and $A_2 \Rw{}^* A_3$.

4189: \end{quote}

4190: 

4191: \begin{proof}

4192: 

4193: There are five cases, one for each of the rules R1-R5 applied

4194: to derive $A_1$ from $A$.

4195: We will give only the argument for R1, since the arguments for

4196: the rest are similar or simpler.

4197: We write $A[B_1, \ldots, B_n]$ for a formula A with

4198: distinguished subformulas $B_1, \ldots, B_n$, and

4199: $A[C_1, \ldots, C_n]$ for that formula with the distinguished

4200: $B_1, \ldots, B_n$ replaced by $C_1, \ldots, C_n$.

4201: 

4202: Let $A$ be $A[(B_1 \Or B_2) \And C]$, and $A_1$ be

4203: $A[(B_1 \And C) \Or (B_2 \And C)]$.  If $A_2$ is derived from

4204: applying R1 to the same location, the result is trivially

4205: true.  $A_2$ cannot be derived from applying R2 to the same

4206: location, because $(B_1 \Or B_2)$ is not negated-disjunction.

4207: $A_2$ also cannot be derived from applying R3-R5 to the same

4208: location.  We therefore have four subcases.

4209: In the first three subcases,

4210: $A_2$ may be one of

4211: $A[(B'_1 \Or B_2) \And C]$,

4212: $A[(B_1 \Or B'_2) \And C]$, or

4213: $A[(B_1 \Or B_2) \And C']$.

4214: In the first subcase, one step from either $A_1$ or $A_2$ will

4215: lead to

4216: $A[(B'_1 \And C) \Or (B_2 \And C)]$. The second subcase is similar.

4217: In the third subcase, two steps from $A_1$ and one from $A_2$ will lead to

4218: $A[(B_1 \And C') \Or (B_2 \And C')]$.

4219: The final subcase is when $A$ can be written as

4220: $A[(B_1 \Or B_2) \And C, D]$, $A_1$ is

4221: $A[(B_1 \And C) \Or (B_2 \And C), D]$, and $A_2$ is

4222: $A[(B_1 \Or B_2) \And C, D']$.  In this case, one step from

4223: either $A_1$ or $A_2$ will lead to 

4224: $A[(B_1 \And C) \Or (B_2 \And C), D']$. 

4225: \end{proof}

4226: 

4227: 

4228: \noindent

4229: {\bf

4230:   Lemma \ref{rule-decreases-pd-lemma}.

4231: }

4232: \begin{quote} \it

4233:   If $G \Rw{} G'$, then $pd(G) \geq pd(G')$.

4234: \end{quote}

4235: 

4236: \begin{proof}

4237: Clearly rules R1-R3 maintain potential depth;

4238: the difficult cases are R4 and R5.

4239: 

4240: Case R4:

4241: If R4 was applied at the top level, then we have

4242: $G  = if[\vec{x}]((B_1 \Or B_2), C)$ and

4243: $G' = if[\vec{x}](B_1, C)

4244:      \Or

4245:      (\Not(\exists \vec{x} B_1)

4246:       \And if[\vec{x}](B_2, C))$.

4247: Let the length of $\vec{x}$ be $n$.

4248: Now we have that

4249: \[\begin{array}{llll}

4250:   pd(G') & = & \multicolumn{2}{l}{pd(if[\vec{x}](B_1, C) \Or

4251:                   (\Not(\exists \vec{x} B_1) \And if[\vec{x}](B_2, C))} \\

4252: 

4253:          & = & max( & pd(if[\vec{x}](B_1, C)+1, \\

4254:          & & &        pd(\Not(\exists \vec{x} B_1) \And if[\vec{x}](B_2, C))+1) \\

4255: 

4256:          & = & max( & 1+n+2pd(B_1)+max(pd(B_1), pd(C)), \\

4257:          & & &        pd(\Not(\exists \vec{x} B_1) \And if[\vec{x}](B_2, C))+1) \\

4258: 

4259:          & = & max( & 1+n+3pd(B_1),  1+n+2pd(B_1)+pd(C), \\

4260:          & & &        pd(\Not(\exists \vec{x} B_1)+2, \\

4261:          & & &        pd(if[\vec{x}](B_2, C))+2) \\

4262: 

4263:          & = & max( & 1+n+3pd(B_1),  1+n+2pd(B_1)+pd(C), \\

4264:          & & &        3+n+pd(B_1), \\

4265:          & & &        2+n+2pd(B_2)+max(pd(B_2), pd(C)) \\

4266: 

4267:          & = & max( & 1+n+3pd(B_1),  1+n+2pd(B_1)+pd(C), \\

4268:          & & &        3+n+pd(B_1), \\

4269:          & & &        2+n+3pd(B_2),  2+n+2pd(B_2)+pd(C)) \\

4270: 

4271:          & = & max( & 1+n+3pd(B_1),  1+n+2pd(B_1)+pd(C), \\

4272:          & & &        2+n+3pd(B_2),  2+n+2pd(B_2)+pd(C)) \\

4273: \end{array}\]

4274: There are now two subcases.  Subcase 1: if $pd(B_1) > pd(B_2)$, then

4275: \[\begin{array}{lll}

4276:   pd(G) & = & pd(if[\vec{x}]((B_1 \Or B_2), C) \\

4277:         & = & n + 2pd(B_1 \Or B_2) + max(pd(B_1 \Or B_2), pd(C)) \\

4278:         & = & n + 2 + 2pd(B_1) + max(1+pd(B_1), pd(C)) \\

4279:         & = & max(3+n+3pd(B_1), 2+n+2pd(B_1)+pd(C)) \\

4280: \end{array}\]

4281: and $pd(G')$ simplifies to $max(1+n+3pd(B_1),  1+n+2pd(B_1)+pd(C))$.

4282: Thus if $pd(C) > pd(B_1)$, we have

4283: \[ pd(G) =~ (2+n+2pd(B_1)+pd(C)) ~>~ (1+n+2pd(B_1)+pd(C)) ~= pd(G')

4284: \]

4285: and otherwise ($pd(C) \leq pd(B_1)$) we have

4286: \[ pd(G) =~ (3+n+3pd(B_1)) ~>~ (1+n+3pd(B_1)) ~= pd(G')

4287: \]

4288: so in both cases, $pd(G) > pd(G')$.

4289: 

4290: Subcase 2: otherwise, $pd(B_2) \geq pd(B_1)$.  We have:

4291: \[\begin{array}{lll}

4292:   pd(G) & = & max(3+n+3pd(B_2), 2+n+2pd(B_2)+pd(C)) \\

4293: \end{array}\]

4294: and $pd(G')$ simplifies to $max(2+n+3pd(B_2), 2+n+2pd(B_2)+pd(C))$.

4295: Thus if $pd(C) > pd(B_2)$, we have

4296: \[ pd(G) =~ (2+n+2pd(B_2)+pd(C)) ~=~ (2+n+2pd(B_2)+pd(C)) ~= pd(G')

4297: \]

4298: and otherwise ($pd(C) \leq pd(B_1)$) we have

4299: \[ pd(G) =~ (3+n+3pd(B_2)) ~>~ (2+n+3pd(B_2)) ~= pd(G')

4300: \]

4301: so in both cases, $pd(G) \geq pd(G')$.

4302: 

4303: Similarly, if R4 was applied not at the top level,

4304: $pd(G) \geq pd(G')$, since if any subformula is transformed

4305: to have lower potential depth, the whole formula has lower

4306: potential depth.

4307: 

4308: If R5 was applied at the top level, we have

4309: $pd(G) = pd(if[\vec{x}](B, C)) = n + 2pd(B) + max(pd(B), pd(C)) =

4310: max(n+3pd(B), n+2pd(B)+pd(C))$, and

4311: $pd(G') = pd(\exists \vec{x} (B \And C)) = 1+n+max(pd(B), pd(C)) =

4312:  max(1+n+pd(B), 1+n+pd(C))$.

4313: If $pd(B) > pd(C)$, then

4314: \[

4315:   pd(G) =~ n+3pd(B) ~>~ 1+n+pd(B) ~= pd(G')

4316: \]

4317: and otherwise

4318: \[

4319:   pd(G) =~ n+2pd(B)+pd(C) ~>~ 1+n+pd(C) ~= pd(G')

4320: \]

4321: Thus in both cases $pd(G) > pd(G')$.

4322: 

4323: Similarly, if R5 was applied not at the top level,

4324: $pd(G) > pd(G')$.

4325: \end{proof}

4326: 

4327: \noindent

4328: {\bf

4329:   Corollary \ref{unique-normal-form-cor}.

4330: }

4331: \begin{quote} \it

4332:   For every formula $G$ not in normal form, there is a unique

4333:   formula $G''$ in normal form, such that for all $G'$ such that

4334:   $G \Rw{} G'$, we have that $G' \Rw{}^* G''$.

4335: \end{quote}

4336: 

4337: \begin{proof}

4338: Let $k$ be the length of the longest chain of

4339: rewritings that starts with $G$ (by Theorem

4340: \ref{termination-thm} we know that this bound exists).  We prove

4341: the corollary by induction on $k$.  In the base case ($k=1$),

4342: we know from Theorem \ref{local-confluence-thm} that there

4343: can be at most one unique $G'$ such that $G \Rw{} G'$; hence,

4344: $G''$ is this $G'$.  In the inductive case, if there is a

4345: unique $G'$ such that $G \Rw{} G'$, the result follows from the

4346: induction hypothesis.  If there is more than one, then for each

4347: pair $G_1$ and $G_2$ such that $G \Rw{} G_1$ and $G \Rw{} G_2$,

4348: by Theorem \ref{local-confluence-thm}

4349: there is some $G_3$ such that $G_1 \Rw{}^* G_3$ and $G_2 \Rw{}^* G_3$.

4350: But by the induction hypothesis, there is some unique normal

4351: form not only of $G_3$ but also of $G_1$ and $G_2$.  Because

4352: $G_1 \Rw{}^* G_3$, the normal form of $G_3$ must be the same as

4353: that of $G_1$, and similarly for $G_2$.  Hence all $G'$

4354: such that $G \Rw{} G'$ must have some unique normal form $G''$.

4355: This therefore is the unique normal form of $G$.  

4356: \end{proof}

4357: 

4358: \noindent

4359: {\bf

4360:   Theorem \ref{general-result-pres-thm}.

4361: }

4362: \begin{quote} \it

4363:   If $\alpha'$ is $\alpha$

4364:   with some formulas transformed by applications of rules R1-R5,

4365:   then $\theta: \alpha \Goes{} \rho$ in the pessimistic semantics iff

4366:   $\theta: \alpha' \Goes{} \rho$ in the pessimistic semantics.

4367: \end{quote}

4368: 

4369: \begin{proof}

4370: By induction on the structure of the assumption computation.

4371: If the application of the rules has not changed

4372: the top-level connective of the first formula in $\alpha$, then the result

4373: follows by the induction hypothesis.  Otherwise, we have cases

4374: according to which of R1-R5 was used to transform the top-level

4375: connective of the first formula.

4376: 

4377: Cases R1-R3 are very similar to the proof in \cite{andrews-lnaf-tcs}

4378: and will not be repeated here.

4379: 

4380: Case R4:  The two computations are

4381: $(\theta: if[\vec{x}((B_1 \Or B_2), C), \alpha \Goes{} \rho)$ and

4382: $(\theta: if[\vec{x}](B_1, C)

4383:      \Or

4384:      (\Not(\exists \vec{x} B_1)

4385:       \And if[\vec{x}](B_2, C)), \alpha \Goes{} \rho)$;

4386: we must show that each implies the other.

4387: There are several subcases.

4388: 

4389: If $(\theta: B_1[\vec{x}:=\vec{x}'] \Goes{} \theta')$ and

4390: $(\theta': C\theta', \alpha \Goes{} \rho)$,

4391: where $\rho$ is either some $\theta''$ or $diverge$,

4392: then we have the following original computation:

4393: \begin{center}

4394: \begin{tabular}{ccc}

4395: $\theta: B_1[\vec{x}:=\vec{x}'] \Goes{} \theta'$ \\

4396: \cline{1-1}

4397: $\theta: (B_1 \Or B_2)[\vec{x}:=\vec{x}'] \Goes{} \theta'$

4398:   & \Sep &

4399:   $\theta': C\theta', \alpha \Goes{} \rho$ \\

4400: \cline{1-3}

4401: \multicolumn{3}{c}{

4402:   $\theta: if[\vec{x}((B_1 \Or B_2), C), \alpha \Goes{} \rho$

4403: } \\

4404: \end{tabular}

4405: \end{center}

4406: The corresponding computation with the transformed formula is:

4407: \begin{center}

4408: \begin{tabular}{ccc}

4409: $\theta: B_1[\vec{x}:=\vec{x}'] \Goes{} \theta'$

4410:   & \Sep \Sep &

4411:   $\theta': C\theta', \alpha \Goes{} \rho$ \\

4412: \cline{1-3}

4413: \multicolumn{3}{c}{

4414:   $\theta: if[\vec{x}](B_1, C) \alpha \Goes{} \rho$

4415: } \\

4416: \cline{1-3}

4417: \multicolumn{3}{c}{

4418:   $\theta: if[\vec{x}](B_1, C)

4419:      \Or

4420:      (\Not(\exists \vec{x} B_1)

4421:       \And if[\vec{x}](B_2, C)), \alpha \Goes{} \rho$

4422: } \\

4423: \end{tabular}

4424: \end{center}

4425: 

4426: If $(\theta: B_1[\vec{x}:=\vec{x}'] \Goes{} \theta')$ but

4427: $(\theta': C\theta', \alpha \Goes{} fail)$,

4428: then we have the following original computation:

4429: \begin{center}

4430: \begin{tabular}{ccc}

4431: $\theta: B_1[\vec{x}:=\vec{x}'] \Goes{} \theta'$ \\

4432: \cline{1-1}

4433: $\theta: (B_1 \Or B_2)[\vec{x}:=\vec{x}'] \Goes{} \theta'$

4434:   & \Sep &

4435:   $\theta': C\theta', \alpha \Goes{} fail$ \\

4436: \cline{1-3}

4437: \multicolumn{3}{c}{

4438:   $\theta: if[\vec{x}((B_1 \Or B_2), C), \alpha \Goes{} fail$

4439: } \\

4440: \end{tabular}

4441: \end{center}

4442: %

4443: The corresponding computation with the transformed formula is:

4444: \begin{center}

4445: \begin{tabular}{ccc}

4446: & &

4447:   $\underline{\theta: B_1[\vec{x}:=\vec{x}'] \Goes{} \theta'}$ \\

4448: & &

4449:   $\vdots$ \\

4450: & &

4451:   $\overline{\theta: \exists \vec{x} B_1 \Goes{} \theta'}$ \\

4452: & &

4453:   $\overline{\theta:

4454:      \Not(\exists \vec{x} B_1),

4455:       if[\vec{x}](B_2, C), \alpha \Goes{} fail}$ \\

4456: \cline{1-1} \cline{3-3}

4457: $\theta: if[\vec{x}](B_1, C) \alpha \Goes{} fail$

4458:   & \Sep &

4459:   $\theta:

4460:      (\Not(\exists \vec{x} B_1)

4461:       \And if[\vec{x}](B_2, C)), \alpha \Goes{} fail$ \\

4462: \cline{1-3}

4463: \multicolumn{3}{c}{

4464:   $\theta: if[\vec{x}](B_1, C)

4465:      \Or

4466:      (\Not(\exists \vec{x} B_1)

4467:       \And if[\vec{x}](B_2, C)), \alpha \Goes{} fail$

4468: } \\

4469: \end{tabular}

4470: \end{center}

4471: where the computation of the left-hand premise of the bottommost

4472: judgement is as follows:

4473: \begin{center}

4474: \begin{tabular}{ccc}

4475:   $\theta: B_1[\vec{x}:=\vec{x}'] \Goes{} \theta'$ & \Sep &

4476:   $\theta': C\theta, \alpha \Goes{} fail$ \\

4477: \cline{1-3}

4478: \multicolumn{3}{c}{

4479:   $\theta: if[\vec{x}](B_1, C) \alpha \Goes{} fail$

4480: } \\

4481: \end{tabular}

4482: \end{center}

4483: 

4484: We have very similar cases when 

4485: $(\theta: B_1[\vec{x}:=\vec{x}'] \Goes{} fail)$ but

4486: $(\theta: B_2[\vec{x}:=\vec{x}'] \Goes{} \theta')$,

4487: depending on the result of $(\theta': C\theta', \alpha)$.

4488: 

4489: When both

4490: $(\theta: B_1[\vec{x}:=\vec{x}'] \Goes{} fail)$ and

4491: $(\theta: B_2[\vec{x}:=\vec{x}'] \Goes{} fail)$, we have

4492: the following original computation:

4493: \begin{center}

4494: \begin{tabular}{c}

4495: $\theta: B_1[\vec{x}:=\vec{x}'] \Goes{} fail$ \Sep

4496:   $\theta: B_2[\vec{x}:=\vec{x}'] \Goes{} fail$ \\

4497: \cline{1-1}

4498: $\theta: (B_1 \Or B_2)[\vec{x}:=\vec{x}'] \Goes{} fail$ \\

4499: $\overline{\theta: if[\vec{x}((B_1 \Or B_2), C), \alpha \Goes{} fail}$ \\

4500: \end{tabular}

4501: \end{center}

4502: %

4503: The corresponding computation with the transformed formula is:

4504: %

4505: \begin{center}

4506: \begin{tabular}{ccc}

4507: $\theta: B_1[\vec{x}:=\vec{x}'] \Goes{} fail$ \\

4508: \cline{1-1}

4509: $\theta: if[\vec{x}](B_1, C), \alpha \Goes{} fail$

4510:   & \Sep &

4511:   $\theta: (\Not(\exists \vec{x} B_1)

4512:       \And if[\vec{x}](B_2, C)), \alpha \Goes{} fail$ \\

4513: \cline{1-3}

4514: \multicolumn{3}{c}{

4515:   $\theta: if[\vec{x}](B_1, C)

4516:      \Or

4517:      (\Not(\exists \vec{x} B_1)

4518:       \And if[\vec{x}](B_2, C)), \alpha \Goes{} fail$

4519: } \\

4520: \end{tabular}

4521: \end{center}

4522: %

4523: where the computation of the right-hand premise of the

4524: bottommost judgement is:

4525: %

4526: \begin{center}

4527: \begin{tabular}{ccc}

4528: $\theta: B_1[\vec{x}:=\vec{x}'] \Goes{} fail$ \\

4529: \cline{1-1}

4530: $\vdots$ & &

4531:   $\theta: B_2[\vec{x}:=\vec{x}'] \Goes{} fail$ \\

4532: \cline{1-1}

4533: \cline{3-3}

4534: $\theta: \exists \vec{x} B_1 \Goes{} fail$

4535:   & \Sep &

4536:   $\theta: if[\vec{x}](B_2, C), \alpha \Goes{} fail$ \\

4537: \cline{1-3}

4538: \multicolumn{3}{c}{

4539:   $\theta: \Not(\exists \vec{x} B_1),

4540:        if[\vec{x}](B_2, C), \alpha \Goes{} fail$

4541: } \\

4542: \multicolumn{3}{c}{

4543:   $\overline{\theta: (\Not(\exists \vec{x} B_1)

4544:       \And if[\vec{x}](B_2, C)), \alpha \Goes{} fail}$

4545: } \\

4546: \end{tabular}

4547: \end{center}

4548: 

4549: The subcases in which a result of $diverge$ arises are similar

4550: to those in which a result of $fail$ arises.

4551: 

4552: Case R5:  The two computations are

4553: $(\theta: if[\vec{x}](B, C), \alpha \Goes{} \rho)$

4554: and $(\theta: \exists \vec{x} (B \And C), \alpha \Goes{} \rho)$;

4555: we must show that one implies the other.

4556: We also know that $B$ is negated-disjunction.

4557: There are two subcases.

4558: 

4559: If $(\theta: B[\vec{x}:=\vec{x}'] \Goes{} \theta')$,

4560: then we have the following original computation:

4561: \begin{center}

4562: \begin{tabular}{ccc}

4563: $\theta: B[\vec{x}:=\vec{x}'] \Goes{} \theta'$

4564:   & \Sep &

4565:   $\theta': C[\vec{x}:=\vec{x}']\theta', \alpha \Goes{} \rho$ \\

4566: \cline{1-3}

4567: \multicolumn{3}{c}{

4568:   $\theta: if[\vec{x}](B, C), \alpha \Goes{} \rho$

4569:   } \\

4570: \end{tabular}

4571: \end{center}

4572: However, because $B$ is negated-disjunction, every computation

4573: in the pessimistic semantics with

4574: substitution and goal stack $(\theta: B[\vec{x}:=\vec{x}'], \alpha')$

4575: must contain a substitution and goal stack

4576: $(\theta': \alpha')$.  (See Lemma 4.6 of 

4577: \cite{andrews-lnaf-tcs}.)  Thus we have

4578: the following computation with the transformed formula:

4579: \begin{center}

4580: \begin{tabular}{c}

4581: $\underline{\theta': C[\vec{x}:=\vec{x}']\theta', \alpha\theta' \Goes{} \rho}$ \\

4582: $\vdots$ \\

4583: \cline{1-1}

4584: $\theta: B[\vec{x}:=\vec{x}'], C[\vec{x}:=\vec{x}'], \alpha \Goes{} \rho$ \\

4585: \cline{1-1}

4586: $\underline{\theta: (B \And C)[\vec{x}:=\vec{x}'], \alpha \Goes{} \rho}$ \\

4587: $\vdots$ \\

4588: $\overline{\theta: \exists \vec{x} (B \And C), \alpha \Goes{} \rho}$ \\

4589: \end{tabular}

4590: \end{center}

4591: However, since $\theta'$ applies only to the free variables

4592: of $B[\vec{x}:=\vec{x}']$, which are $\vec{x}'$, and $\alpha$

4593: does not contain these variables, the topmost judgement is

4594: equivalent to

4595: $(\theta': C[\vec{x}:=\vec{x}']\theta', \alpha \Goes{} \rho)$.

4596: 

4597: Otherwise, $(\theta: B[\vec{x}:=\vec{x}'] \Goes{} \rho)$ where

4598: $\rho$ is $fail$ or $diverge$.  In this subcase, the

4599: bottom of the original computation is as follows:

4600: \begin{center}

4601: \begin{tabular}{c}

4602: $\theta: B[\vec{x}:=\vec{x}'] \Goes{} \rho$ \\

4603: \cline{1-1}

4604: $\theta: if[\vec{x}](B, C), \alpha \Goes{} \rho$ \\

4605: \end{tabular}

4606: \end{center}

4607: %

4608: The bottom of the computation with the transformed formula is as follows:

4609: %

4610: \begin{center}

4611: \begin{tabular}{c}

4612: $\theta: B[\vec{x}:=\vec{x}'], C[\vec{x}:=\vec{x}'], \alpha \Goes{} \rho$ \\

4613: \cline{1-1}

4614: $\underline{\theta: (B \And C)[\vec{x}:=\vec{x}'], \alpha \Goes{} \rho}$ \\

4615: $\vdots$ \\

4616: $\overline{\theta: \exists \vec{x} (B \And C), \alpha \Goes{} \rho}$ \\

4617: \end{tabular}

4618: \end{center}

4619: The presence of the extra formulas

4620: ($C[\vec{x}:=\vec{x}']$ and $\alpha$)

4621: has no effect on the computation.

4622: \end{proof}

4623: 

4624: 

4625: 

4626: \label{lastpage}

4627: \end{document}

4628: