12Tensor Computation

Egison has features developed specifically for conveniently describing tensor computations. This chapter introduces these features.

12.1What Are Tensors?

A tensor is a generalization of vectors and matrices. A vector is a first-order tensor, and a matrix is a second-order tensor. In programs, vectors are often represented as one-dimensional arrays and matrices as two-dimensional arrays. An $$n$$ th-order tensor is represented by an $$n$$ -dimensional array.

Below are examples of a vector, a matrix, and a second-order tensor expressed in mathematical notation.

\begin{pmatrix} a_{1} & a_{2} & a_{3}\\ \end{pmatrix}

\begin{pmatrix} a_{11} & a_{12} & a_{13} \\ a_{21} & a_{22} & a_{23} \end{pmatrix}

\begin{pmatrix} \begin{pmatrix} a_{111} & a_{112} & a_{113} \\ a_{121} & a_{122} & a_{123} \end{pmatrix} \begin{pmatrix} a_{211} & a_{212} & a_{213} \\ a_{221} & a_{222} & a_{223} \end{pmatrix} \begin{pmatrix} a_{311} & a_{312} & a_{313} \\ a_{321} & a_{322} & a_{323} \end{pmatrix} \end{pmatrix}

The above mathematical expressions are represented in Egison as follows. In Egison, tensors are represented by enclosing their components in [| |]. Matrices are represented as vectors of vectors, and second-order tensors as vectors of matrices. This is similar to the notation for multidimensional arrays in languages such as C.

[| a_1, a_2, a_3 |]

[| [| a_11, a_12, a_13 |],
   [| a_21, a_22, a_23 |] |]

[| [| [| a_111, a_112, a_113 |],
      [| a_121, a_122, a_123 |] |],
   [| [| a_211, a_212, a_213 |],
      [| a_221, a_222, a_223 |] |],
   [| [| a_311, a_312, a_313 |],
      [| a_321, a_322, a_323 |] |] |]

12.2Index Notation for Tensors

Most tensor computations can be expressed as combinations of the tensor product, Hadamard product, and inner product of vectors. The tensor product returns a matrix consisting of all combinations of vector components. The Hadamard product returns a vector consisting only of corresponding component pairs. The inner product returns a scalar value obtained by summing the components of the Hadamard product.

\begin{pmatrix} a_{1} & a_{2} \end{pmatrix} \otimes \begin{pmatrix} b_{1} & b_{2} \end{pmatrix} = \begin{pmatrix} a_{1} b_{1} & a_{1} b_{2} \\ a_{2} b_{1} & a_{2} b_{2} \end{pmatrix}

\begin{pmatrix} a_{1} & a_{2} \end{pmatrix} \circ \begin{pmatrix} b_{1} & b_{2} \end{pmatrix} = \begin{pmatrix} a_{1} b_{1} & a_{2} b_{2} \end{pmatrix}

\begin{pmatrix} a_{1} & a_{2} \end{pmatrix} \cdot \begin{pmatrix} b_{1} & b_{2} \end{pmatrix} = a_{1} b_{1} + a_{2} b_{2}

For example, the multiplication of matrix $$A$$ and matrix $$B$$ can be interpreted as an operation that takes the tensor product over the rows of $$A$$ and columns of $$B$$ , and the inner product over the columns of $$A$$ and rows of $$B$$ .

\begin{pmatrix} a_{11} & a_{12} \\ a_{21} & a_{22} \end{pmatrix} \begin{pmatrix} b_{11} & b_{12} \\ b_{21} & b_{22} \end{pmatrix} = \begin{pmatrix} a_{11} b_{11} + a_{12} b_{21} & a_{11} b_{12} + a_{12} b_{22} \\ a_{21} b_{11} + a_{22} b_{21} & a_{21} b_{12} + a_{22} b_{22} \end{pmatrix}

For vectors, there are only three types of multiplication: tensor product, Hadamard product, and inner product. However, for matrices and higher-order tensors, there are infinitely many ways to multiply. Naming all these multiplications would be impractical. Therefore, mathematicians attach symbolic indices to tensors and use these indices as parameters to express these multiplications. For example, when different symbols are attached to each vector, it represents the tensor product; when the same symbol appears at the same position on each vector, it represents the Hadamard product; and when the same symbol appears in the superscript and subscript positions of the vectors, it represents the inner product. There are two types of indices: superscripts and subscripts. The positional relationship distinguishes between the Hadamard product and the inner product. This notation of using symbolic indices to specify how tensors are multiplied is called index notation. The mathematical expressions below can be represented in Egison using the program shown in Section 9.6.

\begin{pmatrix} a_{1} & a_{2} \end{pmatrix}_{i} \begin{pmatrix} b_{1} & b_{2} \end{pmatrix}_{j} = \begin{pmatrix} a_{1} b_{1} & a_{1} b_{2} \\ a_{2} b_{1} & a_{2} b_{2} \end{pmatrix}_{ij}

\begin{pmatrix} a_{1} & a_{2} \end{pmatrix}_{i} \begin{pmatrix} b_{1} & b_{2} \end{pmatrix}_{i} = \begin{pmatrix} a_{1} b_{1} & a_{2} b_{2} \end{pmatrix}_{i}

\begin{pmatrix} a_{1} & a_{2} \end{pmatrix}^{i} \begin{pmatrix} b_{1} & b_{2} \end{pmatrix}_{i} = a_{1} b_{1} + a_{2} b_{2}

Matrix multiplication can also be neatly expressed using index notation. By reversing the superscript/subscript positions and using the same symbol for the columns of A and the rows of B (where the inner product is taken), matrix multiplication can be expressed.

\begin{pmatrix} a_{11} & a_{12} \\ a_{21} & a_{22} \end{pmatrix}^{i}_{\ j} \begin{pmatrix} b_{11} & b_{12} \\ b_{21} & b_{22} \end{pmatrix}^{j}_{\ k} = \begin{pmatrix} a_{11} b_{11} + a_{12} b_{21} & a_{11} b_{12} + a_{12} b_{22} \\ a_{21} b_{11} + a_{22} b_{21} & a_{21} b_{12} + a_{22} b_{22} \end{pmatrix}^{i}_{\ k}

12.3Key Ideas for Introducing Index Notation to Programming

The reason introducing index notation to programming is difficult is that the rules for symbolic indices differ for each operator. In particular, the index rules differ between tensor addition and multiplication. Let us introduce some examples. Let $$u$$ and $$v$$ each be vectors.

$u_{i} + v_{i}$ returns a vector. In contrast, $u_{i} v_{i}$ is an invalid expression.
(In Euclidean space, where superscript and subscript indices can be freely interchanged, $u_{i} v_{i}$ returns the inner product. However, we do not consider such exceptions here.)
$u^{i} + v_{i}$ is invalid. In contrast, $u^{i} v_{i}$ returns the inner product.
$u_{i} + v_{j}$ is invalid. In contrast, $u_{i} v_{j}$ returns the tensor product.

