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

From: Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>
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:13:59 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=klaus.ostermann AT uni-tuebingen.de; spf=Pass smtp.mailfrom=klaus.ostermann AT uni-tuebingen.de; spf=None smtp.helo=postmaster AT mx04.uni-tuebingen.de
Ironport-phdr: 9a23:DRluXxbjzDriQPU/GBEMCYD/LSx+4OfEezUN459isYplN5qZoMS6bnLW6fgltlLVR4KTs6sC17KG9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa+bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjAk7m/XhMx+gqFVrh2vqBNwwZLbbo6OOfpifK7QZ88WSXZPU8tTUSFKH4Oyb5EID+oEJetWqo39qEETrRulGAKiHfjvyiNWiX/s2K01yeIhEQfb1wEnHNIOtG7brMjuNKsIVuC117XIwivZb/NTwzj97o7Ifws8ofGKXLJ8aNbRyVQxGAzej1WQr4PlMC2T1ugXrmeU8fNtWOSygGAkswF8uiWjy8kjh4XTmI4Z0FDJ+T9nzIooKtC0UEF2bN++HJZQrS2WKYt7T8M4T212tis3yrsLsoOhcicQ0pQo3RvfZuSHc4eW5hLjU/6cITJ3hX55d7+znQuy8U6hyuHlSsm0zUhFoTFEktnKuXACyRrT5tKaRfRj5kuh2DCP2B7P6uxcPEw5m6XWJ4Q/zrIqlpcfq1rPEjL5lUnuia+ZbEQk+uym6+T9ZbXmo4eRN4xwig7kL6QugdazAeMjMggSQWeb4+G826fl/U3/W7hKk/s2kqjAvJDGOMQUuLW2Aw5T0oYs9Rm/CS2q38kGknUfNlJKZAqHj5T1O1HJOP33EfC/g021nDh3w/DGI6buD47WLnnDlbfhZaxy51RdyAo119Bf5ohbBqsPIPLpCQfNs4nTCQZ8OAipyc7mDs9838UQQzGhGKicZYDWuEKTrsU0P+SWYYYTvn6pKPws+uWoimQllEUYdK+v9YYRaTWkA/lsIkOWbHyqjtpXQjRChRY3UOG/0A7KajVUfXvnB/tttAF+M5qvCML4fq7ohbWA2CmhGZgPNjJbDFHJDWrlfYSCVPoKLi6fcJY4zm40EIO5Qopk7imA8RfgwuM3fPfS+2gEqJ/p1d566uuVmRxgrWUpXfTY6HmESiRPpk1NRzIy2/ok80ltkgvFzK55xuBFGNZS4fxEVEE2OMyEwg==
Openpgp: preference=signencrypt

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.

[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