blob: bfb08baab3761f5fa9db06587d790e93fc1e24a8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
+++
title = "Weakly embedded memoization"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c3c1"]
forwardlinks = ["3c3c3"]
zettelid = "3c3c2"
+++
Memoization can also be weakly embedded in Coq by using co-inductive
datatypes. This works extremely well for functions that take Peano
numbers as input, as a lazy data structure can be defined using
co-inductive types, which represents unevaluated thunks. Once these are
evaluated, they can just be read back normally.
|
