Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Example of terminating function that are not accepted by Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Example of terminating function that are not accepted by Coq


Chronological Thread 
  • From: Xuanrui Qi <xqi01 AT cs.tufts.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Example of terminating function that are not accepted by Coq
  • Date: Wed, 19 Dec 2018 14:37:37 +0000 (UTC)
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=xqi01 AT cs.tufts.edu; spf=None smtp.mailfrom=xqi01 AT cs.tufts.edu; spf=None smtp.helo=postmaster AT vm-delivery1.eecs.tufts.edu
  • Ironport-phdr: 9a23:K9KbrBWBmZGSCOHlbF5Qwj9x1ljV8LGtZVwlr6E/grcLSJyIuqrYYxWEt8tkgFKBZ4jH8fUM07OQ7/iwHzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9xIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/ZisJ+kqFVrxCvpxJizIHbfIabOeFkca/BZ94VXnBMUtpTWiFHH4iyb5EPD+0EPetArob9ukEBrR2kBQmxBePk1yRGhn7r1qA93OUhCADG0BA9E98VrHvUt8/5NLsPUeC70KnI1i/PYO1L1jfg8YXFdA0qr/KUXb9obMbcx1UjGxnEg1ifs4DpIT2Y2v4DvmWZ9+ZtVfyjh3Q6pw1vojWj3Nogh4fXio4P11zJ9id0zYAoLtOiUkF7e8SrEJ5IuiGaKYR2RsQiTnl2uCY/07EJpIC0fCwLyJQ52RHfcfyGf5WS7h39SumePSx4iGh5eLKiiRay7VOgxvfiWcapzVZGtitFkt/SuXARzxHf98aKRudn8kqg1juDzR7f5+9eLU06l6fXM5shzaQxlpoXv0TDBCj2mEDuga6Zb0Uk+/Sk5/n8b7r6vZ+QLZN0ihzwMqQygcyzG/o3PRUTX2SD4+SzyKXj/VHlQLVNlvA5jq7ZsInDKcsHoq65HhRa35046xe/CjemyM4XkWMGLFJDYhKHjpLmN0vAIPDiXr+DhAGnly4uzPTbNJXgBI/MJz7NiuTPZ7F4vn5BwQwp0NEX3pMcXqEYIaqqckTq8sDFAAMidQG43rC0W51GyooCVDfXUeeiO6TIvArQv7N9E6y3fIYQ/Q3FBb0g7v/qg2U+nAZBL6Kym4cKZmyjWPlqPhfBOCa+spI6CW4P+zEGYqnyklTbDWxYfDCuQqwg/Xc2BJ/0Vd6eFLDou6SI2WKAJrMTZm1CDQrdQ2ntMomJX/YSZTiDe4lsnzcfE6S8RZM6kxyiqV2ixg==

Obviously I was wrong about Ackermann. Please ignore my comment about it.

-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



Archive powered by MHonArc 2.6.18.

Top of Page