As shown, the rules for symbolic indices differ for each operator. Therefore, every time a function that handles tensors is defined, the symbolic index rules must be specified. This is a tedious task. Moreover, a new syntax for describing index rules may be needed in some cases. Such new syntax would make the programming language more complex.

Egison solves this problem by simplifying the rules for symbolic indices. The simplification of index rules does not change the interpretation of valid expressions. However, some expressions that were previously invalid become valid. For example, $v_{i} + v_{j}$ was an invalid expression, but under the new index rules it becomes valid. Figure 12.3 shows the simplified index rules for tensor addition. By relaxing the index rules, many tensor operations can be viewed as variants of tensor addition. For example, tensor multiplication can be viewed as an operation that combines components in the same form as addition, followed by an additional process called contraction (Figure 12.3). Tensor contraction is the operation of summing the diagonal components when there are superscript and subscript indices with the same symbol. This perspective reduces the amount of index rule descriptions needed when defining functions on tensors.

\begin{pmatrix} a \\ b \end{pmatrix}_{i} + \begin{pmatrix} c \\ d \end{pmatrix}_{i} = \begin{pmatrix} a + c \\ b + d \end{pmatrix}_{i}

\begin{pmatrix} a \\ b \end{pmatrix}_{i} + \begin{pmatrix} c \\ d \end{pmatrix}_{j} = \begin{pmatrix} a + c & a + d \\ b + c & b + d \end{pmatrix}_{ij}

\begin{pmatrix} a \\ b \end{pmatrix}_{i} + \begin{pmatrix} c \\ d \end{pmatrix}^{i} = \begin{pmatrix} a + c & a + d \\ b + c & b + d \end{pmatrix}_{i}^{\ i}

Index rules for addition

\begin{pmatrix} a \\ b \end{pmatrix}_{i} \begin{pmatrix} c \\ d \end{pmatrix}_{i} = contract \begin{pmatrix} a c \\ b d \end{pmatrix}_{i} = \begin{pmatrix} a c \\ b d \end{pmatrix}_{i}

\begin{pmatrix} a \\ b \end{pmatrix}_{i} \begin{pmatrix} c \\ d \end{pmatrix}_{j} = contract \begin{pmatrix} a c & a d \\ b c & b d \end{pmatrix}_{ij} = \begin{pmatrix} a c & a d \\ b c & b d \end{pmatrix}_{ij}

\begin{pmatrix} a \\ b \end{pmatrix}_{i} \begin{pmatrix} c \\ d \end{pmatrix}^{i} = contract \begin{pmatrix} a c & a d \\ b c & b d \end{pmatrix}_{i}^{\ i} = a c + b d

Index rules for multiplication

Simplified index rules

12.4Scalar Parameters and Tensor Parameters

The introduction of tensor index notation to programming is achieved through (i) a type system that distinguishes between scalar functions and tensor functions, and (ii) appropriate index reduction rules. Starting from this section, we explain these concepts.

First, we explain the distinction between scalar functions and tensor functions through the type system. In Egison, whether a function is a scalar function or a tensor function is determined by the type annotations of its formal parameters. If the type of a formal parameter is not Tensor a, that parameter is treated as a scalar. If the type of a formal parameter is Tensor a, that parameter is treated as a tensor. When a tensor is passed as an argument to a parameter treated as a scalar, the function's processing is mapped over each component of the tensor. When a tensor is passed as an argument to a parameter treated as a tensor, the tensor is passed as-is to the parameter. In the following example, the type variable a is inferred to be a scalar type, and when a tensor is passed, the processing is mapped over each component.

(\u v -> (u, v)) [| a, b |]_i [| x, y |]_j
-- [| [| (a, x), (a, y) |],
--    [| (b, x), (b, y) |] |]_i_j

On the other hand, when the Tensor type is explicitly specified, the tensor is passed as-is.

(\(u: Tensor a) (v: Tensor a) -> (u, v)) [| a, b |]_i [| x, y |]_j
-- ([| a, b |]_i, [| x, y |]_j)

Egison's type system distinguishes between two kinds of functions: scalar functions (scalar function) and tensor functions (tensor function). A scalar function is a function that, when given a tensor as an argument, maps its processing over each component. For example, “+”, “-”, “*”, “/”, and “ $\partial$ / $\partial$ ” are scalar functions. A tensor function is a function that, when given a tensor as an argument, processes the tensor as a tensor directly. For example, a function that computes the determinant or a function for tensor multiplication cannot be defined by automatically mapping over each component, so they must be defined as tensor functions. Whether a function is a scalar function or a tensor function is determined by type annotations. If the type of a formal parameter is not Tensor a, tensors passed as arguments are automatically mapped component-wise (scalar function). If the type of a formal parameter is Tensor a, tensors are passed as-is (tensor function). Examples of scalar and tensor function definitions are explained in Figures 12.4 and 12.4.

def min (x: a) (y: a) : a := if x < y then x else y

Definition of the min function (the type annotation indicates it works for any comparable type a)

min(\begin{pmatrix} 1 \\ 2 \\ 3 \\ \end{pmatrix}_{i}, \begin{pmatrix} 10 \\ 20 \\ 30 \\ \end{pmatrix}_{j}) = \begin{pmatrix} min(1,10) & min(1,20) & min(1,30) \\ min(2,10) & min(2,20) & min(2,30) \\ min(3,10) & min(3,20) & min(3,30) \\ \end{pmatrix}_{ij} = \begin{pmatrix} 1 & 1 & 1 \\ 2 & 2 & 2 \\ 3 & 3 & 3 \\ \end{pmatrix}_{ij}

}

Applying the min function to vectors with different indices

min(\begin{pmatrix} 1 \\ 2 \\ 3 \\ \end{pmatrix}_{i}, \begin{pmatrix} 10 \\ 20 \\ 30 \\ \end{pmatrix}_{i}) = \begin{pmatrix} min(1,10) & min(1,20) & min(1,30) \\ min(2,10) & min(2,20) & min(2,30) \\ min(3,10) & min(3,20) & min(3,30) \\ \end{pmatrix}_{ii} = \begin{pmatrix} min(1,10) \\ min(2,20) \\ min(3,30) \end{pmatrix}_{i} = \begin{pmatrix} 1 \\ 2 \\ 3 \end{pmatrix}_{i}

}

Applying the min function to vectors with the same index

Definition and application examples of the min function as an example of a scalar function

Figure 12.4 introduces the definition of the min function and its application examples as an example of a scalar function. Since the body uses <, the parameter type is inferred as a type variable under the constraint {Ord a}, which the Tensor type cannot satisfy (a scalar parameter — the precise criterion is given in Section 12.10). Therefore, when a tensor is passed as an argument, the function is automatically applied component-wise. As a result of component-wise application, the function is applied in the same form as a tensor product, as shown in Figure 12.4. The index reduction rules for tensors are simple. The only rule is that when a tensor with two or more indices of the same symbol is generated as a result of applying a scalar function (as in Figure 12.4), it is reduced to a tensor consisting of its diagonal components. The detailed specification of the index reduction rules is discussed in the next section.

