Extensional theorems mostly used intensionally - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-19T22:10:14Z http://mathoverflow.net/feeds/question/18848 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/18848/extensional-theorems-mostly-used-intensionally Extensional theorems mostly used intensionally Jacques Carette 2010-03-20T15:51:44Z 2010-06-29T07:41:45Z <p>Some theorems are stated and proved extensionally, but in practice are almost always used <a href="http://plato.stanford.edu/entries/logic-intensional/" rel="nofollow">intensionally</a>. Let me give an example to make this clear -- integration by parts: $$\int_a^b f(x)g'(x)ds = \left[f(x)g(x)\right]_a^b - \int_a^b f'(x)g(x) dx$$ for two continuously differentiable functions $f$ and $g$. In practice, this is seldom ever applied to <i>functions</i> but rather to <i>expressions</i> denoting functions. Much more importantly, it is almost always applied by 'pattern matching' on a product <i>term</i>. But note that integration is usually described formally as an operation on <i>functions</i> (i.e. extensional objects), but then in first-year calculus the students are taught to master a series of rewrite rules (i.e. operations on intensional objects).</p> <p>Logicians [Leibniz, Frege, Russell, Wittgenstein, Quine, Carnap to name a few] have worried a lot about this. Linguists [Montague comes to mind], and physicists [A. Bressan] have worried about this too.</p> <p>I have two questions:</p> <ol> <li>What other examples have you run into of such mixing of extension and intension?</li> <li>Why is this dichotomy not more widely taught / appreciated?</li> </ol> <p>In the case of algebra (more precisely, equational theories), the answer to #2 is very simple: because this dichotomy does not matter at all, because we have well-behaved adjunctions between the extensional and intensional theories [in fact, we often have isomorphisms]. For example, there is no essential difference between polynomials (over fields of characteristic 0) treated syntactically or semantically. But there is a <b>huge</b> difference between terms in analysis and the corresponding semantic theorems.</p> http://mathoverflow.net/questions/18848/extensional-theorems-mostly-used-intensionally/18857#18857 Answer by Noam Zeilberger for Extensional theorems mostly used intensionally Noam Zeilberger 2010-03-20T16:53:08Z 2010-03-20T16:53:08Z <p>An example of (1) comes from the proof theory of arithmetic, and the way we view proofs of universal statements about the natural numbers. <a href="http://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof" rel="nofollow">Gentzen's original consistency proof</a> took an intensional view, reasoning explicitly about eigenvariables and induction. Schütte later gave a much simpler consistency proof based on an extensional view, where mathematical induction was eliminated in favor of the so-called "$\omega$-rule", an infinitary inference rule which asserts $\forall x.A(x)$ given proofs of $A(n)$ for all $n\in \mathbb N$.</p> <p>Buchholz has <a href="http://www.mathematik.uni-muenchen.de/~buchholz/articles/kgc97.ps" rel="nofollow">connected the two approaches</a>, showing how Gentzen's result can be reconstructed by translation into Schütte's sequent calculus, essentially by reading off the infinite extension of finite, intensionally-defined proofs. (He calls this viewing finite derivations as "notations for infinitary derivations".) There is certainly a much stronger asymmetry here, because once you take an extensional view of primitive recursive functions over the natural numbers, you can't go back to a (finite) symbolic view.</p> http://mathoverflow.net/questions/18848/extensional-theorems-mostly-used-intensionally/18888#18888 Answer by Terry Tao for Extensional theorems mostly used intensionally Terry Tao 2010-03-21T01:02:19Z 2010-03-21T01:26:40Z <p>It seems to me that the mathematical equivalent of the intensional vs. extensional distinction in philosophy would be the distinction between "formal" vs. "functional" objects: formal power series vs. convergent power series, formal integration by parts (with no regard for checking the validity of the operation in a real analysis sense) vs. rigorous integration by parts, formal polynomials vs. functions which happen to be represented by a polynomial, etc. If so, I would say that the formal vs. functional distinction is usually dealt with in more advanced classes, though usually not at the first-year undergraduate level. </p> <p>For instance, in algebra, the concept of an indeterminate variable (and its distinction from the set-theoretic notion of a variable in a fixed domain) tends to be sufficient for keeping the two concepts distinct in most situations involving set-theoretic functions and the formal expressions giving rise to those functions. In particular, polynomials can be formal by living in some polynomial ring $R[x]$ generated by an indeterminate $x$, rather than having to be set-theoretic functions on some domain. Algebraic geometry also takes particular care in distinguishing an ideal of polynomials from the set-theoretic locus that that ideal cuts out over a given field, or more generally by distinguishing a scheme from a variety.</p> <p>Similarly, real analysis, with all its cautionary counterexamples as to how various formal operations (e.g. exchanging limits or sums) can lead to disaster if the appropriate functional hypotheses are not verified, also tends to be pretty good about distinguishing a formal computation from a functional one; often the former is used as an initial heuristic motivation only, with the latter then being brought in for the rigorous proof. Although certainly mistakes have been made by treating a formal computation as if it were functionally valid...</p> <p>Related to this is the ubiquitous "abuse of notation" in which a package of objects, structures, and forms is referred to via its most prominent component (i.e. by synecdoche). Thus, for instance, one often sees a polynomial function $P: {\bf R} \to {\bf R}$ being used to simultaneously represent both the polynomial function and the formal polynomial that represents it, or vice versa (e.g. "the polynomial $x^2$" to refer to the function $x \mapsto x^2$). Another common instance of this is when dealing with spaces (sets with additional structure); one often abuses notation by using the set itself to denote the space, e.g. a group might be denoted by its set $G$ of elements, rather than by the tuple $(G, e, \cdot, ()^{-1})$ of group structures, or a set-theoretic function by just the mapping $f$, rather than than the triplet $(f,X,Y)$ that includes the domain and codomain of that mapping. Such abuses are technically illegal using the strictest interpretations of mathematical notation, but they save a lot of space and, when used correctly, allow readers to focus on the actual content of an argument rather than on its formalism. Still, it is useful and important to point these abuses out explicitly from time to time...</p> http://mathoverflow.net/questions/18848/extensional-theorems-mostly-used-intensionally/21404#21404 Answer by Jacques Carette for Extensional theorems mostly used intensionally Jacques Carette 2010-04-14T23:59:49Z 2010-04-14T23:59:49Z <p>A recent question about <a href="http://mathoverflow.net/questions/21202/what-is-the-combinatorial-intepretation-to-this-identity" rel="nofollow">combinatorial interpretations</a>, namely to find an interpretation for the identity</p> <p>$$\sum_{k=0}^m 2^{-2k} \binom{2k}{k} \binom{2m-k}{m}=4^{-m} \binom{4m+1}{2m}$$</p> <p>gives another full class of such issues. This equation is much more than a tautology when interpreted intensionally as being about combinatorics: a combinatorial interpretation involves give a natural class $C_l$ of objects for the left-hand-side and $C_r$ for the right-hand side and a bijection between these classes. Furthermore, and this is where things get really interesting (with respect to my original question), such classes $C_l$ and $C_r$ would be considered 'natural' if by using the usual rules of combinatorial counting, we would naturally get that the number of objects of $C_l$ of size $m$ is the left-hand side expression (similarly for $C_r$ and the rhs). The point is that these counting expressions would be derived structurally from the combinatorial classes. This is a much more interesting interplay between 3 extensional objects (a counting function and 2 combinatorial classes) and 2 intensional ones (different-but-equal formulas representing the counting function).</p> http://mathoverflow.net/questions/18848/extensional-theorems-mostly-used-intensionally/27733#27733 Answer by T. for Extensional theorems mostly used intensionally T. 2010-06-10T18:50:36Z 2010-06-10T18:50:36Z <p>Is there a formal definition of the intension/extension distinction, or even of "intension" and "extension" as separate terms?</p> <p>In the examples discussed here, the difference is simply that there is a richer type of object A, carrying its own set of allowed operations and relations, that maps (maybe in partially-defined way) to a coarser type of object B. The coarser thing B could be, as in the examples posted, a "forgetting of structure" or "de-categorification" or "numerical evaluation" of A. Some of the allowed operations on A's will not work perfectly or unambiguously on B's per se due to the loss of structure. For example, replacing $(x-1)/(x-1)$ by $1$ is correct for (intensional, formal) rational functions but requires additional input (a domain) to be defined unambiguously for (extensional, numerical) rational functions. The possibly missing additional structure can be seen as a reinstatement of the information lost when passing from A to B, or rigidification data needed to disambiguate the operations on B.</p> <p>From this point of view, intension seems to be just a specification of context A, and an extensional interpretation of such a context is a specification of a map from A to some other, usually less structured, context B. Is there more to this distinction as it appears in the philosophy or computer science literature?</p> http://mathoverflow.net/questions/18848/extensional-theorems-mostly-used-intensionally/29775#29775 Answer by Russell O'Connor for Extensional theorems mostly used intensionally Russell O'Connor 2010-06-28T12:09:21Z 2010-06-29T07:41:45Z <p>Georges Gonthier and François Garillot are doing interesting things with phantom types and unification in Coq to allow one to write, for example, <code>directv (V + W)</code> to mean the proposition that $V \oplus W$ is a direct sum.</p> <p>I haven't fully grasped how it works yet, but let me give you a simplified explanation of what I think is going on. What is happening is that <code>directv X</code> is really notation for <code>directv_def _ (Phantom _ X)</code>.</p> <p><code>Phantom</code> is a constructor of a very trivial inductive type</p> <pre><code>Inductive phantom (A:Type) (a:A) : Type := Phantom : phantom A a </code></pre> <p>The function <code>Phantom</code> is a polymorphic constructor of type <code>forall (A:Type)(a:A), phantom A a</code>. The purpose of <code>Phantom</code> is to lift values to the type level so that type inference can operate on these values.</p> <p><code>directv_def</code> doesn't even use the <code>(Phantom _ X)</code> argument (because it contains no data). The only purpose of this argument is to drive the type inference engine to fill in the first argument. <code>directv_def</code> has type <code>forall (VW : addv_expr) (_ : phantom _ (Vadd VW)), Prop</code>. <code>addv_expr</code> is a record type.</p> <pre><code>Record addv_expr := build_addv_expr { V1 : VectorSpace; V2 : VectorSpace; Vadd : VectorSpace } </code></pre> <p>The definition of <code>directv_def</code> is</p> <pre><code>directv_def (VW : addv_expr) _ := dim (V1 VW) + dim (V2 VW) = dim (Vadd VW) </code></pre> <p>The final ingredient is that <code>fun V1 V2 =&gt; (build_addv_expr V1 V2 (V1 + V2))</code> is declared as a Canoncial Structure.</p> <p>So what does Coq read when you write <code>directv (V + W)</code>? Well it parses this as notation for</p> <pre><code>directv_def _ (Phantom _ (V + W)) </code></pre> <p>The first parameter to Phantom is the type of <code>(V + W)</code> so we can quickly fill that in to get</p> <pre><code>directv_def _ (Phantom VectorSpace (V + W)) </code></pre> <p><code>Phantom VectorSpace (V + W)</code> has type <code>phantom VectorSpace (V + W)</code>, but <code>directv_def</code> is expecting something of type <code>phantom _ (Vadd _)</code> so it tries to unify <code>(V + W)</code> with <code>(Vadd _)</code>. Because <code>Vadd</code> is a record projection, Coq tries to look up in its list of canonical structures to see if there are any declared whose <code>Vadd</code> field is of the form <code>(V + W)</code>. It says, "ahha! there is! I can use <code>build_addv_expr V W (V + W)</code>" (notice the intensional behaviour of canonical inference here). So Coq successfully unifies <code>(V + W)</code> with <code>(Vadd (build_addv_expr V W (V + W))</code>, and this forces the first parameter of directv_def:</p> <pre><code>directv_def (build_addv_expr V W (V + W)) (Phantom VectorSpace (V + W)) </code></pre> <p>And that is it for type inference. Later on this expression might be used, so it will start normalizing:</p> <pre><code>dim (V1 (build_addv_expr V W (V + W))) + dim (V2 (build_addv_expr V W (V + W))) = dim (Vadd (build_addv_expr V W (V + W))) </code></pre> <p>and then to</p> <pre><code>dim V + dim W = dim (V + W) </code></pre> <p>If you try to write something else like <code>directv 0</code> then the canonical structure inference will fail and you will get a (probably obtuse) type error.</p> <hr> <p>This has been as simplified example. In reality, <code>directv</code> is much more complicated and allows one to write <code>directv (\sum_(0 &lt;= i &lt; n) V i)</code> to mean $\bigoplus_{i=0}^n V_i$ is a direct sum and accepts things like <code>directv 0</code> to mean a trivial direct sum.</p> <p>Matita allows you to write unification hints directly without the necessarily building canonical structures. I suspect doing this sort of intentional inference would be easier in such a system.</p> http://mathoverflow.net/questions/18848/extensional-theorems-mostly-used-intensionally/29786#29786 Answer by Nick for Extensional theorems mostly used intensionally Nick 2010-06-28T13:31:58Z 2010-06-28T13:31:58Z <p>After reading some of the answers, I don't think there exists such a difference.</p> <p>Let me explain myself. Take Edgar's comment: we don't say $1$ converges, but we do say $\sum_{n=1}^\infty 2^{-n}$ converges. Strictly speaking, $1$ does not converge, we can't talk about the convergence of a number. It becomes a meaningful statement when we understand $1$ as a constant sequence. It could be said that $\sum_{n=1}^\infty 2^{-n}$ is not defined properly either, but we've accepted that an infinite sum as a limit.</p> <p>I think the same problem occurs here. After all, maths is all about formal objects. Once one starts to omit some of the details (probably for simplicity), for example, not specifying whether a polynomial should be thought of as an element of a ring, or as a function, mistakes might occur. I disagree with Tao in this subject: there are no semantic or functional interpretations of an object (or at least, there are no unique such interpretations). A polynomial can't be interpreted as a function. It is defined to be as an element of $K[x]$. If we want to talk about a polynomial function, then we must state the domain, the codomain and construct the transformation from the variable to the polynomial interpreted by replacement of the variable. But then we are no longer talking about a polynomial.</p> <p>Applied to Carette's example, one can think that before applying the theorem as a rewrite rule, we first have to define the function we identify by the expression, replace the expression by the function, and then apply the theorem to the function. And that's what we are doing (or should be doing), but for simplicity we omit these steps. It would be the same as if we instantiated $aa^{-1}=1$ as $00^{-1}=1$. We can't forget the requirements for the application of the rule.</p>