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: Siddharth Bhat <siddu.druid AT gmail.com>
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 19:10:24 +0530
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=siddu.druid AT gmail.com; spf=Pass smtp.mailfrom=siddu.druid AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi1-f176.google.com
Ironport-phdr: 9a23:8qD37BSwNBB3TiRvXL5qUDLoGdpsv+yvbD5Q0YIujvd0So/mwa69ZRSN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/27ZisNyjKxVrhGvqQFhzYHIe4yaLuZyc7nHcN8GWWZMXMBcXDFBDIOmaIsPCvIMM/tZr4bgulQOrQGxBROwBOPv1zRFm3/20rcm0+88FgzGxw0gEM8Tv3TJttn6Kb0SUf20zKbV1jjDYPZW1i386IjMaBwuvfaMXbdpfMfX1EIhFBvFg02OpYD5Oz6ZzOcAvmiB4+Z9VO+iiXQrpxxzrzWuwMonl5PHiZgPyl/e8CV02IY1KsO8SE58edOkFYFftyCeN4dvRcMiQnxktD80yrEbu5O2fTIGyJsgxx7YZPyHd5aH7gj/W+aWJDd0nHNleLShiBau6UWs1PHwW82u3FtJridJiMTAu3EP2hDJ98SKSPpw8l+k2TmV1gDT7u9EIVozlareM5Mh2b8wmYcOvkTeBCP5hV/2jLKXdko54eWo5OHnba/npp+YLYN7lgb+MqE2lsylHes4KhQOX3Sc+emkyLLj+lT5TKxWgf0yj6nWq4vXJd8bp668Gw9ayJwv6xe5Dze80dQXh2MLLFxfeEHPs4+8MFbXZfv8EP2XglK2kT4tyeqVEKfmB8D2L3TPkL77YbY1wU5V1EJn1tFT648SBqscIf7bVUr4tdieBRg8ZV/ni937Aclwg9tNEVmEBbWUZfuL4A24o9k3KuzJX7c7/TP0Kvwr/fnr1CZrlloUfK3v1pwSOinhQqZWZn6BaH+pue8vVH8Qt1NnHuPvgVyGFzVUYiTqBv9u1nQAEIujSLz7aMWtjbiGhnnpG5RXYiVBCwnJHy63KcOLXPADbC/UKchkwGQJ

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!

[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, Jean-Francois Monin, 12/19/2018