52
$\begingroup$

Yesterday I was shocked to discover that function extensionality (the statement that if two functions $f$ and $g$ on the same domain satisfy $f\left(x\right) = g\left(x\right)$ for all $x$ in the domain, then $f = g$) is not an axiom in the standard constructive logic of Coq. Of course, one can add it as an axiom in one's files, but it is not obviously available in any pre-defined tactics. I am left wondering...

1. What is the thinking behind considering function extensionality as foreign to the calculus of constructions? I thought that from a computational perspective, a function really is there to be applied to things, and cannot carry any more information than what it does to them (and its type). For a moment I suspected that Coq avoids function extensionality in order to allow applying results to models like arbitrary enriched categories whose internal homomorphisms carry some more information than plain morphisms. But this is not the case: Coq (since version 8.4) has a implementation of eta-expansion (saying that any function $f$ equals the function sending every $x$ in its domain to $f\left(x\right)$, provided the types are right). In an enriched category, this would pour any additional structure of an internal Hom down the drain. (I must say the eta-expansion in Coq feels rather weird, too -- it is triggered by the reflexivity tactic. I expected it to be a tactic on its own...) Having eta-expansion but no extensionality is seriously confusing: one can have $f\left(x\right) = g\left(x\right)$ for all $x$, and yet one cannot rewrite the $f\left(x\right)$ in "the function sending every $x$ to $f\left(x\right)$" as a $g\left(x\right)$. And there I thought the bound variable in a lambda term would be like the bound variable in a forall quantification?

