From ac4d614cb0223be8167cc73fe6eaa440bbed74a7 Mon Sep 17 00:00:00 2001
From: Nguyễn Gia Phong <mcsinyx@disroot.org>
Date: Sat, 27 Nov 2021 16:09:14 +0700
Subject: Clean up mistakes

---
 blog/boolin.md | 42 ++++++++++++++++++++++--------------------
 1 file changed, 22 insertions(+), 20 deletions(-)

(limited to 'blog/boolin.md')

diff --git a/blog/boolin.md b/blog/boolin.md
index 6acae55..00f118f 100644
--- a/blog/boolin.md
+++ b/blog/boolin.md
@@ -137,12 +137,12 @@ definitions of an environment marker
 \[\begin{aligned}
   (e_1, \ldots, e_{11})
   &\mapsto \bigvee_{\imath = 1}^n\bigwedge_{\jmath = 1}^{f(\imath)}
-  x(\jmath)\left(e_{k(\jmath)}\right)\\
+  x(\imath, \jmath)\left(e_{k(\imath, \jmath)}\right)\\
   (e_1, \ldots, e_{11})
   &\mapsto \bigwedge_{\imath = 1}^n\bigvee_{\jmath = 1}^{f(\imath)}
-  x(\jmath)\left(e_{k(\jmath)}\right)
+  x(\imath, \jmath)\left(e_{k(\imath, \jmath)}\right)
 \end{aligned}\]
-where $n \in \N$, $f: \N^* \to \N^*$, $x: \N^* \to X$, $k: \N^* \to I$
+where $n \in \N$, $f: \N_1 \to \N_1$, $x: \N_1^2 \to X$, $k: \N_1^2 \to I$
 and an empty Boolean expression is implicitly $c_\top$.
 
 Now it is possible to formalize inclusion for markers as
@@ -152,55 +152,57 @@ Thus, checking if a marker includes another is equivalent to evaluating
 the following expression, for all $(e_1, \ldots, e_{11}) \in E$
 \[\begin{aligned}
   r &= \bigvee_{\imath' = 1}^{n'}\bigwedge_{\jmath' = 1}^{f'(\imath')}
-       x'(\jmath')\left(e_{k'(\jmath')}\right)
+       x'(\imath', \jmath')\left(e_{k'(\imath', \jmath')}\right)
        \le \bigwedge_{\imath = 1}^n\bigvee_{\jmath = 1}^{f(\imath)}
-       x(\jmath)\left(e_{k(\jmath)}\right)\\
+       x(\imath, \jmath)\left(e_{k(\imath, \jmath)}\right)\\
     &= \bigwedge_{\imath' = 1}^{n'}\left(\bigwedge_{\jmath' = 1}^{f'(\imath')}
-       x'(\jmath')\left(e_{k'(\jmath')}\right)
+       x'(\imath', \jmath')\left(e_{k'(\imath', \jmath')}\right)
        \le \bigwedge_{\imath = 1}^n\bigvee_{\jmath = 1}^{f(\imath)}
-       x(\jmath)\left(e_{k(\jmath)}\right)\right)\\
+       x(\imath, \jmath)\left(e_{k(\imath, \jmath)}\right)\right)\\
     &= \bigwedge_{\imath' = 1}^{n'}\bigwedge_{\imath = 1}^n
        \left(\bigwedge_{\jmath' = 1}^{f'(\imath')}
-       x'(\jmath')\left(e_{k'(\jmath')}\right)
+       x'(\imath', \jmath')\left(e_{k'(\imath', \jmath')}\right)
        \le \bigvee_{\jmath = 1}^{f(\imath)}
-       x(\jmath)\left(e_{k(\jmath)}\right)\right)
+       x(\imath, \jmath)\left(e_{k(\imath, \jmath)}\right)\right)
 \end{aligned}\]
 where $r$ is whether the original marker (defined by $n$, $f$, $x$ and $k$)
 includes the declared one (defined by $n'$, $f'$, $x'$ and $k'$). Let
 \[\begin{aligned}
   g(\imath, \ell) &= \{\jmath \mid \jmath \in [1, f(\imath)]
-                              \land k(\jmath) = \ell\}\\
+                              \land k(\imath, \jmath) = \ell\}\\
   g'(\imath, \ell) &= \{\jmath \mid \jmath \in [1, f'(\imath)]
-                               \land k'(\jmath) = \ell\}
+                               \land k'(\imath, \jmath) = \ell\}
 \end{aligned}\]
 and assume $e_1, \ldots, e_{11}$ are orthogonal, we have
 \[\begin{aligned}
   r &= \bigwedge_{\imath' = 1}^{n'}\bigwedge_{\imath = 1}^n\bigvee_{\ell \in I}
        \left(\bigwedge_{\jmath' \in g'(\imath', \ell)}
-       x'(\jmath')\left(e_{\ell}\right)
+       x'(\imath', \jmath')\left(e_{\ell}\right)
        \le \bigvee_{\jmath \in g(\imath, \ell)}
-       x(\jmath)\left(e_{\ell}\right)\right)\\
+       x(\imath, \jmath)\left(e_{\ell}\right)\right)\\
     &= \bigwedge_{\imath' = 1}^{n'}\bigwedge_{\imath = 1}^n\bigvee_{\ell \in I}
        \left(\bigwedge_{\jmath' \in g'(\imath', \ell)}
-       x'(\jmath')\left(e_{\ell}\right)
+       x'(\imath', \jmath')\left(e_{\ell}\right)
        \land \lnot \bigvee_{\jmath \in g(\imath, \ell)}
-       x(\jmath)\left(e_{\ell}\right) = \bot\right)
+       x(\imath, \jmath)\left(e_{\ell}\right) = \bot\right)
 \end{aligned}\]
 where $\bot$ is the Boolean algebra bottom element.  By [De Morgan's laws],
 \[\begin{aligned}
   r &= \bigwedge_{\imath' = 1}^{n'}\bigwedge_{\imath = 1}^n\bigvee_{\ell \in I}
        \left(\bigwedge_{\jmath' \in g'(\imath', \ell)}
-       x'(\jmath')\left(e_{\ell}\right)
+       x'(\imath', \jmath')\left(e_{\ell}\right)
        \land \bigwedge_{\jmath \in g(\imath, \ell)}
-       \lnot x(\jmath)\left(e_{\ell}\right) = \bot\right)
+       \lnot x(\imath, \jmath)\left(e_{\ell}\right) = \bot\right)
 \end{aligned}\]
 
 Essentially, checking if
-\[\bigwedge_{\jmath' \in g'(\imath', \ell)} x'(\jmath')\left(e_{\ell}\right)
+\[\bigwedge_{\jmath' \in g'(\imath', \ell)}
+  x'(\imath', \jmath')\left(e_{\ell}\right)
   \land \bigwedge_{\jmath \in g(\imath, \ell)}
-  \lnot x(\jmath)\left(e_{\ell}\right)\]
+  \lnot x(\imath, \jmath)\left(e_{\ell}\right)\]
 is unsatisfiable for all $e_{\ell}$ is a [SAT problem] which we can write
-a solver for.
+a solver for.  Indeed, the original expression could be formulated as a SAT,
+but it would be more complex due to the multiple dimensions of environments.
 
 ## Implementation
 
-- 
cgit 1.4.1