The Coq mailing list

[Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>]

Am 19.12.18 um 15:13 schrieb Xuanrui Qi:
It is well known and proven that total languages do not have self interpreters (because you can't prove a calculus's termination in itself),
I think the applicability of that result to Coq is not completely obvious. You could argue that, for an interpreter, you'd
need a meta-function "quote" that takes a term of type t to type Rep t (for some type constructor Rep", and a function
"eval : forall t, Rep t -> t" or something like that.

However, with that specification, choosing quote, Rep, and eval to all be identity functions would constitute a
(useless) interpreter of Coq in Coq. Obviously you want your representation of terms to be somehow more informative
than the term itself, but it is not clear what properties a proper representation of terms should have to "count"
as being a self-interpreter.

Klaus