1: \section{Characterizing $3$-Valued Structures by First-Order Formulas}
2: \label{Se:Classic}
3:
4: This section presents our results on characterizing $3$-valued structures
5: using first-order formulas.
6: Given a $3$-valued structure $S$, the question that we
7: wish to answer is whether it is possible to
8: give a formula $\gammaHat(S)$ that
9: accepts exactly
10: the set of $2$-valued structures that $S$ represents, i.e.,
11: $\C{S} \models \gammaHat(S)$ iff $\C{S} \in \gamma(S)$.
12:
13: This question has different answers depending on what assumptions are made.
14: The task of generating a characteristic formula for a $3$-valued structure $S$ is challenging
15: because we have to find a formula
16: that identifies when embedding is possible,
17: i.e., that is satisfied by exactly those $2$-valued structures that embed into $S$.
18: It is not always possible to characterize
19: an \emph{arbitrary} $3$-valued structure by a first-order formula,
20: i.e.,
21: there exists a $3$-valued structure $S$ for which there is no
22: first-order formula with transitive closure that accepts exactly the set of
23: $2$-valued structures $\gamma$(S).
24:
25: For example, consider the $3$-valued structure $S$ shown in \figref{Color}.
26: The absence of a self loop on any of the three summary nodes
27: implies that a $2$-valued structure can be embedded into this
28: structure if and only if it can be colored using $3$
29: colors (\lemref{embedding3color} in the appendix).
30: It is well-known that there exists no first-order formula,
31: even with transitive closure, that
32: expresses
33: $3$-colorability of undirected graphs,
34: unless $P = NP$ (e.g., see~\cite{Book:Immerman98,InCollection:Courcelle96}).\footnote{In fact,
35: the condition is even stronger. First-order
36: logic with transitive closure
37: can only express non-deterministic logspace (NL) computations,
38: thus, the NP-complete problem of $3$-colorability is not expressible in first-order logic,
39: unless $NL = NP$.
40: It is shown in~\cite{Book:Immerman98} using an ordering relation on the nodes.
41: In our context, without the ordering, the logic is less expressive.
42: Thus, the condition under which 3-colorability is expressible is even stronger than $NL = NP$.
43: We believe that there is an example of a $3$-valued structure that is not expressible in
44: the logic, independently of the question whether $P=NP$.
45: However, it is not the main focus of the current paper.}
46: Therefore, there is no first-order formula that accepts exactly the set $\gamma(S)$.
47: %???
48: %\footnote{Another example
49: %of a $3$-valued structure that cannot be characterized by a first-order formula with transitive closure
50: %can be derived by considering lists of even length and applying~cite{ChandraHarel82}.???}
51:
52: \begin{figure}
53: \begin{center}
54: \framebox{
55: \vbox{\xymatrix{
56: \xySummaryNode{u_1}\ar@{<.>}[r] & \xySummaryNode{u_2}\\
57: \xySummaryNode{u_3}\ar@{<.>}[u] \ar@{<.>}[ur] }}}
58: \end{center}
59: \caption{\label{Fi:Color}A $3$-valued structure that
60: represents $3$-colorable undirected graphs.
61: A $2$-valued structure can be embedded into this
62: structure if and only if it can be colored using $3$
63: colors.
64: }
65: \end{figure}
66:
67: \subsection{FO-Identifiable Structures}\label{Se:FOIdentStruct}
68:
69: Intuitively, the difficulty in characterizing $3$-valued structures
70: is how to uniquely identify the
71: correspondence between concrete and abstract nodes using a first-order formula.
72: Fortunately, as we will see,
73: for the subclass of $3$-valued structures used in shape analysis
74: (also known as ``bounded structures''), the correspondence
75: can be easily defined using
76: first-order
77: %propositional
78: formulas.
79: The bounded structures are a subclass of the $3$-valued structures
80: in which it is possible to identify uniquely each node using a first-order formula.
81: %To avoid structures like the one shown in \figref{Color},
82: %We now formalize the notion of FO-identifiability,
83: %which generalizes condition for a
84: %subclass of $3$-valued structures, in which it is possible to
85: %uniquely identify each node using a formula.
86: \begin{definition}\label{De:UniqueFONames}
87: A $3$-valued structure $S$ is called {\bf FO-identifiable\/} if for every
88: node $u \in U^S$ there exists a first-order formula $\nodeFormula{S}{u}(w)$ with designated free variable $w$
89: such that
90: for every $2$-valued structure $\C{S}$ that embeds into $S$ using a function $f$,
91: for every concrete node $\C{u} \in U^{\C{S}}$ and for every node $u_i \in U^S$:
92: \begin{equation}
93: f(\C{u})= u_i
94: \iff
95: \C{S},[w \mapsto \C{u}] \models \nodeFormula{S}{u_i}(w)
96: \end{equation}
97: %$S$ is called FO-identifiable if all the nodes in $S$ are FO-identifiable.
98: %We say that a node $u$ in a $3$-valued structure $S$ is
99: %{\bf FO-identifiable\/} if there exists a first-order formula
100: %$\nodeFormula{S}{u}(w)$ with designated free variable $w$ such that for every
101: %$2$-valued structure $\C{S}$ that embeds into
102: %$S$ using a function $f$, and for every concrete node $\C{u} \in U^{\C{S}}$:
103: %\begin{equation}
104: %f(\C{u})= u
105: %\iff
106: %\C{S},[w \mapsto \C{u}] \models \nodeFormula{S}{u}(w)
107: %\end{equation}
108: %$S$ is called FO-identifiable if all the nodes in $S$ are FO-identifiable.
109: \end{definition}
110: The idea behind this definition is to have a formula that uniquely
111: identifies each node $u$ of the 3-valued structure $S$.
112: This will be used to identify the set of nodes of a $2$-valued
113: structure that are mapped to $u$ by embedding.
114: In other words, a concrete node $\C{u}$ satisfies the $node$ formula of
115: at most one abstract node, as formalized by the lemma:
116: \begin{lemma}\label{Lem:unique}
117: Let $S$ be an FO-identifiable structure, and let $u_1, u_2 \in S$ be distinct nodes.
118: Let $\C{S}$ be a 2-valued structure that embeds into $S$ and let $\C{u} \in \C{S}$.
119: At most one of the following hold:
120: \begin{enumerate}
121: \item $\C{S},[w \mapsto \C{u}] \models \nodeFormula{S}{u_1}(w)$
122: \item $\C{S},[w \mapsto \C{u}] \models \nodeFormula{S}{u_2}(w)$
123: \end{enumerate}
124: \end{lemma}
125: \begin{Remark}
126: \defref{UniqueFONames} can be generalized to handle arbitrary $2$-valued
127: structures, by also allowing extra designated free variables
128: for every concrete node and using equality to check
129: if the concrete node is equal to the designated variable:
130: $\nodeFormula{S}{u_i}(w, v_1, \ldots, v_n) \eqdef w = v_i$.
131: However, the equality formula cannot be used to identify
132: nodes in a $3$-valued structure because equality evaluates to $1/2$
133: on summary nodes.
134: \end{Remark}
135:
136: We now introduce a standard concept for turning valuations into
137: formulas.
138: \begin{definition}\label{De:pb}
139: For a predicate $p$ of arity $k$ and truth value $B \in
140: \{0, 1, 1/2\}$, we define the formula $p^B(v_1, v_2, \ldots, v_k)$
141: to be the {\bf characteristic formula of $B$ for $p$\/}, by
142: \[
143: \begin{array}{lcl}
144: p^0(v_1, v_2, \ldots, v_k) & \eqdef & \neg p(v_1, v_2, \ldots, v_k)\\
145: p^1(v_1, v_2, \ldots, v_k) & \eqdef & p(v_1, v_2, \ldots, v_k) \\
146: p^{1/2}(v_1, v_2, \ldots, v_k) & \eqdef & 1\\
147: \end{array}
148: \]
149: \end{definition}
150:
151: The main idea in the above definition is that,
152: for $B \in \{0,1\}$, $p^B$ holds when the value of $p$ is $B$, and
153: for $B = 1/2$ the value of $p$ is unrestricted.
154: \TrOnly{
155: This is formalized by the following lemma:
156: \begin{lemma}\label{Lem:Trivial}
157: For every $2$-valued structure $\C{S}$ and assignment $Z$
158: \[
159: \C{S}, Z \models p^B(v_1, \ldots, v_k) ~\mbox{iff}~
160: \iota^{\C{S}}(p)(Z(v_1), \ldots, Z(v_k)) \sqsubseteq B
161: \]
162: \end{lemma}
163: }
164:
165: \defref{UniqueFONames} is not a constructive definition, because the
166: premises range over arbitrary $2$-valued structures and
167: arbitrary embedding functions.
168: For this reason, we now introduce a testable condition that implies FO-identifiability.
169:
170: \para{Bounded Structures.}
171: The following subclass of $3$-values structures was defined in
172: \cite{kn:SRW99};\footnote{
173: This definition of bounded structures was given in
174: \cite{kn:SRW99}; it is slightly more restrictive than the one given
175: in~\cite{TOPLAS:SRW02,Thesis:LevAmi00}, which did not impose requirement \ref{De:BoundedStructures}(ii).
176: However, it does not limit the set of problems
177: handled by our method, if the structure that is bounded in the weak sense is also FO-identifiable.} the
178: motivation there was to guarantee that shape analysis was carried
179: out with respect to a finite set of abstract structures,
180: and hence that the analysis would always terminate.
181: \begin{definition}\label{De:BoundedStructures}
182: A {\bf bounded structure\/} over vocabulary $\Voc$ is a structure
183: $S = \B{U^S, \iota^S}$ such that for every $u_1, u_2 \in U^S$,
184: where $u_1 \neq u_2$, there exists a predicate symbol
185: $p \in \Voc_1$ such that (i)~$\iota^S(p)(u_1) \neq
186: \iota^S(p)(u_2)$ and (ii)~both $\iota^S(p)(u_1)$ and
187: $\iota^S(p)(u_2)$ are not $1/2$.
188: %In the sequel,
189: %$\BSTRUCT{\Voc}$ denotes the set of such structures.
190: \end{definition}
191: Intuitively, for each pair of nodes in a bounded structure,
192: there is at least one predicate that has different definite values for these nodes.
193: Thus, there is a finite number of different bounded structures (up to isomorphism).
194: %\begin{Remark}\label{lessBoundedRmark}
195: %This definition of bounded structures was given in
196: %\cite{kn:SRW99}; it is slightly more restrictive than the one given
197: %in~\cite{TOPLAS:SRW02,Thesis:LevAmi00}, which did not impose requirement \ref{De:BoundedStructures}(ii).
198: %However, it does not limit the set of problems
199: %handled by our method.
200: %Let $S$ be a $3$-valued structure that only
201: %satisfies the first requirement.
202: %It is possible to construct from
203: %$S$ a finite set of bounded structures $X$ such that
204: %$\gamma(X) = \gamma(S)$, using new unary predicates.
205: %This is based on the idea that
206: %a structure with an indefinite unary predicate value on a
207: %particular node $u$, can be represented by two (or
208: %three\footnote{when $u$ is a summary node we need to create an
209: %additional structure with two occurrences of $u$, for $0$ and $1$
210: %values for the predicate.}) structures with $0$ and $1$ values on
211: %$u$, respectively.
212:
213:
214: The following lemma shows that bounded structures are FO-identifiable
215: %using propositional formulas:
216: using formulas over unary predicates only (denoted by $\Voc_1$):
217: \begin{lemma}\label{Lem:Bounded}
218: Every bounded $3$-valued structure $S$ is FO-identifiable , where
219: \begin{equation}
220: \nodeFormula{S}{u_i}(w) \eqdef \Land_{p \in \Voc_1} %AbstractionPredicates}
221: p^{\iota^{S}(p)(u_i)}(w)
222: \label{eq:individualFormula}
223: \end{equation}
224: \end{lemma}
225:
226: \begin{example}\label{Ex:foRecognizable}
227: The first-order $node$ formulas for the structure $S$ shown in
228: \figref{threeStruct}, are:
229: \begin{eqnarray*}
230: \nodeFormula{S}{u_1}(w) = &
231: x(w) \land r_x(w) \land \neg y(w) \land \neg t(w) \land \neg e(w) \\
232: & \land \neg r_y(w) \land \neg r_t(w) \land \neg r_e(w) \land \neg is(w) \\
233: \nodeFormula{S}{u_2}(w) = &
234: \neg x(w) \land r_x(w) \land \neg y(w) \land \neg t(w) \land \neg e(w) \\
235: & \land \neg r_y(w) \land \neg r_t(w) \land \neg r_e(w) \land \neg is(w)
236: %\nodeFormula{S}{u_1}(w) & = &
237: %\neg is(w) \land x(w) \land \Land_{q \in \PVar-\{x\}} \neg q(w) \nonumber\\
238: %&& \land r_x(w) \land \Land_{q \in \PVar-\{x\}} \neg r_q(w) \\
239: %%%
240: %\nodeFormula{S}{u_2}(w) & = &
241: %\neg is(w) \land \Land_{q \in \PVar} \neg q(w) \nonumber\\
242: %&& \land r_x(w) \land \Land_{q \in \PVar-\{x\}} \neg r_q(w)
243: %%%
244: \end{eqnarray*}
245: \end{example}
246:
247: \begin{Remark}
248: In the case that $S$ is a bounded $2$-valued structure,
249: the definition of a bounded structure becomes trivial.
250: The reason is that every node in $S$ can be named by
251: a quantifier-free formula built from unary predicates.
252: This is essentially the same as saying that every node can be named by a constant.
253: If structure $S'$ embeds into $S$, then $S'$ must be isomorphic to $S$,
254: therefore it is possible to name all nodes of $S'$ by the same constants.
255: However, this restricted case is not of particular interest for us,
256: because, to guarantee termination, shape analysis operates on structures
257: that contain summary nodes and indefinite values.
258: In the case that $S$ contains a summary node, a structure $S'$ that embeds into $S$ may
259: have an unbounded number of nodes;
260: hence the nodes of $S'$ cannot be named by a finite set of constants in the language.
261: \end{Remark}
262:
263: We already know of interesting cases of FO-identifiable structures that are not bounded,
264: which can be used to generalize the abstraction defined in \cite{kn:SRW99}:
265:
266: \begin{example}\label{Ex:FOIdentNotBounded}
267: The $3$-valued structure $S'$ in \figref{FOIdentNotBounded}
268: is FO-identifiable by:
269: \[
270: \begin{array}{ll}
271: \nodeFormula{S'}{u_1}(w) \eqdef &
272: x(w) \land r_x(w) \land \neg y(w) \land \neg t(w) \land \neg e(w) \\
273: & \land \neg r_y(w) \land \neg r_t(w) \land \neg r_e(w) \land \neg is(w) \\
274:
275: \nodeFormula{S'}{u_2}(w) \eqdef &
276: \underline{\exists w_1 : x(w_1) \land n(w_1, w)} \land \neg x(w) \land r_x(w) \land \neg y(w) \land \neg t(w) \land \neg e(w) \\
277: & \land \neg r_y(w) \land \neg r_t(w) \land \neg r_e(w) \land \neg is(w) \\
278:
279: \nodeFormula{S'}{u_3}(w) \eqdef &
280: \neg(\exists w_1 : x(w_1) \land n(w_1, w)) \land
281: \neg x(w) \land r_x(w) \land \neg y(w) \land \neg t(w) \land \neg e(w) \\
282: & \land \neg r_y(w) \land \neg r_t(w) \land \neg r_e(w) \land \neg is(w)
283: \end{array}
284: \]
285: However, $S'$ is not a bounded structure because nodes $u_2$ and $u_3$ have the same values of
286: unary predicates. To distinguish between these nodes, we extended $\nodeFormula{S'}{u_2}(w)$
287: with the underlined subformula, which captures the fact that only $u_2$ is directly pointed to by an $n$-edge
288: from $u_1$.
289: %\footnote{
290: %\begin{changebar}
291: %In general, every FO-identifiable structure can be transformed into a bounded structure by
292: %adding a new instrumentation predicate for each $node$ formula.
293: %\end{changebar}
294: %}
295: \begin{figure}
296: \begin{center}
297: %\framebox{
298: \begin{tabular}{|@{\hspace{1ex}}c@{\hspace{1ex}}|}
299: \hline
300: \xymatrix@R9pt@C12pt{
301: %\xyEdge &
302: &
303: \xyNonSummaryNode{u_1}
304: %\xyDottedLabeledEdge{n}
305: \ar[r]^{n}
306: &
307: \xyNonSummaryNode{u_2}
308: %\xyDottedLabeledEdge{n}
309: \ar@{.>}[r]^{n}
310: &
311: \xySummaryNode{u_3} \ar@{.>}@(ur, ul)[]|{n} \\
312: & \tx, r_{x}\ar[u] &
313: r_{x}\ar[u] &
314: r_{x}\ar[u]
315: }\\
316: (S')\\
317: \hline
318: \end{tabular}
319: \end{center}
320: \caption{\label{Fi:FOIdentNotBounded}
321: A $3$-valued structure $S'$ is FO-identifiable, but not bounded.
322: }
323: \end{figure}
324: \end{example}
325: It can be shown that every FO-identifiable structure can be converted into a
326: bounded structure by introducing more instrumentation predicates.
327: For methodological reasons, we use the notion of FO-identifiable which directly capture
328: the ability to uniquely identify embedding via (FO) formulas.\footnote{In subsequent sections,
329: we redefine this notion to capture other classes of structures.}
330: One of the interesting features of FO-identifiable structures
331: is that the structures generated by a common TVLA operation ``focus'',
332: defined in \cite{Thesis:LevAmi00}, are all FO-identifiable (see \lemref{focusFOIdent} in \appref{Proofs}).
333: For example, \figref{FOIdentNotBounded}
334: shows the structure $S'$, which is
335: one of the structures resulting from applying the``focus'' operation
336: to the structure $S$ from \figref{threeStruct}(d)
337: with the formula $\exists v_1, v_2 : x(v_1) \land n(v_1, v_2)$.
338: $S'$ is FO-identifiable, but not bounded.
339: However, structures like the one shown in \figref{Color}
340: are not FO-identifiable unless $P = NP$.
341: %even if $P=NP$.
342: %- methodological: it simplifies the explanation and gives insight
343: %to when the abstraction can be characterized by FO+TC.
344: %- practical: the analysis is exponential in the number of predicates,
345: %thus, we prefer to work with "local" node predicates, defined for each structure,
346: %instead of defining the m as instrumentation predicates throughout the analysis.
347:
348: \subsection{Characterizing FO-identifiable structures}\label{Se:FOFormula}
349:
350: To characterize an FO-identifiable $3$-valued structure,
351: we must ensure
352: \begin{enumerate}
353: \item the existence of a surjective embedding function.
354: \item that every concrete node is represented by some abstract node.
355: \item that corresponding concrete and abstract predicate values meet the embedding condition
356: of \equref{EmbeddingCondition}.
357: \end{enumerate}
358:
359: \begin{definition}\label{De:Characteristic}
360: \begin{Name}First-order Characteristic Formula\end{Name}
361: Let $S=\B{U=\{u_1, u_2, \ldots, u_n\}, \iota}$ be an FO-identifiable $3$-valued
362: structure.
363:
364: We define the {\bf totality characteristic formula\/} to be the
365: closed formula:
366: \begin{equation}
367: \characteristicFormula{S}_{total} \eqdef \forall w:
368: \Lor_{i=1}^n
369: \nodeFormula{S}{u_i}(w)
370: \label{eq:ontoFormula}
371: \end{equation}
372:
373: We define the {\bf nullary characteristic formula\/} to be the
374: closed formula:
375: \begin{equation}
376: \characteristicFormula{S}_{nullary} \eqdef \Land_{p \in \Voc_0}
377: p^{\iota^{S}(p)()} \label{eq:nullaryFormula}
378: \end{equation}
379:
380: For a predicate $p$ of arity $r \geq 1$, we define the {\bf
381: predicate characteristic formula\/} to be the closed formula:
382: \begin{eqnarray}
383: \lefteqn{\characteristicFormula{S}[p] \eqdef \forall w_1, \ldots,
384: w_r: \Land_{\{u'_{1}, \ldots, u'_{r}\} \in U}} \nonumber\\
385: & \Land_{j=1}^r \nodeFormula{S}{u'_j}(w_j) \implies
386: p^{\iota^S(p)(u'_{1}, \ldots, u'_{r})}(w_1, \ldots, w_r)
387: \label{eq:naryFormula}
388: \end{eqnarray}
389:
390: %Let $l$ be the largest arity of a predicate in $\Voc$.
391: The {\bf characteristic formula of $S$\/} is defined by:
392: \begin{equation}\label{eq:characteristicFormula}
393: \begin{array}{lll}
394: \characteristicFormula{S} & \eqdef &
395: \Land_{i=1}^n (\exists v: \nodeFormula{S}{u_i}(v)) \\
396: %(\exists v_1, \ldots, v_n: \Land_{i=1}^n \nodeFormula{S}{u_i}(v_i)
397: % \land \Land_{k \neq j} \neg eq(v_k, v_j) ) \\
398: % \left ( \begin{array}{l} \exists v_1, \ldots, v_n:\\
399: % \Land_{i=1}^n \nodeFormula{S}{u_i}(v_i)
400: % \land \Land_{k \neq j} \neg eq(v_k, v_j) \end{array} \right ) \\
401:
402: &\land & \characteristicFormula{S}_{total}\\
403: &\land & \characteristicFormula{S}_{nullary}\\
404: &\land & \Land_{r=1}^{maxR} \Land_{p \in \Voc_r}
405: \characteristicFormula{S}[p]
406: \end{array}
407: \end{equation}
408:
409: The {\bf characteristic formula of set $X \subseteq \STRUCT{\Voc}$\/}
410: is defined by:
411: \begin{equation}\label{eq:gammaHatSet}
412: \widehat{\gamma}(X) = F \land (\Lor_{S \in X} \characteristicFormula{S})
413: \end{equation}
414:
415: Finally, for a singleton set $X = \{S\}$ we write $\widehat{\gamma}(S)$ instead of $\widehat{\gamma}(X)$.
416:
417: \end{definition}
418:
419: The main ideas behind the four conjuncts of \equref{characteristicFormula} are:
420: \begin{itemize}
421: \item
422: The existential quantification in the first conjunct
423: requires that the $2$-valued structures
424: have at least $n$ distinct nodes.
425: For each abstract node in $S$, the first sub-formula locates
426: the corresponding concrete node.
427: Overall, this conjunct guarantees that
428: embedding is surjective.
429: % For each concrete individual, the first sub-formula locates
430: % the corresponding individual in $S$.
431: % Moreover, the first formula requires that these
432: % individuals are represented by the corresponding individuals in
433: % $S$ and are different.
434: \item
435: The totality formula ensures that every concrete node is
436: represented by some abstract node.
437: It guarantees that the embedding function is well-defined.
438: \item
439: The nullary characteristic formula ensures that the values of nullary
440: predicates in the $2$-valued structures are at least as precise as
441: the values of the corresponding nullary predicates in $S$.
442: \item
443: The predicate characteristic formulas guarantee that predicate
444: values in the $2$-valued structures obey the requirements imposed by
445: an embedding into $S$.\footnote{\defref{Characteristic} relates to all FO-identifiable structures,
446: not only to bounded structures. For bounded structures, it can be simplified by omitting
447: $\characteristicFormula{S}[p]$ for all unary predicates $p$, because it is implied
448: by $\characteristicFormula{S}_{total}$. In fact, it can be omitted only for the abstraction predicates, as defined
449: in \cite{TOPLAS:SRW02}; however throughout this paper we consider all unary predicates to be abstraction predicates.}
450: \end{itemize}
451:
452: \begin{example}\label{Ex:charFormula}
453: After a small amount of simplification, the characteristic formula $\widehat{\gamma}(S)$
454: for the structure $S$ shown in \figref{threeStruct}
455: is $F_{List} \land \characteristicFormula{S}$, where
456: $\characteristicFormula{S}$ is:
457: \[
458: \begin{array}{@{\hspace{0ex}}r@{\hspace{1.0ex}}l@{\hspace{0ex}}}
459: & \exists v: \nodeFormula{S}{u_1}(v) \land \exists v: \nodeFormula{S}{u_2}(v)\\
460: \land & \forall w: \nodeFormula{S}{u_1}(w) \lor \nodeFormula{S}{u_2}(w)\\
461: \land & \Land_{p \in \Voc_1} \forall w_1:\Land_{i=1,2}
462: (\nodeFormula{S}{u_i}(w_1)
463: \implies p^{\iota^S(p)(u_i)}(w_1))\\
464: \land & \begin{array}[t]{@{\hspace{0ex}}r@{\hspace{1.0ex}}l@{\hspace{0ex}}}
465: \forall w_1, w_2: & (\nodeFormula{S}{u_1}(w_1) \land \nodeFormula{S}{u_1}(w_2)\implies %\\
466: eq(w_1, w_2) \land \neg n(w_1, w_2) \land \neg n(w_2, w_1)) \\
467: \land & (\nodeFormula{S}{u_1}(w_1) \land \nodeFormula{S}{u_2}(w_2)\implies %\\
468: \neg eq(w_1, w_2) \land \neg n(w_2, w_1))
469: \end{array}
470: \end{array}
471: \]
472: The $node$ formulas are given in \exref{foRecognizable}, and the
473: predicates for the {\tt insert} program in \figref{Insert}(b) are
474: shown in \tableref{Predicates}.
475: Above, we simplified the formula from \equref{characteristicFormula} by combining
476: implications that had the same premises.
477: The integrity formula $F_{List}$ is given in \exref{IntegrityExample}.
478: Note that it uses transitive closure to define the reachability predicates;
479: consequently, $\widehat{\gamma}(S)$ is a formula in first-order logic with transitive closure.
480: \end{example}
481:
482: When a predicate has an indefinite value on some node tuple,
483: a corresponding conjunct of \equref{naryFormula} can be omitted, because it simplifies to $\TRUE$.
484:
485: Thus, the size of this simplified version of $\characteristicFormula{S}$ is
486: linear in the number of definite values of predicates in $S$.
487: Assuming that the $node^S$ formulas contain no quantifiers or transitive-closure operator,
488: e.g., when $S$ is bounded,
489: the $\characteristicFormula{S}$ formula has no quantifier alternation, and does not contain
490: any occurrences of the transitive-closure operator.
491: Thus, the formula $\widehat{\gamma}$ is in Existential-Universal normal form
492: (and thus decidable for satisfiability) whenever $F$ is in Existential-Universal normal form
493: and does not contain transitive closure.\footnote{
494: For practical reasons, we often replace the $node$ formula by a new (definable) predicate,
495: and add its definition to the integrity formula.
496: %Similarly, we can show that \defref{UniqueFONames}
497: %does not allow transitive-closure operator in $node$ formula,
498: }
499: Moreover, if the maximal arity of the predicate in $\Voc$ is $2$,
500: then $\gammaHat$ is in the two-variable fragment of first-order logic~\cite{Mortimer75}, wherever
501: $F$ is.
502: In \secref{Applications}, we discuss other conditions under which $\gammaHat$ can be expressed in a
503: decidable logic.
504:
505: The following theorem shows that for every FO-identifiable structure $S$,
506: the formula $\widehat{\gamma}(S)$
507: accepts exactly the set of $2$-valued structures represented by $S$.
508: \begin{theorem}\label{The:RepresentingStructuresByFormulae}
509: For every FO-identifiable $3$-valued structure $S$,
510: and $2$-valued structure $\C{S}$,
511: $\C{S} \in \gamma(S)~ \mbox{iff}~\C{S} \models
512: \widehat{\gamma}(S)$.
513: \end{theorem}
514: