Differences
This shows you the differences between two versions of the page.
| Next revision Both sides next revision | |||
|
complexity [2007/10/04 19:56] philippe.suter created |
complexity [2007/10/04 22:06] philippe.suter |
||
|---|---|---|---|
| Line 21: | Line 21: | ||
| The proof is straightforward, but still requires that the dimensions match, otherwise the intersection could be empty for this other reason. | The proof is straightforward, but still requires that the dimensions match, otherwise the intersection could be empty for this other reason. | ||
| + | |||
| + | ==== Translation of the assumptions/axioms ==== | ||
| + | |||
| + | We will always use unary relations to represent sets (and therefore set membership): $x \in A$ will be translated to $A(x)$, and $x \notin A$ to $\neg A(x)$. | ||
| + | |||
| + | For each statement which we want to prove or disprove, we make use of the user-provided informations about properties on the class hierarchy and the extractors. | ||
| + | |||
| + | These properties are always in one of the following forms: | ||
| + | |||
| + | * Set of extractors covering a given type: $E_1 \cup \ldots \cup E_n \supseteq T$ | ||
| + | * Sealed and abstract classes: $T = S_1 \cup \ldots \cup S_n$ | ||
| + | * Disjointness of extractors: $E \cap F = \emptyset$ | ||
| + | |||
| + | This translates to: | ||
| + | |||
| + | * $\forall x . E_1(x) \vee \ldots \vee E_n(x) \Rightarrow T(x)$ | ||
| + | * $\forall x . S_1(x) \vee \ldots \vee S_n(x) \Leftrightarrow T(x)$ | ||
| + | * and $\forall x . \neg (E(x) \wedge F(x))$ respectively. | ||
| ==== Verifying disjunction ==== | ==== Verifying disjunction ==== | ||
| Line 28: | Line 46: | ||
| - ...or they have the same signature, in which case we simply verify that the conjunction of their guards is //false//. | - ...or they have the same signature, in which case we simply verify that the conjunction of their guards is //false//. | ||
| - | Since we limit our boolean expressions to QFBAPA (FIXME do we?) | ||
| + | |||
| + | Since we limit our boolean expressions to QFBAPA (FIXME do we?), the formula for verifying the disjointness of two guards $g_1$ and $g_2$, namely $\neg(g_1 \wedge g_2)$ is itself in QFBAPA and its satisfiability can hence be checked with an algorithm in NP [1]. This solves the second case. | ||
| + | |||
| + | The first case is not much harder. We can use the abovementioned equivalence for the intersection of cartesian products of same dimensions, and we need only one quantifier to transform it to the desired form: | ||
| + | |||
| + | * $(A_1 \times A_2 \times \ldots \times A_n) \cap (B_1 \times B_2 \times \ldots \times B_n) = \emptyset$ | ||
| + | ...is translated to: | ||
| + | * $\forall x . \neg(A_1(x) \wedge B_1(x)) \vee \ldots \vee \neg(A_n(x) \wedge B_n(x))$ | ||
| + | |||
| + | Note that checking the satifiability should be doable in polynomial time, as all needs to be done is find one pair of sets among a finite list which are disjoint (and this information can only come from the assumptions/axioms, which are themselves in a finite number. (FIXME : I know this doesn't sound convincing.. let's do better). | ||
| + | |||
| + | |||
| + | |||
| + | [1] Quantifier Free Boolean Algebra with Presburger Arithmetic is NP-Complete, technical report somewhere IIRC. | ||