Stream: Coq users

Topic: Choices for axioms


view this post on Zulip Patrick Nicodemus (May 28 2022 at 19:32):

I am fairly used to debates among mathematicians, constructivists, intuitionists etc. over principles like the law of excluded middle or the axiom of choice. However I am somewhat at a loss when it comes to some of the axioms that arise in type theory, like function extensionality.

I understand that when we assume an axiom we are fabricating an element of a type which cannot actually be constructed. So in the case of function extensionality, one is asserting that there's an inhabitant of the equality type.
This leads to something like

Definition p : f = g := (proof involving function extensionality)
Definition t : nat := match p  with
| refl f => 0
end

where the match statement will not simplify to zero because p is not constructed with refl. Therefore we have some blocked computation. This destroys canonicity because now we have a term of natural number type which is not a numeral. Ok.

However I don't really understand the practical repercussions of this. As a mathematician interested in formalizing mathematics can someone give me a reason why I might be concerned about this? What justification might someone have for trying to avoid this?

I guess in the case above, the term t is propositionally equal to zero even if not judgementally equal.

view this post on Zulip Ali Caglayan (May 28 2022 at 19:36):

Short answer: For mathematicians proving things, it mostly doesn't matter. For people wanting to compute things, it can get in the way. (The first group overlaps with the second).

view this post on Zulip Ali Caglayan (May 28 2022 at 19:37):

It is possible to come up with a model of type theory where function extensionality doesn't hold, but I don't know if that is of much interest to somebody formalizing mathematics unrelated to logic.

view this post on Zulip Stefan Monnier (May 28 2022 at 19:47):

Reminds me of a related question: contrary to some axioms like excluded middle, it's easy to provide a computation rule for FunExt which just returns refl, making it possible to compute with it. I think having such a computation rule in the empty context should be safe, but has anyone worked out the implications of having such a reduction rule in other (potentially inconsistent) contexts?

view this post on Zulip Gaëtan Gilbert (May 28 2022 at 19:54):

what does "safe" mean? refl does not have type (fun x : bool => x) = (fun x : bool => if x then true else false) so it would break subject reduction

view this post on Zulip Patrick Nicodemus (May 28 2022 at 20:30):

Ali Caglayan said:

Short answer: For mathematicians proving things, it mostly doesn't matter. For people wanting to compute things, it can get in the way. (The first group overlaps with the second).

Ok, this is helpful. This problem is intangible to me. Can you think of any good examples of computations we would want to carry out which would be hindered by assuming function extensionality? I am not sure whether the kinds of computations I'm interested in would be hindered by assuming this axiom. If I only use it for proving correctness results about algorithms rather than defining the algorithms themselves it should be fine.

view this post on Zulip Théo Winterhalter (May 28 2022 at 20:31):

I would guess that's basically it. If you only use it "at the end", for proving equalities, but not for defining programs, then you should be mostly fine.

view this post on Zulip Paolo Giarrusso (May 28 2022 at 20:41):

agree with Théo — the exception is ver e.g. if you use Definition some_function. ... rewrite foo. ... Defined., and foo is an equality proof that does not reduce to eq_refl (or is not even propositionally equal to it) because it is stuck on functional extensionality. However, such definitions are questionable even without axioms, because they'll often be stuck on Qed

view this post on Zulip Paolo Giarrusso (May 28 2022 at 20:41):

(https://gmalecha.github.io/reflections/2017/qed-considered-harmful has examples of the problems, but I would NOT recommend those solutions).

view this post on Zulip Paolo Giarrusso (May 28 2022 at 20:42):

(also OTOH, equalities on types with decidable equalities can be okay, since those equalities are provably proof irrelevant anyway)

view this post on Zulip Patrick Nicodemus (May 28 2022 at 21:49):

@Paolo Giarrusso Hm, ok so just to be sure I understand you correctly, if f, g are not themselves judgementally equivalent then we can never have that some p : f =g is even propositionally equivalent to refl, right? Because f =f and f=g are different types.

view this post on Zulip Patrick Nicodemus (May 28 2022 at 21:49):

Or do you mean up to transport along p or something?

view this post on Zulip Patrick Nicodemus (May 28 2022 at 21:50):

I am not sure if your point about decidable equality is meant to be directly related to the functional extensionality question.

view this post on Zulip Paolo Giarrusso (May 28 2022 at 21:56):

I probably spoke too quickly; the decidable equality point is about equalities which are "easier" to mix with data (the example I use most often is { x : T | bool_pred T = true })

view this post on Zulip Paolo Giarrusso (May 28 2022 at 21:58):

and it remains true that if you don't mix proofs and computations, you won't get stuck on funext in computation

view this post on Zulip Paolo Giarrusso (May 28 2022 at 21:59):

(at least IIANM)


Last updated: Feb 06 2023 at 12:04 UTC