def (.) (t1: Tensor a) (t2: Tensor a) : Tensor a := contractWith (+) (t1 * t2)

Definition of the “.” function (the type annotation indicates it receives tensors and returns a tensor)

\begin{pmatrix} 1 \\ 2 \\ 3 \\ \end{pmatrix}^{i} \cdot \begin{pmatrix} 10 \\ 20 \\ 30 \\ \end{pmatrix}_{i} = contractWith(+, \begin{pmatrix} 10 & 20 & 30 \\ 20 & 40 & 60 \\ 30 & 60 & 90 \\ \end{pmatrix}^{i}_{\;i}) = 10 + 40 + 90 = 140

\begin{pmatrix} 1 \\ 2 \\ 3 \\ \end{pmatrix}_{i} \cdot \begin{pmatrix} 10 \\ 20 \\ 30 \\ \end{pmatrix}_{i} = contractWith(+, \begin{pmatrix} 10 \\ 40 \\ 90 \\ \end{pmatrix}_{i}) = \begin{pmatrix} 10 \\ 40 \\ 90 \\ \end{pmatrix}_{i}

$\begin{pmatrix} 1 \\ 2 \\ 3 \\ \end{pmatrix}_{i} \cdot \begin{pmatrix} 10 \\ 20 \\ 30 \\ \end{pmatrix}_{j} = contractWith(+, \begin{pmatrix} 10 & 20 & 30 \\ 20 & 40 & 60 \\ 30 & 60 & 90 \\ \end{pmatrix}_{ij}) = \begin{pmatrix} 10 & 20 & 30 \\ 20 & 40 & 60 \\ 30 & 60 & 90 \\ \end{pmatrix}_{ij}$
}

Application of the “.” function

Definition and application examples of the “.” function as an example of a tensor function

Figure 12.4 introduces the definition and application examples of the “.” function, a tensor multiplication function, as an example of a tensor function. Since the formal parameter type is Tensor a, when a tensor is passed as an argument, it is passed as-is. As shown in Figure 12.4, Egison has built-in support for both superscript and subscript indices. When the same symbol is used for a superscript and subscript, contraction can be performed using the contractWith function.

Superscripts are represented in programs using “~” and subscripts using “_”. For example, the first computation example in Figure 12.4 is expressed in Egison as follows.

[| 1, 2, 3 |]~i . [| 10, 20, 30 |]_i
-- 140

12.5Three Types of Indices

Egison introduces three types of indices for handling tensor index notation. The first two are the superscripts and subscripts introduced in the previous section, represented by ~ and _. The third is called the superscript-subscript index, represented by ~_. Superscript-subscript indices appear when a scalar function is applied to a tensor that has both a superscript and subscript index with the same symbol.

[| 1 2 3 |]_i * [| 10 20 30 |]_i -- [| 10, 40, 90 |]_i
[| 1 2 3 |]~i * [| 10 20 30 |]~i -- [| 10, 40, 90 |]~i
[| 1 2 3 |]~i * [| 10 20 30 |]_i -- [| 10, 40, 90 |]~_i

The contractWith function, which also appeared in the previous section, converts diagonal components of superscript-subscript indices into a list and folds it with the function given as the first argument.

contractWith (+) [| 10, 40, 90 |]_i -- [| 10, 40, 90 |]_i
contractWith (+) [| 10, 40, 90 |]~i -- [| 10, 40, 90 |]~i
contractWith (+) [| 10, 40, 90 |]~_i -- 130

contractWith is a library function defined using the built-in function contract. The built-in function contract returns the list of components at the slot with a superscript-subscript index.

contract [| 1, 2, 3 |]~_i -- [1, 2, 3]
contract [| [| 11, 12 |], [| 21, 22 |] |]~_i_j -- [[| 11, 12 |]_j, [| 21, 22 |]_j]
contract [| [| 11, 12 |], [| 21, 22 |] |]_i~_j -- [[| 11, 21 |]_j, [| 12, 22 |]_i]
contract [| [| 11, 12 |], [| 21, 22 |] |]~_i~_j -- [11, 12, 21, 22]

12.6Index Reduction Rules

