From 91c696fc52ffb1eeb894328c722ba4473c8027c1 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 12 May 2023 15:26:18 +0100 Subject: Update themes and add content --- .gitmodules | 5 +--- content/zettel/1b1.md | 2 +- content/zettel/1b2.md | 43 +----------------------------- content/zettel/1d1.md | 4 +-- content/zettel/3a8g5h.md | 51 +++++++++++++++++++++++++++++++++++- content/zettel/3a8g5h2.md | 2 +- content/zettel/3a8g5h3.md | 2 +- content/zettel/3a8g5h4.md | 2 +- content/zettel/4e1.md | 2 +- layouts/_default/list.html | 9 ++++--- layouts/_default/single.html | 34 +++++++++++++----------- layouts/partials/head_custom.html | 1 + layouts/partials/post-element.html | 8 +++--- layouts/shortcodes/transclude-1.html | 2 +- layouts/shortcodes/transclude-2.html | 2 +- layouts/shortcodes/transclude-3.html | 2 +- themes/hugo-xmin | 2 +- 17 files changed, 93 insertions(+), 80 deletions(-) diff --git a/.gitmodules b/.gitmodules index e5e02d5..0e861c2 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,6 +1,3 @@ -[submodule "themes/hugo-blog-awesome"] - path = themes/hugo-blog-awesome - url = https://github.com/hugo-sid/hugo-blog-awesome.git [submodule "themes/hugo-xmin"] path = themes/hugo-xmin - url = https://github.com/yihui/hugo-xmin + url = https://git.sr.ht/~ymherklotz/zk-theme 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 >}} -
-
- -\[2\] -G. Winskel, *The formal semantics -of programming languages: An introduction*. MIT press, 1993. - -
-
[\#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 >}} -
}} + +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" +++ diff --git a/layouts/_default/list.html b/layouts/_default/list.html index 744f390..4cf7dd1 100644 --- a/layouts/_default/list.html +++ b/layouts/_default/list.html @@ -6,12 +6,15 @@ {{ .Content }} -
    {{ $pages := .Pages }} {{ if .IsHome }}{{ $pages = .Site.RegularPages }}{{ end }} - {{ range (where $pages "Section" "!=" "") }} + {{ range $pages.GroupByDate "2006" }} +

    {{ .Key }}

    + + {{ range .Pages }} {{ partial "post-element.html" . }} {{ end }} - +
    + {{ end }} {{ partial "footer.html" . }} diff --git a/layouts/_default/single.html b/layouts/_default/single.html index f3953af..e1f98a7 100644 --- a/layouts/_default/single.html +++ b/layouts/_default/single.html @@ -1,6 +1,6 @@ {{ partial "header.html" . }}
    -

    {{ .Title | markdownify }}

    +

    {{ .Title | markdownify }}{{ if .Params.zettelid }} [#{{ .Params.zettelid }}]{{ end }}

    {{ if (gt .Params.date 0) }}

    {{ .Date.Format "2006/01/02" }}

    {{ end }}
    @@ -9,22 +9,26 @@ {{ .Content }} - {{ if (.Page.Param "backlinks") }} -

    Referenced from

    - {{ range (.Page.Param "backlinks") }} - {{ with ($.Site.GetPage (printf "/zettel/%s" .)) }} - {{ partial "post-element.html" . }} - {{- end }} - {{ end }} +{{ with (.Page.Param "backlinks") }} +

    Referenced from

    + +{{ range . }} + {{ with ($.Site.GetPage (printf "/zettel/%s" .)) }} + {{ partial "post-element" . }} {{ end }} +{{ end }} +
    +{{ end }} - {{ if (.Page.Param "forwardlinks") }} -

    Links to

    - {{ range (.Page.Param "forwardlinks") }} - {{ with ($.Site.GetPage (printf "/zettel/%s" .)) }} - {{ partial "post-element.html" . }} - {{- end }} - {{ end }} +{{ with (.Page.Param "forwardlinks") }} +

    Links to

    + +{{ range . }} + {{ with ($.Site.GetPage (printf "/zettel/%s" .)) }} + {{ partial "post-element" . }} {{ end }} +{{ end }} +
    +{{ end }} {{ partial "footer.html" . }} diff --git a/layouts/partials/head_custom.html b/layouts/partials/head_custom.html index 47ba699..93e3874 100644 --- a/layouts/partials/head_custom.html +++ b/layouts/partials/head_custom.html @@ -17,3 +17,4 @@ }); }); + diff --git a/layouts/partials/post-element.html b/layouts/partials/post-element.html index b45a1e1..28fff85 100644 --- a/layouts/partials/post-element.html +++ b/layouts/partials/post-element.html @@ -1,4 +1,4 @@ -
  • - {{ .Date.Format "2006/01/02" }} - {{ .Title | markdownify }} -
    • + + {{ .Title | markdownify }}{{ if .Params.zettelid }} [#{{ .Params.zettelid }}]{{ end }} + {{ with .Date }}{{ .Format "2006/01/02" }}{{ end }} + diff --git a/layouts/shortcodes/transclude-1.html b/layouts/shortcodes/transclude-1.html index 80a24da..cfc6a86 100644 --- a/layouts/shortcodes/transclude-1.html +++ b/layouts/shortcodes/transclude-1.html @@ -1,4 +1,4 @@
    -

    {{ .Get "zettel" }}: {{ with ($.Site.GetPage (printf "/zettel/%s" (.Get "zettel"))) }}{{ .Title | markdownify }}{{ end }}

    + {{ with ($.Site.GetPage (printf "/zettel/%s" (.Get "zettel"))) }}

    {{ .Title | markdownify }} [#{{ .Params.zettelid }}]

    {{ end }} {{ .Inner | markdownify }}
    diff --git a/layouts/shortcodes/transclude-2.html b/layouts/shortcodes/transclude-2.html index a63de87..20987ae 100644 --- a/layouts/shortcodes/transclude-2.html +++ b/layouts/shortcodes/transclude-2.html @@ -1,4 +1,4 @@
    -

    {{ .Get "zettel" }}: {{ with ($.Site.GetPage (printf "/zettel/%s" (.Get "zettel"))) }}{{ .Title | markdownify }}{{ end }}

    + {{ with ($.Site.GetPage (printf "/zettel/%s" (.Get "zettel"))) }}

    {{ .Title | markdownify }} [#{{ .Params.zettelid }}]

    {{ end }} {{ .Inner | markdownify }}
    diff --git a/layouts/shortcodes/transclude-3.html b/layouts/shortcodes/transclude-3.html index 1e43c85..6e73cd4 100644 --- a/layouts/shortcodes/transclude-3.html +++ b/layouts/shortcodes/transclude-3.html @@ -1,4 +1,4 @@
    -

    {{ .Get "zettel" }}: {{ with ($.Site.GetPage (printf "/zettel/%s" (.Get "zettel"))) }}{{ .Title | markdownify }}{{ end }}

    + {{ with ($.Site.GetPage (printf "/zettel/%s" (.Get "zettel"))) }}

    {{ .Title | markdownify }} [#{{ .Params.zettelid }}]

    {{ end }} {{ .Inner | markdownify }}
    diff --git a/themes/hugo-xmin b/themes/hugo-xmin index 67f2ed0..d291868 160000 --- a/themes/hugo-xmin +++ b/themes/hugo-xmin @@ -1 +1 @@ -Subproject commit 67f2ed048d0494891a6e9ea8ed2e2bffda431908 +Subproject commit d29186892211056822e976689c0c6b3eb026f6e9 -- cgit