Update themes and add content

8 files changed, 58 insertions, 50 deletions

diff --git a/content/zettel/1b1.md b/content/zettel/1b1.md
index 14b0c84..fa8535f 100644
--- a/content/zettel/1b1.md
+++ b/content/zettel/1b1.md
@@ -3,7 +3,7 @@ title = "Guarded commands"
 author = "Yann Herklotz"
 tags = []
 categories = []
-backlinks = ["1d1", "1b2", "1b"]
+backlinks = ["1d1", "1b"]
 forwardlinks = ["1b2"]
 zettelid = "1b1"
 +++
diff --git a/content/zettel/1b2.md b/content/zettel/1b2.md
index 150523f..c0b9e07 100644
--- a/content/zettel/1b2.md
+++ b/content/zettel/1b2.md
@@ -4,7 +4,7 @@ author = "Yann Herklotz"
 tags = []
 categories = []
 backlinks = ["1d1", "1b1"]
-forwardlinks = ["3a", "1b1", "1b3"]
+forwardlinks = ["3a", "1b3"]
 zettelid = "1b2"
 +++
 
@@ -33,39 +33,6 @@ to support a subset of possible recursive functions. Even though these
 are as powerful as loops, it may be more natural to write their
 definitions as a recursive function instead of a loop.
 
-{{< transclude-1 zettel="1b1" >}}
-
-Guarded commands \[2\] are an interesting construct which can be added
-to languages. They look similar to `case` statements, but behave in a
-parallel and nondeterministic way. Each guard has a boolean value
-followed by a program which may be executed if the guard evaluates to
-true. The following shows the main syntax that guards may have.
-
-``` grammar
-e ::= if gc fi | do gc od ...
-
-gc ::= (b e) || gc
-```
-
-One reason these are interesting language constructs, is because they
-allow for the encoding of commands that may be executed when a condition
-is true, but that it isn't necessary. Often, when giving instructions,
-one does not really specify the order, just the commands that should
-eventually be executed.
-
-The guarded commands `gc` will either return a match if a boolean
-evaluates to true, or `abort`. There are two constructs that are built
-around guarded commands which adds more functionality to them.
-`if gc fi` matches one rule in the guarded statement and executes it. If
-it does not match a rule, it then acts like `abort`. `do gc od` loops
-over the guarded commands while any rule matches. If there no match is
-found, it acts like `skip`.
-
-These allow for nice encoding of common algorithms, using two other
-constructs that use the guarded commands.
-
-{{< /transclude-1 >}}
-
 <div id="refs" class="references csl-bib-body" markdown="1">
 
 <div id="ref-leroy06_formal_certif_compil_back_end" class="csl-entry"
@@ -81,14 +48,6 @@ doi: [10.1145/1111037.1111042].</span>
 
 </div>
 