E({A, xs}) =
  if e(xs) = [] then
    {A, xs})
  elsif e(xs) = [{k,j}, …] & p(k,xs) = p(j,xs) then
    E({diag(k, j, A), remove(j, xs))
  elsif e(xs) = [{k,j}, …] & p(k,xs) != p(j,xs) then
    E({diag(k, j, A), update(k, 0, remove(j, xs)))

Pseudocode for index reduction

This section explains the index reduction rules using pseudocode. As explained in Section 12.4, since applying a scalar function to tensors always maps the processing component-wise in the form of a tensor product, we only need to define the reduction rules for a single tensor.

Figure 12.6 shows the pseudocode for index reduction. E(A,xs) is a function that reduces an indexed tensor. A is the array of tensor components, and xs is the list of indices attached to A. For example, E(A,xs) operates on a tensor with indices “~i_j_i” as follows. The flags 1, -1, and 0 represent superscript, subscript, and superscript-subscript indices, respectively.

E({[|[|[|1,2|],[|3,4|]|]
    ,[|[|5,6|],[|7,8|]|]|]
 ,[{i,1}, {j,-1}, {i,-1}]}) =
{[|[|1,3|],[|6,8|]|], [{i,0}, {j,-1}]}

Let us explain the auxiliary functions used in the pseudocode. e(xs) finds pairs of indices with the same symbol in xs. diag(k, j, A) computes the tensor consisting of the diagonal components of A with respect to the k-th and j-th slots. remove(k, xs) removes the k-th element from the list xs. p(k, xs) retrieves the value of the k-th entry from the association list xs. update(k, p, xs) updates the value of the k-th entry in the association list xs to p. These auxiliary functions operate as follows.

e([{i, 1}, {j, -1}, {i, -1}])        = [{1,3}]
diag(1, 2, [|[|11,12|],[|21,22|]|]) = [|11,22|]
p(2, [{i, 1}, {j, -1}])             = -1
remove(2, [{i, 1}, {j, -1}])        = [{i, 1}]
update(2, 0, [{i, 1}, {j, -1}])     = [{i, 1}, {j, 0}]

12.7Differences from Classical Index Notation — Unified Index Rules

In classical tensor index notation, the validity conditions for indices differ from operation to operation. For example, $$u_i + v_i$$ is valid but $$u_i + v_j$$ is not, and under the Einstein summation convention $$u^i v_i$$ denotes a contraction while the same-variance repetition $$u_i v_i$$ is invalid. Egison simplifies and unifies these rules: every operation is treated by one semantics — element-wise lifting (tensorMap insertion) followed by index reduction. As a result, expressions valid in the classical notation keep their meaning, and formerly invalid expressions receive a consistent meaning as well.

declare symbol i, j

[|1,2,3|]_i + [|10,20,30|]_j
-- [| [| 11, 21, 31 |], [| 12, 22, 32 |], [| 13, 23, 33 |] |]_i_j

[|1,2,3|]_i + [|10,20,30|]_i
-- [| 11, 22, 33 |]_i

[|1,2,3|]_i * [|10,20,30|]_j
-- [| [| 10, 20, 30 |], [| 20, 40, 60 |], [| 30, 60, 90 |] |]_i_j

[|1,2,3|]_i * [|10,20,30|]_i
-- [| 10, 40, 90 |]_i

[|1,2,3|]~i . [|10,20,30|]_i
-- 140

Note that + and * follow exactly the same rules. With distinct indices the result takes the shape of a tensor product (all combinations); a repeated subscript extracts the diagonal (for * this coincides with the Hadamard product). The classically invalid $$u_i + v_j$$ becomes a tensor with the natural meaning “all combinations of the sum”. Contraction happens when a superscript--subscript pair is passed to a tensor function such as . (Section 12.8).

In the repeated-index case, the intermediate form right after lifting is a square array holding all combinations, but index reduction (Section 12.6) extracts the diagonal immediately, so the user only ever observes the reduced value.

12.8Application of Tensor Functions

When an indexed tensor is passed to a tensor function, it is applied to the tensor function together with its indices. Let us verify this behavior with the “.” function defined in Figure 12.4. Figure 12.4 displays the expansion step by step when the “.” function is applied. Indexed tensors appear inside contractWith, which is made possible by tensors being passed to tensor functions together with their indices. Thanks to this behavior, tensor functions can be applied using tensor index notation as follows.

[|1,2,3|]~i . [|10,20,30|]_i -- 140
[|1,2,3|]_i . [|10,20,30|]_j -- [|[|10,20,30|],[|20,40,60|],[|30,60,90|]|]_i_j
[|1,2,3|]_i . [|10,20,30|]_i -- [|10,40,90|]_i

Sometimes, additional indices need to be attached to a tensor passed as an argument inside a tensor function. To attach new indices, insert ... between the tensor and the indices as follows. This feature is implemented as syntactic sugar using the built-in functions subrefs and suprefs, which are introduced in Section 12.14. Usage examples of this feature are presented in Chapter 14.

A..._i_j

12.9Index Completion for Omitted Indices

When a tensor with omitted indices is applied to a function, Egison automatically completes the indices. This section explains the rules for this completion.

Let A and B be second-order tensors, i.e., matrices. When A and B are applied to a scalar function simultaneously with their indices omitted, the same combination of indices is completed as shown below.

A + B -- A_t1_t2 + B_t1_t2

When “!” is prefixed to the function application, different indices are completed as shown below.

A !+ B -- A_t1_t2 + B_t3_t4

When a tensor with omitted indices is applied to a tensor function, no completion is performed.

The above index completion rules are in fact necessary for a reason. Setting the index completion rules for omitted indices as described above allows differential form operators to be defined concisely. Concrete examples of differential form operator definitions are presented in Chapter 14. As also mentioned later in Chapter 14, “!” only needs to be used within the definitions of differential form operators. Therefore, users generally do not need to be aware of “!”.

12.10Mechanism of Automatic `tensorMap` Insertion

This section explains the mechanism of automatic tensorMap insertion by the type system.

12.10.1Basic Principle

For every function application, Egison's type system decides whether the formal parameter's type can—taking its type class constraints into account—be instantiated to Tensor a. A parameter for which this is possible is called tensor-compatible. tensorMap is inserted exactly when the following two conditions hold:

the formal parameter is not tensor-compatible (it is a scalar parameter), and
the actual argument's type is Tensor a.

tensorMap is a built-in function that applies the function given as the first argument to each component of the tensor given as the second argument and returns a tensor.

Whether a parameter type is tensor-compatible is determined as follows:

concrete scalar types such as Integer — not tensor-compatible (scalar parameters);
explicit Tensor a types — tensor-compatible;
type variables — decided by whether the Tensor type can satisfy all the attached class constraints.
An unconstrained type variable is always tensor-compatible. The a of {Eq a} is tensor-compatible as well, because the library provides instance {Eq a} Eq (Tensor a). By contrast, the a of {Ord a} or {AddSemigroup a} is not tensor-compatible: the Tensor type has no instances of those classes.

This classification is determined by the function's principal type (its inferred type) alone, so where tensorMap is inserted is deterministic, and type annotations are never needed to control insertion. Moreover, the decision stays entirely within Hindley--Milner inference: no index information is lifted to the type level, and no dependent typing is required.

12.10.2Concrete Example

Let us verify the behavior using the min function defined in Figure 12.4.

def min (x: a) (y: a) : a := if x < y then x else y

min [|1,2,3|]_i [|10,20,30|]_j
-- Internally transformed to:
-- tensorMap (\xi -> tensorMap (\yi -> min xi yi) [|10,20,30|]_j) [|1,2,3|]_i
-- Result: [|[|1,1,1|],[|2,2,2|],[|3,3,3|]|]_i_j

min [|1,2,3|]_i [|10,20,30|]_i
-- Result: [|1,2,3|]_i

Since the body of min uses <, its parameter type is inferred as the type variable a under the constraint {Ord a}. The Tensor type is not an instance of the Ord class, so a cannot be instantiated to a Tensor type. The parameters of min are therefore scalar parameters, and when a tensor is passed, tensorMap is inserted automatically. Writing the definition without any annotations, def min x y := if x < y then x else y, infers the same type and behaves identically — whether to lift follows from the inferred principal type alone.

The indices of the resulting tensor for the first expression are “_i_j”. When the result of applying the first argument's function to the second argument's tensor components in tensorMap is itself a tensor, tensorMap moves the indices of that result tensor to the end of the indices of the overall result tensor. This is why the result tensor has the indices “_i_j”. This mechanism enables the application of scalar functions using tensor index notation.

12.10.3Tensor-Compatibility of Type Variables

For type variables, the dividing line is not the presence of constraints but whether the Tensor type can satisfy the attached constraints. An unconstrained type variable can be instantiated to any type — including Tensor types — so it is tensor-compatible. Passing a tensor to the identity function, for example, inserts no tensorMap: the tensor passes through as-is.

def myId (x: a) : a := x

myId [|1,2,3|]_i -- [| 1, 2, 3 |]_i

It is thanks to this classification that generic higher-order functions carrying tensors as elements (list operations and the like) work as expected.

A constrained type variable stays tensor-compatible when the Tensor type has an instance of the class. For example, {Eq a} poses no obstacle because of instance {Eq a} Eq (Tensor a): equality is decided on whole tensors, not lifted component-wise.

def eqTest {Eq a} (x: a) (y: a) : Bool := x == y

eqTest [|1,2|]_i [|1,2|]_i -- True
eqTest [|1,2|]_i [|1,3|]_i -- False

By contrast, a constraint whose class has no Tensor instance makes the parameter a scalar parameter.

def double {AddSemigroup a} (x: a) : a := x + x

double [|1,2,3|]_i
-- Since Tensor is not an instance of AddSemigroup,
-- tensorMap is automatically inserted:
-- tensorMap (\xi -> double xi) [|1,2,3|]_i
-- Result: [|2,4,6|]_i

The constraint AddSemigroup a restricts a to instances of the AddSemigroup class. The Tensor type is not among them, so when a tensor is passed, tensorMap is inserted automatically and double is applied to each component (of type Integer).

12.10.4The Case of Tensor Functions

On the other hand, when the formal parameter type is explicitly Tensor a, tensorMap is not inserted.

def (.) (t1: Tensor a) (t2: Tensor a) : Tensor a :=
  contractWith (+) (t1 * t2)

[|1,2,3|]~i . [|10,20,30|]_i
-- tensorMap is not inserted; the tensor is passed as-is
-- Result: 140

12.10.5Functions Passed to Higher-Order Functions

Insertion also applies to functions passed as arguments to higher-order functions. In this case, tensorMap is inserted not at an application site but by eta-expanding the function argument itself: the supplied function f is transformed into a wrapper such as \x -> tensorMap f x or \x y -> tensorMap2 f x y, and the component-wise application happens in the wrapper's body.

def inc (x: Integer) : Integer := x + 1

map inc [[|1,2|]_i, [|10,20|]_i]
-- inc is eta-expanded to \x -> tensorMap inc x
-- Result: [[|2,3|]_i, [|11,21|]_i]

foldl1 (+) [[|1,2|]_i, [|10,20|]_i]
-- (+) is eta-expanded to \x y -> tensorMap2 (+) x y
-- Result: [|11,22|]_i

The condition for eta-expansion depends on the shape of the function argument. A unary scalar function is eta-expanded when the callback type expected by the call site mentions tensors (in the map example above, the types reveal that the list elements are tensors). By contrast, a binary scalar function is eta-expanded to its tensorMap2 version without exception, whether or not tensors are visible in the types. Since tensorMap and tensorMap2 act as the identity on scalar values, this unconditional wrapping is always safe. Thanks to this design, arguments that turn from scalars into tensors mid-computation — such as the accumulator of foldl — are handled correctly.

foldl (+) 0 [[|1,2|]_i, [|10,20|]_i]
-- The accumulator starts as the scalar 0 and becomes
-- a tensor at the first addition
-- Result: [|11,22|]_i

Callbacks whose parameters have Tensor a types, such as “.”, are not eta-expanded; tensors are passed to them as-is.

12.10.6Optimization Techniques

In the actual implementation, a built-in function called tensorMap2 is also used for optimization. When using nested tensorMap, a tensor with non-diagonal components is generated even when only diagonal components are needed for diagonalization. tensorMap2 takes a binary function and two tensors as arguments and is implemented to compute only the components needed for the result tensor.

12.11Index Reversal and the `flipIndices` Function

The partial differentiation function $\partial$ / $\partial$ is a scalar function. However, $\partial$ / $\partial$ is not just an ordinary scalar function. $\partial$ / $\partial$ reverses the superscript/subscript positions of the second argument tensor's indices. For example, ( $\partial$ / $\partial$ $\Gamma$ ~i_j_k x~l) returns a fourth-order tensor with indices “~i_j_k_l”.

To achieve this behavior, Egison provides a built-in function called flipIndices. flipIndices reverses the superscript/subscript positions of all indices of its argument tensor. Superscript-subscript indices remain as superscript-subscript indices even after reversal.

The $\partial$ / $\partial$ function is defined using flipIndices as follows.

def `$\partial$`/`$\partial$` (f: Tensor MathValue) (x: Tensor MathValue)
    : Tensor MathValue :=
  tensorMap2 partialDiffMV f (flipIndices x)

-- partialDiffMV is an auxiliary function that computes
-- partial differentiation on scalar values
def partialDiffMV (f: MathValue) (x: MathValue) : MathValue := ...

Through tensorMap2, the partialDiffMV function is applied to each component of f and flipIndices x. Since flipIndices x reverses the indices of the second argument, the indices of the result tensor are also reversed.

Below is a usage example of $\partial$ / $\partial$ .

declare symbol r, `$\theta$`, i, j

`$\partial$`/`$\partial$` [|(r * (sin `$\theta$`)),(r * (cos `$\theta$`))|]_i [|r,`$\theta$`|]_j
-- [| [| 'sin `$\theta$`, ('cos `$\theta$`) * r |], [| 'cos `$\theta$`, - ('sin `$\theta$`) * r |] |]_i~j
`$\partial$`/`$\partial$` [|(r * (sin `$\theta$`)),(r * (cos `$\theta$`))|]_i [|r,`$\theta$`|]_i
-- [| 'sin `$\theta$`, - ('sin `$\theta$`) * r |]~_i