2. On a more practical note (and more on-topic in MathOverflow), how much do the axiom of function extensionality and the (weaker) axiom of eta-expansion contribute to the strength of the logic? (At this point I have to admit that I don't really know the definition of the logic involved, so I'll just say I'm talking about the logic of Coq with no additional axioms assumed; it has so far been agreeing with my intuitive understanding of constructivism, until extensionality came along.) If I can define two terms $a$ and $b$ of type $\mathrm{nat}$ (natural numbers) and use function extensionality (resp. eta-reduction, both ways) to prove their equality, can I also do it without? If I can prove a (more complicated) statement using function extensionality, is there a way to transform it into a (possibly clumsier) statement which can be proven without function extensionality and which can be transformed into the former statement using some straightforward applications of function extensionality?

I'm sorry for logical naivety. The way I am posing the question, I fear it would qualify as soft; nevertheless I am pretty sure that there is some precise statements to be made here (or maybe just a reference to a textbook to be given).

$\endgroup$
10
  • 2
    $\begingroup$ Maybe you can find something by looking at the reference in the function extensionality entry at the nlab. $\endgroup$ Jan 31, 2014 at 4:04
  • 13
    $\begingroup$ One way I have heard this explained is that a constructive way to view equality of functions is as equality of the computer programs that output those functions. Two functions may extensionally give the same output, but intensionally be very different. For example, the function f(n)="0 unless 2n+1 is perfect" and the constant function g(n) = 0 are very different in a sense. I think this distinction between extensional/intentional is very important in constructive reasoning. (That being said, I think you are asking something more specific and technical. Hence this is just a comment.) $\endgroup$
    – Jason Rute
    Jan 31, 2014 at 4:10
  • 3
    $\begingroup$ In fact it might be true that for any intensional notion of function (say, polynomial, etc.) one might extend the domain of application in such a way that extensionality will hold. Example: polynomials over a finite field cannot be extensional (there are infinitely many of them); however one may apply such a polynomial to any element of any algebra over this field, and in this broader context extensionality will hold. There must be an abstract-nonsensical very general version of this. $\endgroup$ Jan 31, 2014 at 7:06
  • 8
    $\begingroup$ I'm no expert, but if I recall correctly from my conversations with my constructivist logician colleague, it isn't enough that two functions agree on all points; they are only equal (constructively) if every proof for "f(x)=y" is translatable into a proof of "g(x)=y", or something like that. I'll ask him if he shows up today. $\endgroup$ Jan 31, 2014 at 8:20
  • 2
    $\begingroup$ @SamHopkins: This is not what I'm talking about; the type signatures are the same for both functions. $\endgroup$ Jan 31, 2014 at 16:22

3 Answers 3

60
$\begingroup$

I am going to draw heavily from Github discussion on HoTT book pull request 617.

There are different kinds of equality. Let us say that equality is "intensional" if it distinguishes objects based on how they are defined, and "extensional" if it distinguishes objects based on their "extension" or "observable behavior". In Frege's terminology, intensional equality compares sense and extensional equality compares reference.

To use Russell's example, intensionally the morning star and the evening star are clearly not the same (because their definitions are different), but they are extensionally the same because they both denote the same object (planet Venus). A more mathematical example is comparison of $x + y$ and $y + x$. These are extensionally equal, but intensionally differ because (the usual) definition of $+$ treats its arguments asymmetrically. It should be clear that two functions may be extensionally equal (have same behavior) even though they differ intensionally (have different definitions).

It is possible for two kinds of equality to coexist. Thus in type theory there are two equalities. The intensional one is called "judgmental" or "definitional equality" $\equiv$ and the extensional one is known as "propositional equality" $=$. Mathematicians are aware of $=$ as a "real thing" while they think of $\equiv$ as "formal manipulation of symbolic expressions" or some such.

We may control the two kinds of equality and the relationship between them with additional axioms. For instance, the reflection rule collapses $\equiv$ and $=$ by allowing us to conclude $a \equiv b$ from $a = b$ (the other direction is automatic). There are also varying degrees of extensionality of $=$. Without any extra axioms, $=$ is already somewhat extensional. For instance, we can prove commutativity of $+$ on natural numbers by induction in the form $x + y = y + x$, but we cannot prove $x + y \equiv y + x$. Function extensionality is an axiom which describes what constitutes an "observation" on functions: by saying that two functions are equal when they give equal values we are in essence saying that only values matter (but not for example the "running time" or some other aspect of evaluation). Another axiom which makes $=$ "more extensional" is the Univalence axiom.

It is hard to do mathematics without function extensionality, but type theorists have their reasons for not including it as an axiom by default. But before I explain the reason, let me mention that there is a standard workaround. We may introduce user-defined equalities on types by equipping types with equivalence relations. This is what Bishop did in his constructive mathematics, and this is what we do in Coq when we use setoids. With such user-defined equalities we of course recover function extensionality by construction. However, setoids are often annoying to work with, and they drag in technical problems which we would prefer to avoid. Incidentally, the setoid model shows that function extensionality does not increase the power of type theory (it is a model validating function extensionality built in type theory without function extensionality).

So why don't type theorist adopt function extensionality? If we want to have a type theory with nice properties, and a useful proof assistant, then $\equiv$ should be "easy" to deal with. Technically speaking, we would like a strongly normalizing $\equiv$. By assuming function extensionality we throw into type theory a new constant funext without explaining how it interacts with the process of strong normalization, and things break. Type theorists would say that we failed to explain the computational meaning of funext.

Consequently, Coq does not adopt function extensionality because that would lead to a lot of problems. Coq would not be able to handle $\equiv$ automagically anymore, and the whole system would just have worse behavior. Type theorists of course recognize that having a good computational explanation of function extensionality, and more generally of the univalence problem, would be extremely desirable. This is why the HoTTest open problem is to give a computational interpretation of the univalence axiom. Once this is accomplished, we ought to have at our disposal type systems and proof assistants which are much more natural from a mathematician's point of view. Until then, you can always assume funext as an axiom and work around the resulting complications. To see how this can be done, have a loot at the Funext axiom in the HoTT library.

[This P.S. is outdated after the question was edited.] P.S. The title of your question points to a common leap of reasoning from "not accepting function extensionality" to "denying function extensionality". While there are models in which function extensionality has counter-examples, one should be aware of the difference between "not accept" and "deny". (I am complaining because this sort of leap is often made about the law of excluded middle, and there it leads to absurdity.)

$\endgroup$
27
  • 4
    $\begingroup$ Oh. I updated my answer to make it clear that the setoid model shows that function extensionality does not add any power, in the sense that we can build a model satisfying it starting from a theory without function extensionality. Regarding "not accept" versus "deny", I suggest strongly that you do not confuse them. There are a lot of ordinary mathematicians who confuse "not accept excluded middle" with "deny excluded middle". Because the denial of excluded middle is false (constructively and otherwise), they then wrongly conclude that constructive mathematicians are crazy. $\endgroup$ Jan 31, 2014 at 16:43
  • 5
    $\begingroup$ "HoTTest open problem" :) $\endgroup$
    – Jason Rute
    Jan 31, 2014 at 20:31
  • 5
    $\begingroup$ That's nothing, ask Google about HoTT models. $\endgroup$ Feb 1, 2014 at 7:16
  • 4
    $\begingroup$ @AndrejBauer: I don't think it's accurate to say that having a computational interpretation of function extensionality is "desirable", as though we do not already have one. Indeed, the only extensionality principle that (so far) lacks a satisfying computational interpretation is univalence. Since the 90s, we have known how to integrate extensionality principles like funext into intensional type theory by internalizing the setoid construction you mention into the syntax of TT itself. Altenkirch/McBride's OTT is an example of doing this which does not lose any of the nice properties of ITT. $\endgroup$ May 28, 2014 at 2:30
  • 7
    $\begingroup$ It is (or can be) consistent even to deny excluded middle, just not to deny any instance of it. That is, you may assert $\neg(\forall P\colon \operatorname{Prop}, P \vee \neg{P})$ but not $\exists P\colon \operatorname{Prop}, \neg(P \vee \neg{P})$. The Russian and intuitionistic schools of constructivism do this (not directly, but as a consequence of other, more interesting axioms). $\endgroup$ Jun 27, 2014 at 3:37
