blob: d9faa24d28a6a7dec917e6a61a9ce929800eecfd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
+++
title = "Represent external functions as non-deterministic"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3b6"]
forwardlinks = ["3b6"]
zettelid = "3b6a"
+++
By representing external function as being non-deterministic, one can
better reason about the basic properties that the OCaml function gives,
such as not allowing the property proven in `cong` in ([\#3b6]).
To do this in the Coq type-system, one can represent return values as
the type of all predicates of the function type. The return value of
non-deterministic computations which may return a value `A` can be
represented as $\mathcal{P}(A)$, which represents `A -> Prop`, all the
predicates of `A`.
This *may-return* monad is encoded in the [Impure Library].
[\#3b6]: /zettel/3b6
[Impure Library]: https://github.com/boulme/Impure
|
