blob: 76eb7d83a0fb0f1c9b7086ada26952338712294c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
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.
|
