The Coq mailing list

[Xuanrui Qi <xqi01 AT cs.tufts.edu>]

Hello Klaus,

What you have in mind is (almost) the Brown-Palsberg self interpreter, not the impossible self interpreter. Please refer to Andrej Bauer's note here on what is possible and what is not: http://math.andrej.com/2016/01/04/a-brown-palsberg-self-interpreter-for-godels-system-t/.

Best,

Ray

On Wed, Dec 19, 2018 at 9:34 AM -0500, "Klaus Ostermann" <klaus.ostermann AT uni-tuebingen.de> wrote:

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