From dec5d77063d8235b49d57e759b4ba6553943cba5 Mon Sep 17 00:00:00 2001 From: konstin Date: Fri, 8 Dec 2023 14:11:43 +0100 Subject: [PATCH 1/2] 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 From 4d56dbf2bbb836aac942468f60ffe2aeae7d4fd0 Mon Sep 17 00:00:00 2001 From: konstin Date: Fri, 8 Dec 2023 14:12:04 +0100 Subject: [PATCH 2/2] Explain math symbols in rust terms Split out of https://github.com/pubgrub-rs/guide/pull/8 for separate discussion, I tried to make it clearer what the operations means for someone who knows rust but doesn't have an academic math education otherwise. --- src/internals/terms.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/internals/terms.md b/src/internals/terms.md index e4b2042..7d2e784 100644 --- a/src/internals/terms.md +++ b/src/internals/terms.md @@ -24,6 +24,7 @@ In this guide, for any given range \\(r\\), we will note \\([r]\\) its associated positive term, and \\(\neg [r]\\) its associated negative term. And for any term \\(T\\), we will note \\(\overline{T}\\) the negation of that term. +(\\( \neg A \\) and \\( \overline{A} \\) are different notations for the same thing.) Therefore we have the following rules, \\[\begin{eqnarray} @@ -58,7 +59,10 @@ based on those ranges is defined as follows, \neg [r_1] \land \neg [r_2] &=& \neg [r_1 \cup r_2]. \nonumber \\\\ \end{eqnarray}\\] -And for any two terms \\(T_1\\) and \\(T_2\\), their union and intersection are related by +In rust terms, "\\( \neg \\)" means "not"/`!` (\\( \neg T \\), +"\\( \land \\)" means "and"/, "\\( \lor \\)" means "or"/`||`. + +And for any two terms \\(T_1\\) and \\(T_2\\), their union and intersection are related by De Morgan's laws \\[ \overline{T_1 \lor T_2} = \overline{T_1} \land \overline{T_1}. \\]