1: \documentclass{LMCS}

2: \usepackage{amsmath, amssymb, hyperref}

3: 

4: %\usepackage[margin=1.5in]{geometry}

5: %\usepackage{srcltx}

6: %\usepackage{showkeys}

7: 

8: %\usepackage{csh}

9: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

10: %

11: % begin contents of csh.sty

12: %

13: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

14: 

15: % General typesetting stuff -- not specific to KA.

16: 

17: % \dsp = display space, the space before punctuation in displayed formulas.

18: \newcommand\dsp{\enspace} 

19: \newcommand\eg{\textit{e.g.}} 

20: \newcommand\Eg{\textit{E.g.}} 

21: \newcommand\ie{\textit{i.e.}} 

22: \newcommand\Ie{\textit{I.e.}}

23: \newcommand\etc{\textit{etc}} %Must add . yourself.

24: \newcommand\set[2]{\{\,#1 \mid #2\,\}}

25: \renewcommand\emptyset{\varnothing}

26: 

27: % Classes of algebras

28: 

29: \newcommand\IS{\ensuremath{\mathsf{IS}}}

30: \newcommand\IST{\ensuremath{\mathsf{IST}}}

31: \newcommand\KA{\ensuremath{\mathsf{KA}}}

32: \newcommand\KAT{\ensuremath{\mathsf{KAT}}}

33: \newcommand\KAS{\ensuremath{\mathsf{KA}^*}}

34: \newcommand\KATS{\ensuremath{\mathsf{KAT}^*}}

35: \newcommand\RKA{\ensuremath{\mathsf{RKA}}}

36: \newcommand\PRKA{\ensuremath{\mathsf{PRKA}}}

37: \newcommand\RKAT{\ensuremath{\mathsf{RKAT}}}

38: \newcommand\NRKA{\ensuremath{\mathsf{NRKA}}}

39: \newcommand\NRKAT{\ensuremath{\mathsf{NRKAT}}}

40: %\newcommand\BIG{\ensuremath{\mathsf{BIG}}}

41: %\newcommand\SMALL{\ensuremath{\mathsf{SMALL}}}

42: 

43: %\newcommand\comp{\mathbin{\circ}}

44: \newcommand\imp{\mathbin{\rightarrow}}

45: \newcommand\Imp{\mathbin{\Rightarrow}}

46: \newcommand\Rex{\ensuremath{\mathsf{RExp}}}

47: \newcommand\RexS{\ensuremath{\Rex_\Sigma}}

48: %\newcommand\ostar{\odot\!\!*}  %Make me better.

49: \newcommand\ostar{{\mathpunct{\circledast}}} % We want it to be treated like *.

50: 

51: \newcommand\Tr{\ensuremath{\mathsf{Tr}}}

52: 

53: \renewcommand\P{\ensuremath{\mathsf{P}}}

54: \newcommand\B{\ensuremath{\mathsf{B}}}

55: \newcommand\C{\ensuremath{\mathsf{C}}}

56: \newcommand\RexPB{\ensuremath{\Rex_{\P,\B}}}

57: \newcommand\Rexpb{\RexPB\typeout{Rexpb deprecated}} %deprecated

58: 

59: \newcommand\REG{\ensuremath{\mathsf{REG}}}

60: \newcommand\id{\iota}

61: \newcommand\Horn[1]{\ensuremath{\mathcal{H}#1}}

62: \newcommand\complementop{\ensuremath{\overline{\vphantom{t}~~}}}

63: 

64: \newcommand\nats{\mathbb{N}}

65: 

66: %\newcommand\rel[1]{\mathcal{R}(#1)}

67: \newcommand\rel[1]{2^{#1 \times #1}}

68: 

69: \newcommand\PSPACE{{\it PSPACE}}

70: \newcommand\swap{\mathrm{swap}}

71: 

72: %\def\ifundefined#1{\expandafter\ifx\csname#1\endcsname\relax}

73: %\ifundefined{qed}\newcommand\qed{\mbox{}~\hfill~$\Box$}\else\relax\fi

74: %\newenvironment{proof}[1][\proofname]{\textbf{#1\ \ }}{\qed}

75: %\providecommand{\proofname}{Proof}

76: 

77: \newenvironment{comment}{\sf}{}

78: %\newenvironment{proofof}[1]{\textbf{Proof of #1\ \ }}{\qed}

79: %\newtheorem{dfn}{Definition}[chapter]

80: %\newtheorem{dfn}{Definition}[section]

81: % \newtheorem{dfn}{Definition}

82: % \newtheorem{lemma}[dfn]{Lemma}

83: % \newtheorem{theorem}[dfn]{Theorem}

84: % \newtheorem{corollary}[dfn]{Corollary}

85: % \newtheorem{proposition}[dfn]{Proposition}

86: % \newtheorem{conjecture}[dfn]{Conjecture}

87: % \newtheorem{example}[dfn]{Example}

88: 

89: % For prooftheory

90: \newcommand\con{\ensuremath{\mathrm{CON}}}

91: \newcommand\nfa{\ensuremath{\mathrm{NFA}}}

92: \newcommand\comb{\ensuremath{\mathrm{comb}}}

93: \newcommand\below{\ensuremath{\mathrm{below}}}

94: \newcommand\new{\ensuremath{\mathrm{new}}}

95: \newcommand\cl{\ensuremath{\mathrm{cl}}}

96: \newcommand\starp{\ensuremath{\mathrm{sp}}}

97: \newcommand\edge[1]{\stackrel{#1}{\rightarrow}}

98: \newcommand\nedge[1]{\stackrel{#1}{\nrightarrow}}

99: \newcommand\ins{\ensuremath{\mathsf{insert}}}

100: \newcommand\insr{\ensuremath{\ins}}

101: \newcommand\insf{\ensuremath{\ins_F}}

102: \newcommand\insone{\ensuremath{\ins_{1}}}

103: 

104: % For rkacomplete

105: %\newcommand\Mred{\ensuremath{\rightarrow_M}}

106: \newcommand\Mred{\ensuremath{\edge{M}}}

107: %\newcommand\Mredstar{\ensuremath{\stackrel{M}{\rightarrow^*}}}

108: \newcommand\Mredstar{\mathrel{\Mred\!\!{}^*}}

109: \newcommand\nMred{\ensuremath{\nedge{M}}}

110: %\newcommand\tred{\ensuremath{\rightarrow_t}}

111: \newcommand\tred{\ensuremath{\edge{t}}}

112: \newcommand\ntred{\ensuremath{\nedge{t}}}

113: \newcommand\red{\ensuremath{\rightarrow}}

114: \newcommand\der{\ensuremath{\leftarrow}}

115: \newcommand\rest{\restriction}

116: 

117: % For source-simple

118: \newcommand\Cl{\mathsf{Th}\typeout{Cl deprecated; use Th}}

119: \newcommand\Th{\mathrm{Th}}

120: \newcommand\clp{\ensuremath{\textup{cl}^{+}}}  %closure under finite sums

121: \newcommand\cld{\ensuremath{\textup{cl}{\downarrow}}}  %downward closure

122: \newcommand\I{\ensuremath{\mathcal{I}}\typeout{use II instead of I}}

123: \newcommand\X{\ensuremath{\mathcal{X}}\typeout{change X to XX}}

124: \newcommand\Rexpbzero{\ensuremath{\Rex^0_{\P,\B}}}

125: \newcommand\idX{\ensuremath{\id_X}}

126: \newcommand\Ax[1]{\mathrm{Ax}(#1)}

127: \newcommand\Atoms{\mathsf{Atoms}}

128: \newcommand{\GS}{{\rm GS}}

129: \renewcommand\AA{\ensuremath{\mathcal{A}}}

130: \newcommand\LL{\ensuremath{\mathcal{L}}}

131: \def\false{\mathbf{false}}

132: \newcommand\Lpb{\ensuremath{\mathcal{L}_{\P,\B}}}

133: 

134: % For source-reduce

135: \newcommand{\redh}{\rightharpoonup}

136: \newcommand{\Rred}{\stackrel{R}{\redh}}

137: \newcommand{\SIred}{\stackrel{S,I}{\redh}}

138: \newcommand{\TIred}{\stackrel{T,I}{\redh}}

139: \newcommand{\RExp}{\mathsf{RExp}}

140: \newcommand{\sigs}{\ensuremath{{\Sigma^*}}}

141: \newcommand{\ol}[1]{\overline{#1}}

142: 

143: % For ideas/automatareduction

144: \newcommand\nf{\mathrm{nf}}

145: \newcommand\auto[1]{[#1]}

146: \newcommand\regex[1]{\{#1\}}

147: 

148: 

149: \newcommand\romanize{\def\theenumi{\roman{enumi}}\def\labelenumi{{\rm(\theenumi)}}}

150: \newcommand\intersect{\mathbin{\cap}}

151: \newcommand\union{\mathbin{\cup}}

152: 

153: % Miscellaneous

154: 

155: \newcommand\M{\mathcal{M}}

156: 

157: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

158: %

159: % end contents of csh.sty

160: %

161: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

162: 

163: \newcommand\note[1]{} %omit notes

164: \newcommand\mynote[1]{} %omit mynotes

165: \newcommand\longnote[1]{} %omit longnotes

166: 

167: \listfiles

168: 

169: \def\doi{1 (3:4) 2005}

170: \lmcsheading%

171: {\doi}

172: {15}

173: {}

174: {}

175: {Apr.~20, 2005}

176: {Dec.~21, 2005}

177: {}

178: 

179: \begin{document}

180: 

181: \title{Modularizing the Elimination of $r=0$ in Kleene Algebra}

182: \author[C.~Hardin]{Christopher Hardin}

183: \address{Department of Mathematics\\

184: Smith College\\

185: Northampton, Massachusetts 01063, USA}

186: % Cornell University\\

187: % Ithaca, New York 14853-4201, USA}

188: \email{chardin@math.smith.edu}

189: 

190: \keywords{Kleene algebra with tests, program verification, Horn formulas,

191:    proof theory}

192: \subjclass{F.3.1}

193: 

194: \begin{abstract}

195: \noindent %seems to be unnecessary, but the sample includes it.

196:   Given a universal Horn formula of Kleene algebra with hypotheses of

197:   the form $r=0$, it is already known that we can efficiently

198:   construct an equation which is valid if and only if the original

199:   Horn formula is valid.  This is an example of \emph{elimination of

200:   hypotheses}, which is useful because the equational theory of Kleene

201:   algebra is decidable while the universal Horn theory is not.  We

202:   show that hypotheses of the form $r=0$ can still be eliminated in

203:   the presence of other hypotheses.  This lets us extend any technique

204:   for eliminating hypotheses to include hypotheses of the form $r=0$.

205: % HTML version of abstract:

206: %   Given a universal Horn formula of Kleene algebra with hypotheses of

207: %   the form <I>r</I>&nbsp;=&nbsp;0, it is already known that we can

208: %   efficiently construct an equation which is valid if and only if the

209: %   Horn formula is valid.  This is an example of \emph{elimination of

210: %   hypotheses}, which is useful because the equational theory of Kleene

211: %   algebra is decidable while the universal Horn theory is not.  We show

212: %   that hypotheses of the form <I>r</I>&nbsp;=&nbsp;0 can still be

213: %   eliminated in the presence of other hypotheses.  This lets us extend

214: %   any technique for eliminating hypotheses to include hypotheses of the

215: %   form <I>r</I>&nbsp;=&nbsp;0.

216: \end{abstract}

217: 

218: \maketitle

219: 

220: %\input{intro}

221: \section{Introduction}

222: 

223: Kleene algebra (\KA) arises in many areas of computer science,

224: such as automata

225: theory, the design and analysis of algorithms, dynamic logic, and program

226: semantics.  Many of these applications are enhanced by using Kleene algebra

227: with tests (\KAT), which combines \KA\ with Boolean algebra.

228: %The use of \KAT\ in program verification largely motivates our work here.

229: 

230: We can use \KAT\ to reason propositionally about programs (see

231: \cite{BK02, KP00} for examples).

232: The equivalence of an optimized and unoptimized program, the

233: equivalence of an annotated and unannotated program, and partial correctness

234: assertions can all be expressed as equations.

235: The equational theory of \KAT\ is well understood

236: and has many useful properties; in particular, it is decidable (in

237: \PSPACE) and the theory remains unchanged when we restrict to relational

238: interpretations \cite{CKS96,KS96}.

239: (Relational interpretations are of the greatest

240: interest because the intended semantics are generally relational.)

241: 

242: However, we frequently wish to reason

243: about programs under certain assumptions about the interaction of atomic

244: programs and tests.  For example, if

245: $p$ is the program ``x := 0'' and $b$ is the assertion

246: ``x = 0'', 

247: then we want to be able to make use of the facts

248: $pb = p$ (``after running $p$, test $b$ always succeeds'')

249: and $bp = b$ (``after test $b$ succeeds, $p$ is redundant'')

250: when reasoning about programs in which $p$ and $b$

251: appear; 

252: for instance, the equation $p^2 = p$ is not valid in \KAT,

253: but the formula

254: $(pb = p~\wedge~bp = b) \rightarrow p^2 = p$ is.  Thus, 

255: the \emph{universal Horn theory} is of interest.

256: A \emph{universal Horn formula} is an implication $E \rightarrow s=t$, where

257: $E$ is a finite set of equations.  The word ``universal'' refers to the fact

258: that the atomic symbols of $E$, $s$, and $t$ are implicitly universally

259: quantified.

260: %, although we are usually only interested in specific substitution

261: %instances

262: The \emph{universal Horn theory} of a class of structures $\C$,

263: denoted $\Horn{\C}$, is the set

264: of universal Horn formulas valid under all interpretations over structures

265: in $\C$.

266: 

267: The increased generality of the universal

268: Horn theory is accompanied by greater complexity, and the theory does not

269: remain the same when we restrict to important classes of Kleene algebras

270: such as $*$-continuous Kleene algebras with tests ($\KAT^*$)

271: and relational Kleene algebras with tests (\RKAT).  $\Horn{\KAT}$ is

272: $\Sigma^0_1$-complete (undecidable),

273: $\Horn{\KAT^*}$ and $\Horn{\RKAT}$ are $\Pi^1_1$-complete (highly

274: undecidable),

275: and we have proper inclusions

276: $\Horn{\KAT} \subsetneq \Horn{\KAT^*}\subsetneq \Horn{\RKAT}$

277: \cite{Koz02,HK03}. 

278: 

279: Although these Horn theories are very complex in general, there are

280: fragments of them that are both practical and of lower complexity.

281: Consider the following theorem, fundamentally due to Cohen \cite{Coh94}

282: and extended to the form below by Kozen and Smith \cite{KS96, Koz00}.

283: (The statement uses some notions that will not be defined until later,

284: but we only need a vague understanding of it here.)

285: \begin{thm}

286: \label{thm:subsumehoare}

287: Let $r,s,t\in\RexPB$, and let $u\in\RexPB$ be the universal regular

288: expression.  Then the following are equivalent.

289: \begin{align}

290: \KAT &\models r = 0 \imp s= t\\

291: \KAT^* &\models r = 0 \imp s= t\\

292: \RKAT &\models r = 0 \imp s= t\\

293: \KAT &\models s + uru = t +uru

294: \end{align}

295: \end{thm}

296: The primary consequence of this theorem is that the Horn theory of Kleene

297: algebra, restricted to formulas with hypotheses of the form $r=0$, is

298: decidable, and remains unchanged if we restrict to $*$-continuous or

299: relational algebras: to decide if $r=0 \imp s=t$ is valid, we simply decide

300: if $s+uru = t+uru$ is valid.

301: In this way, we say that we have \emph{eliminated} the hypothesis $r=0$.

302: It is also possible to eliminate other forms of hypotheses

303: \cite{Coh94, HK02}.  

304: 

305: The case $r=0$ has particular significance, because partial correctness

306: assertions can be expressed in $\KAT$ with equations of the form $r=0$

307: (and multiple equations $r_1=0 \wedge \cdots \wedge r_k = 0$ can be

308: combined into $r_1+\cdots+r_k = 0$).

309: So Theorem~\ref{thm:subsumehoare}

310: shows that the Horn theory of $\KAT$, restricted to hypotheses of the form

311: $r=0$, subsumes propositional Hoare logic, is decidable, and is furthermore

312: complete for relational interpretations \cite{Koz00}.

313: 

314: Our main result,

315: Theorem~\ref{thm:genzeroelim} (p.~\pageref{thm:genzeroelim}),

316: improves

317: Theorem~\ref{thm:subsumehoare}

318: so that $r=0$ can be eliminated in the presence of other hypotheses.

319: This allows any other technique for eliminating hypotheses to

320: be extended to include $r=0$.  For example, if we have a technique for

321: eliminating $f=g$ alone, we can eliminate $f=g \wedge r=0$ by first eliminating

322: $r=0$ using Theorem~\ref{thm:genzeroelim}, leaving hypothesis $f=g$, which

323: can then be eliminated.  In this way, Theorem~\ref{thm:genzeroelim} is like

324: a module for eliminating $r=0$ that can be added on to any other technique

325: for eliminating hypotheses.

326: 

327: A related result, Corollary~\ref{cor:syntactichomo}, shows that

328: hypotheses of the form $cp=c$ (where

329: $c$ is Boolean and $p$ is atomic) can

330: be eliminated in the presence of other hypotheses, although the

331: remaining hypotheses are modified.

332: Hypotheses of the form $cp=c$ are useful for eliminating

333: redundant code (consider our example $bp = b$ above; it

334: expresses the fact that $p$ is redundant when $b$ already holds).

335: (The procedure for eliminating $cp=c$ was introduced in \cite{HK02},

336: where it was shown how to eliminate $cp=c$ and $r=0$ at the same time.

337: Without the benefit of Theorem~\ref{thm:genzeroelim}, this required

338: a construction that simultaneously dealt with both $cp=c$ and $r=0$.)

339: 

340: %\input{prelim}

341: \section{Preliminaries}

342: 

343: For a more complete introduction to Kleene algebra and Kleene algebra

344: with tests, see \cite{Koz97}.

345: 

346: \subsection{Kleene Algebra}

347: 

348: \begin{defi}

349: An \emph{idempotent semiring} is a structure $(S,+,\cdot,0,1)$

350: satisfying

351: %$$\begin{array}{rclcrcl}

352: %x+x&=&x~~~\mbox{(idempotence)} &~ &1\cdot x &=&x\cdot 1=x\\

353: %x+0&=&x & & x\cdot(y\cdot z)&=&(x\cdot y)\cdot z\\

354: %x+y&=&y+x & & x\cdot(y+z)&=&x\cdot y + x\cdot z\\

355: %x+(y+z)&=&(x+y)+z & & (y+z)\cdot x&=&y\cdot x + z\cdot x\\

356: %0\cdot x &=&x\cdot 0=0 & & & &

357: %\end{array}$$

358: \begin{align*}

359: x+x&= x~~~\mbox{(idempotence)}\\

360: x+0&= x\\

361: x+y&= y+x\\

362: x+(y+z)&= (x+y)+z\\

363: 0\cdot x &= x\cdot 0=0\\

364: 1\cdot x &= x\cdot 1=x\\

365: x\cdot(y\cdot z)&= (x\cdot y)\cdot z\\

366: x\cdot(y+z)&= x\cdot y + x\cdot z\\

367: (y+z)\cdot x&= y\cdot x + z\cdot x \dsp.

368: \end{align*}

369: (In other words, $(S,+,0)$ is an upper semilattice with bottom element $0$,

370: $(S,\cdot,1)$ is a monoid, $0$ is an annihilator for $\cdot$,

371: and $\cdot$ distributes over $+$ on the right

372: and left.)

373: \end{defi}

374: 

375: We often write $xy$ for $x\cdot y$.

376: The upper

377: semilattice structure induces a natural

378: partial order on any idempotent semiring:

379: $x \leq y \Leftrightarrow x +y = y$. 

380: %(Note also that this means

381: %inequalities $s\leq t$ may appear anywhere equations appear, such as

382: %in universal Horn formulas.)

383: 

384: \begin{defi}

385: A \emph{Kleene algebra} is a structure

386: %\linebreak

387: $(K,+,\cdot,^*,0,1)$ such that

388: $(K,+,\cdot,0,1)$ forms an idempotent semiring, and which satisfies

389: \begin{align}

390: 1+xx^*&\leq x^*\label{eq:closeleft}\\

391: 1+x^*x&\leq x^*\label{eq:closeright}\\

392: p+qx \leq x &\imp  q^*p\leq x\label{eq:left}\\

393: p+xq \leq x &\imp pq^*\leq x\label{eq:right}\dsp.

394: \end{align}

395: (The order of precedence among the operators is $^* > \cdot > +$, so that

396: $p+qr^* = p+(q\cdot(r^*))$.)  We let $\KA$ denote the category of all

397: Kleene algebras and their homomorphisms.

398: Equations (\ref{eq:closeleft})--(\ref{eq:right}) are called the

399: \emph{Kleene algebra $*$-axioms}.

400: 

401: Given a set $\Sigma$ of constant symbols, let

402: $\Rex_\Sigma$ be the set of Kleene algebra terms over $\Sigma$.

403: We call the elements of $\Rex_\Sigma$ \emph{regular expressions}, and

404: the elements of $\Sigma$ \emph{atomic program symbols}.  

405: An \emph{interpretation} is a homomorphism $I:\Rex_\Sigma \to K$,

406: where $K$ is a Kleene algebra.  $I$ is determined uniquely by its values

407: on $\Sigma$.  

408: \end{defi}

409: 

410: Equations

411: (\ref{eq:closeleft})  and (\ref{eq:left}) say that

412: $q^*p$ is the least solution of $p+qx \leq x$,

413: while

414: (\ref{eq:closeright}) and (\ref{eq:right}) say that $pq^*$ is the least

415: solution to $p + xq \leq x$.  

416: 

417: 

418: 

419: A straightforward and vital consequence of the \KA\ axioms%

420: \footnote{

421: The names of the categories we consider

422: serve as convenient abbreviations for the type

423: of algebra they contain.  So, for example, ``the \KA\ axioms'' means

424: ``the axioms of Kleene algebra''.}

425: is that

426: the operations $+$, $\cdot$, and $^*$ are monotone:

427: if $x_0\leq x_1$ and $y_0\leq y_1$, then $x_0+y_0\leq x_1+y_1$,

428: $x_0y_0 \leq x_1y_1$, and $x_0^* \leq x_1^*$.

429: 

430: %\longnote{

431: %\begin{proposition}

432: %The following are valid in $\KA$.

433: %\begin{align}

434: %x^{**} &= x^*\\

435: %x+y\leq z & \leftrightarrow (x \leq z \wedge y \leq z)

436: %\end{align}

437: %\end{proposition}

438: %}

439: 

440: We use $\models$ to denote ordinary Tarskian satisfaction.

441: %\mynote{Is this the correct term?  Is ``ordinary'' redundant?}

442: However, since we have constant symbols from $\Sigma$ not

443: in the signatures of the underlying algebras, we will pair each algebra

444: with an interpretation when speaking about satisfaction.  For example, given

445: a Kleene algebra $K$, interpretation $I:\Rex_\Sigma \to K$, and

446: formula $\varphi$ whose atomic program symbols are among

447: $\Sigma$,

448: we will write $K,I \models \varphi$ to indicate that $K$ satisfies $\varphi$

449: when the symbols in $\Sigma$ are evaluated according to $I$.

450: $K \models \varphi$ means that $K, I \models \varphi$ for every

451: interpretation $I:\Rex_\Sigma\to K$.  We also use $\models$ in two

452: other standard ways: for a class $\C$ of algebras,

453: $\C \models \varphi$ means that $K \models \varphi$ for each

454: $K \in \C$; for a set $\Phi$ of formulas, $\Phi \models \varphi$

455: means that $K \models \varphi$ for each algebra $K$ satisfying every formula

456: in $\Phi$.

457: 

458: We now introduce two particularly important types of Kleene algebras:

459: \emph{language algebras} and \emph{relational algebras}.

460: 

461: \begin{defi}

462: \label{defi:candef}

463: For an arbitrary monoid $M$, its powerset $2^M$ forms a Kleene

464: algebra as follows.

465: \begin{eqnarray*}

466: 0 & = &\emptyset\\

467: 1&=&\{1^M\}~~~\mbox{(where $1^M$ is the identity of $M$)}\\

468: A+B&=&A\cup B\\

469: A\cdot B &=&\{xy~~|~~x\in A,~y\in B\}\\

470: A^*&=&\bigcup_{k\in\nats} A^k

471: \end{eqnarray*}

472: We let $\REG~M$ denote the smallest subalgebra of $2^M$ containing the

473: singletons $\{x\}$, $x\in M$.  (The elements of $\REG~M$ are the

474: \emph{regular subsets} of $M$.)  $2^M$ and its subalgebras are known

475: as \emph{language algebras}.

476: 

477: Of particular interest is the case $M = \Sigma^*$, 

478: the monoid of all strings over alphabet $\Sigma$ under

479: concatenation.  The empty string $\varepsilon$ is the identity of this

480: monoid.

481: We define the canonical

482: interpretation $R:\Rex_\Sigma\to \REG~\Sigma^*$ by

483: letting $R(p) = \{p\}$ (and extending $R$ homomorphically to the rest 

484: of $\Rex_\Sigma$).  Note that we can interpret elements of $\Sigma^*$

485: as elements of $\RexS$ in the obvious fashion.

486: \end{defi}

487: 

488: \begin{defi}

489: \label{defi:reldef}

490: For an arbitrary set

491: $X$, the set $2^{X \times X}$ of all binary relations on $X$ forms a

492: Kleene algebra %$\rel{X}$

493: as follows.

494: \begin{eqnarray*}

495: 0 &=& \emptyset\\

496: 1 &=& \id_X = \{(x,x)~~|~~x\in X\}\\

497: S + T &=& S \cup T\\

498: S \cdot T &=& S \circ T~~~\mbox{(the composition of $S$ with $T$)}\\

499: S^* &=& \bigcup_{k\in\nats} S^k~~~\mbox{(the reflexive transitive closure of

500: $S$)}

501: \end{eqnarray*}

502: A Kleene algebra $K$ is \emph{relational} if it is a subalgebra

503: of $\rel{X}$ for some $X$; $X$ is called the \emph{base}

504: of $K$.

505: We let $\RKA$ denote the category of all

506: relational Kleene algebras and their homomorphisms.

507: \end{defi}

508: 

509: The definitions of $^*$ in $2^M$ and $\rel{X}$ exemplify the most common

510: intuition about the meaning of $^*$, which is that

511: $y^* = \sup_{n \in \nats} y^n$,

512: or informally, $y^* = 1+y+y^2+\cdots$.  (More generally, if we require

513: that multiplication distributes over this supremum, we have

514: $xy^*z = x1z + xyz +xy^2 z + \cdots = \sup_{n\in\nats}xy^n z$.)

515: However, this property of $^*$

516: does not follow from the $\KA$ $*$-axioms,

517: and must be postulated separately.

518: 

519: \begin{defi}

520: A Kleene algebra $K$ is \emph{$*$-continuous} if it satisfies

521: $$xy^* z = \sup_{k\in\nats} xy^k z$$

522: for all $x,y,z\in K$.  We let $\KA^*$ denote the category of all

523: $*$-continuous Kleene algebras and their homomorphisms.

524: \end{defi}

525: 

526: Since relational composition distributes over arbitrary union,

527: it is immediate from the definition of $^*$ in $\rel{X}$ that relational

528: Kleene algebras are $*$-continuous, so $\RKA \subseteq \KA^*$.

529: 

530: The following ubiquitous lemma is a useful generalization of $*$-continuity.

531: 

532: \begin{lem}

533: \label{lem:starlem}

534: Suppose $K\in\KA^*$, $I: \Rex_\Sigma \to K$ is an interpretation, 

535: and $t\in\Rex_\Sigma$.  Then

536: $$I(t) = \sup_{\sigma \in R(t)} I(\sigma)\dsp .$$

537: \end{lem}

538: 

539: \proof

540: By induction on structure of $t$.  For details,

541: see \cite[Lemma 7.1, pp. 246--248]{Koz91}.~%

542: \qed

543: 

544: % \begin{corollary}

545: % \label{cor:starcor}

546: % Suppose $K\in\RKA$, $I: \Rex_\Sigma \to K$ is an interpretation, 

547: % and $t\in\Rex_\Sigma$.  Then

548: % $$I(t) = \bigcup_{\sigma \in R(t)} I(\sigma)\dsp.$$

549: 

550: % In particular, if $(x,y) \in I(t)$, then there exists

551: % $\sigma\in R(t)$ such that $(x,y) \in I(\sigma)$.

552: % \end{corollary}

553: 

554: % \proof

555: % Let $X$ be the base of $K$.  Union coincides with supremum in $\rel{X}$,

556: % and we can treat $I$ as an interpretation into $\rel{X}$; applying

557: % Lemma~\ref{lem:starlem} to $\rel{X}$ and $I$ gives the desired result.

558: % (This trick was necessary to get around the fact that in an arbitrary

559: % \RKA\ such as $K$, infinite

560: % suprema do not always coincide with union, although,

561: % as this lemma shows, suprema over regular sets must coincide with union.)

562: % \qed

563: 

564: 

565: %\begin{lem}

566: %\label{lem:regmlem}

567: %For any monoid $M$, $2^M$ and its subalgebras are

568: %isomorphic to relational Kleene algebras.  In particular,

569: %$\REG~M$ is isomorphic to a relational Kleene algebra.

570: %\end{lem}

571: %

572: %\proof

573: %Define $\varphi:2^M \to \rel{M}$ by

574: %$$\varphi(A) = \{(x,xy)~~|~~x\in M,~y\in A\}\dsp.$$

575: %It is straightforward to show that $\varphi$ is an injective homomorphism.

576: %So, $2^M$ (or any subalgebra of $2^M$)

577: %is isomorphic to its image under $\varphi$.

578: %\qed\qed

579: 

580: 

581: 

582: %\begin{defi}

583: %A \emph{Horn formula} is a formula of the form

584: %$$s_1 = t_1 \wedge \cdots \wedge s_n = t_n \imp s=t.$$

585: %\end{defi}

586: 

587: 

588: 

589: 

590: \subsection{Kleene Algebra with Tests}

591: \label{subsec:kat}

592: 

593: We can combine Kleene algebra with Boolean algebra to get

594: \emph{Kleene algebra with tests}. 

595: The Boolean aspect is

596: useful for capturing Boolean aspects of

597: programming semantics, particularly control flow and assertions.

598: %(For example,

599: %``while $b$ do $p$'' can be expressed as $(bp)^*\overline{b}$.)

600: 

601: %While the results of

602: %Section~\ref{sec:mainresults} apply to Kleene algebra with tests, they

603: %also apply to ordinary Kleene algebra by ignoring any mention of

604: %tests.  So___

605: 

606: \begin{defi}

607: \label{defi:rkat}

608: A \emph{Kleene algebra with tests} is a two-sorted structure

609: %\linebreak[4]

610: $(K,B,+,\cdot,^*,\complementop,0,1)$, where

611: $(K,+,\cdot,^*,0,1)$ is a Kleene algebra, and

612: $(B,+,\cdot,\complementop,0,1)$ is a Boolean subalgebra.

613: The elements of $B$ are called \emph{tests}.

614: We let $\KAT$ denote the category of all Kleene algebras with tests

615: and their homomorphisms; we let $\KAT^*$ denote the subcategory of all

616: $*$-continuous Kleene algebras with tests.

617: 

618: We now have two types of atomic symbols: programs and tests.

619: For a finite set $\P$ of atomic program symbols

620: and a finite set $\B$ of atomic test symbols,

621: $\RexPB$ is the set of $\KAT$ terms over $\P$ and $\B$; negation can only

622: be applied to Boolean terms, which are terms built from

623: $0$,$1$,$+$,$\cdot$,$\complementop$, and atomic test symbols.

624: An interpretation $I:\RexPB \to K$

625: must map each atomic test to a test in $K$ (and it follows by induction

626: that it will map all Boolean terms to tests).

627: 

628: $\rel{X}$ forms a Kleene algebra with tests by keeping the previously 

629: defined Kleene algebra structure, and letting

630: $B = \{ r \in \rel{X}~~|~~r \leq 1\}$, $\overline{b} = \id_X - b$.

631: A Kleene algebra with tests $K$ is relational if it is a

632: subalgebra

633: %\footnote{When taking a subalgebra of a $\KAT$, we do not

634: %need to preserve the property of being a test.  That is, tests

635: %in the larger algebra appearing in the subalgebra do not need to be

636: %tests in the subalgebra.  Of course, tests in the subalgebra must be

637: %tests in the larger algebra.}

638: %If $K_1,K_2\in\KAT$, with Boolean subalgebras

639: %$B_1$ and $B_2$, we say that $K_2$ is a subalgebra of $K_1$ if it is a

640: %subalgebra in the $\KA$ sense, and $B_2$ is a subalgebra of $B_1$.  In

641: %particular, we do not require $B_2 = B_1 \cap K_2$.}

642: of $\rel{X}$ for some $X$.

643: We let $\RKAT$ denote the category of all relational Kleene algebras with

644: tests and their homomorphisms.

645: \end{defi}

646: 

647: Every Kleene algebra induces a Kleene algebra with tests by letting

648: $B = \{0,1\}$, the two-element Boolean algebra;

649: conversely, every Kleene algebra with tests induces a Kleene algebra by

650: taking its reduct to the signature of Kleene algebra

651: (\emph{i.e.}, taking its image under the map

652: $(K,B,+,\cdot,^*,\complementop,0,1) \mapsto

653: (K,+,\cdot,^*,0,1)$).  With this in mind, it is easy to see that for any

654: formula $\varphi$ in the language of Kleene algebra,

655: $\KAT \models \varphi \Leftrightarrow \KA \models \varphi$,

656: $\KAT^* \models \varphi \Leftrightarrow \KA^* \models \varphi$, and

657: $\RKAT \models \varphi \Leftrightarrow \RKA \models \varphi$.

658: 

659: There is an analog of $\REG~\sigs$ for \KAT\ called the 

660: \emph{guarded-string model}, with its own analog of the canonical

661: interpretation $R$.

662: Though the guarded-string model is in general very important

663: for studying \KAT, we will not need it for our results here, and refer

664: the reader to \cite{KS96} for further information on guarded strings.

665: 

666: The following elementary lemma about subalgebras will be needed in

667: Lemma~\ref{lem:mainlemone}.

668: 

669: \begin{lem}

670: \label{lem:idealalgebras}

671: Let $K\in\KA$ and let $x\in K$.  Then 

672: $\{y\in K~~|~~y\leq x\}$

673: is a subalgebra of $K$ iff

674: $x = y^*$ for some $y\in K$ (or equivalently, $x=x^*$).  The same also holds

675: for $\KAT$s.  (Note that this is not claiming that all subalgebras

676: of $K$ have this form.)

677: \end{lem}

678: 

679: The proof is straightforward and may safely be skipped.

680: 

681: \proof\note{Omit proof?}

682: Let $K' = \{y\in K~~|~~y\leq x\}$.

683: 

684: Suppose $K'$ is a subalgebra of $K$.  Then $x^*\in K'$, so $x^*\leq x$,

685: so $x = x^*$.

686: 

687: Suppose $x = y^*$ for some $y\in K$.  Then $x^* = y^{**} = y^* = x$.

688: The necessary closure conditions follow from monotonicity and

689: the fact that $0 + 1 + xx + (x + x) + x^* \leq x^*$.  (For example,

690: for any $y_1,y_2\in K'$, we have $y_1 y_2 \leq xx \leq x^*$.)

691: \qed

692: 

693: \subsection{Universal Horn Formulas}

694: 

695: %---Clarify the proof below?

696: \begin{defi}

697: A \emph{universal Horn formula} is a formula of the form

698: $$s_1 = t_1 \wedge \cdots \wedge s_t = t_k

699: \imp s = t\dsp,$$

700: where $s_i, t_i, s, t$ are terms.

701: % in the appropriate language.

702: The set of universal

703: Horn formulas valid over a class $\C$ of algebras is the

704: \emph{universal Horn theory}

705: of $\C$, which we denote by $\Horn{\C}$.

706: \end{defi}

707: 

708: We will often drop the word ``universal''.

709: Note that in \KA\ and \KAT, because any inequality $x\leq y$ is actually

710: an equation $x+y = y$, inequalities are allowed in Horn formulas.

711: We will allow 

712: finite sets of equations to appear in the hypotheses of a Horn

713: formula, by taking their conjunction; \eg, if $E = \{pq = qp,~p \leq 1\}$,

714: then $E\imp s=t$ means $(pq =qp \wedge p\leq 1)\imp s=t$.

715: 

716: 

717: \begin{lem}

718: \label{lem:littlestarlem}

719: Let $\Gamma$ be any class of $*$-continuous Kleene algebras with

720: interpretations.  (That is, $\Gamma$ consists of pairs

721: $(K,I)$ where $K\in\KA^*$ and $I:\RexS\to K$ is an interpretation.)

722: Then for any Horn formula of the form $E\imp s\leq t$,

723: $$\Gamma\models E\imp s\leq t \Longleftrightarrow

724: (\forall \sigma\in R(s))~~\Gamma\models E\imp \sigma\leq t\dsp.$$

725: \end{lem}

726: 

727: \proof

728: For any $K\in\KA^*$ with interpretation $I:\RexS\to K$, the

729: equivalence

730: $$K,I\models E\imp s\leq t

731: \Longleftrightarrow

732: (\forall \sigma\in R(s))~~K,I\models E\imp \sigma\leq t$$

733: is a straightforward consequence of Lemma~\ref{lem:starlem}.

734: The lemma then

735: follows by exchanging the universal quantifiers

736: $(\forall \sigma\in R(s))$ and $(\forall (K,I)\in\Gamma)$.  (This latter

737: quantifier comes from $\Gamma\models E\imp s\leq t

738: \Leftrightarrow (\forall (K,I)\in\Gamma)~K,I\models E\imp s\leq t$.)

739: \qed

740: 

741: %

742: %\begin{proposition}

743: %\label{prop:properinc}

744: %$\Horn{\KA} \subsetneq \Horn{\KA^*} \subsetneq \Horn{\RKA}$

745: %\end{proposition}

746: %

747: %\proof

748: %The inclusions are immediate, since $\RKA \subseteq \KA^* \subseteq \KA$.

749: %

750: %$\Horn{\KA} \neq \Horn{\KA^*}$ because the former is $\Sigma^0_1$-complete,

751: %while the latter is $\Pi^1_1$ complete \cite{Koz02}.

752: %

753: %$\Horn{\KA^*} \neq \Horn{\RKA}$ is witnessed by the formula

754: %$p \leq 1 \imp p^2 = p$.

755: %\qed

756: 

757: \subsection{A Proof System for \Horn{\RKA}}

758: \label{sec:proofsystem}

759: 

760: Later, in the proof of Lemma~\ref{lem:mainlemthree}, we will use a

761: proof-theoretic argument based on the infinitary proof system

762: %The material in this section is needed for the proof

763: %of Lemma~\ref{lem:mainlemthree}.  We 

764: %present the infinitary proof system

765: for $\Horn{\RKA}$ introduced in \cite{Hard05proof}.  We will only present

766: the material that we will need in Section~\ref{sec:genzeroelim}

767: for the proof of Lemma~\ref{lem:mainlemthree};

768: for a more thorough treatment, please see \cite{Hard05proof}.

769: % Note that the details of the system that will be relevant in the proof of

770: % Lemma~\ref{lem:mainlemthree} are what happens at leaf nodes in the proofs.

771: 

772: \longnote{

773: The definition of $R(s)$ when $s$ has tests is handled

774: as in the LICS abstract: we assume WLOG that only atomic tests are

775: negated, and for any atomic test $b$, we treat $b$ and

776: $\overline{b}$ as atomic programs, and pretend that any Horn formulas

777: have the additional hypotheses $b\overline{b} = 0$ and $b+\overline{b}=0$.

778: (Admittedly, it would be nice to refine the proof system so that tests are

779: more naturally incorporated.)

780: If you are uncomfortable with the use of tests in the proof

781: of (\ref{eq:relimthree}) above,

782: we can just use the above proof with $\RKA$ in

783: place of $\RKAT$, and use the following lemma to extend the result to

784: $\RKAT$.

785: (The translation defined in the following lemma is

786: essentially the above process: replace Boolean terms with

787: terms in which only atomic tests are negated, treat $b$ and

788: $\overline{b}$ as atomic programs, and add hypotheses $b+\overline{b} = 1$

789: and $b\overline{b} = 0$.)

790: }

791: 

792: \subsubsection{Finite Automata and Trees}

793: 

794: Our proof system for $\Horn{\RKA}$ is based

795: on trees of finite automata, and we must define a number of notions related

796: to trees and automata before continuing.

797: 

798: Assume we have a fixed finite alphabet $\Sigma$.

799: We let \nfa\ denote 

800: the set of all nondeterministic finite automata over $\Sigma$,

801: allowing $\varepsilon$-moves (also called $\varepsilon$-edges).

802: %requiring that all states be natural numbers;

803: % , and that {\bf each automaton has unique

804: % start and accept states, distinct from each other};

805: %$\varepsilon$-moves (also

806: %called $\varepsilon$-edges) are allowed.

807: 

808: We will also use NFA as shorthand

809: for \emph{nondeterministic finite automaton}.  For any NFA $A$, $L(A)$ denotes

810: the language of $A$, and $|A|$ denotes the states of $A$.

811: For states $v,w\in |A|$,

812: let $A^{v,w}$ denote the NFA which is

813: identical to $A$ except that it has $v$ and $w$ as its unique start and accept

814: states, respectively.

815: We fix distinct states $a$ and $b$,

816: and let $\nfa^{a,b}$ be the set of all $A\in\nfa$

817: which have unique start state $a$ and unique accept state $b$.

818: %We will only work with automata in $\nfa^{a,b}$.

819: 

820: % Assume we have a fixed finite alphabet $\Sigma$.

821: % We let \nfa\ denote 

822: % the set of all nondeterministic finite automata over $\Sigma$, requiring

823: % that all states are natural numbers, and that {\bf each automaton has unique

824: % start and accept states, distinct from each other};

825: % $\varepsilon$-moves (also

826: % called $\varepsilon$-edges) are allowed.  In all diagrams of automata,

827: % the leftmost state will be the start state, and the rightmost state will be

828: % the accept state.

829: 

830: % We will also use NFA as shorthand

831: % for \emph{nondeterministic finite automaton}.  For any NFA $A$, $L(A)$ denotes

832: % the language of $A$, and $|A|$ denotes the states of $A$.

833: % For states $v,w\in |A|$,

834: % let $A^{v,w}$ denote the NFA which is

835: % identical to $A$ except that it has $v$ and $w$ as its unique start and accept

836: % states, respectively.

837: % We let $\nfa^{v,w}_\Sigma$ be the set of all nondeterministic finite

838: % automata over $\Sigma$ which have start state $v$ and accept state

839: % $w$.

840: 

841: % We fix distinct states $a$ and $b$ (for concreteness, say $a=0$, $b=1$),

842: % that will be the default start and accept states for the automata we

843: % consider.  

844: 

845: We define $F_0\in \nfa^{a,b}$ to have states

846: $\{a,b\}$ and no edges.

847: 

848: % Given $A,B\in\nfa$, we define their \emph{wedge product} $A \wedge B$

849: % to be the NFA defined as follows.  $A \wedge B$ consists of

850: % disjoint copies of $A$ and $B$, except that the start states of $A$ and $B$

851: % are combined into a single start state, and the accept

852: % states of $A$ and $B$ are combined into a single accept state.  

853: % (So $A \wedge B $ is essentially the result of gluing $A$ and $B$ together, in parallel,

854: % at their start and end states.)

855: % If $a$ and $b$

856: % are the start and accept states of $A$, we assume that they are also the

857: % start and accept states of $A \wedge B$;

858: % apart from this bias in numbering states,

859: % the wedge product is commutative.  It is also associative.

860: 

861: % %---Illustration of a wedge product?

862: 

863: % We now define some special NFAs.  Each of the following will have start

864: % state $a$ and accept state $b$ (we can say for concreteness that

865: % $a=0$ and $b=1$, though there is nothing significant about this choice).

866: 

867: % $F_0$ has states $\{a,b\}$ and no edges.

868: 

869: %$F_1$ has states $\{a,b\}$ and an $\varepsilon$-edge from $a$ to $b$.

870: %

871: % $F_2$ has states $\{a,b\}$ and 

872: % $\varepsilon$-edges from $a$ to $b$ and

873: % from $b$ to $a$.

874: 

875: % For $\sigma  = p_1\cdots p_k\in \Sigma^*$, we define $F_\sigma$ so that

876: % $L(F_\sigma) = \{\sigma\}$ as follows.

877: % For the case $\sigma = \varepsilon$, we let $F_\sigma = F_\varepsilon = F_1$;

878: % otherwise, we let $F_\sigma$ have

879: % states $\{a,x_1,x_2,\ldots,x_{k-1},b\}$ and edges

880: % $$a

881: % \stackrel{p_1}{\rightarrow} x_1

882: % \stackrel{p_2}{\rightarrow} \cdots

883: % \stackrel{p_{k-1}}{\rightarrow} x_{k-1}

884: % \stackrel{p_{k}}{\rightarrow} b\enspace.$$

885: 

886: % For finite $S =\{\sigma_1,\ldots,\sigma_k\} \subseteq \Sigma^*$,

887: % we let $$F_S = F_{\sigma_1}\wedge\cdots\wedge F_{\sigma_k}\enspace.$$

888: % ($F_\emptyset$ is the empty wedge product, $F_0$.)  Note that

889: % $L(F_S) = S$.  We call $F_S$ the \emph{free automaton with language $S$}.

890: % Note that a free automaton is uniquely determined by its language, so we

891: % can essentially identify a free automaton with its language.

892: % (Here, ``free'' refers to the fact that $F_S$ has as little internal

893: % structure as possible---all paths from the start state to the end state

894: % are disjoint.)

895: 

896: % For $A\in\nfa$ with $L(A)$ finite, we define

897: % $$\comb(A) = F_{L(A)}\enspace.$$

898: % Note that $L(\comb(A)) = L(A)$.  The free automaton $\comb(A)$ is essentially

899: % the result of ``combing'' $A$ into disjoint paths.

900: 

901: % %---Illustration of uncombed and combed automaton?

902: 

903: Given an NFA $A$ and states $v,w\in |A|$, we will sometimes want to

904: ``insert'' a string $\tau\in \Sigma^*$ into $L(A^{v,w})$.  For this

905: purpose, we define $A' = \ins_2(A,v,w,\tau)$ as follows.

906: \begin{enumerate}

907: \item If $\tau=p_1\cdots p_k$, with $p_i\in \Sigma$ and $k > 0$, we obtain $A'$

908: from $A$ by adding $k-1$

909: new states $x_1,\ldots,x_{k-1}$ and adding edges

910: $$v

911: \stackrel{p_1}{\rightarrow} x_1

912: \stackrel{p_2}{\rightarrow} \cdots

913: \stackrel{p_{k-1}}{\rightarrow} x_{k-1}

914: \stackrel{p_{k}}{\rightarrow} w\dsp.$$

915: 

916: \item If $\tau = \varepsilon$, then we add an $\varepsilon$-edge from

917: $v$ to $w$

918: and also from $w$ to $v$.

919: (Where it is used,

920: $\ins_2(A, v,w,\varepsilon)$

921: corresponds to identifying $v$ and $w$ with each other.

922: The edge from $w$ to $v$,

923: called a \emph{reverse $\varepsilon$-edge},

924: is needed to capture the

925: symmetry of the identity relation.)

926: \end{enumerate}

927: 

928: % The insert operations can be viewed in terms of wedge products.  If $A$

929: % has start and accept states $a$ and $b$, then for $\tau \neq \varepsilon$,

930: % $$\ins(A,v,w,\tau) = \ins_2(A,v,w,\tau) = (A^{v,w}\wedge F_\tau)^{a,b}\enspace,$$

931: % and for the case $\tau = \varepsilon$,

932: % \begin{eqnarray*}

933: % \ins(A,v,w,\varepsilon) &=& (A^{v,w}\wedge F_1)^{a,b}\\

934: % \ins_2(A,v,w,\varepsilon) &=& (A^{v,w}\wedge F_2)^{a,b}\enspace.

935: % \end{eqnarray*}

936: 

937: We now move on to trees.

938: %$\nats$ is the set of naturals $\{0,1,\ldots\}$.

939: $\nats^*$ is the set of all finite strings of naturals (including

940: the empty string).

941: A set $T \subseteq \nats^*$ is a \emph{tree} if it is closed under

942: taking initial segments.

943: A function $f:\nats\to \nats$ can be treated as an infinite

944: sequence of naturals, and for $n\in\nats$, we let $f\restriction n$ denote

945: the initial segment of $f$ of length $n$.

946: Such an $f$ is a \emph{path} through a tree $T$ if

947: $(f\restriction n )\in T$ for all $n \in\nats$.

948: (We find this a concise framework for countably-branching trees, but it is

949: not strictly necessary to define trees in this manner.)

950: 

951: \subsubsection{Relational Proofs}

952: 

953: The following definition of \emph{relational proof} captures, with

954: trees of finite automata, the combinatorics of attempting to construct a

955: relational counterexample to a Horn formula.

956: A path through such a tree yields a relational model in which

957: the formula fails, while

958: well-foundedness establishes the impossibility of a counterexample

959: ({\it i.e.}, the relational validity of the formula).

960: 

961: \begin{defi}

962: \label{defi:relproof}

963: Let $E \imp \sigma\leq t$ be a

964: Horn formula in the language of $\KA$ with $\sigma \in\Sigma^*$ and

965: $t\in\RexS$.  We assume that

966: all hypotheses in $E$ are inequalities $x \leq y$, by breaking any equations

967: $x = y$ into $x \leq y \wedge y \leq x$ as necessary.  

968: We fix distinct states $a$ and $b$ as above.

969: We fix a special symbol \con, which will signify

970: contradiction.

971: 

972: A \emph{relational tree for $E \imp \sigma \leq t$} is a pair

973: $(T,A)$ where $T \subseteq \nats^*$ is a tree and

974: $A:T \to \nfa^{a,b} \cup \{\con\}$ such that the following

975: conditions hold.  ($A_f$ will denote $A(f)$.)

976: \begin{enumerate}

977: \item At the root, we have 

978: $A_{\langle\rangle} = \ins_2(F_0,a,b,\sigma)$.

979: 

980: % be the automaton

981: %$$\rightarrow a \stackrel{\sigma}{\rightarrow} \fbox{b}$$\note{Typeset the

982: %automaton properly.}

983: %so $L(A_{\langle\rangle}) = \{p\}$.  

984: 

985: \item $f\in T$ is a leaf node if and only if $A_f = \con$ or 

986: $R(t)\cap L(A_f)\neq \emptyset$.

987: 

988: %The following reworded at referee's request.

989: \item If $f$ is not a leaf node, then

990: there exist $v,w\in |A_f|$

991: (possibly equal),

992: %$\rho \in L(A_f^{v,w})$, 

993: an inequality $r\leq r'$ in $E$,

994: and $\rho \in L(A_f^{v,w}) \cap R(r)$ such that

995: \begin{enumerate}

996: \item if $R(r') = \emptyset$ (typically because $r' = 0$), then $f$

997: has one child $g$, with $A_g = \con$;

998: \item if $R(r') \neq \emptyset$, then $f$ has one child $g_\tau$ for each

999: $\tau \in R(r')$, with

1000: $A_{g_\tau} = \linebreak \ins_2 (A_f, v,w, \tau)$.

1001: \end{enumerate}

1002: (We say that the hypothesis $r\leq r'$ is \emph{applied at $f$}.)

1003: \end{enumerate}

1004: 

1005: A \emph{relational proof of $E\imp \sigma\leq t$} is a well-founded

1006: relational tree for $E\imp \sigma \leq t$.

1007: We say $E\imp \sigma\leq t$

1008: is \emph{relationally provable} if such a proof exists.

1009: \end{defi}

1010: 

1011: % Although our proof of soundness and completeness will stand on its own,

1012: % Definition~\ref{defi:relproof} is best understood in terms of the

1013: % reasoning 

1014: % done in Section~\ref{subsec:preview}.  The root node corresponds

1015: % to the supposition that $(x,y)\in I(\sigma)$.  

1016: % The $\con$ nodes

1017: % indicate that we have followed a subcase that has $(x,y)\in I(0)$,

1018: % a contradiction; the other type of leaf node indicates that, within

1019: % the current subcase, we have $(x,y)\in I(t)$ as desired.

1020: % The intermediate steps are essentially just a matter of bookkeeping.

1021: % %The reason that $\varepsilon$-edges are added in both directions is that

1022: % %in all relational models, $I(\varepsilon) = I(1)$ is the identity relation;

1023: % %if $(v,w)\in I(1)$, this indicates that $v=w$, and the definition captures

1024: % %this by adding $\varepsilon$-edges from $v$ to $w$ and from $w$ to $v$,

1025: % %instead of explicitly equating the states $v$ and $w$.

1026: % The well-foundedness

1027: % of the tree essentially expresses the fact that the cases are exhaustive.

1028: 

1029: % We can reinterpret the tree of automata in Section~\ref{subsec:preview}

1030: % as a relational proof.  We now give two further examples that illustrate

1031: % the purpose of $\con$ and the $\varepsilon$-edges.

1032: 

1033: % Consider the formula $p \leq 0 \imp p \leq q$.  If we follow

1034: % the same reasoning as in the motivating example, the assumption that

1035: % $(x,y) \in I(p)$ will lead to a contradiction if we apply the hypothesis

1036: % $p\leq 0$.  As a relational proof, we would have a tree

1037: % with $F_p$ at the root, and one child, $\con$.

1038: 

1039: % Now consider the formula $p\leq 1 \imp p \leq p^2$.  The

1040: % assumption that $(x,y)\in I(p)$ lets us conclude that

1041: % $(x,y)\in I(1)$ by applying the hypothesis $p\leq 1$.  Since $I(1)$ is

1042: % the identity relation, we can conclude that $x = y$.

1043: % Letting $P = I(p)$ and $E=I(1)$, we

1044: % now have $xPyExPy$, so $(x,y)\in PEP = I(p)I(1)I(p) = I(p^2)$.

1045: % Note that this argument required the reflexivity of $E$: from

1046: % $xEy$, we needed to conclude $yEx$ to finish the argument.  This is

1047: % essentially why,

1048: % in relational proofs, $\varepsilon$-edges are added in both directions.

1049: % In terms of relational proofs,

1050: % we start with $F_p$ at the root.  We then apply

1051: % the hypothesis $p \leq 1$ by adding $\varepsilon$-edges in both directions

1052: % between $a$ and $b$, yielding one child, $F_p \wedge F_2$.

1053: % We have $p^2 \in L(F_p \wedge F_2)$ (we can

1054: % follow the reverse $\varepsilon$-edge from $b$ to

1055: % $a$, just as we used $yEx$ above), so this is a leaf and we are done.

1056: 

1057: % Note that the above two examples had no branching.  This is because the

1058: % right hand side $t$ of each hypothesis had no more than one element in

1059: % $R(t)$.  Branching can occur only when $|R(t)| > 1$, and infinite branching

1060: % can occur only when $R(t)$ is infinite; note

1061: % that $R(t)$ is finite whenever $t$ is $*$-free.

1062: % %(This is essentially why the $\Pi^1_1$-completeness of

1063: % %$\Horn{\RKA}$ disappears when $*$ is not allowed to appear on the right

1064: % %hand side of a hypothesis \cite{Hard04}.)

1065: 

1066: \begin{lem}

1067: \label{lem:mainrkalem}

1068: For any Horn formula of the form $E \imp \sigma \leq t$,

1069: the following are equivalent.

1070: \begin{enumerate}

1071: \romanize

1072: \item $\RKA \models E \imp \sigma \leq t$

1073: \item $E \imp \sigma \leq t$ is relationally provable.

1074: \end{enumerate}

1075: \end{lem}

1076: 

1077: \proof

1078: See \cite{Hard05thesis} or \cite{Hard05proof}.

1079: \mynote{Careful here: the proof only appears in the appendix of

1080: \cite{Hard05proof}, which does not appear in the proceedings version.}

1081: \qed

1082: 

1083: The notion of relational provability can be extended

1084: to arbitrary Horn formulas, but we will not need it for the proof

1085: of Lemma~\ref{lem:mainlemthree}.

1086: 

1087: % \begin{defi}

1088: % We say that $E\imp s\leq t$ is \emph{relationally provable}

1089: % if $E\imp \sigma\leq t$ is \emph{relationally provable}

1090: % for all $\sigma\in R(s)$. 

1091: % We say that $E\imp s=t$ is \emph{relationally provable} if

1092: % both $E\imp s\leq t$ and $E\imp t \leq s$ are

1093: % relationally provable.

1094: % \end{defi}

1095: 

1096: % \begin{thm}

1097: % \label{thm:mainrkathm}

1098: % The following are equivalent for any Horn formula $E\imp s = t$.

1099: % \begin{itemize}

1100: % \item[(i)] $\RKA\models E \imp s=t$

1101: % \item[(ii)] $E\imp s=t$ is relationally provable.

1102: % \end{itemize}

1103: % \end{thm}

1104: 

1105: % \proof

1106: % It suffices to show that equivalence holds for the formulas

1107: % $E\imp s \leq t$ and $E\imp t \leq s$.  The former equivalence

1108: % is as follows.

1109: % \begin{eqnarray*}

1110: % & &\RKA\models E\imp s\leq t\\

1111: % &\Leftrightarrow&

1112: % (\forall \sigma\in R(s))~~\RKA\models E\imp

1113: % \sigma\leq t~~~~\mbox{(Lemma \ref{lem:littlestarlem})}\\

1114: % &\Leftrightarrow&

1115: % (\forall \sigma\in R(s))~~\mbox{$E\imp \sigma\leq t$ is

1116: % relationally provable}\\

1117: % &\Leftrightarrow&

1118: % \mbox{$E\imp s\leq t$ is relationally provable}

1119: % \end{eqnarray*}

1120: % The equivalence for $E\imp t\leq s$ is similar.

1121: % \qed

1122: 

1123: \subsection{The Relationship Between \Horn{\RKA} and \Horn{\RKAT}}

1124: \label{sec:relationship}

1125: 

1126: The system presented in Section~\ref{sec:proofsystem} is a tool

1127: for studying \Horn{\RKA}, while in Lemma~\ref{lem:mainlemthree}, we

1128: will wish to use it to draw conclusions about \Horn{\RKAT}.

1129: This must be rectified,

1130: and there are multiple ways to proceed.  One would be to modify the

1131: notion of relational proof so that it applies to \Horn{\RKAT};

1132: this would present no

1133: particular difficulty, but would require a closer look at relational proofs

1134: than we would like to get into here.  Instead, we will show how to

1135: reduce questions about \Horn{\RKAT}\ to \Horn{\RKA}, in a way that will

1136: allow us to use the existing definition of relational proof

1137: when proving Lemma~\ref{lem:mainlemthree}.

1138: 

1139: \begin{lem}

1140: \label{lem:trlem}

1141: For any Horn formula $\varphi$ of \KAT, there is a Horn

1142: formula $\Tr(\varphi)$ of \KA\ such that

1143: $\RKAT \models \varphi$ iff $\RKA \models \Tr(\varphi)$. 

1144: \end{lem}

1145: 

1146: The lemma is uninteresting without putting restrictions on

1147: the translation $\Tr$.  However, instead of trying to

1148: capture the desired properties of $\Tr$ for inclusion in the lemma,

1149: we just give the proof, and observe

1150: later that the translation works for a particular purpose when the need

1151: arises.  \note{(Informally, the property of $\Tr$ that we will need is that it

1152: commutes with certain other syntactic operations.)}

1153: 

1154: \proof

1155: (Outline: we first assume that negation is only applied to atomic

1156: tests, then replace the negations of atomic tests with fresh program symbols,

1157: and finally

1158: add new hypotheses to ensure that the new program symbols behave like

1159: the negated tests they replace.)

1160: 

1161: Fix a set $\P$ of atomic program symbols, and a set $\B$ of atomic tests.

1162: Given any $s\in\RexPB$, we can assume without loss of generality that

1163: negation is only applied to atomic tests, in light of DeMorgan's 

1164: Laws\note{Law?}.

1165: %   To make this precise,

1166: % we define $\nu: \Rex_{\P,\B} \to \Rex_{\P,\B}$ by recursion:

1167: % \note{typesetting in double negation part?}

1168: % \begin{eqnarray*}

1169: % \nu(t_1 + t_2) &=& \nu(t_1)+\nu(t_2)\\

1170: % \nu(t_1 \cdot t_2) &=& \nu(t_1)\cdot\nu(t_2)\\

1171: % \nu(t^*) &=& \nu(t)^*\\

1172: % \nu\big(\overline{\overline{t}}\big) &=& t\\

1173: % \nu(\overline{t_1 \cdot t_2})&=&\nu(\overline{t_1}) + \nu(\overline{t_2})\\

1174: % \nu(\overline{t_1 + t_2})&=&\nu(\overline{t_1}) \cdot \nu(\overline{t_2})\\

1175: % %\nu(\overline{t^*})&=&0\\

1176: % \nu(\overline{0})&=&1\\

1177: % \nu(\overline{1})&=&0\\

1178: % \nu(\overline{b})&=&\overline{b}~~~\mbox{($b\in\B$)}\\

1179: % \nu(p)&=&p~~~\mbox{($p\in\P\bigcup\B\bigcup\{0,1\}$)}

1180: % \end{eqnarray*}

1181: % For any $t\in\RexPB$, $\KAT \models t = \nu(t)$, and in $\nu(t)$,

1182: % negation is only applied to atomic tests.

1183: 

1184: For each $b\in\B$, we introduce two new atomic program symbols

1185: $\tilde{b}$

1186: and

1187: $\tilde{\overline{b}}$, and we let

1188: $\Sigma = \P \bigcup \{\tilde{b},\tilde{\overline{b}}~~|~~b\in\B\}$.  For

1189: any $t\in\RexPB$, we let $\tilde{t}$ be the result of taking $t$, 

1190: and replacing all occurrences of $\overline{b}$ with $\tilde{\overline{b}}$,

1191: and all positive occurrences of $b$ with $\tilde{b}$ (for each $b\in\B$).

1192: Note that $\tilde{t}\in\Rex_{\Sigma}$. For any formula $\varphi$, we let

1193: $\tilde{\varphi}$ be the result of replacing each term $t$ in $\varphi$

1194: with $\tilde{t}$.

1195: 

1196: Now take any Horn formula $\varphi$ of the form

1197: $\theta \imp \psi$ (with

1198: all terms in $\RexPB$).

1199: Let $\Tr(\varphi)$ be the formula

1200: $$\left(\tilde{\theta} \wedge

1201: \bigwedge_{b\in\B}

1202: (\tilde{b}+\tilde{\overline{b}} = 1 \wedge

1203: \tilde{b}\cdot\tilde{\overline{b}} = 0) \right)

1204: \imp \tilde{\psi}\dsp.$$

1205: (The extra hypotheses make $\tilde{b}$ and $\tilde{\overline{b}}$

1206: behave like Boolean complements of each other.)

1207: 

1208: We now show 

1209: $\RKAT \models \varphi$ iff $\RKA \models \Tr(\varphi)$.

1210: 

1211: For the right-to-left implication,

1212: suppose $\RKAT \not \models \varphi$.  Let $K\in\RKAT$ with

1213: interpretation $I:\RexPB\imp K$

1214: such that $K,I\not\models \varphi$.  Then

1215: $K,I\models\theta \wedge \neg\psi$.

1216: Define the interpretation $\tilde{I}: \Rex_\Sigma \to K$ by

1217: $$\tilde{I}(p) = \left\{

1218: \begin{array}{ll}

1219: I(p), & \mbox{if $p \in \P$,}\\

1220: I(b), &\mbox{if $p=\tilde{b}$,}\\

1221: I(\overline{b}), &\mbox{if $p=\tilde{\overline{b}}$.}

1222: \end{array}\right.$$

1223: %extended homomorphically.

1224: 

1225: A simple induction shows that for any $t\in\RexPB$,

1226: $\tilde{I}(\tilde{t}\,) =

1227: %I(\nu(t)) =

1228: I(t)$.  It follows that

1229: $K,\tilde{I}\models \tilde{\theta}\wedge\neg\tilde{\psi}$, since

1230: $K,I\models \theta\wedge\neg\psi$.  Also,

1231: $$K,\tilde{I}\models\bigwedge_{b\in\B}

1232: (\tilde{b}+\tilde{\overline{b}} = 1 \wedge

1233: \tilde{b}\cdot\tilde{\overline{b}} = 0)\dsp.$$

1234: Thus $K,\tilde{I}\not\models \Tr(\varphi)$, so

1235: $\RKA \not\models\Tr(\varphi)$ (recall that we can treat $K$ as a member

1236: of \RKA\ by passing it through the forgetful functor which drops negation).

1237: Therefore, $\RKA \models \Tr(\varphi) \imp \RKAT \models \varphi$.

1238: 

1239: For the left-to-right implication,

1240: suppose that $\RKA \not\models\Tr(\varphi)$.  Let $K\in\RKA$ with

1241: interpretation $I:\Rex_{\Sigma}\to K$

1242: such that $K,I\not\models\Tr(\varphi)$.  Let $X$ be the base of $K$.

1243: Then $K \subseteq \rel{X}$, so 

1244: $\rel{X}, I \not\models\Tr(\varphi)$; that is,

1245: $$\rel{X},I\models

1246: \tilde{\theta} \wedge

1247: \bigwedge_{b\in\B}

1248: (\tilde{b}+\tilde{\overline{b}} = 1 \wedge

1249: \tilde{b}\cdot\tilde{\overline{b}} = 0)

1250: \wedge\neg\tilde{\psi}\dsp.$$

1251: In particular, for any $b\in\B$,

1252: $I(\tilde{b}) \bigcup I(\tilde{\overline{b}}) = I(1)$, and

1253: $I(\tilde{b}) \circ I(\tilde{\overline{b}}) = \emptyset$; it follows that

1254: $I(\tilde{b}) \bigcap I(\tilde{\overline{b}}) = \emptyset$ (since

1255: $R \bigcap S = R \circ S$ whenever $R,S \subseteq I(1)$), so

1256: $I(\tilde{\overline{b}}) = I(1) - I(\tilde{b})$.

1257: 

1258: Define the interpretation $I':\RexPB\to \rel{X}$ by

1259: \begin{eqnarray*}

1260: I'(p)&=&I(p)\dsp,\\

1261: I'(b)&=&I(\tilde{b})\dsp.

1262: \end{eqnarray*}

1263: We have

1264: \begin{eqnarray*}

1265: I'(\overline{b}) &= &I'(1) - I'(b)\\

1266: &=& I(1) - I(\tilde{b})\\

1267: &=& I(\tilde{\overline{b}})\dsp.

1268: \end{eqnarray*}

1269: It follows that, for any $t\in\RexPB$, $I'(t) = I(\tilde{t}\,)$.

1270: So, $\rel{X}, I' \models \theta \wedge\neg\psi$, since

1271: $\rel{X}, I \models \tilde{\theta} \wedge\neg\tilde{\psi}$, giving us

1272: $\RKAT \not\models \varphi$.

1273: Therefore,

1274: $\RKAT \models \varphi

1275: \imp

1276: \RKA \models \Tr(\varphi)$, completing the proof.

1277: \qed

1278: 

1279: %%% Local Variables: 

1280: %%% mode: latex

1281: %%% TeX-master: "main"

1282: %%% End: 

1283: 

1284: 

1285: %\input{mainres}

1286: \section{Main Results}

1287: \label{sec:mainresults}

1288: 

1289: \subsection{Eliminating $r=0$}

1290: \label{sec:genzeroelim}

1291: 

1292: \begin{defi}

1293: For a fixed set $\P = \{p_1,\ldots,p_n\}$ of atomic program symbols,

1294: the \emph{universal regular expression $u$} is defined by

1295: $$u = (p_1+\cdots+p_n)^*\dsp.$$

1296: \end{defi}

1297: 

1298: We trivially have $\KAT \models u = uu = u^*$, and a straightforward

1299: induction shows that, for any $s\in\RexPB$, $\KAT \models s \leq u$.

1300: 

1301: Our goal is the following theorem.

1302: 

1303: \begin{thm}

1304: \label{thm:genzeroelim}

1305: Let $u$ be the universal regular expression,

1306: let $E$ be any finite set of hypotheses, and let $r,s,t\in\RexPB$.

1307: Then the following equivalences hold.

1308: \begin{alignat}{2}

1309: \KAT \models E\wedge r=0 \imp s=t

1310: &\iff &

1311: \KAT \models E\imp s+uru=t+uru\label{eq:relimone}\\

1312: \KAT^* \models E\wedge r=0 \imp s=t

1313: &\iff &

1314: \KAT^* \models E\imp s+uru=t+uru\label{eq:relimtwo}\\

1315: \RKAT \models E\wedge r=0 \imp s=t

1316: &\iff&

1317: \RKAT \models E\imp s+uru=t+uru\label{eq:relimthree}

1318: \end{alignat}

1319: \end{thm}

1320: 

1321: Note that the special case $E = \emptyset$ is essentially

1322: Theorem~\ref{thm:subsumehoare} (when $E = \emptyset$, the right

1323: hand sides of \eqref{eq:relimone}--\eqref{eq:relimthree}

1324: are equivalent, since the equational theories of $\KAT$,

1325: $\KAT^*$, and $\RKAT$ coincide; when $E\neq \emptyset$, the right hand sides

1326: of \eqref{eq:relimone}--\eqref{eq:relimthree} are no longer necessarily

1327: equivalent, which prevents Theorem~\ref{thm:genzeroelim} from having the

1328: same form as Theorem~\ref{thm:subsumehoare}).

1329: Note also that for any formula $\varphi$ in the language of $\KA$,

1330: we have $\KA\models \varphi$ iff $\KAT\models\varphi$,

1331: $\KA^*\models \varphi$ iff $\KAT^* \models\varphi$, {\it etc.}, so

1332: Theorem~\ref{thm:genzeroelim} also applies to $\KA$, $\KA^*$, and $\RKA$.

1333: (Alternatively, omitting the Boolean aspects of the proof that

1334: follows would yield

1335: a proof of the analogous theorem for $\KA$, $\KA^*$, and $\RKA$.)

1336: 

1337: We prove each equivalence as a separate lemma.  Fix $u$, $E$,

1338: $r$, $s$, $t$,

1339: as above.

1340: 

1341: \begin{lem}

1342: \label{lem:mainlemone}

1343: $$\KAT \models E\wedge r=0 \imp s=t

1344: \iff

1345: \KAT \models E\imp s+uru=t+uru$$

1346: \end{lem}

1347: 

1348: \proof

1349: The right-to-left implication is trivial:

1350: reasoning under $E\wedge r=0$,

1351: we have $s = s+0 = s+uru= t+uru= t+0=t$.  (Note that this

1352: argument also applies to $\KAT^*$ and $\RKAT$.)

1353: 

1354: For the left-to-right implication,

1355: suppose

1356: $\KAT\models E\wedge r=0\imp s=t$.

1357: Take any $K\in\KAT$ with interpretation $I$ such that

1358: $K,I\models E$.  

1359: Let $\bot = I(uru)$, $\top = I(u)$, noting that

1360: $\top^* = \top$, $\bot= \top\bot = \bot\top$, and

1361: $\bot\bot\leq\bot$.

1362: Let $K' = \{x\in K~~|~~x\leq \top\}$.

1363: This is a subalgebra of $K$ by

1364: Lemma~\ref{lem:idealalgebras},

1365: since $\top = \top^*$.

1366: $I$ is an interpretation into $K'$.  

1367: 

1368: Define the map $f:K'\rightarrow K'$ by $f(x) = x+\bot$.

1369: Let $L = f[K']$, the image of $K'$ under $f$.

1370: $\top$ and $\bot$ are respectively the

1371: greatest and least elements of $L$.

1372: Note that for any $x\in K'$, $x\top\leq \top$, so

1373: $x\bot = x\top\bot \leq \top\bot = \bot$.  We similarly have

1374: $\bot x \leq \bot$.

1375: 

1376: Define %$0^L = \bot = f(0)$ and $1^L = 1+\bot = f(1)$.

1377: \begin{eqnarray*}

1378: 0^L &=& \bot ~~=~~ f(0)\\

1379: 1^L &=& 1 + \bot ~~=~~ f(1)\\

1380: v\cdot^L w &=& v\cdot w + \bot = f(vw)\dsp.

1381: %v +^L w &=& v+w

1382: %v^{*^L} &=& v^*

1383: \end{eqnarray*}

1384: 

1385: Let $L$ be the structure

1386: %$*$-algebra with tests \note{Get rid of this term?}

1387: $(L,f[B],+,\cdot^L,{}^*,\tilde{\enspace},0^L,1^L)$, 

1388: in the signature of \KAT,

1389: where

1390: $B$ is the set of tests of $K'$, and the 

1391: Boolean complement $\tilde{\enspace}$ is defined by

1392: $\widetilde{f(c)} = f(\overline{c})$.  We must show that

1393: $\tilde{\enspace}$ is well-defined.

1394: Suppose $f(c) = f(d)$.

1395: Then

1396: \begin{eqnarray*}

1397: f(\overline{c}) &=& \overline{c}+\bot\\

1398: &\leq& (\overline{c}+\bot)(1+\bot)\\

1399: &=& (\overline{c}+\bot)(d +\overline{d} + \bot)\\

1400: &=& (\overline{c}+\bot)(c +\overline{d} + \bot)\quad\mbox{(since

1401: $c+\bot =f(c)=f(d)= d+\bot$)}\\

1402: &=& \overline{c}c + \overline{c}\overline{d} + \overline{c}\bot

1403: +\bot c + \bot \overline{d} +\bot\bot\\

1404: &\leq& 0+\overline{d}+\bot\\

1405: &=&f(\overline{d})\dsp.

1406: \end{eqnarray*}

1407: %\begin{eqnarray*}

1408: %f(\overline{c}) &=& \overline{c}+\bot\\

1409: %&=& (\overline{c}+\bot)(1+\bot) + \bot\quad\mbox{(by various inequalities

1410: %involving $\bot$)}\\

1411: %&=& (\overline{c}+\bot)\cdot^L (1+\bot)\\

1412: %&=& (\overline{c}+\bot)\cdot^L (d +\overline{d} + \bot)\\

1413: %&=& (\overline{c}+\bot)\cdot^L (c +\overline{d} + \bot)\quad\mbox{(since

1414: %$c+\bot = d+\bot$)}\\

1415: %&=& (\overline{c}+\bot)\cdot (c +\overline{d} + \bot)+\bot\\

1416: %&=& \overline{c}c + \overline{c}\overline{d} + \overline{c}\bot

1417: %+\bot c + \bot \overline{d} +\bot\bot+\bot\\

1418: %&\leq& 0+\overline{d}+\bot\\

1419: %&=&f(\overline{d})\dsp.

1420: %\end{eqnarray*}

1421: Similarly, $f(\overline{d})\leq f(\overline{c})$,

1422: so $f(\overline{c})=f(\overline{d})$.  Therefore, 

1423: $\tilde{\enspace}$ is well-defined.

1424: 

1425: %Terminology?

1426: We claim that $f:K'\rightarrow L$ is a homomorpishm.  (Note that

1427: this is different from claiming that $f:K'\rightarrow K'$ is a homomorphism,

1428: which is not true unless $\bot = 0$.)

1429: For any $x,y\in K$, and $c$ a test in $K$,

1430: \begin{eqnarray*}

1431: f(0) &=& 0^L\\

1432: f(1) &=& 1^L\\

1433: f(x+y) &=& x+y+\bot = x+\bot+y+\bot = f(x) + f(y)\\

1434: f(xy) &=&xy+\bot\\

1435:      & =& xy + \bot y + x \bot +\bot\bot+ \bot

1436: \quad\mbox{(since $\bot y + x\bot+\bot\bot \leq \bot$)}\\

1437: &=& (x+\bot)(y+\bot)+\bot\\

1438: &=& f(x)\cdot^L f(y)\\

1439: f(\overline{c}) &=&\widetilde{f(c)}\dsp.

1440: \end{eqnarray*}

1441: It remains to verify $f(x^*) = (f(x))^*$.

1442: We have

1443: $$1 + (x+\bot)(x^*+\bot) = 1 + xx^* + x\bot + \bot x^* +\bot\bot

1444: \leq  x^* + \bot\dsp,$$

1445: so the $*$-axioms give us $(x+\bot)^* \leq x^* + \bot$.

1446: We have $x^* \leq (x+\bot)^*$ and $\bot \leq (x+\bot)^*$ trivially,

1447: so

1448: $x^* + \bot \leq (x+\bot)^*$.

1449: Therefore, $f(x^*) = x^*+\bot = (x+\bot)^* = (f(x))^*$.

1450: So $f:K'\rightarrow L$ is a homomorphism.

1451: 

1452: We now claim that $L\in\KAT$.  Since $f:K'\rightarrow L$ is a homomorphism

1453: and $K'\in\KAT$,

1454: $L$ automatically satisfies the

1455: equational $\KAT$ axioms. We must now verify that $L$ satisfies the

1456: two remaining axioms, $p+q\cdot^L x \leq x \imp q^* \cdot^L p \leq x$

1457: and $p+x\cdot^L q \leq x \imp p\cdot^L q^* \leq x$.

1458: 

1459: Suppose that $p+q\cdot^L x \leq x$.  We must show $q^* \cdot^L p \leq x$.

1460: We have $p+qx+\bot = p+q\cdot^L x \leq x$.  

1461: From $p+qx\leq x$ we conclude

1462: $q^* p \leq x$; combining this with $\bot \leq x$, we have

1463: $q^*\cdot^L p = q^* p + \bot \leq x$, as desired.

1464: Similarly, $p+x\cdot^L q \leq x \imp p\cdot^L q^* \leq x$.

1465: So $L\in\KAT$.

1466: 

1467: Define the interpretation $J:\RexPB\rightarrow L$

1468: by $J(q) = f(I(q))$.

1469: Since $K',I\models E$, it immediately follows

1470: that $L,J\models E$.  Also,

1471: $J(r) \leq J(uru) = f(I(uru)) = f(\bot) = \bot+\bot = 0^L$, so

1472: $L,J\models r=0$.  Therefore, the assumption

1473: $\KAT\models E\wedge r=0 \imp s=t$ gives us

1474: $L,J\models s=t$.

1475: Therefore,

1476: $$I(s+uru) = I(s)+I(uru) = I(s) +\bot = f(I(s)) = J(s) = J(t) =

1477: I(t+uru)\dsp.$$

1478: Thus, $K,I\models s+uru=t+uru$.

1479: \qed

1480: 

1481: \begin{lem}

1482: \label{lem:mainlemtwo}

1483: $$\KAT^* \models E\wedge r=0 \imp s=t

1484: \iff

1485: \KAT^* \models E\imp s+uru=t+uru$$

1486: \end{lem}

1487: 

1488: \proof

1489: The right-to-left implication is as in Lemma~\ref{lem:mainlemone}.

1490: 

1491: For the left-to-right implication, it suffices to verify that

1492: the construction in the proof of Lemma~\ref{lem:mainlemone}

1493: preserves $*$-continuity.  Letting $q^{(n)}$ denote the $n^\mathrm{th}$

1494: power of $q$ under $\cdot^L$ (with $q^{(0)} = 1^L$), we have

1495: \begin{align*}

1496: \sup_n p\cdot^L q^{(n)} \cdot^L r & = 

1497: \sup_n (pq^n r + \bot)\\

1498: &= pq^* r + \bot\\

1499: &= p\cdot^L q^* \cdot^L r\dsp.

1500: \end{align*}

1501: (For the second equality above, one can observe that

1502: $pq^n r + \bot \leq pq^* r + \bot$ for all $n$, and that

1503: if $x$ is any upper bound for $pq^n r + \bot$, then 

1504: $pq^* r = \sup_n pq^n r \leq x$ and $\bot \leq x$, so

1505: $pq^* r + \bot \leq x$.  So $\sup_n (pq^n r + \bot) = pq^* r + \bot$.)

1506: \qed

1507: 

1508: \begin{lem}

1509: \label{lem:mainlemthree}

1510: $$\RKAT \models E\wedge r=0 \imp s=t

1511: \iff

1512: \RKAT \models E\imp s+uru=t+uru$$

1513: \end{lem}

1514: 

1515: \proof

1516: The right-to-left implication is as in

1517: Lemma~\ref{lem:mainlemone}.

1518: 

1519: For the left-to-right implication,

1520: using the above construction would require

1521: verifying that $L$ has a relational representation, which is not clear.

1522: Instead,

1523: we use a proof-theoretic argument.

1524: Suppose

1525: $\RKAT\models E\wedge r=0\imp \sigma\leq t$, where $\sigma\in R(s)$.

1526: $r=0$ is equivalent to $r\leq 0$, and $\KAT\models t\leq t+uru$, so 

1527: $\RKAT\models E\wedge r\leq 0\imp \sigma\leq t+uru$.

1528: 

1529: For the moment, suppose that the formulas are in the language of \KA, so

1530: that we can speak about relational proofs without worrying about tests.

1531: Let $(T,A)$ be a relational proof of

1532: $E\wedge r\leq 0 \imp \sigma\leq t+uru$.

1533: 

1534: We claim that the hypothesis $r\leq 0$ is never even applied in the proof!

1535: Suppose $r\leq 0$ is applied at node $f\in T$ (so 

1536: $f$ has

1537: one child $g$ with $A_g = \con$).

1538: For $r\leq 0$ to be applied at $f$,

1539: there must be states $v,w\in |A_f|$ and $\rho\in R(r)$ with

1540: $\rho\in L(A_f^{v,w})$.

1541: A property that is preserved in the automata of relational

1542: trees is that every state is accessible from the start state $a$,

1543: and the accept state $b$ is accessible from every state.  So

1544: there exist $\pi\in L(A_f^{a,v})$ and $\pi' \in L(A_f^{w,b})$.  Thus,

1545: we have $\pi\rho\pi'\in 

1546: %L(A_f^{a,v})L(A_f^{v,w})L(A_f^{w,b})\subseteq

1547: L(A_f)$;

1548: we also have $\pi\rho\pi'\in R(uru) \subseteq R(t+uru)$.

1549: Therefore, $R(t+uru)\cap L(A_f)\neq \emptyset$, so $f$ is in fact a leaf

1550: node, contradicting the assumption that we are applying $r\leq 0$ at $f$.

1551: (In other words, at any point in a relational tree for

1552: $E\wedge r \leq 0 \imp \sigma \leq t+uru$ where we could apply

1553: $r\leq 0$, we would already have to be at a leaf.)

1554: 

1555: So, because $r\leq 0$ is never applied,

1556: $(T,A)$ is also a relational proof of

1557: $E\imp \sigma \leq t+uru$.

1558: Therefore, $\RKA\models E\imp\sigma \leq t+uru$ for all

1559: $\sigma\in R(s)$.  By Lemma~\ref{lem:littlestarlem},

1560: $\RKA\models E\imp s \leq t+uru$, so

1561: $\RKA\models E\imp s+uru \leq t+uru$.

1562: $\RKA\models E\imp t+uru \leq s+uru$ is similar, and we now have

1563: $\RKA\models E\imp s+uru = t+uru$.

1564: 

1565: In case the formulas are not in the language of \KA, we can use

1566: the translation from Section~\ref{sec:relationship} as follows.

1567: We use the above argument to get

1568: \[

1569: \RKA\models\Tr(E\wedge r=0 \imp s=t)

1570: \Rightarrow

1571: \RKA\models\Tr(E\imp s+uru=t+uru)\dsp.\]

1572: (The extra hypotheses introduced by the translation may be

1573: treated the same

1574: as the hypotheses in $E$.  

1575: A subtle point here is that the translation introduces new program symbols,

1576: without adding them to the universal regular expression; however,

1577: the hypotheses added by the tranlation force the interpretations of these

1578: extra symbols to be below 1, so they could be added to the universal

1579: regular expression without affecting the validity of any formulas involved.)

1580: We then have

1581: \begin{align*}

1582: \RKAT\models E\wedge r=0 \imp s=t &\Rightarrow

1583: \RKA\models\Tr(E\wedge r=0 \imp s=t)\\

1584: &\Rightarrow \RKA\models\Tr(E\imp s+uru=t+uru)\\

1585: &\Rightarrow \RKAT\models E\imp s+uru=t+uru\dsp.

1586: \end{align*}

1587: % The lmcs class doesn't allow \qed to appear inside the align environment,

1588: % and doesn't have an AMS-like \qedhere.  So look the other way for a

1589: % moment.

1590: \vspace{-0.42in}

1591: 

1592: \qed

1593: 

1594: 

1595: \proof[Proof of Theorem~\ref{thm:genzeroelim}]

1596: Immediate from Lemmas~\ref{lem:mainlemone}--\ref{lem:mainlemthree}.

1597: \qed

1598: 

1599: 

1600: %%% Local Variables: 

1601: %%% mode: latex

1602: %%% TeX-master: "main"

1603: %%% End: 

1604: 

1605: 

1606: %\input{mainres2}

1607: \subsection{Idempotent Syntactic Homomorphisms}

1608: 

1609: We can also eliminate hypotheses of the form $cp = c$ ($c$ Boolean, $p$

1610: atomic) in the presence of other hypotheses, but not as cleanly as

1611: we eliminated $r=0$:

1612: %in Section~\ref{sec:genzeroelim}: 

1613: in this case, the remaining hypotheses

1614: will be modified.

1615: 

1616: The basic idea behind the technique was introduced in \cite{HK02},

1617: which showed how to simultaneously eliminate hypotheses of

1618: the form $cp = c$ and $r=0$.

1619: Ernie Cohen later observed that

1620: the portion of the proof specific to $cp=c$ was unnecessarily complicated

1621: \cite{ErnieCohenEmail}.

1622: What we present here is a simplified argument, that is also

1623: more general because it works in the presence of other hypotheses.

1624: Furthermore, in light of Theorem~\ref{thm:genzeroelim},

1625: we no longer

1626: need to worry about integrating the elimination of $r=0$ into

1627: the argument, since that can be done separately.

1628: 

1629: \begin{defi}

1630: \label{defi:syntactichomo}

1631: $H : \RexPB \to \RexPB$ is a \emph{syntactic homomorphism}

1632: if for any 

1633: %$K\in\KAT$ with 

1634: interpretation $I:\RexPB\to K$ (where $K\in\KAT$),

1635: $I\circ H :\RexPB \to K$ is also an interpretation.

1636: \note{In thesis, write this up in terms of guarded-string interpretation.}

1637: 

1638: For any syntactic homomorphism $H : \RexPB \to \RexPB$,

1639: let $E_H$ be the set of hypotheses

1640: \[\{p = H(p)~~|~~p\in\P\}\union\{b = H(b)~~|~~b\in\B\}\dsp.\]

1641: \end{defi}

1642: 

1643: Definition~\ref{defi:syntactichomo} is equivalent to saying that

1644: $H$ is a homomorphism up to $\KAT$-provable equality.  A

1645: consequence is that $H$ is uniquely determined (up to $\KAT$-provable

1646: equality) by its action on $\P$ and $\B$; the set of equations $E_H$ then,

1647: in a certain sense, captures the action of $H$.

1648: 

1649: (For readers familiar with

1650: guarded strings, Definition~\ref{defi:syntactichomo} is equivalent to

1651: saying that $G\circ H$ is an interpretation, where $G$ is the

1652: guarded-string interpretation.  More abstractly, the definition is equivalent

1653: to saying that $H$ is a lift of an endomorphism on the guarded-string

1654: model---that is, there is an endomorphism $h$ on the guarded-string model

1655: such that $G\circ H = h\circ G$.)

1656: 

1657: \begin{lem}

1658: \label{lem:syntactichomo}

1659: If $H:\RexPB\to\RexPB$ is a syntactic homomorphism, then for any

1660: $r\in\RexPB$,

1661: \[\KAT\models E_H\rightarrow r = H(r)\dsp.\]

1662: \end{lem}

1663: 

1664: \proof

1665: Straightforward induction on the structure of $r$.

1666: \note{More detail?}

1667: \qed

1668: 

1669: \begin{defi}

1670: \label{defi:idempotent}

1671: $H :\RexPB \to \RexPB$ is \emph{idempotent} if for all $r\in\RexPB$,

1672: \[\KAT\models H(r) = H(H(r))\dsp.\]

1673: \end{defi}

1674: 

1675: \begin{thm}

1676: \label{thm:syntactichomo}

1677: Suppose $H:\RexPB\to\RexPB$ is an idempotent syntactic homomorphism,

1678: and that $E$ is a set of hypotheses.  Let $H(E)$ denote

1679: the set of hypotheses

1680: \[\{H(r) = H(r')~~|~~\mbox{$r=r'$ is in $E$}\}\dsp.\]  Then for any

1681: $s,t\in\RexPB$ and $K\in\KAT$,

1682: \[K\models E \wedge E_H \imp s=t

1683: \iff K\models H(E) \imp H(s) = H(t)\dsp.\]

1684: \end{thm}

1685: 

1686: \proof

1687: For the right-to-left implication, suppose

1688: $K\models H(E) \imp H(s) = H(t)$ and that 

1689: we have an intepretation

1690: $I:\RexPB\to K$ with $K,I\models E\wedge E_H$.

1691: Then by Lemma~\ref{lem:syntactichomo}, $K,I \models H(E) \wedge

1692: s = H(s) \wedge t = H(t)$.  It follows by assumption that

1693: $K,I\models H(s) = H(t)$.  We now have

1694: $K,I\models s = H(s) = H(t) = t$.  Therefore,

1695: $K\models E\wedge E_H \imp s=t$.

1696: 

1697: For the left-to-right implication,

1698: suppose $K\models E\wedge E_H \imp s=t$,

1699: and that 

1700: we have an intepretation

1701: $I:\RexPB\to K$ with $K,I\models H(E)$.

1702: Define $I':\RexPB\to K$ by $I' = I \circ H$. $I'$ is an interpretation

1703: by Definition~\ref{defi:syntactichomo}.  For any $p\in\P$,

1704: idempotence of $H$ gives us $I'(p) = I(H(p)) = I(H(H(p))) = I'(H(p))$;

1705: similarly, $I'(b) = I'(H(b))$ for $b\in\B$, so $K,I'\models E_H$.

1706: For any equation $r = r'$ in $E$, $K,I\models H(E)$ gives us

1707: $I'(r) = I(H(r)) = I(H(r')) = I'(r')$, so $K,I' \models E$.

1708: Therefore, by the assumption $K\models E\wedge E_H\imp s=t$,

1709: we have $K,I' \models s=t$, and hence $I(H(s)) = I'(s) = I'(t) = I(H(t))$.

1710: Therefore $K,I \models H(s) = H(t)$, as desired.

1711: \qed

1712: 

1713: \begin{cor}

1714: \label{cor:syntactichomo}

1715: Suppose $F$ is a set of hypotheses $c_i p_i = c_i$, $1 \leq i \leq k$,

1716: where $p_i \in \P$ are distinct, and each $c_i$ is a Boolean term.

1717: Define $H:\RexPB \to\RexPB$ by $H(r) = r[p_i/\overline{c_i}p_i + c_i]$,

1718: the result of substituting $\overline{c_i}p_i + c_i$ for $p_i$

1719: in $r$ (for each $i$).  Then for any set $E$ of hypotheses,

1720: $s,t\in\RexPB$, and $K\in\KAT$, we have

1721: \[K\models E\wedge F \rightarrow s=t

1722: \iff

1723: K\models H(E) \rightarrow H(s) = H(t)\dsp.\]

1724: \end{cor}

1725: 

1726: \proof

1727: It is easy to verify that $H$ is an idempotent syntactic homomorphism.

1728: 

1729: Next, observe that $\KAT \models c_i p_i = c_i \leftrightarrow

1730: p_i = \overline{c_i}p_i + c_i$.

1731: Every equation in $E_H$ is either of the

1732: form $p_i = \overline{c_i}p_i + c_i$, or is a tautology such as $b=b$,

1733: so $F$ is equivalent to $E_H$.  

1734: The corollary now follows immediately from

1735: Theorem~\ref{thm:syntactichomo}.

1736: \qed

1737: 

1738: %Corollary~\ref{cor:syntactichomo} is not as satisfying as

1739: %Theorem~\ref{thm:genzeroelim}, because the remaining hypotheses have

1740: %been modified.  It could nevertheless 

1741: 

1742: The restriction that the $p_i$ be distinct in

1743: Corollary~\ref{cor:syntactichomo} is not a significant imposition,

1744: since we can combine $c_i p_i = c_i$ and $c_j p_j = c_j$, for $p_i = p_j$,

1745: into $(c_i + c_j)p_i = c_i+c_j$.

1746: %%The following reworded at referee's request.

1747: %($\KAT \models cp = c \wedge dp = d\leftrightarrow(c+d)p = c+d$ is 

1748: %easy to verify: $\imp$ is trivial, and $\leftarrow$ follows by multiplying

1749: %$(c+d)p = c+d$ on the left by $c$ or $d$.)

1750: (Supposing $cp=c$ and $dp = d$, we have $(c+d)p = cp + dp = c+d$.

1751: Supposing $(c+d)p = c + d$, we have $c\leq c+d$, so $c(c+d) = c$,

1752: giving us $cp = c(c+d)p = c(c+d) = c$; $dp = d$ follows similarly.)

1753: 

1754: %%% Local Variables: 

1755: %%% mode: latex

1756: %%% TeX-master: "main"

1757: %%% End: 

1758: 

1759: 

1760: %\input{further}

1761: \section{Conclusion and Further Questions}

1762: 

1763: Statements about the semantics of a program can often be expressed as

1764: Horn formulas in Kleene algebra with tests, and that is our primary

1765: motivation for studying the Horn theory of Kleene algebra with tests here.

1766: Hypotheses of the form $r=0$ are of particular interest, because they

1767: can capture partial correctness assertions, which are vital to studying the

1768: semantics of imperative programs.

1769: 

1770: While the validity of Horn formulas in Kleene algebra is not in

1771: general decidable, the validity of equations is.  We have shown how to

1772: eliminate hypotheses of the form $r=0$, even in the presence of other

1773: hypotheses; this allows us to extend any other technique for

1774: eliminating hypotheses to include hypotheses of the form $r=0$.  We

1775: have also shown how to eliminate hypotheses of the form $cp=c$ in the

1776: presence of other hypotheses (though not as cleanly: the remaining

1777: hypotheses might be modified).  This allows us to decide the validity

1778: of Horn formulas that have hypotheses of these forms.

1779: 

1780: The following are a few questions for further work.

1781: What other forms of hypotheses can be eliminated?  Can they be

1782: eliminated in the presence of other hypotheses?  Are there useful

1783: decision procedures for the validity of certain classes of Horn

1784: formulas that are not based on eliminating hypotheses?

1785: 

1786: %%% Local Variables: 

1787: %%% mode: latex

1788: %%% TeX-master: "main"

1789: %%% End: 

1790: 

1791: 

1792: \section{Acknowledgments}

1793: 

1794: This work was supported in part by NSF grant CCR-0105586 and by ONR Grant

1795: N00014-01-1-0968.  The views and conclusions contained herein are those of

1796: the author and should not be interpreted as necessarily representing the

1797: official policies or endorsements, either expressed or implied, of these

1798: organizations or the US Government.

1799: 

1800: \bibliographystyle{plain}

1801: %\bibliography{main}

1802: \begin{thebibliography}{10}

1803: 

1804: \bibitem{BK02}

1805: Adam Barth and Dexter Kozen.

1806: \newblock Equational verification of cache blocking in {LU} decomposition using

1807:   {K}leene algebra with tests.

1808: \newblock Technical Report 2002-1865, Computer Science Department, Cornell

1809:   University, June 2002.

1810: 

1811: \bibitem{Coh94}

1812: Ernie Cohen.

1813: \newblock Hypotheses in {K}leene algebra.

1814: \newblock Unpublished, 1994.

1815: 

1816: \bibitem{ErnieCohenEmail}

1817: Ernie Cohen, 2003.

1818: \newblock Private communication.

1819: 

1820: \bibitem{CKS96}

1821: Ernie Cohen, Dexter Kozen, and Frederick Smith.

1822: \newblock The complexity of {K}leene algebra with tests.

1823: \newblock Technical Report 96-1598, Computer Science Department, Cornell

1824:   University, July 1996.

1825: 

1826: \bibitem{Hard05thesis}

1827: Chris Hardin.

1828: \newblock {\em The {H}orn Theory of Relational {K}leene Algebra}.

1829: \newblock PhD thesis, Cornell University, 2005.

1830: 

1831: \bibitem{Hard05proof}

1832: Chris Hardin.

1833: \newblock Proof theory for {K}leene algebra.

1834: \newblock In {\em Proc. of the 20th Symp. on Logic in Computer Science (LICS

1835:   2005)}, pages 290--299, Los Alamitos, CA, June 2005. IEEE.

1836: 

1837: \bibitem{HK02}

1838: Chris Hardin and Dexter Kozen.

1839: \newblock On the elimination of hypotheses in {K}leene algebra with tests.

1840: \newblock Technical Report 2002-1879, Computer Science Department, Cornell

1841:   University, October 2002.

1842: 

1843: \bibitem{HK03}

1844: Chris Hardin and Dexter Kozen.

1845: \newblock On the complexity of the {H}orn theory of {REL}.

1846: \newblock Technical Report 2003-1896, Computer Science Department, Cornell

1847:   University, May 2003.

1848: 

1849: \bibitem{Koz91}

1850: Dexter Kozen.

1851: \newblock {\em The Design and Analysis of Algorithms}.

1852: \newblock Springer-Verlag, New York, 1991.

1853: 

1854: \bibitem{Koz97}

1855: Dexter Kozen.

1856: \newblock Kleene algebra with tests.

1857: \newblock {\em Transactions on Programming Languages and Systems}, pages

1858:   427--443, 1997.

1859: 

1860: \bibitem{Koz00}

1861: Dexter Kozen.

1862: \newblock On {H}oare logic and {K}leene algebra with tests.

1863: \newblock {\em Trans.~Computational Logic}, 1(1):60--76, July 2000.

1864: 

1865: \bibitem{Koz02}

1866: Dexter Kozen.

1867: \newblock On the complexity of reasoning in {K}leene algebra.

1868: \newblock {\em Information and Computation}, 179:152--162, 2002.

1869: 

1870: \bibitem{KP00}

1871: Dexter Kozen and Maria-Cristina Patron.

1872: \newblock Certification of compiler optimizations using {K}leene algebra with

1873:   tests.

1874: \newblock In J.~Lloyd, V.~Dahl, U.~Furbach, M.~Kerber, K.-K. Lau,

1875:   C.~Palamidessi, L.~M. Pereira, Y.~Sagiv, and P.~J. Stuckey, editors, {\em

1876:   Proc. 1st Int. Conf. Computational Logic (CL2000)}, volume 1861 of {\em

1877:   Lecture Notes in Artificial Intelligence}, pages 568--582, London, July 2000.

1878:   Springer-Verlag.

1879: 

1880: \bibitem{KS96}

1881: Dexter Kozen and Frederick Smith.

1882: \newblock Kleene algebra with tests: completeness and decidability.

1883: \newblock In D.~van Dalen and M.~Bezem, editors, {\em Proc.~10th Int.~Workshop

1884:   on Computer Science Logic (CSL'96)}, volume 1258 of {\em Springer-Verlag

1885:   Lecture Notes in Computer Science}, pages 244--259, Utrecht, The Netherlands,

1886:   September 1996.

1887: 

1888: \end{thebibliography}

1889: 

1890: 

1891: 

1892: \end{document}

1893: