From dec5d77063d8235b49d57e759b4ba6553943cba5 Mon Sep 17 00:00:00 2001
From: konstin <konstin@mailbox.org>
Date: Fri, 8 Dec 2023 14:11:43 +0100
Subject: [PATCH] Make terms clearer using boolean expressions
I tried to make it clear that a CDNL terms is a conjunction of negations of conjunctions by desugaring them into boolean expressions.
I'm having trouble making what's going on sufficiently clear since we need to write the negations out to apply transformation rules to them, but then they are not incompatibilities anymore but constraints that must be satisfied.
---
src/internals/incompatibilities.md | 28 ++++++++++++++++------------
1 file changed, 16 insertions(+), 12 deletions(-)
diff --git a/src/internals/incompatibilities.md b/src/internals/incompatibilities.md
index 5a83a8a..4461742 100644
--- a/src/internals/incompatibilities.md
+++ b/src/internals/incompatibilities.md
@@ -89,28 +89,32 @@ With incompatibilities, we would note
\Rightarrow \quad \\{ a: T_a, c: \overline{T_c} \\}. \\]
This is the simplified version of the rule of resolution.
-For the generalization, let's reuse the "more mathematical" notation of conjunctions
-for incompatibilities \\( T_a \land T_b \\) and the above rule would be
+For the generalization, let's write them as [boolean expressions][boolean_expression].
-\\[ T_a \land \overline{T_b}, \quad
- T_b \land \overline{T_c} \quad
-\Rightarrow \quad T_a \land \overline{T_c}. \\]
+\\[ \neg (T_a \land \overline{T_b}) \quad \land \quad
+ \neg (T_b \land \overline{T_c}) \quad
+\Rightarrow \quad \neg (T_a \land \overline{T_c}). \\]
In fact, the above rule can also be expressed as follows
-\\[ T_a \land \overline{T_b}, \quad
- T_b \land \overline{T_c} \quad
-\Rightarrow \quad T_a \land (\overline{T_b} \lor T_b) \land \overline{T_c} \\]
+\\[ \neg (T_a \land \overline{T_b}) \quad \land \quad
+ \neg (T_b \land \overline{T_c}) \quad
+\Rightarrow \quad \neg (T_a \land (\overline{T_b} \lor T_b) \land \overline{T_c}) \\]
since for any term \\( T \\), the disjunction \\( T \lor \overline{T} \\) is always true.
-In general, for any two incompatibilities \\( T_a^1 \land T_b^1 \land \cdots \land T_z^1 \\)
-and \\( T_a^2 \land T_b^2 \land \cdots \land T_z^2 \\) we can deduce a third,
-called the resolvent whose expression is
+In general, for any two incompatibilities \\( \\{ a: T_a^1, \cdots, z: T_z^1 \\} \\) and
+\\( \\{ a: T_a^2, \cdots, z: T_z^2 \\}, \\)
+or
-\\[ (T_a^1 \lor T_a^2) \land (T_b^1 \land T_b^2) \land \cdots \land (T_z^1 \land T_z^2). \\]
+\\[ \neg (T_a^1 \land T_b^1 \land \cdots \land T_z^1) \land \neg (T_a^2 \land T_b^2 \land \cdots \land T_z^2), \\]
+we can deduce a third, called the resolvent whose expression is
+
+\\[ \neg ((T_a^1 \lor T_a^2) \land (T_b^1 \land T_b^2) \land \cdots \land (T_z^1 \land T_z^2)). \\]
In that expression, only one pair of package terms is regrouped as a union (a disjunction),
the others are all intersected (conjunction).
If a term for a package does not exist in one incompatibility,
it can safely be replaced by the term \\( \neg [\varnothing] \\) in the expression above
as we have already explained before.
+
+[boolean_expression]: https://en.wikipedia.org/wiki/Boolean_expression#Boolean_operators