Usually in books such as Schaum's outline of theory and problems of tensor calculus by David Kay, the summation convention is introduced with notes and remarks, at best some warnings and identities are given.

I have the feeling that one can develop a formal system for this notation from which identities (simply) follow. If anything, the treatment of free and dummy variables reminds me very much of free and bound variables in untyped lambda calculus, while expanding a formula to 'full form' (where all dummy indices disappear) sounds very much like $\beta$-reduction.

If one recovers the range of the indices into a context like one does in natural deduction or typed lambda calculus, one could write something like:

$$ \{I=3,J=2\} \vdash a_{ij}b_i \to_{\beta} \Sigma_{j=1}^{2}\Sigma_{i=1}^{3} a_{ij}b_i \to_{\beta} \Sigma_{j=1}^{2} a_{1j}b_1+a_{2j}b_2+a_{3j}b_3 \to_{\beta} \cdots $$


$$ \{I=3,J=2\} \vdash a_{ij}b_i \twoheadrightarrow_{\beta} a_{11}b_1+a_{21}b_2+a_{31}b_3 + a_{12}b_1+a_{22}b_2+a_{32}b_3 $$

Similarly, the rules governing equivalence of formulas feel like $\alpha$-equivalence.

Has anyone treated the summation convention in this way, giving deduction-like formal manipulation/subsitution/reduction/equivalence rules?


First, looking at summation notation (not the summation convention), i.e. $\sum_{i=0}^N a_i$, this is just a binding form like many other binding forms that occur in mathematics besides the lambda calculus. For example, quantifiers in logic, and differentiation and integration in calculus as well as taking of limits, also indexed forms of union and intersection in set theory. In all of these cases, you could, if you wanted, instead view these constructs as higher-order functions. That is, instead of viewing summing as a binding form, you can view it as a function that takes a function, e.g. $\sum_{i=0}^N a_i$ becomes $\sum_{0,N}(\lambda i.a_i)$ (or even $\sum_{0,N}(a)$). Of course, you need to then define these higher-order functions, e.g. $$\sum_{i,N}(f) = \begin{cases}0,&\text{if }i > N \\f(i)+\sum_{i+1,N}(f),&\text{if }i\leq N\end{cases}$$

The summation convention, as the name suggests, is just a convention for implicitly binding variables. Once you insert the summation symbols, it reduces to just normal rules for binding forms. As you point out, it does require some contextual information to insert the bounds. One could imagine making some formal calculus that directly gave meaning to expression utilizing the summation convention without introducing summation symbols, but it would be somewhat tedious, a bit limiting, and mostly pointless.

  • $\begingroup$ Thanks for the note about higher-order. But I don't understand the 'pointless' part. How is it pointless to be able to be fully formal and clear about the rules of a calculus as opposed to keeping it a half-baked not clearly defined dialect. That seems anti-mathematical. Or do we choose to be rigorous only when it suits us or when the tradition dictates it, to the chagrin of the newcomer? $\endgroup$ – weakmoons Aug 20 '17 at 21:43
  • $\begingroup$ You wrote '∑0,N(λi.ai)' is this actually done in any book? I would love to see it. $\endgroup$ – weakmoons Aug 20 '17 at 21:44
  • 1
    $\begingroup$ What I'm saying is pointless is to try to interpret the summation convention directly without introducing summation symbols. It would be much simpler and easier to understand to describe rules for inserting summation symbols. It's completely reasonable to want to formalize the insertion of summation symbols. SICM takes an approach like this, though more focused on differentiation and integration. Most texts that would take that sort of approach are more likely to be in a logic-oriented setting. $\endgroup$ – Derek Elkins Aug 20 '17 at 22:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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