coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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:
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
I think the applicability of that result to Coq is not completely obvious. You could argue that, for an interpreter, you'dAm 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),
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
- [Coq-Club] Example of terminating function that are not accepted by Coq, Vincent Siles, 12/19/2018
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Klaus Ostermann, 12/19/2018
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Siddharth Bhat, 12/19/2018
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Xuanrui Qi, 12/19/2018
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Robbert Krebbers, 12/19/2018
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Thorsten Altenkirch, 12/19/2018
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Klaus Ostermann, 12/19/2018
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Xuanrui Qi, 12/19/2018
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Xuanrui Qi, 12/19/2018
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Jan Bessai, 12/19/2018
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Thorsten Altenkirch, 12/19/2018
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Jan Bessai, 12/19/2018
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Xuanrui Qi, 12/19/2018
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Siddharth Bhat, 12/19/2018
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Jean-Francois Monin, 12/19/2018
- [Coq-Club] Why Qwire was verified precisely in Coq?, José Manuel Rodriguez Caballero, 12/21/2018
- Re: [Coq-Club] Why Qwire was verified precisely in Coq?, Robert Rand, 12/21/2018
- Re: [Coq-Club] Why Qwire was verified precisely in Coq?, José Manuel Rodriguez Caballero, 12/21/2018
- Re: [Coq-Club] Why Qwire was verified precisely in Coq?, Robert Rand, 12/21/2018
- [Coq-Club] Why Qwire was verified precisely in Coq?, José Manuel Rodriguez Caballero, 12/21/2018
- Re: [Coq-Club] Example of terminating function that are not accepted by Coq, Klaus Ostermann, 12/19/2018
Archive powered by MHonArc 2.6.18.