The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

What is the problem with Ackermann? It is definable in System T hence in COQ.

Thorsten

Sent from my iPhone

On 19 Dec 2018, at 14:14, Xuanrui Qi <xqi01 AT cs.tufts.edu> wrote:

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!

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.