52

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

Community
  • 1
darij grinberg
  • 33,095
  • 2
    Maybe you can find something by looking at the reference in the function extensionality entry at the nlab. – Michael Greinecker Jan 31 '14 at 04:04
  • 13
    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 04:10
  • 1
    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 04:27
  • 3
    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 07:06
  • 8
    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 08:20
  • 2
    @SamHopkins: This is not what I'm talking about; the type signatures are the same for both functions. – darij grinberg Jan 31 '14 at 16:22
  • 1
    @KetilTveiten: A proof that f(x) = g(x) for all x does yield a way to translate proofs for f(x) = y into proofs for g(x) = y. The translation is not direct rewriting using $\beta\delta\iota\zeta\epsilon$ (otherwise the proof wouldn't be necessary), but it follows from the proof. – darij grinberg Jan 31 '14 at 16:24
  • @JasonRute: This sounds like it could be their reason! So they really mean functions == algorithms, not functions == algorithms modulo equivalence. (I'm still wondering about question 2., i. e., how much difference this makes.) – darij grinberg Jan 31 '14 at 16:25
  • @MichaelGreinecker: I'll have to admit this is not something nlab is illumating for me (all I got out of the page was that univalence implies function extensionality, but I don't want to assume univalence -- it certainly adds more strength than I wish for). – darij grinberg Jan 31 '14 at 16:26
  • @darijgrinberg: You're probably right, like I said I remember this only vaguely from listening to my friend talk about his multiset-based model of type theory (or whatever it was). – Ketil Tveiten Jan 31 '14 at 20:09

3 Answers3

60

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

Andrej Bauer
  • 47,834
  • Thanks for the reply! +1 (but no accept because I'd really love to see question 2. answered, nothing personal). So funext would break some normalization/diamond properties that equalities otherwise have? Also, a quick remark: I abused "deny" to mean "leave out of the axioms". (I have yet to see an axiom whose pure negation would be of any interest.) Is "not accept" really much less confusing? If so, I'll fix the title. – darij grinberg Jan 31 '14 at 16:31
  • 4
    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
  • Thanks -- I accepted the answer and edited the question. If you could hint me towards a setoid tutorial (for Coq), I'd be particularly indebted. – darij grinberg Jan 31 '14 at 16:47
  • 5
    "HoTTest open problem" :) – Jason Rute Jan 31 '14 at 20:31
  • 5
    That's nothing, ask Google about HoTT models. – Andrej Bauer Feb 01 '14 at 07:16
  • 4
    @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 02:30
  • To elaborate, if all you want is funext and quotients in ITT, you need only look back a decade to find all the tools you need to construct them without resorting to a clunky setoid construction. HoTT is awesome, but we don't need to figure out the computational content of univalence just to get extensionality principles for hsets. – Jonathan Sterling May 28 '14 at 02:34
  • 1
    @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 05:06
  • 1
    Here's a link to the relevant paper: Observational Equality, Now!.

    All I claimed is that an explicit setoid construction is not necessary to get proper equality for functions and quotients of hsets. It is very unlikely that the original post had in mind an extensional equality for anything higher than hsets. It will be very interesting to watch type theorists make extensionality principles for types in general compute, of course!

     – Jonathan Sterling May 28 '14 at 17:42
  • 7
    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 03:37
  • 1
    "To use Russell's example, intensionally the morning star and the evening star are clearly not the same " - Isn't it Frege's example from Über Sinn und Bedeutung (1892)? – Bruno Bentzen Dec 30 '15 at 03:19
  • Possibly yes, I read it somewhere in Russell and wasn't careful about the fact that he could have picked it up from Frege. – Andrej Bauer Dec 30 '15 at 09:27
  • If "automagically" was a typo and you meant "automatically", then I think it should still not be corrected: "automagically" is a great portmanteau! – Todd Trimble Sep 02 '16 at 12:08
  • @ToddTrimble the word has a longer history than you realise – Ben Millwood Sep 27 '16 at 16:00
  • @BenMillwood: it's dangerous to introduce mathematicians to the jargon file. They'll start saying things like "I had a nasty bug. It turned out to be an Obi-Wan." – Andrej Bauer Sep 27 '16 at 16:23
  • @BenMillwood Thanks for educating me here (although the application of the word, as for example in Andrej's post, seems to be wider than what was explained in the jargon file). Here's another place where '-matic' is changed to '-magic': http://www.kurims.kyoto-u.ac.jp/EMIS/journals/SLC/wpapers/s44cartier1.pdf – Todd Trimble Sep 29 '16 at 13:41
  • Equally cute :) – Ben Millwood Sep 29 '16 at 14:27
  • I don't understand why is addition of natural numbers not judgmentally commutative. Isn't it true that if two functions are pointwise judgmentally equal then they are judgmentally equal? Then considering addition and addition with transposed arguments as terms of $\mathbb{N}\to\mathbb{N}\to\mathbb{N}$ we can prove judgmental equality for a fixed value of the first parameter and from that conclude judgmental equality. – Faris Feb 14 '21 at 05:08
  • @Faris: you can prove for any closed terms $e_1$ and $e_2$ that $e_1 + e_2 \equiv e_2 + e_1$, but you cannot prove the judgemental equality $x + y \equiv y + x$ where $x$ and $y$ are variables. The induction principle for the natural numbers works on types, not judgemental equalities. – Andrej Bauer Feb 14 '21 at 09:24
  • Thank you for your explanation. Then I wonder for which types $T$ is it true that given any two closed terms $t, t':T$ if the type $\mathrm{Id}_{T}(t, t')$ is inhabited then $t\equiv t'$? This is of course a metatheoretical property because it features judgmental equality. It seems to hold for $\mathbb{N}$ and also for any type with only finitely many judgmentally distinct closed terms. As you point out it's not true for $\mathbb{N}\to\mathbb{N}\to\mathbb{N}$. – Faris Feb 17 '21 at 09:01
  • That would be all types, at least in a strongly normalizing theory. Suppose $p : \mathrm{Id}_T(t, t')$. Because $p$ is closed it normalizes to $\mathrm{refl}$, therefore $t \equiv t'$. – Andrej Bauer Feb 17 '21 at 09:14
  • Thank you. So then if we defined addition as a closed term $\mathrm{add}:\mathbb{N}\times \mathbb{N}\to\mathbb{N}$ and considered the transposition of arguments $\mathrm{tr}:(\mathbb{N}\times \mathbb{N}\to\mathbb{N})\to (\mathbb{N}\times \mathbb{N}\to\mathbb{N})$ the judgment $\mathrm{tr}(\mathrm{add})\equiv \mathrm{add}$ would hold? – Faris Feb 17 '21 at 13:10
  • No it would not. How do you indent to prove $\mathrm{Id}(\mathrm{tr}(\mathrm{add}), \mathrm{add})$? – Andrej Bauer Feb 17 '21 at 13:36
  • I see. But then the sentence "The intensional one is called "judgmental" or "definitional equality" $\equiv$ and the extensional one is known as "propositional equality" $=$" in your answer is misleading (since $\mathrm{add}$ and $\mathrm{tr}(\mathrm{add})$ are not propositionally equal but are extensionally equal). – Faris Feb 28 '21 at 10:26
  • $\mathrm{tr}(\mathrm{add})$ and $\mathrm{add}$ cannot be proved to be equal in any sense, extensional or intensional. You might be confusing $\mathrm{Id}(\mathrm{tr}(\mathrm{add}), \mathrm{add})$ and $\Pi(x, y : \mathbb{N}) , \mathrm{Id}(\mathrm{tr}(\mathrm{add})(x,y)), \mathrm{add}(x,y))$ (that's another notion of equality for functions, confusingly know as "extensional equality of functions"). – Andrej Bauer Mar 01 '21 at 07:07
  • But then doesn't extensional equality always imply intensional equality? Can you specify a type system, a type in it and two terms of that type that are extensionally equal but not intensionally equal? As you say $\mathrm{add}, \mathrm{tr}(\mathrm{add}):\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ in Martin-Löf type theory doesn't work since these terms are neither extensionally equal nor intensionally equal. – Faris Mar 01 '21 at 12:12
  • Sure, let $\Gamma$ be the context $m : \mathbb{N}, n : \mathbb{N}, p : \mathrm{Id}(m, n)$. Then $\Gamma \vdash p : \mathrm{Id}(m, n)$ but $\Gamma \not\vdash m \equiv n : \mathbb{N}$. In pure Martin-Löf type theory this is the best we can do (i.e., for closed term propositional equality implies judgemental equality). If we pass to some other kind of type theory, such as Observational type theory, then we will have "real" example (in OTT $\mathrm{tr}(\mathrm{add})$ and $\mathrm{add}$ are closed terms that are propositionally equal but not judgementally equal). – Andrej Bauer Mar 01 '21 at 13:28
17

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

Christoph-Simon Senjak
  • 757
16

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.

Neil Strickland
  • 55,003
  • 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
  • 4
    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