diff options
| -rw-r--r-- | .build.yml | 2 | ||||
| -rw-r--r-- | _css/style.css | 37 | ||||
| -rw-r--r-- | blog/boolin.md | 42 |
3 files changed, 29 insertions, 52 deletions
diff --git a/.build.yml b/.build.yml index 7d54b98..a6f6ce1 100644 --- a/.build.yml +++ b/.build.yml @@ -7,7 +7,7 @@ packages: sources: - https://git.sr.ht/~cnx/site tasks: - - katex: | + - inject: | mkdir -p site/_libs/katex cp /usr/lib/node_modules/katex/dist/katex.min.js site/_libs/katex cp -r /usr/lib/node_modules/katex/dist/{fonts,katex.min.css} site/_css diff --git a/_css/style.css b/_css/style.css index dbd1874..5185744 100644 --- a/_css/style.css +++ b/_css/style.css @@ -56,11 +56,6 @@ body { margin: 0 1rem } .franklin-content .right { float: right } -.franklin-content .container img { - width: auto; - padding-left: 0; -} - /* Text geometry */ .franklin-content p { hyphens: auto; @@ -107,45 +102,25 @@ body { margin: 0 1rem } .franklin-content .bibref a, .franklin-content .eqref a { color: var(--link-fg) } +.franklin-content .fndef { + border: none; + margin: 1ex 0; +} .franklin-content .fndef tr { text-align: left } +.franklin-content .fndef td { padding: 0 } .franklin-content .fndef td, .franklin-content sup { font-size: 80% } -.franklin-content .fndef td.fndef-content { width: 100% } .franklin-content .fndef td.fndef-backref { padding-left: 0 } -.franklin-content table.fndef { - border: none; - margin: 0; -} +.franklin-content .fndef td.fndef-content { padding-left: 1ch } /* Images */ .franklin-content img { display: block; margin: auto; max-width: 100%; - width: auto; } /* KaTeX */ .katex { font-size: 1em !important } -.katex-display .katex { - /* Overwrite KaTeX settings. */ - display: inline-block; - - /* Allow display equations to wrap on small screens. */ - white-space: normal; -} - -/* - * No numbering, for now - * body { counter-reset: eqnum } - * - * .katex-display::after { - * counter-increment: eqnum; - * content: "(" counter(eqnum) ")"; - * position: relative; - * float: right; - * padding-right: 5px; - * } - */ /* Boxes */ .franklin-content blockquote, .note { 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 |