1 files changed, 27 insertions, 0 deletions
diff --git a/content/zettel/3a8g2a.md b/content/zettel/3a8g2a.md
new file mode 100644
index 0000000..ee613b4
--- /dev/null
+++ b/content/zettel/3a8g2a.md
@@ -0,0 +1,27 @@
++++
+title = "Detailed implementation"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a8g2"]
+forwardlinks = ["3a8g2b"]
+zettelid = "3a8g2a"
++++
+
+Destruction of GSA is actually quite tricky to do correctly, as a lot of
+information was lost during it's construction, and there are currently
+not enough strong well-formedness conditions about the predicates in the
+γ and η functions. Especially the γ functions need to be turned into φ
+functions, which essentially means reconstructing control-flow
+information just from the predicates.
+
+These predicates should be correct, which is hard to quantify itself,
+and actually does not relate to the control-flow in any way without
+having additional restrictions. The only thing one knows for certain is
+that the semantics ensure that the program will not block, meaning there
+will always be a predicate that is true, which allows the semantics to
+advance. This does not help for the destruction though, as this does not
+guarantee that the predicates talk about the control-flow paths in any
+way. For that one will have to add a well-formedness condition
+specifically for the destruction which will be true when the predicates
+do relate to control-flow in some way.