-<div id="ref-winskel93" class="csl-entry" markdown="1">
-
-<span class="csl-left-margin">\[2\]
-</span><span class="csl-right-inline">G. Winskel, *The formal semantics
-of programming languages: An introduction*. MIT press, 1993.</span>
-
-</div>
-
 </div>
 
   [\#3a]: /zettel/3a
diff --git a/content/zettel/1d1.md b/content/zettel/1d1.md
index dcd131c..cc902c4 100644
--- a/content/zettel/1d1.md
+++ b/content/zettel/1d1.md
@@ -38,6 +38,8 @@ to support a subset of possible recursive functions. Even though these
 are as powerful as loops, it may be more natural to write their
 definitions as a recursive function instead of a loop.
 
+{{< /transclude-1 >}}
+
 {{< transclude-2 zettel="1b1" >}}
 
 Guarded commands \[2\] are an interesting construct which can be added
@@ -71,8 +73,6 @@ constructs that use the guarded commands.
 
 {{< /transclude-2 >}}
 
-{{< /transclude-1 >}}
-
 <div id="refs" class="references csl-bib-body" markdown="1">
 
 <div id="ref-leroy06_formal_certif_compil_back_end" class="csl-entry"
diff --git a/content/zettel/3a8g5h.md b/content/zettel/3a8g5h.md
index 31ab96c..86f9892 100644
--- a/content/zettel/3a8g5h.md
+++ b/content/zettel/3a8g5h.md
@@ -4,7 +4,7 @@ author = "Yann Herklotz"
 tags = []
 categories = []
 backlinks = ["3a8g5g"]
-forwardlinks = ["3a8g5i", "3a8g5h1"]
+forwardlinks = ["3a8g5h1", "3a8g5h2", "4e1", "3a8g5h3", "3a8g5h4", "3a8g5i"]
 zettelid = "3a8g5h"
 +++
 
@@ -31,4 +31,53 @@ independent before the simplification to $1 \lor \neg 1$ and
 $\neg1 \land \neg 2$, where the left hand branch will actually always be
 true.
 
+{{< transclude-1 zettel="3a8g5h1" >}}
+
+The first solution to this problem would be to add quantifiers to the
+atoms that cannot always be evaluated at the current spot. However, this
+would significantly increase the complexity of the Sat solver, as well
+as make predicates unevaluatable in general, because it might contain
+quantifiers that don't evaluate to one specific value.
+
+However, with a suitably strong SAT solver, it should be possible to
+show the independence between the different predicates. However, the
+correctness property should probably be correct as well and should be
+checkable with the SAT solver.
+
+{{< /transclude-1 >}}
+
+{{< transclude-1 zettel="3a8g5h2" >}}
+
+The second possible solution could be to use Craig interpolation
+([\#4e1]), which was a suggestion by John. This is close to what we
+currently already do, however a bit more sound (replacing positive
+literals by T and replacing negative literals by $\perp$). This does not
+seem to completely solve the problem, because it only really works for
+implication, and for the independence property that's not enough.
+
+{{< /transclude-1 >}}
+
+{{< transclude-1 zettel="3a8g5h3" >}}
+
+Tri-state logic is also an interesting solution and it goes back to what
+we had initially thought about implementing, however, the problem with
+that is again the SAT solver, as we want to be able to assume that we do
+get an answer out of it. However, maybe it's possible to use the SAT
+solver natively on 3-state logic. We would then be able to construct the
+evaluation rules for our gates so that they follow the correctness
+property that we are hoping for.
+
+{{< /transclude-1 >}}
+
+{{< transclude-1 zettel="3a8g5h4" >}}
+
+Finally, the fourth solution could be to have lazy evaluation of the
+expressions, and order the predicates so that the more general property
+comes first, followed by the more specific properties. However, the main
+problem with this is that we don't really know which predicate came from
+which node, and what the order should be for those predicates.
+
+{{< /transclude-1 >}}
+
   [1]: attachment:gsa-simplification-problem.png
+  [\#4e1]: /zettel/4e1
diff --git a/content/zettel/3a8g5h2.md b/content/zettel/3a8g5h2.md
index b8facdd..2041559 100644
--- a/content/zettel/3a8g5h2.md
+++ b/content/zettel/3a8g5h2.md
@@ -3,7 +3,7 @@ title = "Second possible solution: Craig interpolation"
 author = "Yann Herklotz"
 tags = []
 categories = []
-backlinks = ["3a8g5h1"]
+backlinks = ["3a8g5h1", "3a8g5h"]
 forwardlinks = ["4e1", "3a8g5h3"]
 zettelid = "3a8g5h2"
 +++
diff --git a/content/zettel/3a8g5h3.md b/content/zettel/3a8g5h3.md
index 73576e5..e521c44 100644
--- a/content/zettel/3a8g5h3.md
+++ b/content/zettel/3a8g5h3.md
@@ -3,7 +3,7 @@ title = "Third possible solution: Tri-state logic"
 author = "Yann Herklotz"
 tags = []
 categories = []
-backlinks = ["3a8g5h2", "3a8g5g1"]
+backlinks = ["3a8g5h2", "3a8g5h", "3a8g5g1"]
 forwardlinks = ["3a8g5h4"]
 zettelid = "3a8g5h3"
 +++
diff --git a/content/zettel/3a8g5h4.md b/content/zettel/3a8g5h4.md
index 9e044b8..e11af4c 100644
--- a/content/zettel/3a8g5h4.md
+++ b/content/zettel/3a8g5h4.md
@@ -3,7 +3,7 @@ title = "Fourth possible solution: Ordering of predicates"
 author = "Yann Herklotz"
 tags = []
 categories = []
-backlinks = ["3a8g5h3"]
+backlinks = ["3a8g5h3", "3a8g5h"]
 forwardlinks = ["3a8g5h5"]
 zettelid = "3a8g5h4"
 +++
diff --git a/content/zettel/4e1.md b/content/zettel/4e1.md
index 71407e9..754204c 100644
--- a/content/zettel/4e1.md
+++ b/content/zettel/4e1.md
@@ -3,7 +3,7 @@ title = "Craig interpolation"
 author = "Yann Herklotz"
 tags = []
 categories = []
-backlinks = ["4e", "3a8g5h2"]
+backlinks = ["4e", "3a8g5h2", "3a8g5h"]
 forwardlinks = ["4e2"]
 zettelid = "4e1"
 +++