1: \documentclass[fleqn,12pt]{article}
2: \usepackage{msrtr}\msrtrno{2003-08}
3:
4: % K. Rustan M. Leino
5:
6: \def \OpusText {KRML 118 / VK0099 / MSR-TR-2003-08}
7: \def \DocumentTitle {On computing the fixpoint of a set of boolean equations}
8: \def \RevisionDate {30 December 2003}
9: % Revision history:
10: % 31 Jan 2003 Typed in first draft
11: % 1 Feb 2003 Revised and finished proofs
12: % 3 Feb 2003 Typed in revisions
13: % 5 Feb 2003 Final revisions
14: % 26 Feb 2003 Simplified proof of Lemma 3 (by monotonicity only,
15: % no induction needed)
16: % 22 Feb 2003 Started new intro, based on feedback from Tony
17: % Hoare, and from Patrick Cousot and Carroll Morgan at
18: % the IFIP WG 2.3 Biarritz meeting.
19: % 5 May 2003 Worked on intro
20: % 23 Dec 2003 Continued editing
21: % 24 Dec 2003 vkuncak: minor edits
22: % 30 Dec 2003 Changed the quadratic forms of Expanded Closed Form into cubic forms
23: % 19 Aug 2004 vkuncak made trivial changes to allow arxiv processing and submitted to arxiv
24:
25: \input{macros}
26:
27: % macros used in this paper
28: \newcommand{\Bool}{\mathbb{B}}
29: \newcommand{\DomA}{\mathbb{A}}
30: \newcommand{\tup}[1]{\overrightarrow{#1}}
31: \newcommand{\tupatmost}{\mathrel{\tup{\atmost}}}
32: \newcommand{\comp}{\circ}
33: \newcommand{\LambdaExpr}[3]{\QuantExpr{\lambda}{#1}{#2}{#3}}
34: \newcommand{\zerotup}{\tup{0}}
35: \newcommand{\zerofunc}{\dot{0}}
36: \newtheorem{theorem}{Theorem}
37: \newtheorem{lemma}[theorem]{Lemma}
38: \newtheorem{corollary}[theorem]{Corollary}
39: \setcounter{theorem}{-1}
40: \newcommand{\Gets}{\,{:=}\;}
41: \newcommand{\Case}[1]{\par\noindent \textsc{Case $#1$:~~}}
42: \newcommand{\SubCase}[1]{\par\noindent \textsc{Sub-case $#1$:~~}}
43: \newcommand{\Proof}{\par\noindent\textit{Proof.}}
44: \newcommand{\ProofOf}[1]{\par\noindent\textit{Proof of #1.}}
45: \newcommand{\EndProof}{\qquad\EndProofBullet}
46:
47: \newcommand{\foo}{\mathfrak{f}}
48: \newcommand{\goo}{\mathfrak{g}}
49: \newcommand{\hoo}{\mathfrak{h}}
50:
51: \newcommand{\down}[2]{\QuantExpr{{\downarrow}}{#1}{}{#2}}
52: % Note, in order to write \'c in the tabbing environment, one
53: % needs to write it as {\accent"13 c}.
54: \newcommand{\BL}{Beki{\accent"13 c}-Leszczy{\l}owski}
55: \newcommand{\Let}{\mathbf{let}~}
56: \newcommand{\In}{~\mathbf{in}~}
57:
58: % end of macros used in this paper
59:
60: \setcounter{page}0
61:
62: \title{\DocumentTitle}
63: \author{Viktor Kuncak\\\normalsize MIT\\\normalsize\texttt{vkuncak@mit.edu} \and
64: K. Rustan M. Leino\\\normalsize Microsoft Research\\\normalsize\texttt{leino@microsoft.com}}
65: \date{\RevisionDate}
66:
67: \begin{abstract}
68: This paper presents a method for computing a least fixpoint of a
69: system of equations over booleans. The resulting computation can
70: be significantly shorter than the result of iteratively evaluating
71: the entire system until a fixpoint is reached.
72: \end{abstract}
73:
74: \maketitle
75:
76:
77: \Section{Introduction}
78:
79: Many problems in computer science, in particular those arising in the
80: context of program analysis, involve the computation of a least (or,
81: dually, greatest) fixpoint of a system of equations. In this paper,
82: we consider a way to compute a least fixpoint when the equations
83: involved are over the booleans. In some important cases, the
84: resulting computation can be significantly shorter than the
85: computation that iteratively evaluates the entire system until a
86: fixpoint is reached.
87:
88: Let us begin with an overview of our result. We restrict our
89: attention to a finite lattice. A finite lattice is a complete
90: lattice and has no infinite ascending chains, and any monotonic
91: function on such a lattice is also continuous. Hence, the Kleene
92: Fixpoint Theorem~\cite{Kleene:fixpoint} states that the least fixpoint
93: of any monotonic function $F$ is the lattice join of the sequence of
94: elements
95: \[ F^0(\bot),~ F^1(\bot),~ F^2(\bot),~ \ldots \]
96: where exponentiation denotes successive function applications and
97: $\bot$ denotes the bottom element of the lattice. Because this
98: sequence is ascending and because the lattice is finite, % we have that
99: there exists a natural number $K$ such that
100: \[ F^K(\bot) \]
101: is the least fixpoint of $F$. We call the least such $K$ the
102: \emph{fixpoint depth} of $F$.
103:
104: If we are able to evaluate function $F$ and if we are able
105: to determine whether two given lattice elements are equal,
106: then we can compute the least fixpoint of $F$: starting from
107: the value $\bot$, repeatedly apply $F$ until the application
108: of $F$ leaves the value unchanged. The existence of a
109: fixpoint depth guarantees that this process terminates. In
110: this paper, we consider the problem of computing an
111: \emph{expression} for the least fixpoint, without computing
112: the \emph{value} of the expression. By first computing a small
113: expression for the least fixpoint, we can relegate the
114: computation of the value of the expression to an external
115: tool such as a SAT solver \cite{Leino:SPIN2003}. In the
116: sequel we therefore do not assume that we are able to
117: compute the value of an expression into a particular
118: lattice element.
119:
120: The fixpoint depth of a function $F$ on a lattice is bounded by the
121: height of the lattice. Therefore, for the 2-element lattice $\Bool$
122: of the booleans (which has height 1), the least fixpoint of $F$ is
123: given by $F(\bot)$, and for the $2^n$-element lattice $\Bool^n$ that is
124: the Cartesian product space of $n$ booleans (which has height $n$),
125: the least fixpoint of $F$ is given by $F^n(\bot)$.
126:
127: Any function $F \colon \Bool^n \to \Bool^n$ can be represented
128: isomorphically by $n$ functions $f_i \colon \Bool^n \to \Bool$. We
129: write
130: \[ F \Equal (f_1,\ldots,f_n) \]
131: where the tuple of functions is itself defined to be a function, as
132: follows, for any $n$-tuple $X$ of booleans:
133: \[
134: (f_1,\ldots,f_n)(X)
135: \Equal
136: (f_1(X),~ \ldots,~ f_n(X))
137: \]
138: For example, let $n=3$ and let $F=(f,g,h)$. Then, the least fixpoint
139: of $F$ equals $F^3(\bot,\bot,\bot)$, as we have argued above. In
140: terms of the functions $f,g,h$, this expands to:
141: \[\begin{array}{@{}l@{}l@{}l@{}}
142: ( & f( & f( f(\bot,\bot,\bot),~ g(\bot,\bot,\bot),~ h(\bot,\bot,\bot)), \\
143: & & g( f(\bot,\bot,\bot),~ g(\bot,\bot,\bot),~ h(\bot,\bot,\bot)), \\
144: & & h( f(\bot,\bot,\bot),~ g(\bot,\bot,\bot),~ h(\bot,\bot,\bot))), \\
145: & g( & f( f(\bot,\bot,\bot),~ g(\bot,\bot,\bot),~ h(\bot,\bot,\bot)), \\
146: & & g( f(\bot,\bot,\bot),~ g(\bot,\bot,\bot),~ h(\bot,\bot,\bot)), \\
147: & & h( f(\bot,\bot,\bot),~ g(\bot,\bot,\bot),~ h(\bot,\bot,\bot))), \\
148: & h( & f( f(\bot,\bot,\bot),~ g(\bot,\bot,\bot),~ h(\bot,\bot,\bot)), \\
149: & & g( f(\bot,\bot,\bot),~ g(\bot,\bot,\bot),~ h(\bot,\bot,\bot)), \\
150: & & h( f(\bot,\bot,\bot),~ g(\bot,\bot,\bot),~ h(\bot,\bot,\bot))))
151: \end{array}\]
152: We refer to this closed form of the fixpoint as the \emph{Expanded
153: Closed Form}.
154: A different way to write down the Expanded Closed Form, which shares
155: common subexpressions, is:
156: \[
157: \begin{array}{@{}l@{}l@{~}l@{}l@{~}l@{}l@{~~}l@{}}
158: \Let a_1 & = \bot, &
159: a_2 & = \bot, &
160: a_3 & = \bot & \In \\
161: \Let b_1 & = f(a_1,a_2,a_3), &
162: b_2 & = g(a_1,a_2,a_3), &
163: b_3 & = h(a_1,a_2,a_3) & \In \\
164: \Let c_1 & = f(b_1,b_2,b_3), &
165: c_2 & = g(b_1,b_2,b_3), &
166: c_3 & = h(b_1,b_2,b_3) & \In \\
167: \Let d_1 & = f(c_1,c_2,c_3), &
168: d_2 & = g(c_1,c_2,c_3), &
169: d_3 & = h(c_1,c_2,c_3) & \In \\
170: \multicolumn{2}{l}{
171: \quad (d_1,d_2,d_3)}
172: \end{array}
173: \]
174: This representation is cubic in $n$, which means that computing it
175: may take time and space that is cubic in $n$.\footnote{%
176: If we allow ourselves to write functions of $n$ arguments as
177: functions over $n$-tuples, then we can obtain a quadratic
178: representation. For example, with $n=3$, we have
179: $
180: \Let a_1=\ldots, a_2=\ldots, a_3=\ldots \In \Let a=(a_1,a_2,a_3) \In
181: \Let b_1=f(a), b_2=g(a), b_3=h(a) \In \Let b=(b_1,b_2,b_3) \In
182: \ldots
183: $.
184: }
185:
186: Let us consider another closed form, which we call the \emph{Pruned
187: Closed Form}. In the Pruned Closed Form, an application of a
188: function $f_i$ is replaced by $\bot$ if it occurs in another
189: application of the same function $f_i$. For
190: the example above, where $n=3$, the Pruned Closed Form is:
191: \[
192: \begin{array}{@{}l@{}l@{}l@{}l@{}l@{}l@{}}
193: ( & f( & \bot, \\
194: & & g( \bot,~ & \bot,~ & h(\bot,\bot,\bot)&), \\
195: & & h( \bot,~ & g(\bot,\bot,\bot),~ & \bot&)), \\
196: & g( & f( \bot,~ & \bot,~ & h(\bot,\bot,\bot)&), \\
197: & & \bot, \\
198: & & h( \bot,~ & \bot,~ & \bot&)), \\
199: & h( & f( \bot,~ & g(\bot,\bot,\bot),~ & \bot&), \\
200: & & g( \bot,~ & \bot,~ & \bot&), \\
201: & & \bot &&&\;))
202: \end{array}
203: \]
204:
205: If we do not have any interpretation for the functions $f_i$---in other
206: words, if each $f_i$ is just a symbolic name for an uninterpreted
207: function---then the cubic-sized Expanded Closed Form may be a
208: reasonably small closed-form representation of the fixpoint. The
209: Pruned Closed Form is generally much larger than cubic in $n$: for
210: every subset $S$ of $f_2,\ldots,f_n$, function $f_1$ appears expanded
211: in a context where the set of enclosing functions is $S$. (A smaller
212: Pruned Closed Form can be obtained by taking advantage of common
213: subexpressions.) However, there are cases where the Pruned Closed
214: Form can be significantly smaller than the Expanded Closed Form, for
215: example when the fixpoint computation is dominated by the computation
216: of local fixpoints, meaning fixpoints that involve only a small number
217: of the functions. An important situation in program analysis where
218: this case applies is when each function represents a control point in
219: a given program, a function is defined in terms of the functions
220: corresponding to the successor (or predecessor) control points, and
221: the given program contains many local loops.
222:
223: For example, suppose
224: \[
225: f(x,y,z) \Equal \foo(x,y)
226: \qquad
227: g(x,y,z) \Equal \goo(x)
228: \qquad
229: h(x,y,z) \Equal \hoo(y,z)
230: \]
231: for some functions $\foo$, $\goo$, and $\hoo$. Then the Expanded
232: Closed Form is
233: %\[
234: % (\begin{array}[t]{@{}l@{}l}
235: % \foo( & \foo(\foo(\bot,\bot),\goo(\bot)), \\
236: % & \goo(\foo(\bot,\bot)), \\
237: % & \hoo(\goo(\bot),\hoo(\bot,\bot))), \\
238: % \goo( & \foo(\foo(\bot,\bot), \goo(\bot))), \\
239: % \hoo( & \goo(\foo(\bot,\bot)), \\
240: % & \hoo(\goo(\bot),\hoo(\bot,\bot))))
241: % \end{array}
242: %\]
243: \[
244: \begin{array}{@{}l@{}l@{~}l@{}l@{~}l@{}l@{~~}l@{}}
245: \Let a_1 & = \bot, &
246: a_2 & = \bot, &
247: a_3 & = \bot & \In \\
248: \Let b_1 & = \foo(a_1,a_2), &
249: b_2 & = \goo(a_1), &
250: b_3 & = \hoo(a_2,a_3) & \In \\
251: \Let c_1 & = \foo(b_1,b_2), &
252: c_2 & = \goo(b_1), &
253: c_3 & = \hoo(b_2,b_3) & \In \\
254: \Let d_1 & = \foo(c_1,c_2), &
255: d_2 & = \goo(c_1), &
256: d_3 & = \hoo(c_2,c_3) & \In \\
257: \multicolumn{2}{l}{
258: \quad (d_1,d_2,d_3)}
259: \end{array}
260: \]
261: In contrast, the Pruned Closed Form yields the much shorter expression
262: \[
263: (\begin{array}[t]{@{}l@{}l}
264: \foo( & \foo(\bot,\goo(\bot)), \\
265: & \goo(\bot)), \\
266: \goo( & \foo(\bot, \bot)), \\
267: \hoo( & \goo(\foo(\bot,\bot)), \\
268: & \bot))
269: \end{array}
270: \]
271: More generally, for an even $n$, suppose $f_i(x_1,\ldots,x_n)$ is
272: $\foo_i(x_i, x_{i+1})$ when $i$ is odd and $\foo_i(x_{i-1}, x_i)$ when
273: $i$ is even. Then the Expanded Closed Form is still cubic, whereas the Pruned
274: Closed Form is the linear-sized expression
275: \[\begin{array}{ll}
276: (
277: & \foo_1(\bot, \foo_2(\bot, \bot)),
278: \quad \foo_2(\foo_1(\bot, \bot), \bot),
279: \\ & \ldots
280: \\ & \foo_i(\bot, \foo_{i+1}(\bot, \bot)),
281: \quad \foo_{i+1}(\foo_i(\bot, \bot), \bot),
282: \\ & \ldots
283: \\ & \foo_{n-1}(\bot, \foo_n(\bot, \bot)),
284: \quad \foo_n(\foo_{n-1}(\bot, \bot), \bot)
285: \\ )
286: \end{array}\]
287:
288: In the rest of this paper, we define the Pruned Closed Form more
289: precisely and prove that it yields the same value as the Expanded
290: Closed Form.
291:
292: \Section{Using the \BL{} Theorem} \label{sec:bl}
293:
294: In this section, we sketch how to obtain the Pruned Closed Form by
295: applications of the \BL{}
296: Theorem~\cite{Bekic:theorem,Leszczylowski:theorem}.
297:
298: We write
299: \[ \down{x}{R(x)} \]
300: for the lattice meet of all values for $x$ that satisfy the predicate
301: $R(x)$. For any monotonic function $F$, we then write
302: \begin{equation}\label{fixpoint:notation}
303: \down{x}{x = F(x)}
304: \end{equation}
305: to denote the least fixpoint of $F$, because the Tarski Fixpoint
306: Theorem~\cite{Tarski:theorem} says that the meet of all fixpoints is
307: itself a fixpoint.
308: Using for a function $F \colon \Bool^n \to \Bool^n$ the isomorphic
309: representation of $n$ functions $f_i \colon \Bool^n \to \Bool$, we
310: can write (\ref{fixpoint:notation}) equivalently as:
311: \[\begin{array}{@{}ll@{}c@{}l@{}l@{}}
312: \down{x_1,\ldots,x_n}{
313: & x_1 & \Equal & f_1(x_1,\ldots,x_n) & \And \\
314: & & \vdots & & \And \\
315: & x_n & \Equal & f_n(x_1,\ldots,x_n)}
316: \end{array}\]
317:
318: We can now state the \BL{}
319: Theorem~\cite{Bekic:theorem,Leszczylowski:theorem}, for any monotonic
320: functions $F$ and $G$ (possibly over different lattices):
321: \[\begin{array}{@{}ll@{}}
322: & \down{a,b}{a = F(a,b) \And b = G(a,b)} \\
323: = \\
324: & \down{a,b}{a = F(a,b) \And b = \down{b}{b=G(a,b)}}
325: \end{array}\]
326: Note that each side of the equality expresses a fixpoint in the
327: lattice $\Bool^n$ if $F$ and $G$ are functions of types $\Bool^p \times
328: \Bool^q \to \Bool^p$ and $\Bool^p \times
329: \Bool^q \to \Bool^q$, respectively, for $p$ and $q$ such that $p+q=n$.
330:
331: A consequence of the \BL{} Theorem and the Kleene Fixpoint Theorem for a
332: known fixpoint depth is the following lemma:
333: \begin{lemma}\label{BLK:lemma}
334: For any lattice domain $\DomA$ and monotonic functions
335: $F \colon \DomA \times \Bool \to \DomA$ and
336: $G \colon \DomA \times \Bool \to \Bool$,
337: \[\begin{array}{@{}ll@{}}
338: & \down{a,b}{a = F(a,b) \And b = G(a,b)} \\
339: = \\
340: & \down{a,b}{a = F(a,b) \And b = G(a,\bot)}
341: \end{array}\]
342: \end{lemma}
343: \Proof{}
344: \Calc{
345: $ \down{a,b}{a = F(a,b) \And b = G(a,b)} $
346: \Conn{ \BL{} Theorem }
347: $ \down{a,b}{a = F(a,b) \And b = \down{b}{b=G(a,b)}} $
348: \Conn{ $\LambdaExpr{b}{}{G(a,b)}$ is a function on $\Bool$, and
349: \nlhint therefore its fixpoint depth is at most 1, and
350: \nlhint therefore $\down{b}{b=G(a,b)} \Equal G(a,\bot)$ }
351: $ \down{a,b}{a = F(a,b) \And b = G(a,\bot)} $
352: \EndProof
353: }
354:
355: Using Lemma~\ref{BLK:lemma}, we now show that the Pruned Closed Form
356: is indeed the least fixpoint in $\Bool^2$. For any monotonic boolean
357: functions $f$ and $g$:
358: \Calc{
359: \calcEqLabel{spec:thm:2}
360: $ \down{a,b}{a=f(a,b) \And b=g(a,b)} $
361: \Conn{ Lemma~\ref{BLK:lemma} with $F,G:=f,g$ }
362: $ \down{a,b}{a=f(a,b) \And b=g(a,\bot)} $
363: \Conn{ substitute equals for equals }
364: $ \down{a,b}{a=f(a,g(a,\bot)) \And b=g(a,\bot)} $
365: \Conn{ Lemma~\ref{BLK:lemma} with \nlhint
366: $G,F:= \LambdaExpr{a,b}{}{f(a,g(a,\bot))},
367: \LambdaExpr{a,b}{}{g(a,\bot)}$ }
368: $ \down{a,b}{a=f(\bot,g(\bot,\bot)) \And b=g(a,\bot)} $
369: }
370: This calculation shows that an expression for the least solution of
371: $a$ in equation (\ref{spec:thm:2}) is
372: \[ f(\bot,g(\bot,\bot)) \]
373: By a symmetric argument, an expression for the least solution of $b$
374: in equation (\ref{spec:thm:2}) is
375: \[ g(f(\bot,\bot),\bot) \]
376: That is, an expression for (\ref{spec:thm:2}) is
377: \[
378: ( ~~
379: f(\bot,g(\bot,\bot)), ~~
380: g(f(\bot,\bot),\bot) ~~
381: )
382: \]
383: which is the Pruned Closed Form.
384:
385: Using the result for $\Bool^2$, we can show that the Pruned Closed
386: Form is also the least fixpoint in $\Bool^3$. For any monotonic
387: boolean functions $f$, $g$, and $h$:
388: \Calc{
389: \calcEqLabel{spec:thm:3}
390: $ \down{a,b,c}{a=f(a,b,c) \And b=g(a,b,c) \And c=h(a,b,c)} $
391: \Conn{ Lemma~\ref{BLK:lemma} with $G:=h$ (and with $F$ as the
392: isomorphic \nlhint representation of functions $f$ and $g$) }
393: $ \down{a,b,c}{a=f(a,b,c) \And b=g(a,b,c) \And c=h(a,b,\bot)} $
394: \Conn{ substitute equals for equals }
395: $ \down{a,b,c}{a=f(a,b,c) \And b=g(a,b,h(a,b,\bot)) \And c=h(a,b,\bot)} $
396: \Conn{ Lemma~\ref{BLK:lemma} with
397: $G:=\LambdaExpr{a,b,c}{}{g(a,b,h(a,b,\bot))}$ }
398: $ \down{a,b,c}{a=f(a,b,c) \And b=g(a,\bot,h(a,\bot,\bot)) \And
399: c=h(a,b,\bot)} $
400: \Conn{ substitute equals for equals }
401: $ \down{a,b,c}{\begin{array}[t]{l}
402: a=f(a,~ g(a,\bot,h(a,\bot,\bot)),~ c) \And \\
403: b=g(a,\bot,h(a,\bot,\bot)) \And
404: c=h(a,b,\bot)}
405: \end{array} $
406: \Conn{ the first 3 steps of this calculation, in reverse order }
407: $ \down{a,b,c}{\begin{array}[t]{l}
408: a=f(a,~ g(a,\bot,h(a,\bot,\bot)),~ c) \And \\
409: b=g(a,b,c) \And
410: c=h(a,b,c)}
411: \end{array} $
412: \Conn{ Lemma~\ref{BLK:lemma} with $G:=g$ }
413: $ \down{a,b,c}{\begin{array}[t]{l}
414: a=f(a,~ g(a,\bot,h(a,\bot,\bot)),~ c) \And \\
415: b=g(a,\bot,c) \And
416: c=h(a,b,c)}
417: \end{array} $
418: \Conn{ substitute equals for equals }
419: $ \down{a,b,c}{\begin{array}[t]{l}
420: a=f(a,~ g(a,\bot,h(a,\bot,\bot)),~ c) \And \\
421: b=g(a,\bot,c) \And
422: c=h(a,g(a,\bot,c),c)}
423: \end{array} $
424: \Conn{ Lemma~\ref{BLK:lemma} with
425: $G:=\LambdaExpr{a,b,c}{}{h(a,g(a,\bot,c),c)}$ }
426: $ \down{a,b,c}{\begin{array}[t]{l}
427: a=f(a,~ g(a,\bot,h(a,\bot,\bot)),~ c) \And \\
428: b=g(a,\bot,c) \And
429: c=h(a,g(a,\bot,\bot),\bot)}
430: \end{array} $
431: \Conn{ substitute equals for equals }
432: $ \down{a,b,c}{\begin{array}[t]{l}
433: a=f(a,~
434: g(a,\bot,h(a,\bot,\bot)),~
435: h(a,g(a,\bot,\bot),\bot)) \And
436: \\
437: b=g(a,\bot,c) \And
438: c=h(a,g(a,\bot,\bot),\bot)}
439: \end{array} $
440: \Conn{ Lemma~\ref{BLK:lemma} with
441: $G:=$ \nlhint $\LambdaExpr{a,b,c}{}{
442: f(a,~ g(a,\bot,h(a,\bot,\bot)),~ h(a,g(a,\bot,\bot),\bot))}$ }
443: $ \down{a,b,c}{\begin{array}[t]{l}
444: a=f(\bot,~
445: g(\bot,\bot,h(\bot,\bot,\bot)),~
446: h(\bot,g(\bot,\bot,\bot),\bot)) \And \\
447: b=g(a,\bot,c) \And
448: c=h(a,g(a,\bot,\bot),\bot)}
449: \end{array} $
450: }
451: This calculation shows that an expression for the least solution of
452: $a$ in (\ref{spec:thm:3}) is
453: \[
454: f(\bot,~
455: g(\bot,\bot,h(\bot,\bot,\bot)),~
456: h(\bot,g(\bot,\bot,\bot),\bot))
457: \]
458: and similarly for $b$ and $c$.
459:
460: Our main result is that the Pruned Closed Form is the least fixpoint
461: in $\Bool^n$ for any $n$. In the next section, we prove this result
462: directly, not using Lemma~\ref{BLK:lemma}.
463:
464:
465: \Section{The theorem}
466:
467: We are given $n \atleast 1$ monotonic functions $f_1, \ldots, f_n \colon \Bool^n
468: \to \Bool$, where $\Bool$ is the boolean domain $\{0,1\}$ ordered by
469: $\atmost$ (with $0 \atmost 1$). To represent an indexed $n$-tuple of
470: things, like a list of booleans $x_1,\ldots,x_n$, we write
471: $\tup{x}$. The fact that the given functions are monotonic is written
472: as follows, for any index $i$ and any tuples of booleans $\tup{x}$ and
473: $\tup{y}$:
474: \[
475: \tup{x} \tupatmost \tup{y}
476: ~~\Imp~~
477: f_i.\tup{x} \atmost f_i.\tup{y}
478: \]
479: where an infix dot (with the highest operator precedence) denotes
480: function application, and the order $\tupatmost$ is the component-wise
481: ordering of tuples:
482: \[
483: \tup{x} \tupatmost \tup{y}
484: \Equiv
485: \Forall{i}{}{
486: x_i \atmost y_i
487: }
488: \]
489:
490: We are interested in viewing the functions as specifying a system of
491: equations, namely:
492: \begin{equation}\label{system}\begin{array}{rrcl}
493: x_1, \ldots, x_n :
494: & x_1 & = & f_1.(x_1,~ \ldots,~ x_n) \\
495: & \multicolumn{2}{l}{\ldots} \\
496: & x_n & = & f_n.(x_1,~ \ldots,~ x_n)
497: \end{array}\end{equation}
498: where the variables to the left of the colon show the unknowns.
499: We take a tuple of functions $(f_1,~\ldots,~f_n)$, which we can also
500: write as $\tup{f}$, to itself be a
501: function, one which produces a tuple from the results of applying the
502: given argument to each of the functions. For example, for the
503: functions given above and an argument $\tup{x}$, we have:
504: \[
505: (f_1,~\ldots,~f_n).\tup{x}
506: \Equal
507: (f_1.\tup{x},~\ldots,~f_n.\tup{x})
508: \]
509: Thus, we can write the system (\ref{system}) of equations as:
510: \[\begin{array}{rl}
511: \tup{x} :
512: & \tup{x} \Equal \tup{f}.\tup{x}
513: \end{array}\]
514: We are interested in the \emph{least} (in the sense of the ordering
515: $\tupatmost$) solution $\tup{x}$ that satisfies this equation. That
516: is, we are interested in the \emph{least fixpoint} of the function
517: $\tup{f}$. Because the lattice of boolean $n$-tuples has height $n$,
518: the least fixpoint of $\tup{f}$ can be reached by applying $\tup{f}$
519: $n$ times starting from the bottom element of the lattice. That is,
520: the least fixpoint of $\tup{f}$ is given by:
521: \[ \tup{f}^n.\zerotup \]
522: where exponentiation denotes successive function applications and
523: $\zerotup$ is the tuple of $n$ 0's.
524:
525: %
526: % vkuncak: removed this old introduction
527: %
528: % If $n$ is large, say in the 100's or 1000's or even higher, we may not
529: % want to do all of these repeated applications of $\tup{f}$, especially
530: % if we expect each function $f_i$ to depend only on a small number of
531: % the elements in the argument tuple. Instead, we can start from the
532: % tuple $\tup{x}$, repeatedly expanding occurrences of each $x_i$
533: % according to the corresponding equation in (\ref{system}), namely
534: % replacing $x_i$ with $f_i.\tup{x}$. If, in this expansion, a term
535: % $x_i$ occurs as a subexpression of an argument to an application of
536: % function $f_i$, then this occurrence can be replaced by 0, rather than
537: % by $f_i.\tup{x}$. Hence, a computation that performs the expansion
538: % eventually terminates. We next prove that such a computation
539: % arrives at the correct result.
540:
541: To precisely specify the Pruned Closed Form, we introduce a
542: notation that keeps track of which functions have been
543: applied in the enclosing context. In particular, we use a
544: set that contains the indices of the functions already
545: applied. Formally, we define the following family of
546: functions, for any index $i$ and set $S$ of indices:
547: \[
548: g_{S,i} \Equal \left\{
549: \begin{array}{ll}
550: f_i \comp (g_{S \cup \{i\},1},~\ldots,~g_{S \cup \{i\},n})
551: & \mbox{if $i \not\in S$} \\
552: \LambdaExpr{\tup{x}}{}{0}
553: & \mbox{if $i \in S$}
554: \end{array}
555: \right.
556: \]
557: Taking advantage of our previous notation and using $\zerofunc$ to
558: denote the function that always returns 0 (that is, the boolean 0
559: extended pointwise to a boolean function), we can write the definition
560: of $g$ as follows:
561: \[
562: g_{S,i} \Equal \left\{
563: \begin{array}{ll}
564: f_i \comp \tup{g_{S \cup \{i\}}}
565: & \mbox{if $i \not\in S$} \\
566: \zerofunc
567: & \mbox{if $i \in S$}
568: \end{array}
569: \right.
570: \]
571:
572: Our goal is now to prove the following:
573: \begin{theorem}\label{main:theorem}
574: \[
575: \tup{g_{\emptyset}}.\zerotup \Equal \tup{f}^n.\zerotup
576: \]
577: \end{theorem}
578:
579:
580: \Section{Proof} \label{sec:proof}
581:
582: We start by proving some lemmas that we use in the proof of this
583: theorem.
584:
585: \begin{lemma}\label{lemma:1}
586: For any index $i$ and for any $S \subsetneqq \{1,\ldots,n\}$,
587: \[
588: g_{S,i}.\zerotup ~~\atmost~~ (f_i \comp \tup{f}^{n-|S|-1}).\zerotup
589: \]
590: \end{lemma}
591: \Proof{}
592: By induction on $n-|S|$. Let $T$ denote $S \cup \{i\}$. We consider
593: three cases.
594: \Case{i \in S}
595: \Calc{
596: $ g_{S,i}.\zerotup $
597: \Conn{ definition of $g$, since $i \in S$ }
598: $ \zerofunc.\zerotup $
599: \Conn{ definition of $\zerofunc$ }
600: $ 0 $
601: \conn{\atmost}{ $0$ is bottom element of $\atmost$ }
602: $ (f_i \comp \tup{f}^{n-|S|-1}).\zerotup $
603: }
604: \Case{i \not\in S \And |T| < n}
605: \Calc{
606: $ g_{S,i}.\zerotup $
607: \Conn{ definition of $g$, since $i \not\in S$ }
608: $ (f_i \comp \tup{g_T}).\zerotup $
609: \Conn{}
610: $ (f_i \comp (g_{T,1},~ \ldots,~ g_{T,n})).\zerotup $
611: \Conn{ distribute $.\zerotup$ }
612: $ f_i.(g_{T,1}.\zerotup,~ \ldots,~ g_{T,n}.\zerotup) $
613: \conn{\atmost}{ for each index $j$, induction hypothesis with
614: $i,S \Gets j,T$, since \nlhint $|S|+1 = |T| < n$;
615: and monotonicity of $f_i$ }
616: $ f_i.((f_1 \comp \tup{f}^{n-|S|-2}).\zerotup,~
617: \ldots,~
618: (f_n \comp \tup{f}^{n-|S|-2}).\zerotup) $
619: \Conn{ distribute $.\zerotup$ }
620: $ (f_i \comp
621: (f_1 \comp \tup{f}^{n-|S|-2},~
622: \ldots,~
623: f_n \comp \tup{f}^{n-|S|-2})).\zerotup $
624: \Conn{ distribute ${}\comp \tup{f}^{n-|S|-2}$ }
625: $ (f_i \comp
626: (f_1,~
627: \ldots,~
628: f_n) \comp \tup{f}^{n-|S|-2}).\zerotup $
629: \Conn{ exponentiation }
630: $ (f_i \comp \tup{f}^{n-|S|-1}).\zerotup $
631: }
632: \Case{i \not\in S \And |T| = n}
633: \Calc{
634: $ g_{S,i}.\zerotup $
635: \Conn{ see first 3 steps of previous case }
636: $ f_i.(g_{T,1}.\zerotup,~ \ldots,~ g_{T,n}.\zerotup) $
637: \Conn{ for each index $j$, $j \in T$, so $g_{T,j} = \zerofunc$ }
638: $ f_i.\zerotup $
639: \Conn{ $|S|=n-1$, so $f^{n-|S|-1}$ is the identity function }
640: $ (f_i \comp f^{n-|S|-1}).\zerotup $
641: \EndProof
642: }
643:
644: The following corollary of Lemma~\ref{lemma:1} proves one direction
645: of Theorem~\ref{main:theorem}.
646: \begin{corollary}\label{cor:1}
647: \[
648: \tup{g_{\emptyset}}.\zerotup \tupatmost \tup{f}^n.\zerotup
649: \]
650: \end{corollary}
651: \Proof{}
652: \Calc{
653: $ \tup{g_{\emptyset}}.\zerotup $
654: \Conn{}
655: $ (g_{\emptyset,1}.\zerotup,~ \ldots,~ g_{\emptyset,n}.\zerotup) $
656: \conn{\tupatmost}{ for each index $j$, Lemma~\ref{lemma:1}
657: with $i,S \Gets j,\emptyset$ }
658: $ ((f_1 \comp \tup{f}^{n-1}).\zerotup,~
659: \ldots,~
660: (f_n \comp \tup{f}^{n-1}).\zerotup) $
661: \Conn{ distribute $.\zerotup$ and ${}\comp \tup{f}^{n-1}$ }
662: $ ((f_1,~ \ldots,~ f_n) \comp \tup{f}^{n-1}).\zerotup $
663: \Conn{ exponentiation }
664: $ \tup{f}^n.\zerotup $
665: \EndProof
666: }
667:
668: To support the remaining lemmas, we define one more family of
669: functions. For any index $i$ and set $S$ of indices,
670: \[
671: h_{S,i} \Equal \left\{
672: \begin{array}{ll}
673: f_i
674: & \mbox{if $i \not\in S$} \\
675: \zerofunc
676: & \mbox{if $i \in S$}
677: \end{array}
678: \right.
679: \]
680:
681: \begin{lemma}\label{lemma:pre-2}
682: For any index $i$, monotonic function $H \colon \Bool^n \to \Bool^n$,
683: and $m \atleast 0$,
684: \[
685: (f_i \comp H^m).\zerotup \Equal 0
686: ~~\Imp~~
687: \Forall{p}{0 \atmost p \atmost m}{(f_i \comp H^p).\zerotup \Equal 0}
688: \]
689: \end{lemma}
690: \Proof{}
691: We prove the term of the quantification as follows:
692: \Calc{
693: $ (f_i \comp H^p).\zerotup $
694: \conn{\atmost}{ monotonicity of $f_i$ and $H$, since
695: $\zerotup \tupatmost H^{m-p}.\zerotup$ }
696: $ (f_i \comp H^p).(H^{m-p}.\zerotup) $
697: \Conn{}
698: $ (f_i \comp H^m).\zerotup $
699: \Conn{ antecedent }
700: $ 0 $
701: \EndProof
702: }
703:
704: \begin{lemma}\label{lemma:2}
705: For any index $i$, set $S$ of indices, $m \atleast 0$, and $T = S \cup
706: \{i\}$,
707: \[
708: (f_i \comp \tup{h_S}^m).\zerotup \Equal 0
709: ~~\Imp~~
710: \Forall{p}{0 \atmost p \atmost m}{
711: \tup{h_S}^p.\zerotup \Equal \tup{h_T}^p.\zerotup}
712: \]
713: \end{lemma}
714: \Proof{}
715: If $i \in S$, then $S=T$ and the consequent follows
716: trivially. For $i \not\in S$, we prove the term of the quantification
717: by induction on $p$.
718: \Case{p=0}
719: Trivial---exponentiation with 0 gives identity function.
720: \Case{p>0}
721: \Calc{
722: $ \tup{h_S}^p.\zerotup $
723: \Conn{ exponentiation, since $p>0$ }
724: $ \tup{h_S}.(\tup{h_S}^{p-1}.\zerotup) $
725: \Conn{ distribute $.(\tup{h_S}^{p-1}.\zerotup)$ }
726: $ (h_{S,1}.(\tup{h_S}^{p-1}.\zerotup),~
727: \ldots,~
728: h_{S,n}.(\tup{h_S}^{p-1}.\zerotup)) $
729: \Conn{ for any index $j$,
730: $h_{S,j}.(\tup{h_S}^{p-1}.\zerotup)
731: =
732: h_{T,j}.(\tup{h_S}^{p-1}.\zerotup)$, see below }
733: $ (h_{T,1}.(\tup{h_S}^{p-1}.\zerotup),~
734: \ldots,~
735: h_{T,n}.(\tup{h_S}^{p-1}.\zerotup)) $
736: \Conn{ distribute $.(\tup{h_S}^{p-1}.\zerotup)$ }
737: $ \tup{h_T}.(\tup{h_S}^{p-1}.\zerotup) $
738: \Conn{ induction hypothesis with $p \Gets p-1$ }
739: $ \tup{h_T}.(\tup{h_T}^{p-1}.\zerotup) $
740: \Conn{ exponentiation }
741: $ \tup{h_T}^p.\zerotup $
742: }
743: Now for the proof of the third step in the calculation above.
744: If $j \neq i$, then $j \in S \Equiv j \in T$, so $h_{S,j} = h_{T,j}$.
745: If $j=i$, then:
746: \Calc{
747: $ h_{S,i}.(\tup{h_S}^{p-1}.\zerotup) $
748: \Conn{ definition of $h$, since $i \not\in S$ }
749: $ f_i.(\tup{h_S}^{p-1}.\zerotup) $
750: \Conn{ Lemma~\ref{lemma:pre-2} with $H,p \Gets \tup{h_S},~p-1$,
751: using the antecedent of \nlhint Lemma~\ref{lemma:2} to fulfill the
752: antecedent of Lemma~\ref{lemma:pre-2} }
753: $ 0 $
754: \Conn{ definition of $\zerofunc$ }
755: $ \zerofunc.(\tup{h_S}^{p-1}.\zerotup) $
756: \Conn{ definition of $h$, since $i \in T$ }
757: $ h_{T,i}.(\tup{h_S}^{p-1}.\zerotup) $
758: \EndProof
759: }
760:
761: We need one more lemma.
762: \begin{lemma}\label{prop:3}
763: For any index $i$, set $S$ of indices, and $m$ satisfying $0 \atmost m
764: \atmost n-|S|$,
765: \begin{equation}\label{prop:3:formula}
766: (h_{S,i} \comp \tup{h_S}^m).\zerotup
767: ~~\atmost~~
768: g_{S,i}.\zerotup
769: \end{equation}
770: \end{lemma}
771: \Proof{}
772: By induction on $m$. We consider three cases.
773: \Case{i \in S}
774: \Calc{
775: $ h_{S,i} \comp \tup{h_S}^m $
776: \Conn{ definition of $h$, since $i \in S$ }
777: $ \zerofunc \comp \tup{h_S}^m $
778: \Conn{ $\zerofunc$ is left zero element of $\comp$ }
779: $ \zerofunc $
780: \Conn{ definition of $g$, since $i \in S$ }
781: $ g_{S,i} $
782: }
783: \Case{i \not\in S \And m=0}
784: \Calc{
785: $ (h_{S,i} \comp \tup{h_S}^m).\zerotup $
786: \Conn{ exponentiation, since $m=0$ }
787: $ h_{S,i}.\zerotup $
788: \Conn{ definition of $h$, since $i \not\in S$ }
789: $ f_i.\zerotup $
790: \conn{\atmost}{ monotonicity of $f_i$, since
791: $\zerotup \tupatmost \tup{g_T}.\zerotup$ }
792: $ f_i.(\tup{g_T}.\zerotup) $
793: \Conn{ definition of $g$, since $i \not\in S$ }
794: $ g_{S,i}.\zerotup $
795: }
796: \Case{i \not\in S \And m>0}
797: It suffices to prove that the left-hand side of (\ref{prop:3:formula})
798: is 0 whenever the right-hand side is 0. Therefore, we assume the
799: latter to be 0:
800: \begin{equation}\label{s:0}
801: g_{S,i}.\zerotup \Equal 0
802: \end{equation}
803: and prove the former to be 0:
804: \Calc{
805: $ (h_{S,i} \comp \tup{h_S}^m).\zerotup $
806: \Conn{ definition of $h$, since $i \not\in S$ }
807: $ (f_i \comp \tup{h_S}^m).\zerotup $
808: \Conn{ exponentiation, since $m>0$ }
809: $ (f_i \comp
810: (h_{S,1},~\ldots,~h_{S,n}) \comp
811: \tup{h_S}^{m-1}).\zerotup $
812: \Conn{ distribute ${}\comp \tup{h_S}^{m-1}$ and $.\zerotup$ }
813: $ f_i.((h_{S,1} \comp \tup{h_S}^{m-1}).\zerotup,~
814: \ldots,~
815: (h_{S,n} \comp \tup{h_S}^{m-1}).\zerotup) $
816: \conn{\atmost}{ (\ref{s:1}), see below; and monotonicity of $f_i$ }
817: $ f_i.(g_{T,1}.\zerotup,~ \ldots,~ g_{T,n}.\zerotup) $
818: \Conn{}
819: $ (f_i \comp \tup{g_T}).\zerotup $
820: \Conn{ definition of $g$, since $i \not\in S$ }
821: $ g_{S,i}.\zerotup $
822: \Conn{ assumption (\ref{s:0}) }
823: $ 0 $
824: }
825: In this calculation, we used the following fact:
826: for every index $j$,
827: \begin{equation}\label{s:1}
828: (h_{S,j} \comp \tup{h_S}^{m-1}).\zerotup
829: ~~\atmost~~
830: g_{T,j}.\zerotup
831: \end{equation}
832: which we now prove. We divide the proof of (\ref{s:1}) up into two
833: sub-cases.
834: \SubCase{(h_{S,j} \comp \tup{h_S}^{m-1}).\zerotup = 0}
835: Formula (\ref{s:1}) follows immediately.
836: \SubCase{(h_{S,j} \comp \tup{h_S}^{m-1}).\zerotup \neq 0}
837: First, we derive some consequences of assumption (\ref{s:0}):
838: \Calc{
839: $ g_{S,i}.\zerotup \Equal 0 $
840: \conn{\imp}{ induction hypothesis with $S,i,m \Gets S,i,m-1$ }
841: \calcEqLabel{s:2}
842: $ (h_{S,i} \comp \tup{h_S}^{m-1}).\zerotup \Equal 0 $
843: \Conn{ definition of $h$, since $i \not\in S$ }
844: $ (f_i \comp \tup{h_S}^{m-1}).\zerotup \Equal 0 $
845: \conn{\imp}{ Lemma~\ref{lemma:2} with $m,p \Gets m-1,m-1$ }
846: \calcEqLabel{s:3}
847: $ \tup{h_S}^{m-1}.\zerotup \Equal \tup{h_T}^{m-1}.\zerotup $
848: }
849: Now, calculating from the assumption we made in this sub-case:
850: \Calc{
851: $ (h_{S,j} \comp \tup{h_S}^{m-1}).\zerotup \neq 0 $
852: \Conn{ (\ref{s:2}) }
853: $ (h_{S,j} \comp \tup{h_S}^{m-1}).\zerotup \neq 0 \And i \neq j $
854:
855: \conn{\imp}{ $i \neq j$, so $j \in S \Equiv j \in T$, so
856: $h_{S,j} = h_{T,j}$ }
857: $ (h_{T,j} \comp \tup{h_S}^{m-1}).\zerotup \neq 0 $
858: \Conn{ (\ref{s:3}) }
859: $ (h_{T,j} \comp \tup{h_T}^{m-1}).\zerotup \neq 0$
860: \conn{\imp}{ induction hypothesis with $S,i,m \Gets T,j,m-1$ }
861: $ g_{T,j}.\zerotup \neq 0 $
862: \conn{\imp}{}
863: $ \mbox{(\ref{s:1})} $
864: }
865: This concludes the proof of Lemma~\ref{prop:3}.
866: \EndProof
867:
868: And finally, the proof of the theorem:
869: \ProofOf{Theorem~\ref{main:theorem}}
870: The proof is a ping-pong argument.
871: \Calc{
872: $ \tup{g_{\emptyset}}.\zerotup $
873: \conn{\tupatmost}{ Corollary~\ref{cor:1} }
874: \calcComment{\makebox[3cm]{---ping!}}
875: $ \tup{f}^n.\zerotup $
876: \Conn{ exponentiation, since $n \atleast 1$ }
877: $ ((f_1,~ \ldots,~ f_n) \comp \tup{f}^{n-1}).\zerotup $
878: \Conn{ distribute ${}\comp \tup{f}^{n-1}$ and $.\zerotup$ }
879: $ ((f_1 \comp \tup{f}^{n-1}).\zerotup,~
880: \ldots,~
881: (f_n \comp \tup{f}^{n-1}).\zerotup) $
882: \Conn{ by definition of $h$, $h_{\emptyset,i} = f_i$ for each index
883: $i$; and \nlhint thus also $\tup{h_{\emptyset}} = \tup{f}$ }
884: $ ((h_{\emptyset,1} \comp \tup{h_{\emptyset}}^{n-1}).\zerotup,~
885: \ldots,~
886: (h_{\emptyset,n} \comp \tup{h_{\emptyset}}^{n-1}).\zerotup) $
887: \conn{\tupatmost}{ Lemma~\ref{prop:3} with $S,i,m \Gets
888: \emptyset,i,n-1$ for each $i$ }
889: $ (g_{\emptyset,1}.\zerotup,~
890: \ldots,~
891: g_{\emptyset,n}.\zerotup) $
892: \Conn{ distribute $.\zerotup$ }
893: \calcComment{\makebox[3cm]{---pong!}}
894: $ \tup{g_{\emptyset}}.\zerotup $
895: \EndProof
896: }
897:
898: \Section{Related Work and Acknowledgments}
899:
900: Our theorem has already found a use, namely in the translation of
901: boolean programs into satisfiability formulas~\cite{Leino:SPIN2003}.
902:
903: Before we knew of the \BL{} Theorem, one of us (Kuncak) proved the
904: theorem as detailed in Section~\ref{sec:proof}. Tony Hoare then
905: proposed a way to prove the theorem in a way that would eliminate
906: recursive uses of variables, one by one. In doing this, Hoare also
907: proved what essentially amounts to the \BL{} Theorem, appealing only
908: to the Tarski Fixpoint Theorem~\cite{Tarski:theorem}. We elaborated
909: this format in Section~\ref{sec:bl}, to whose formulation Carroll
910: Morgan also contributed. We learnt about the \BL{} Theorem from
911: Patrick Cousot. The theorem is often called simply the Beki\'c
912: Theorem, but de~Bakker~\cite{deBakker:book} traces an independent
913: proof thereof to Leszczy{\l}owski. Finally, we are grateful for
914: feedback from the Eindhoven Tuesday Afternoon Club and the participants
915: of the IFIP WG 2.3 meeting in Biarritz, France (March 2003).
916:
917:
918: \bibliography{krml118}
919:
920: \end{document}
921: