coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Extracting runnable relations

From: Cao Qinxiang <caoqinxiang AT gmail.com>
To: coq-club AT inria.fr
Cc: danya.berezun AT gmail.com
Subject: Re: [Coq-Club] Extracting runnable relations
Date: Fri, 26 Oct 2018 02:27:03 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=caoqinxiang AT gmail.com; spf=Pass smtp.mailfrom=caoqinxiang AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f54.google.com
Ironport-phdr: 9a23:Ary0dhBQKAGBgqdc6zrtUyQJP3N1i/DPJgcQr6AfoPdwSPryr8bcNUDSrc9gkEXOFd2Cra4c1KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhjexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoIODA5/2PXhMJ+j6xVvQyvqABkzoHOfI2YLuBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d4YCEfAOPeFFpIfmplsOqxS/BQi2C+PpxT9Dm3j70rEg3OQmCAHG3QogHt0PsHvOqtX1O7wfUe+wzKbSzDXDa+la1iv66IjNax0sp+yHU7FoccfJ10UjCwfIgk+TpIHlJT+ZyPgBvmuB4+dgWu+ijXMspRtrrTi13Mgsj5HEhoILxVDA8iV02IM1Kse5SE5/eNKrDoZfuzyDO4t4Qs4vTHtkuCk9yr0Btp67eDYFxI47yB7YbvyLa4mI4hT9W+aNOTp0mm5pdbalixux8UWs0PPwWtW33VpQridIncHAtnUX2BzS7siHROF9/kCk2TuXyw/c8OZEIVk1lardJJ8hw6Q/lpwcsUnYES/2nV/5jK6Sdkk+5ueo7OHnbq38ppCAL490lh3+MqM2l8OjBuQ4KxECUHSf+eShz7Lu5lb5QbVPjv0uiKbVqpHaJcIBpq64GQBZyIgj6wzsRwuhhd8fhDwMKE9PUBOBlYngfV/Uc97iCvLqqF2r2A5qweDHN7vuSsHGJ3/akbHxfL975GZTzQMyyZZU4JcCWeJJG+76RkKk7I+QNRQ+KQHhm7+2WuU47ZsXXCe0OoHcNarTtVGS4ed2eruDYYYUvHD2LP13vqey3098okcUeOyS5bVScGqxR600LECQYH6qidAEQz9T41gOCdfygVjHagZ9Ina/W6Vmu2M+AYOiSIrPH8Wj3eDH0yC8EZlbIGtBDwLUHA==

This is an interesting idea.

Coq requires functions to terminate (and we have to shows its termination by kind of structure recursion) but ocaml does not require that. A ``function'' may be more convenient to be formalized as a relation instead of a function in Coq. And it will be amazing if those relations can be extracted as functions.

Here is an example,

Inductive log2: nat -> nat -> Prop :=

| log2_base: log2 1 0

| log2_step: forall n k, log2 (div2 n) k -> log2 n (S k).

Qinxiang Cao

Tenure Track Assistant Professor

Shanghai Jiao Tong University, John Hopcroft Center

Room 1102-2, SJTUSE Building

800 Dongchuan Road, Shanghai, China, 200240

On Thu, Oct 25, 2018 at 2:20 PM Xuanrui Qi <xqi01 AT cs.tufts.edu> wrote:

Hello Kakadu,

This would look interesting to me. I can envision a miniKanren-style
program relation correct w/ respect to some specification, and then
extract the relation to miniKanren, e.g. for program synthesis.

I do not know if Will Byrd is on this list, but I guess he would be a
person to approach.

-Ray

--
Xuanrui "Ray" Qi

Department of Computer Science
Tufts University
161 College Ave, Halligan Hall
Medford, MA 02144, USA

Email: xqi01 AT cs.tufts.edu

On Thu, 2018-10-25 at 10:52 +0000, Kakadu wrote:
> Hello,
>
>
> AFAIU, proving something in terms of relations is convenient but it's
> difficult to extract them to runnable code. Let's say we can extract
> them to a logical programming language embedded into OCaml. How
> useful can it be? Can you easily imagine any concrete use cases?
>
>
> Happy hacking,
> Kakadu
>
>

[Coq-Club] Extracting runnable relations, Kakadu, 10/25/2018
- Re: [Coq-Club] Extracting runnable relations, Xuanrui Qi, 10/25/2018
  - Re: [Coq-Club] Extracting runnable relations, Cao Qinxiang, 10/26/2018
    - Re: [Coq-Club] Extracting runnable relations (from Impure Library), Sylvain Boulmé, 10/26/2018
    - Re: [Coq-Club] Extracting runnable relations, Dominique Larchey-Wendling, 10/26/2018
      - Re: [Coq-Club] Extracting runnable relations, mukesh tiwari, 10/27/2018