The Coq mailing list

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

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), but I'm actually not sure what happens in the presence of coinductive families. I think the answer should still be no. Alternatively, though, you can definitely write a Brown-Palsberg self-interpreter for Coq. See Matt Brown and Jens Palsberg's POPL 2016 paper for an example (in System F-omega).

Also, Ackermann is not definable in Coq, unless you trick Coq using Program Fixpoint. IIRC it's actually a loophole, but you won't break anything by introducing inconsistency.

-Ray

On Wed, Dec 19, 2018 at 8:40 AM -0500, "Siddharth Bhat" <siddu.druid AT gmail.com> wrote:

Is it not possible to provide conductive semantics to such an interpreter, and thereby get coq to accept an interpreter? 

Thanks,

Siddharth

On Wed, 19 Dec, 2018, 18:45 Klaus Ostermann, <klaus.ostermann AT uni-tuebingen.de> wrote:

I assume an interpreter of Coq in Coq would be such a function.

Klaus


Am 19.12.18 um 13:53 schrieb Vincent Siles:
> Hi !
> Today I've been asked if there are some examples of known terminating
> programs that can't be expressed at all in Coq. I know the usual
> 'fuel' encoding where one can add an integer to recurse on, and then
> prove that there always exists an integer big enough for the program
> to terminante. But are there examples that are not accepted by Coq
> even with such technics ?
>
> Best,
> V.

--

Sending this from my phone, please excuse any typos!