17
$\begingroup$

You will lose canonicity, which is - mathematically - not that much of a problem, but when you want to extract programs, you want it. The problem is that not every proof of equality reduces to reflexivity.

See also http://coq.inria.fr/cocorico/extensional_equality

$\endgroup$
4
  • $\begingroup$ What exactly is canonicity? And thanks for the link! $\endgroup$ Jan 31, 2014 at 16:34
  • $\begingroup$ Is canonicity the idea that the equality type should be an inductive type? $\endgroup$ Jan 31, 2014 at 16:37
  • 6
    $\begingroup$ Canonicity means that every closed term of an inductive type normalizes into its canonical form, which is a term only containing its constructors. Like everything of type Nat normalizing to SSS...S0. $\endgroup$ Feb 1, 2014 at 0:14
  • $\begingroup$ I wonder if you can restrict this to Prop. Something like forall (a : Type) (b : Prop) (forall (x : a), f x = g x) -> f = g $\endgroup$ Feb 17, 2021 at 21:28
16
$\begingroup$

This worried me a lot when I started using Agda, but I got used to it. I expect that the issues in Coq are similar. The basic point is that one should not think of equality as being so important. In classical mathematics equality is very basic, and we routinely use quotient sets to replace the statement "$a$ is equivalent to $b$" by the apparently simpler statement that the equivalence class of $a$ is equal to the equivalence class of $b$. However, in a constructive framework this is not very natural. You need to keep hold of the equivalence relation and remember the proof that $a\sim b$ as an additional piece of data which can itself be fed into other functions and so on. Most of the time you end up working with "setoids", ie sets equipped with a specified equivalence relation; very few interesting mathematical structures can be constructed without an equivalence relation creeping in somewhere. After a while you get used to the idea that equality is not much better than other equivalence relations. So you can introduce extensional equality as a new equivalence relation, and not worry about the fact that it is different from the intensional version.

$\endgroup$
3
  • $\begingroup$ OK, so I take it I should learn about setoids before doing even elementary combinatorics. I hoped this wasn't the case (I specifically wanted to start formalizing combinatorics because I expected that all the foundational complications only creep in when one starts doing algebra) but I guess it's an issue that has to be faced. $\endgroup$ Jan 31, 2014 at 16:33
  • 4
    $\begingroup$ If you want to do elementary combinatorics then you can try working only with sets like $\{0,\dotsc,n-1\}$ and encoding functions as lists of values; then you will have extensionality. This kind of approach runs out of steam after a while, but it may be good to get started. $\endgroup$ Jan 31, 2014 at 16:39
  • $\begingroup$ What sort of theorem would you like to formalize? $\endgroup$ Jan 31, 2014 at 17:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.