In the first example, the index of the second argument is reversed from _j to ~j, and the result has indices _i~j.

12.12Generating Tensors with `generateTensor` Expressions

The generateTensor expression is a convenient built-in syntax for initializing tensors. generateTensor takes a function that accepts a list as the first argument and the desired tensor size as the second argument. For example, to generate a matrix of size $$(3, 4)$$ with all components equal to $$1$$ , write the generateTensor expression as follows.

generateTensor [2]#1 [3, 4]
-- [| [| 1, 1, 1, 1 |], [| 1, 1, 1, 1 |], [| 1, 1, 1, 1 |] |]

When combined with anonymous match functions, various tensors can be generated with concise descriptions. For example, to generate the identity matrix, do the following.

generateTensor (\match as list integer with
                  | [$n, #n] -> 1
                  | _ -> 0)
               [3, 3]
-- [| [| 1, 0, 0 |], [| 0, 1, 0 |], [| 0, 0, 1 |] |]

12.13Declaring Tensors

This section explains how to bind tensors to variables. First, tensors can be defined using def or let expressions, just like ordinary values.

def A : Tensor Integer := [| [| 11, 12 |], [| 21, 22 |] |]

A -- [| [| 11, 12 |], [| 21, 22 |] |]

In mathematics and physics, it is common to assign different values to tensors with the same variable name but different index types (superscript vs.subscript). Egison supports this convention by allowing different tensors to be defined for each index type. When referencing a variable, Egison uses both the variable name and the index type. The index type is specified by writing indices after the variable name in the variable definition.

def g_i_j : Tensor MathValue := [| [| 2, 2 |], [| 2, 2 |] |]_i_j
def g~i~j : Tensor MathValue :=
  [| [| 1 / 2, 1 / 2 |], [| 1 / 2, 1 / 2 |] |]~i~j

g_1_1 -- 2
g~1~1 -- 1 / 2

To reference a variable that has been bound with a specified index type, it is convenient to use dummy symbols (dummy symbol). Dummy symbols are represented by #, and each occurrence is treated as a unique symbol. Dummy symbols are a mechanism built into Egison. Using dummy symbols, g~i~j and g_i_j defined above can be referenced as follows.

g_#_# -- [| [| 2, 2 |], [| 2, 2 |] |]_#_#
g~#~# -- [| [| 1 / 2, 1 / 2 |], [| 1 / 2, 1 / 2 |] |]~#~#

You can also specify the index type using declared symbols to reference tensors, but using dummy symbols is more convenient since it requires no declaration.

declare symbol i, j

g_i_j -- [| [| 2, 2 |], [| 2, 2 |] |]_i_j
g~i~j -- [| [| 1 / 2, 1 / 2 |], [| 1 / 2, 1 / 2 |] |]~i~j

Note that multiple dummy symbols appearing in a single expression are each treated as distinct symbols.

As in mathematical notation for tensors, symbols can also be written as indices on the left-hand side variable.

def A_i_j : Tensor Integer := [| [| 11, 12 |], [| 21, 22 |] |]_i_j
def B_i_j : Tensor Integer := [| [| 11, 12 |], [| 21, 22 |] |]_j_i

A_#_# -- [| [| 11, 12 |], [| 21, 22 |] |]_#_#
B_#_# -- [| [| 11, 21 |], [| 12, 22 |] |]_#_#

This feature is implemented in Egison as the following syntactic sugar.

def A_i_j := ...
-- => def A__ := withSymbols [i, j]
--                 transpose [i, j] ...

The transpose function is a built-in function that transposes tensor components in the order specified by the first argument.

12.14Convenient Syntax for Attaching Indices

For a tensor $$A$$ whose rank varies with a parameter $$n$$ , one may want to attach indices like $A_{i_{1}...i_{n}}$ . For this purpose, Egison provides built-in functions subrefs and subrefs!. These functions attach the list of indices given as the second argument to the tensor given as the first argument. subrefs appends the index list from the second argument to the existing indices of the first argument's tensor, while subrefs! removes the existing indices and attaches new ones.

subrefs! A (map 1#i_$1 [1..n])
subrefs  A (map 1#i_$1 [1..n])

Since tensors of the form $A_{i_{1}...i_{n}}$ appear frequently in mathematical expressions, the following syntactic sugar is provided for the programs using subrefs! and subrefs above.

A_(i_1)...(i_n)
A..._(i_1)...(i_n)

The above also applies to tensors with superscripts like $A^{i_{1}...i_{n}}$ , for which Egison provides the built-in functions suprefs and suprefs!.

The feature of subrefs and suprefs for appending indices to existing ones is used when defining functions for differential forms, which are introduced in Chapter 14.

12.15Declaring Symmetry and Antisymmetry of Tensors

\begin{pmatrix} a_{11} & a_{12} & a_{13} \\ a_{12} & a_{22} & a_{23} \\ a_{13} & a_{23} & a_{33} \\ \end{pmatrix}

Example of a symmetric tensor

\begin{pmatrix} 0 & a_{12} & a_{13} \\ -a_{12} & 0 & a_{23} \\ -a_{13} & -a_{23} & 0 \\ \end{pmatrix}

Example of an antisymmetric tensor

Symmetry and antisymmetry of tensors

A tensor is said to be symmetric when, as in the example of Figure 12.15, the upper triangular components and lower triangular components coincide. A tensor is said to be antisymmetric when, as in the example of Figure 12.15, the signs of the upper triangular and lower triangular components are reversed. When a tensor is antisymmetric, the diagonal components are 0.

Many tensors encountered in mathematics and physics possess symmetry. For example, the Riemann curvature tensor $R_{abcd}$ computed in Section 14.2 has multiple symmetries: $R_{abcd} = -R_{abdc}$ , $R_{abcd} = -R_{bacd}$ , and $R_{abcd} = R_{cdab}$ . Mathematicians and physicists exploit these symmetries to skip unnecessary calculations. We would like to implement such symmetry-aware computation optimization in Egison, but to do so in a programming language, the tensor's symmetry must be explicitly declared. Egison has a notation for declaring tensor symmetry. This section explains the usage and implementation of this notation.

12.15.1Notation for Declaring Tensor Symmetry

In addition to the symmetries above, the Riemann curvature tensor also has a symmetry known as the first Bianchi identity: $R_{abcd} + R_{acdb} + R_{adbc} = 0$ . There is a notation $R_{a[bcd]} = 0$ that expresses this first Bianchi identity. The notation implemented in Egison for declaring tensor symmetry was inspired by this notation.

We introduce the notation using concrete examples. In Egison, the Riemann curvature tensor $R_{abcd}$ can be defined as follows. The right-hand side contains a complex expression, but it can be ignored for this section. Please focus only on the left-hand side.

def R_a_b_c_d : Tensor MathValue := withSymbols [i, j]
  g_a_i . (`$\partial$`/`$\partial$` `$\Gamma$`~i_b_d x~c - `$\partial$`/`$\partial$` `$\Gamma$`~i_b_c x~d +
           `$\Gamma$`~j_b_d . `$\Gamma$`~i_j_c - `$\Gamma$`~j_b_c . `$\Gamma$`~i_j_d)

To declare the antisymmetry $R_{abcd} = -R_{abdc}$ , enclose the indices _a_b in curly braces {}.

def R{_a_b}_c_d : Tensor MathValue := withSymbols [i, j]
  g_a_i . (`$\partial$`/`$\partial$` `$\Gamma$`~i_b_d x~c - `$\partial$`/`$\partial$` `$\Gamma$`~i_b_c x~d +
           `$\Gamma$`~j_b_d . `$\Gamma$`~i_j_c - `$\Gamma$`~j_b_c . `$\Gamma$`~i_j_d)

When $R_{abcd}$ is defined this way, referencing $R_{21cd}$ will return the sign-reversed value of the computed result for $R_{12cd}$ . Multiple symmetries can be declared simultaneously. To declare both $R_{abcd} = -R_{abdc}$ and $R_{abcd} = -R_{bacd}$ , enclose both _a_b and _c_d in curly braces {}.

def R{_a_b}{_c_d} : Tensor MathValue := withSymbols [i, j]
  g_a_i . (`$\partial$`/`$\partial$` `$\Gamma$`~i_b_d x~c - `$\partial$`/`$\partial$` `$\Gamma$`~i_b_c x~d +
           `$\Gamma$`~j_b_d . `$\Gamma$`~i_j_c - `$\Gamma$`~j_b_c . `$\Gamma$`~i_j_d)

With this declaration, referencing $R_{2121}$ will return the computed result of $R_{1212}$ .

More complex symmetries such as $R_{abcd} = R_{cdab}$ can also be described. To express this symmetry, enclose _a_b and _c_d each in parentheses () to treat them as groups. Then enclose them in square brackets []. While curly braces {} are used to declare antisymmetry, square brackets [] are used to declare symmetry.

def R[(_a_b)(_c_d)] : Tensor MathValue := withSymbols [i, j]
  g_a_i . (`$\partial$`/`$\partial$` `$\Gamma$`~i_b_d x~c - `$\partial$`/`$\partial$` `$\Gamma$`~i_b_c x~d +
           `$\Gamma$`~j_b_d . `$\Gamma$`~i_j_c - `$\Gamma$`~j_b_c . `$\Gamma$`~i_j_d)

All three symmetries $R_{abcd} = -R_{abdc}$ , $R_{abcd} = -R_{bacd}$ , and $R_{abcd} = R_{cdab}$ can also be declared simultaneously.

def R[{_a_b}{_c_d}] : Tensor MathValue := withSymbols [i, j]
  g_a_i . (`$\partial$`/`$\partial$` `$\Gamma$`~i_b_d x~c - `$\partial$`/`$\partial$` `$\Gamma$`~i_b_c x~d +
           `$\Gamma$`~j_b_d . `$\Gamma$`~i_j_c - `$\Gamma$`~j_b_c . `$\Gamma$`~i_j_d)

In summary, Egison uses three types of brackets to declare symmetry. Square brackets [] are used to declare symmetry. Curly braces {} are used to declare antisymmetry. Parentheses () are used to group multiple indices together.

Since the indices of symmetric tensors are usually adjacent, the symmetries of tensors encountered in mathematics and physics can almost always be declared using this notation. A nice aspect of this notation is that symmetry can be declared without changing the program on the right-hand side of := at all.

12.15.2Example Where Symmetry Declaration Shortens Tensor Definitions

Earlier, we mentioned that an advantage of this approach is that no changes to the program on the right-hand side of := are needed, but there are also cases where the program on the right-hand side can be simplified. For example, this occurs for tensors whose values are defined using different expressions for each block, as shown below.

def R'_i_j_k_l : Tensor MathValue :=
  generateTensor
    (\match as list integer with
       | [#1, #1, _, _] -> 0
       | [_, _, #1, #1] -> 0
       | [#1, $b, #1, $d] -> -1 * p^2 * `$\delta$`~(b - 1)_(d - 1)
       | [$a, #1, #1, $d] ->      p^2 * `$\delta$`~(a - 1)_(d - 1)
       | [#1, $b, $c, #1] ->      p^2 * g_(b - 1)_(c - 1)
       | [$a, #1, $c, #1] -> -1 * p^2 * g_(a - 1)_(c - 1)
       | [#1, $b, $c, $d] -> -1 * p * `$\nabla$`J_(b - 1)_(c - 1)~(d - 1)
       | [$a, #1, $c, $d] ->      p * `$\nabla$`J_(a - 1)_(c - 1)~(d - 1)
       | [$a, $b, #1, $d] -> -1 * p * `$\nabla$`J~(d - 1)_(a - 1)_(b - 1)
       | [$a, $b, $c, #1] ->      p * `$\nabla$`J_(c - 1)_(a - 1)_(b - 1)
       | [$a, $b, $c, $d] -> R_(a - 1)_(b - 1)_(c - 1)~(d - 1)
                             + -1 * p^2 * J_(b - 1)_(c - 1) * J_(a - 1)~(d - 1)
                             +      p^2 * J_(a - 1)_(c - 1) * J_(b - 1)~(d - 1)
                             +  2 * p^2 * J_(a - 1)_(b - 1) * J_(c - 1)~(d - 1))
    [5, 5, 5, 5]

Symmetry can greatly reduce the number of conditional branches.

def R'[{_i_j}{_k_l}] : Tensor MathValue :=
  generateTensor
    (\match as list integer with
       | [#1, #1, _, _] -> 0
       | [#1, $b, #1, $d] -> -1 * p^2 * `$\delta$`~(b - 1)_(d - 1)
       | [#1, $b, $c, $d] -> -1 * p * `$\nabla$`J_(b - 1)_(c - 1)~(d - 1)
       | [$a, $b, $c, $d] -> R_(a - 1)_(b - 1)_(c - 1)~(d - 1)
                             + -1 * p^2 * J_(b - 1)_(c - 1) * J_(a - 1)~(d - 1)
                             +      p^2 * J_(a - 1)_(c - 1) * J_(b - 1)~(d - 1)
                             +  2 * p^2 * J_(a - 1)_(b - 1) * J_(c - 1)~(d - 1))
    [5, 5, 5, 5]

12.15.3Implementation

This section explains the implementation of the notation for declaring tensor symmetry. This notation is implemented as syntactic sugar using generateTensor expressions. We explain the transformation through several concrete examples.

First, let us explain how square brackets [] for declaring symmetry are expanded. The ... in the following program is where some program that returns a tensor is placed.

def X[_i_j] := ...

A program of the above form is expanded into the following program.

def X_i_j : Tensor a :=
 let tmpX_i_j := ...
   generateTensor
     (\i j -> if i > j then tmpX_j_i
              else          tmpX_i_j)
     (tensorShape tmpX_#_#)

A new variable tmpX is introduced and assigned the tensor to be defined. X itself is defined using a generateTensor expression. This generateTensor expression is defined so that the lower-half components reference the upper-half components. Since Egison lazily evaluates tensor components, the lower-half components of tmpX are never computed. Therefore, the computation cost of tensor components is halved.

Curly braces {} for declaring antisymmetry are expanded in the same way.

def X{_i_j} := ...

The interior of the generateTensor expression is modified so that the lower-half components have their signs reversed relative to the upper-half components, and the diagonal components are $$0$$ .

def X_i_j : Tensor a :=
  let tmpX_i_j := ...
    generateTensor
      (\i j -> if i > j      then -tmpX_j_i
               else if i = j then 0
               else               tmpX_i_j)
      (tensorShape tmpX_#_#)

12.16Detailed Mechanism of tensorMap Insertion

In Egison, the compiler automatically inserts tensorMap and tensorMap2 so that polymorphic functions work correctly with tensor arguments. This section provides a detailed explanation of this automatic insertion mechanism.

12.16.1Processing Flow and Timing

The insertion of tensorMap is executed after type inference (Phase 5-6) and before type class expansion (Phase 8-2), at Phase 8-1. The processing flow is as follows:

Phase 5-6: Type inference assigns types to all expressions.
Phase 8-1: TensorMap insertion automatically inserts tensorMap/tensorMap2 where needed.
Phase 8-2: Type class expansion converts type class methods (e.g., (+)) into dictionary lookup form (dict_AddSemigroup_("plus")).

The reason TensorMap insertion is executed before type class expansion is to first determine the argument types (scalar or tensor), so that instance selection can be performed correctly during type class expansion.

12.16.2Two-Phase Transformation per Application Spine

Insertion operates in two phases on each application spine (f a1 ... an). The first phase determines, from the function's principal type, which argument positions of the spine are scalar parameters. The second phase wraps the scalar positions that receive tensors with tensorMap or tensorMap2, all at once. Because position determination and wrapping are separated, the insertion result does not depend on the order in which arguments are processed (the confluence of Section 12.16.7).

12.16.3Basic Principles of Insertion

TensorMap insertion is based on the following principles:

Principle 1: Insertion for Operations on Scalar Types Inside Type Constructors

When a scalar type, or a type variable constrained by classes of which Tensor has no instance, exists inside a type constructor (list [a], tuple (a, b), etc.), tensorMap or tensorMap2 is always inserted for operations on that type.

For example, when an element x extracted from a variable xs: [a] is subjected to an operation (+) that expects a scalar type, it is transformed to tensorMap2 (+).

Principle 2: Behavior of tensorMap on Scalars

tensorMap and tensorMap2 are implemented so that they can be applied to scalar values directly:

tensorMap f scalar returns f scalar (acts as identity when not a tensor)
tensorMap2 f s1 s2 returns f s1 s2

This property eliminates the need to insert conditional branches for determining at runtime whether arguments are scalars or tensors, greatly simplifying the implementation.

12.16.4Handling of Eta-Expanded Type Class Methods

Eta-expansion of functions passed to higher-order functions — the conditions and examples — was explained in Section 12.10.5. This section supplements the implementation-level handling when type class methods are involved.

At the TensorMap insertion stage, type class methods still appear in eta-expanded form. For example, the (+) operator appears in the following form:

\etaVar1 etaVar2 -> dict_AddSemigroup_("plus") etaVar1 etaVar2

When the body of this two-argument lambda is a two-argument function application, the entire body is wrapped with tensorMap2:

\etaVar1 etaVar2 -> tensorMap2 (\x y -> dict_AddSemigroup_("plus") x y) etaVar1 etaVar2

This transformation ensures that tensorMap insertion is correctly applied to type class methods as well.

12.16.5Concrete Example: The sum Function

By tracing the transformation of the polymorphic sum function, we can understand the TensorMap insertion mechanism more concretely.

Original Definition

def sum {AddMonoid a} (xs: [a]) : a := foldl (+) zero xs

This function has the polymorphic type [a] -> a with the type class constraint {AddMonoid a}.

Phase 5-6: After Type Inference

Type inference instantiates the type variable a to a concrete type (e.g., t0):

def sum : {AddMonoid t0} [t0] -> t0 :=
  \xs ->
    foldl ((+) : {AddSemigroup t0} t0 -> t0 -> t0) (zero : {AddMonoid t0} t0) (xs : [t0])

Here, the type of xs is [t0], and the type variable t0 with a type class constraint exists inside the type constructor []. Also, the type of (+) is {AddSemigroup t0} t0 -> t0 -> t0, a binary function taking scalar types as arguments.

Phase 8-1: After TensorMap Insertion

(+) is a binary function with both parameters being scalar types (t0), so it is wrapped with tensorMap2:

def sum : {AddMonoid t0} [t0] -> t0 :=
  \xs ->
    foldl (tensorMap2 (+)) zero xs

At this point, even if the elements of xs are tensors, tensorMap2 correctly performs component-wise addition.

Phase 8-2: After Type Class Expansion

The type class method (+) is expanded into dictionary lookup form:

def sum : {AddMonoid t0} [t0] -> t0 :=
  \dict_AddMonoid xs ->
    foldl (tensorMap2 (dict_AddMonoid_("plus"))) (dict_AddMonoid_("zero")) xs

Here, dict_AddMonoid is the method dictionary for the AddMonoid t0 instance. Note that the AddMonoid dictionary contains both its own method (zero) and the inherited AddSemigroup method (+) through the superclass relationship.

Runtime Behavior

This transformation makes the sum function work correctly for both scalars and tensors:

Scalar case (`t0 = Integer`):

sum [1, 2, 3]
-- foldl1 (tensorMap2 (+)) [1, 2, 3]
-- tensorMap2 (+) 1 2  -->  (+) 1 2  -->  3
-- tensorMap2 (+) 3 3  -->  (+) 3 3  -->  6
-- Result: 6

For scalars, tensorMap2 acts as identity, so ordinary addition is performed.

Tensor case (`t0 = Tensor Integer`):

sum [[| 1, 2 |], [| 3, 4 |]]
-- foldl1 (tensorMap2 (+)) [[| 1, 2 |], [| 3, 4 |]]
-- tensorMap2 (+) [| 1, 2 |] [| 3, 4 |]  -->  [| 1+3, 2+4 |]  -->  [| 4, 6 |]
-- Result: [| 4, 6 |]

For tensors, tensorMap2 applies addition component-wise.

Mixed case:

sum [[| 1, 2 |], 3]
-- tensorMap2 (+) [| 1, 2 |] 3  -->  tensorMap (\x -> x + 3) [| 1, 2 |]
--                                -->  [| 1+3, 2+3 |]  -->  [| 4, 5 |]
-- Result: [| 4, 5 |]

Even when one argument is a tensor and the other is a scalar, tensorMap2 handles it appropriately.

12.16.6Summary

Through the TensorMap insertion mechanism, Egison achieves the following:

Users only need to define polymorphic functions with type class constraints, and tensor operations are automatically supported.
The compiler automatically inserts tensorMap/tensorMap2 based on type information, so users do not need to write them explicitly.
Depending on the runtime type, scalar and tensor operations are automatically switched.
Functions passed as arguments to higher-order functions (foldl, map, etc.) also have appropriate transformations applied automatically.

This design allows Egison's computer algebra system to handle scalars and tensors uniformly, while providing an intuitive and user-friendly interface.

12.16.7Properties of the Insertion (Guarantees)

Type-directed tensorMap insertion is designed to satisfy the following properties.

Conservativity: programs that use no tensors are entirely unaffected by insertion.
The meaning of scalar-only programs is exactly what it was before the insertion mechanism existed.
Determinism: where tensorMap is inserted is determined uniquely by the functions' principal types alone.
Type annotations are not needed to control insertion; the same inferred types yield the same insertion.
Confluence: multi-argument lifting via tensorMap2 or nested tensorMap yields the same result no matter which argument is processed first (the nesting order carries no semantic difference).
Idempotence of the Tensor type: at the type level, Tensor (Tensor a) is identified with Tensor a.
This corresponds to the fact that an Egison tensor is a flat multi-dimensional array with an index list; no nested tensor-of-tensor structure exists at the value level.

Together with type preservation and type safety, these properties are established as theorems in the theory of Egison's typed tensor calculus.