1 files changed, 19 insertions, 0 deletions
diff --git a/content/zettel/3b4.md b/content/zettel/3b4.md
new file mode 100644
index 0000000..76eb7d8
--- /dev/null
+++ b/content/zettel/3b4.md
@@ -0,0 +1,19 @@
++++
+title = "General Recursion"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3b3"]
+forwardlinks = ["3b5"]
+zettelid = "3b4"
++++
+
+One can define a well-formed relation on a recursive function and
+therefore prove that it terminates by using the `Fix` inductive.
+However, one can also define a termination monad which can represent
+functions that terminate and that don't terminate. Using it, one can
+define recursive without functions having to prove if they terminate or
+not, and one can still reason about them if the arguments terminate.
+
+Finally, one can also use co-inductive types to represent termination in
+a nicer way.