1: \section{Supervaluational Semantics for First-Order Formulas}\label{Se:Supervaluation}
2:
3: In this section, we consider the problem of how to extract
4: information from a $3$-valued structure by evaluating a query.
5: A compositional semantics for $3$-valued first-order logic is defined
6: in \cite{TOPLAS:SRW02};
7: however, that semantics is not as precise as the one defined here.
8: The semantics given in this section can be seen as providing the limit
9: of obtainable precision.
10:
11: \para{The Notion of Supervaluational Semantics} %\label{Se:SpecificationSupervaluation}
12: defined below,
13: has been used in \cite{JPhil:vanFraassen66,CONCUR:BG00}.
14: %generalizes \cite{JPhil:vanFraassen66}.
15: %,LICS:RLS02}.
16:
17: \begin{definition}\label{De:Supervaluation}
18: \begin{Name}Supervaluational Semantics of First-Order Formulas\end{Name}
19: Let $X$ be a set of $3$-valued structures and $\varphi$ be a closed
20: formula.
21: The {\bf supervaluational semantics of $\varphi$ in $X$\/},
22: denoted by $\superval{\varphi}(X)$, is defined to be the join of
23: the values of $\varphi$ obtained from each of the $2$-valued structures
24: that $X$ represents, i.e., the most-precise conservative
25: value that can be reported for the value of formula $\varphi$ in
26: the $2$-valued structures represented by $X$ is
27: \begin{equation}
28: \label{Eq:SpecificationOfSupervaluational1}
29: \superval{\varphi}(X) =
30: \left\{\begin{array}{l@{\hspace{.4cm}}l}
31: 1 & \mbox{{\rm if\/}~} \C{S} \models \varphi~\mbox{{\rm for all\/}~} \C{S} \in \gamma(X) \\
32: 0 & \mbox{{\rm if\/}~} \C{S} \not\models \varphi~\mbox{{\rm for all\/}~} \C{S} \in \gamma(X) \\
33: 1/2 & \mbox{{\rm otherwise\/}~}
34: \end{array}\right.
35: \end{equation}
36: \end{definition}
37:
38: %Also notice that the embedding theorem
39: %implies that $\superval{\varphi}(S) \sqsubseteq
40: %\threeValue{\varphi}{S}{[]}$. It is possible to define
41: %supervaluational semantics for formulas with free variables.
42:
43: The compositional semantics given in~\cite{TOPLAS:SRW02} and used in TVLA
44: can yield $1/2$ for $\varphi$, even when the value of $\varphi$
45: %${\semp{\varphi}}_2^{\C{S}}$
46: is $1$ for all the $2$-valued structures $\C{S}$ that $S$ represents
47: (or when the value of $\varphi$
48: is $0$ for all the $\C{S}$).
49: In contrast, when the supervaluational semantics yields $1/2$,
50: we \emph{know} that any sound extraction of information from
51: $S$ must return $1/2$.
52:
53: \begin{example}\label{Ex:SupExample}
54: We demonstrate now that the supervaluational semantics of
55: the formula
56: $\varphi_{ {\tt x\rightarrow next \neq NULL} } \eqdef \exists v_1, v_2: x(v_1) \land n(v_1, v_2)$
57: on the structure $S$
58: from \figref{threeStruct}(d) is $1$.
59: That is, we wish to argue that for all of the $2$-valued structures that
60: structure $S$ from \figref{threeStruct}(d) represents,
61: the value of the formula
62: $\varphi_{ {\tt x\rightarrow next \neq NULL} }$
63: must be $1$.
64:
65: We reason as follows: $S$ represents
66: a list with at least two nodes;
67: i.e., all $2$-valued structures represented by $S$ have at least two nodes.
68: One node, $u^\natural_1$, corresponding to $u_1$ in $S$,
69: is pointed to by program variable {\tt x}.
70: The other node, corresponding to the summary node $u_2$, must be
71: reachable from \tx. Consider the sequence of nodes reachable from \tx,
72: starting with $u^\natural_1$.
73: Denote the first node in the sequence that embeds into $u_2$
74: by $u^\natural_2$. By the definition of reachability,
75: there must be an \tn-link to $u^\natural_2$ from a node embedded into $u_1$.
76: But the integrity rules guarantee that there is exactly one node
77: that embeds into $u_1$, namely, $u^\natural_1$.
78: Therefore, the formula $x(v_1) \land n(v_1, v_2)$
79: holds for $[v_1 \mapsto u^\natural_1, v_2 \mapsto u^\natural_2]$.
80:
81: Note that this formula will be evaluated to $1/2$ by TVLA,
82: because $x(v_1) \land n(v_1, v_2)$ evaluates to $1/2$ under the assignment
83: $[v_1 \mapsto u_1, v_2 \mapsto u_2]$:
84: the compositional semantics yields
85: $x(u_1) \land n(u_1, u_2) = 1 \land 1/2 = 1/2$.
86: \end{example}
87:
88: Notice that \defref{Supervaluation} does not provide a constructive
89: way to compute $\superval{\varphi}(X)$ because $\gamma(X)$ is
90: usually an infinite set.
91:
92: \para{Computing Supervaluational Semantics using Theorem Provers.} %\label{Se:ImplementationSupervaluation}
93: If an appropriate theorem prover is at hand,
94: $\superval{\varphi}(S)$ can be computed with
95: the procedure shown in \figref{ImplementationOfSupervaluational}.
96: This procedure is not an algorithm, because the theorem prover might not terminate.
97: Termination can be assured by using standard techniques (e.g., having the theorem prover return a
98: safe answer if a time-out threshold is exceeded) at the cost of losing
99: the ability to guarantee that a most-precise result is obtained.
100: If the queries posed by operation {\tt Supervaluation} can be expressed in
101: a decidable logic, the algorithm for computing supervaluation can be implemented
102: using a decision procedure for that logic.
103: In \secref{Applications}, we discuss such decidable logics that are useful for shape analysis.
104: \begin{figure}
105: \begin{center}
106: \framebox{
107: \begin{minipage}{1in}
108: \begin{alltt}
109: \begin{tabbing}
110: proc\=edure Supervaluation(\=$\varphi$: Formula,\+\+\\
111: X: Set of $3$-valued structures): Value\-\\
112: if ($\gammaHat(X) \implies \varphi$ is valid) return $1$;\\
113: else if ($\gammaHat(X) \implies \neg \varphi$ is valid) return $0$;\\
114: otherwise return $1/2$;
115: \end{tabbing}
116: \end{alltt}
117: \end{minipage}
118: }
119: \end{center}
120: \caption{\label{Fi:ImplementationOfSupervaluational}A procedure for computing
121: the supervaluational value of a formula $\varphi$ that
122: encodes a query on a $3$-valued structures $S$.
123: }
124: \end{figure}
125: %\begin{equation}
126: % \label{eq:ImplementationOfSupervaluational}
127: % \superval{\varphi}(S) =
128: % \left\{\begin{array}{l@{\hspace{.4cm}}l}
129: % 1 & \mbox{{\rm if\/}~} \gammaHat(S) \implies \varphi~\mbox{{\rm is valid}} \\
130: % 0 & \mbox{{\rm if\/}~} \gammaHat(S) \implies \neg\varphi~\mbox{{\rm is valid}} \\
131: % 1/2 & \mbox{{\rm otherwise\/}~}
132: % \end{array}\right.
133: %\end{equation}
134: