# Function extensionality: does it make a difference? why would one keep it out of the axioms?

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).

-
Maybe you can find something by looking at the reference in the function extensionality entry at the nlab. – Michael Greinecker Jan 31 '14 at 4:04
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.) – Jason Rute Jan 31 '14 at 4:10
I don't know how relevant this is to your question, but strictly speaking two functions (e.g. in the sense of Bourbaki) could be different even if they agree on every input if their codomains are different. – Sam Hopkins Jan 31 '14 at 4:27
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. – მამუკა ჯიბლაძე Jan 31 '14 at 7:06
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. – Ketil Tveiten Jan 31 '14 at 8:20

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.)

-
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. – Andrej Bauer Jan 31 '14 at 16:43
@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. – Jonathan Sterling May 28 '14 at 2:30
@JonathanSterling: yes of course it is worth referring to Observational Type Theory (OTT), maybe even with a URL? That would be helpful. I disagree that a final "solution to quotients" was found by type theorists a decade ago. In fact, I would say we only know how to handle quotients of $0$-types (hsets). – Andrej Bauer May 28 '14 at 5:06
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). – Toby Bartels Jun 27 '14 at 3:37

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.

-
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. – darij grinberg Jan 31 '14 at 16:33
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. – Neil Strickland Jan 31 '14 at 16:39
What sort of theorem would you like to formalize? – Andrej Bauer Jan 31 '14 at 17:18

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.

-
What exactly is canonicity? And thanks for the link! – darij grinberg Jan 31 '14 at 16:34
Is canonicity the idea that the equality type should be an inductive type? – darij grinberg Jan 31 '14 at 16:37
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. – Christoph-Simon Senjak Feb 1 '14 at 0:14