Stream: MetaCoq

Topic: properties of MetaCoq/PCUIC


view this post on Zulip walker (Oct 20 2022 at 11:56):

I understand that strong normalization of PCUIC terms is not proven in metacoq, and the property is turned into Axiom.

I understand the general idea of godel incompleteness but not the details on any level and from there I have four questions:

1- what inspires confidence that PCUIC is strong normalizing if we cannot prove it in Coq ?
2- is there an axiom-free system stronger than Coq that can prove normalization of PCUIC ?
3- if yes then why that system is not the base for Coq ?
4- If yes .. lets call that system "FOO" and I will be asking again the previous 4 questions for FOO instead of PCUIC (It sounds ridiculus but I want to know how to get system with no trusted computing base, if possible).
Edit:
5- given that PCUIC is encoded in coq, does that mean PCUIC is strongly normalizing iff coq is strongly normalizing (implicitly)?

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2022 at 12:17):

Your point 4. is unrelated to the TCB, it's a foundational regression ad infinitum.

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2022 at 12:18):

In theory you could prove that CIC has all the good metatheoretical properties on paper in ZFC + ω universes

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2022 at 12:18):

but this does not affect the code

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2022 at 12:21):

As for the other points:

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2022 at 12:22):

but probably the most important thing about reasonable type theories is that you don't really care about SN in practice. What matters for inspectability of proofs is that they can be run (in theory) and you can check that on Σ01 formulae you get something that makes sense.

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2022 at 12:22):

if it converges, you're fine, otherwise just wait a bit more.

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2022 at 12:23):

The things one should be concerned about when talking about SN are the gaps between CIC as implemented in Coq, and the smaller toy theories.

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2022 at 12:24):

Typical sources of concern of mine: Prop, the guard condition, modules

view this post on Zulip walker (Oct 20 2022 at 12:57):

I assumed that type systems are axiom free, they come with judgements and indution principle.

I am sure what is Σ01 formulae,

Also can you point me to a simple proof layout for one of those languages with some form of dependent types ?

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2022 at 13:09):

this is probably the best you can find publicly: https://github.com/mr-ohman/logrel-mltt

view this post on Zulip Paolo Giarrusso (Oct 22 2022 at 01:14):

I am sure what is Σ01 formulae

If you're not sure, I understand https://en.wikipedia.org/wiki/Arithmetical_hierarchy is relevant

view this post on Zulip Kenji Maillard (Oct 22 2022 at 09:27):

I don't know how faithful it is, but whenever I talk with @Pierre-Marie Pédrot and he mentions a property only valid of Σ10\Sigma^0_1 formula I automatically translate that in my head into "plain finitary inductive data-types" (that do not involve functions for instance).

view this post on Zulip walker (Oct 22 2022 at 10:56):

Paolo Giarrusso said:

I am sure what is Σ01 formulae

If you're not sure, I understand https://en.wikipedia.org/wiki/Arithmetical_hierarchy is relevant

oh that was one crucial missing word I meant "I am not sure" ...

view this post on Zulip Pierre-Marie Pédrot (Oct 22 2022 at 11:01):

not only finitary, stuff like Σn : nat. n = 0 is also fine.

view this post on Zulip Kenji Maillard (Oct 22 2022 at 11:18):

Pierre-Marie Pédrot said:

not only finitary, stuff like Σn : nat. n = 0 is also fine.

That's composed only of finitary inductives (finitary != finite)

view this post on Zulip Paolo Giarrusso (Oct 22 2022 at 12:55):

Ooooh! Sigma01 etc is about first-order arithmetic not logic, and that's why you can't say "exists f : nat -> nat. ..."

view this post on Zulip Paolo Giarrusso (Oct 22 2022 at 12:56):

(and yes, I understand quantifying over any sort of syntax for such functions is fine)

view this post on Zulip Paolo Giarrusso (Oct 22 2022 at 13:01):

@Kenji Maillard so I guess in first-order arithmetic you can only quantify over N, and today we can take for granted that adding finitary data types is conservative thanks to Gödelization?

view this post on Zulip Paolo Giarrusso (Oct 22 2022 at 13:05):

IIUC, a signature for a finitary datatype induces a specification, and Gödelization shows that you can implement it using nat as support, and primitive recursive functions for the introduction and elimination arrows?

view this post on Zulip Paolo Giarrusso (Oct 22 2022 at 13:08):

My first guess was "Gödelization implements parsing and printing", but "parsing" can't be a function inside Peano arithmetic; you'd have to compose your functions on inductive type T with the T <-> nat isomorphism, normalize, and prove that T can be completely removed...

view this post on Zulip walker (Oct 22 2022 at 13:12):

I am not sure I understand and the wikipedia isn't making things simpler. :(

view this post on Zulip Paolo Giarrusso (Oct 22 2022 at 13:14):

Sorry, what I just wrote needs context, but you can ignore that

view this post on Zulip Paolo Giarrusso (Oct 22 2022 at 13:15):

Sigma 01 just means a formula in peano arithmetic which can start with "exists a, b, c : nat, ..." and use no other quantifiers

view this post on Zulip Paolo Giarrusso (Oct 22 2022 at 13:16):

if you have other datatypes for "syntax" they can be encoded, but that's the trickier part

view this post on Zulip Paolo Giarrusso (Oct 22 2022 at 13:16):

Does that make sense @walker ?

view this post on Zulip walker (Oct 22 2022 at 13:19):

yes, but how does this form of statements relate to showing that PCUIC can be used as logic?

view this post on Zulip Paolo Giarrusso (Oct 22 2022 at 13:22):

I also wanted to ask! All I can see is that it's good for testing: running such a proof gives me witnesses for the existentials, and a proof of a decidable property.

view this post on Zulip Paolo Giarrusso (Oct 22 2022 at 13:23):

(because quantifier-free properties in Peano arithmetic are decidable?)

view this post on Zulip Paolo Giarrusso (Oct 22 2022 at 13:25):

So if after reduction you get (n, p) : exists n, P n, then you can double-check independently that P n holds.

view this post on Zulip Paolo Giarrusso (Oct 22 2022 at 13:28):

But not sure if this is what @Pierre-Marie Pédrot is thinking about

view this post on Zulip Pierre-Marie Pédrot (Oct 22 2022 at 21:00):

Indeed this is what I had in mind.


Last updated: Feb 04 2023 at 01:03 UTC