Stream: Coq users

Topic: Non termination with UIP

François Thiré (Aug 20 2020 at 07:25):

Looking at the doc on master, there is an example of a non-terminating term: https://coq.github.io/doc/master/refman/addendum/sprop.html?highlight=sprop#non-termination-with-uip . Termination is the key behind consistency (or at least weak normalization). I am not sur to understand the implication of this for the consistency of Coq. In particular, I am surprised that it is not mentioned in the documentation.

Karl Palmskog (Aug 20 2020 at 07:42):

is this a question or an observation? It's well known that some axioms are fine when added to Coq in isolation, but lead to inconsistency when combined (in this case, UIP and an impredicative Set/Type). More discussion on what axioms don't go together here: https://coq.discourse.group/t/what-do-you-think-of-axioms/231

François Thiré (Aug 20 2020 at 07:54):

I am trying to understand the implications here. Because from what I understand, Definitional UIP may reduce a match using a local hypothesis. Therefore if we follow the paper : https://arxiv.org/pdf/1911.08174.pdf , it says that normalisation breaks IIUC. So is it related to an extra axiom?
If just having Definitional UIP breaks normalisation (without other axioms), why is it interesting to activate it since it breaks consistency?

Gaëtan Gilbert (Aug 20 2020 at 07:57):

It doesn't break consistency

François Thiré (Aug 20 2020 at 07:59):

So you mean having a non-terminating term does not break the consistency? It is indeed clearly stated in the paper but I found it surprsing, thanks.

Pierre-Marie Pédrot (Aug 20 2020 at 09:29):

Consistency is broken by fixpoints, but a merely non-terminating term is not enough to break it.

Pierre-Marie Pédrot (Aug 20 2020 at 09:30):

You lose decidability of type-checking though...

Hugo Herbelin (Aug 20 2020 at 14:59):

By the way, would we lose something to restrict definitional UIP on equality-like types with indices in small types (i.e. types in Prop or Set)? The most interesting uses of SProp are with equality in data-types such as nat, no?

Hugo Herbelin (Aug 20 2020 at 15:14):

Also, I only recently started to explore what we can do with SProp, but would there be negative consequences of allowing elimination from SProp to Type for syntactic singleton types (i.e. not only from False:SProp but also from True:SProp, and:SProp->SProp->SProp)? Associated reduction rules could typically be derived as if eta-expanding on the fly.

Last updated: Sep 28 2023 at 10:01 UTC