coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is Coq SN?

From: roux cody <cody.roux AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Is Coq SN?
Date: Thu, 22 Dec 2016 14:27:36 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=cody.roux AT gmail.com; spf=Pass smtp.mailfrom=cody.roux AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f47.google.com
Ironport-phdr: 9a23:faic8BXKZdm4z9ret07qyWmocRjV8LGtZVwlr6E/grcLSJyIuqrYYxCGt8tkgFKBZ4jH8fUM07OQ6PG7Hzxcqs/b7TgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal8IRiyowjdrMobjIRtJqos1BfEomZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhN9zY7aYI+bOvljcK3DYdwXXnBOUtpLWiFbHo+wc4kCAuwcNuhYtYn9oF4OoAOkBQmrGePuxSJDiWPx3aIn0+UqDAbL0xAnH90TsHXYts/1NKAPUeG616TIwjDDYOlX2Tf58oTHbhchofSVUL92bMHfx04vFwbfgVWRr4zoJzKV1uIXs2ia9eVsT+yvi3Q/pwFrozig2tkjhpPXiY0I11DJ8zhyzoUtJdCgVkJ3fdqpHIFTuiyaLYd6XN4uTmJytCs1yLALv4OwcjIQx5Q93RHfbuSKc4iW7RLnU+acOTJ4i2hkeLK7nhqy9kmgxvHlWsm631tHrDBJktbLtnAK2BzT7taIRuFh8Uem3DaDzwHT6udaLkAojafXNYItz7oqmpcQsUnPBDH6lFj1gaOMeUgp+PCk6+H9bbXnop+cOZV0igb7Mqk2hsO/Bvk3MwgUU2iB/uS8ybLi8Fb2QLVPlPI2k63ZvIrGKsQco661GxVV3Zo76xajEzem18wVkmUALFJcYR6Ik4zpO0zVL/3jFve+g1GskC9xyPzcP73hBI/NLnnZn7v7c7Z98R0U9A1mxtdGoplQF7spIfTpW0a3usaLIAU+NlmuxPv3QN562pJWDWmIDr7fKqTPoXeH4+suJ6+HY4pD62W1EOQs+/O71SxxolQaZ6T8hZY=

As the discussed example (and the example discussed last week) shows, Gallina/Coq is *not* SN, though as far as we know it *is* WN, which is enough for consistency.

This issue comes up regularly on the list, and I believe that the summary is as follows:

- It's extremely difficult for the theory to keep up with the practical demands of the system.

- We should be trying to have a reasonable meta-theory anyways.

- There are a few papers which prove normalization of various fragments and variants of Coq. However, I know of none that handle CiC + Impredicative Prop + Universes + Large Elimination (don't even ask about impredicative set!). I can try to list them if required, but I always worry about forgetting a crucial one.

- The above works are extremely technical and hard to fully check, this seems to be begging for a machine formalized proof.

- Such a proof is extremely tough, given the technical complexities involved, and the Godelian meta-theoretical issues (certainly something will have to be assumed as an axiom).

My constant call is for a more thorough exploration of the abstract structure of such proofs, so we can clearly separate it into combinatorial considerations + a model construction, which may be more tractable. There's a bunch of work on this as well, including the whole sub-field about normalization-by-evaluation, but CiC + universes seems a bit out of reach for now with such techniques, and again, writing down the whole construction is extremely tedious and error prone.

Hope this helps give the high overview,

Best,

Cody

On Thu, Dec 22, 2016 at 8:10 AM, Bas Spitters <b.a.w.spitters AT gmail.com> wrote:

This page refers to an example showing that Coq is not SN (due to the
guard condition).
https://coq.inria.fr/cocorico/CoqTerminationDiscussion

However, this (unpublished) report claims that CiC (with Prop and
universes) is SN.
http://csweb.rice.edu/uploadedFiles/Computer_Science/Research/Tech_Reports/TR11-01.pdf
Uniform Logical Relations - Eddy Westbrook

Has there been any progress on this? It would be good to update the
wiki/FAQ with this information.

[Coq-Club] Is Coq SN?, Bas Spitters, 12/22/2016
- Re: [Coq-Club] Is Coq SN?, roux cody, 12/22/2016
  - Re: [Coq-Club] Is Coq SN?, Gabriel Scherer, 12/22/2016
  - Re: [Coq-Club] Is Coq SN?, Bas Spitters, 12/23/2016