blob: 63e06eeb4346622645cd7f5ad72e8ea49c762e24 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
+++
title = "Reflexive Types"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3b3a"]
forwardlinks = ["3b3c"]
zettelid = "3b3b"
+++
Reflexive types are of the nature of taking an argument which is a
function and returning the Inductive type. Some of these are not legal
in Coq, even though they would be legal in Haskell/ML, as they might
produce computations that run forever. This would destroy all the
confidence that one could have in the proof system, as that would mean
that one could produce a proof for any theorem using an infinite loop.
This can be done because proofs are combined with functions. For
example, a reflexive type that takes the type it defines as an argument
could recurse indefinitely, which should not be allowed to be defined.
|
