Modeling of languages for tensor manipulation
Norman A. Rink
cs.PL











	Modeling of languages for tensor manipulation

    
	Norman A. Rink 

	norman.rink@tu-dresden.de 

	Technische Universität Dresden 

	Germany

    January 26, 2018
===============================================================================================






Numerical applications and, more recently, machine learning applications rely on high-dimensional data that is typically organized into multi-dimensional tensors.
Many existing frameworks, libraries, and domain-specific languages support the development of efficient code for manipulating tensors and tensor expressions.
However, such frameworks and languages that are used in practice often lack formal specifications.
The present report formally defines a model language for expressing tensor operations.
The model language is simple and yet general enough so that it captures the fundamental tensor operations common to most existing languages and frameworks. 
It is shown that the given formal semantics are sensible, in the sense that well-typed programs in the model language execute correctly, without error.
Moreover, an alternative implementation of the model language is formally defined.
The alternative implementation introduces padding into the storage of tensors, which may benefit performance on modern hardware platforms.
Based on their formal definitions, the original implementation of the model language and the implementation with padding are proven equivalent.
Finally, some possible extensions of the presented model language for tensor manipulation are discussed.










§ INTRODUCTION



High-dimensional data structures are ubiquitous.
For decades, numerical applications have relied heavily on storing and processing data that is organized in multi-dimensional arrays.
More recently, machine learning applications have also started to make extensive use of large vectors, matrices, and arrays of higher dimensions.
Multi-dimensional arrays are not merely an organization of data in memory; 
they also support a number of natural operations.
Matrix multiplication is perhaps the most widely used such operation, but other operations from linear algebra are important too.
In the context of software engineering, multi-dimensional arrays that are accompanied by natural operations are casually referred to as tensors, to emphasize the presence of algebraic structure beyond the mere organization of data into arrays.

Over the years, many libraries and frameworks have appeared that support the development of efficient codes for manipulating tensors, e.g. <cit.>.
Frameworks often define domain-specific languages (DSLs) that facilitate that code can be written at a high level of abstraction while guaranteeing good performance when code is executed.
[
	Sometimes the DSL appears in the guise of a library's API. 
	In this case, the definition of the DSL is implicit in the API specification. 
] 
The formal semantics of these DSLs are often left implicit or are introduced in an ad-hoc fashion.
Since the mathematical operations that underlie tensor manipulation are very well understood, it is perhaps unsurprising that formalizing the semantics is not always considered a high-priority task in the design and implementation of such DSLs.
However, the absence of a formal specification of language semantics makes it difficult to verify correct behavior of implementations.
This is particularly problematic when a language implementation applies many code transformations to optimize code for fast, potentially parallel <cit.> execution.

	
In order to verify that each transformation preserves the language semantics, the semantics have to be defined in the first place.


As a step towards overcoming the problems introduced by the absence of formal definitions, the present report specifies formal semantics for tensor manipulation.
To this end, we define a model language that captures essential tensor operations (Section <ref>), 
namely: 
element-wise operations, e.g. addition or subtraction; 
transposition of dimensions; 
and tensor contraction, which is the natural generalization of matrix multiplication to tensors of more than two dimensions.
By supporting these operations, our model language can express the same tensor manipulations that are commonly supported by libraries and frameworks <cit.>.
Therefore, our analysis and results should carry over to these frameworks.
Specifically, we formally establish a reference implementation of the model language (Section <ref>) that we also prove to be safe, in the sense that there are no out-of-bounds accesses to multi-dimensional arrays (Section <ref>).
We then introduce an alternative implementation that uses padding in the storage layout of tensors (Section <ref>).
Padding can achieve alignment of tensors in memory and may generally lead to better performance on modern hardware platforms.
Thanks to the formal definition of language semantics, the implementation with padding can be proven equivalent to the reference implementation (Section <ref>).
Finally, a number of straightforward extensions of the model language are discussed (Section <ref>), and the present report is summarized (Section <ref>).








§ BACKGROUND



Numerical applications rely heavily on linear algebra, 
and hence matrix multiplication is the key operation in many of these applications.
Depending on the specific application, matrix multiplication may appear in different variants and guises.
Nonetheless, the multiplication of matrices A and B is fundamentally defined as

    (A B)_ij = ∑_k=1^d A_ik· B_kj.

Of course, this only makes sense if the extent of the second dimension of A equals the extent of the first dimension of B; 
both are denoted as d in Equation (<ref>).
For multi-dimensional tensors u and v, tensor contraction generalizes matrix multiplication, 
and applications that work with high-dimensional data may rely more on tensor contraction than matrix multiplication.

The contraction of the m-th dimension of u with the n-th dimension of v is defined as

    ∑_l=1^d u_i_1… i_m-1 l  i_m+1… i_k_1· v_j_1… j_n-1 l  j_n+1… j_k_2 .

As for matrix multiplication, the contraction only makes sense if the m-th dimension of u and the n-th dimension of v have the same extent d.
This clearly hints at a need for typing of tensors and for type checking of operations <cit.>.

Henceforth, we refer to the number of dimensions of a tensor as the tensor's rank.
Thus, in the previous example, k_1 = u and k_2 = v.
It follows that the contraction of u and v has rank k_1+k_2-2, regardless of which pair of dimensions is contracted over.
This implies that the type of a tensor must contain more fine-grained information than the tensor's rank.

It is of course also possible to contract over a pair of dimensions of the same tensor.

This kind of contraction naturally occurs in traces of matrix products, which are related to the Euclidean norm <cit.> or Frobenius norm <cit.>:

    tr(A B) =
    		∑_k_1=1^d_1( ∑_k_2=1^d_2 A_k_1 k_2 B_k_2 k_1) ,

where parentheses have been added to stress that the result of the inner contraction is a tensor (of rank 2) in its own right.

While contraction reduces the rank, the outer product of tensors u and v, denoted u ⊗ v, constructs a tensor of rank k_1 + k_2:

    (u ⊗ v)_i_1… i_k_1 j_1… j_k_2 = 
    		u_i_1… i_k_1· v_j_1… j_k_2 .

In practical applications, however, rather than forming higher-rank tensors by using the outer product, high-dimensional data is often decomposed into a product of lower-rank tensors <cit.>.
The product structure can reduce the complexity of numerical operations, which then benefits performance.
Moreover, this decomposition of data into outer products is often the reason that tensors are introduced into an application in the first place <cit.>.
Note that the outer product is frequently also referred to as the tensor product.

Another operation that generalizes from matrices to tensors of higher rank is transposition.
The tensor v is obtained from u by transposition of the m-th and n-th dimension if

    v_i_1… i_m … i_n … i_k = u_i_1… i_n … i_m … i_k .

Transposition is very important in the implementation of numerical operations since the layout of a data structure in memory can have a big impact on performance <cit.>.

Finally, the usual arithmetic operations generalize to element-wise operations on tensors:

    (u ⊙ v)_i_1… i_k_1 =
    		u_i_1… i_k_1⊙ v_i_1… i_k_2,
    		  ⊙∈{+,-,*,/} .

For this to make sense, we must have k_1 = k_2 and each of the dimensions of u and v must have the same extent.
Once again, this calls for type checking of expressions involving tensors.

Any library, framework, or DSL that aims to support tensor operations will offer an interface or syntax for expressing the operations that have been introduced above.
Beyond merely offering sufficient expressiveness, frameworks and DSLs are typically designed to achieve one or several of the following goals:

	
  * reduction of development time by offering high levels of abstraction, e.g. <cit.>;
	 

	
  * automatic optimization of codes for high performance, e.g. <cit.>;
	
	
	
	 

	
  * ability to re-target codes at different platforms, ideally without losing performance, e.g. <cit.>.

Achieving these goals typically requires that high-level code undergoes a number of transformations, as is the case in optimizing compilers for general-purpose languages <cit.>.
To verify formally that transformations do not change the behavior of programs, one first requires a formal definition of program behavior, i.e. a definition of program execution and its effects.
The present report provides this definition for a model language designed for expressing operations on tensors.
The language, which is introduced and defined formally in the next section, serves as a model for most existing DSLs for tensor manipulation.








§ THE MODEL LANGUAGE



The previous section has introduced the relevant tensor operations that ought to be supported by any framework or language for tensor manipulation.
Based on this requirement, the present section defines a model language for expressing tensor operations.
In order to focus attention specifically on tensor manipulation, the model language is deliberately kept as minimal as possible.

Another reason for keeping the model language small is to make it easy to see that many existing frameworks and DSLs can be mapped to it.
By establishing a suitable mapping for a given DSL for tensor manipulation, e.g. <cit.>, one can carry our subsequent analyses over to that DSL.
Thus, one should not think of the model language as a “silver bullet” for all problems related to tensors.
It is rather an intermediate language that is intended for the study of formal properties, in particular safety, and correctness of transformations.


0.5in





 §.§ Syntax and examples



A program in the model language consists of a sequence of declarations followed by a sequence of statements, cf. Figure <ref>.
The declaration of a variable starts with the keyword , after which the identifier appears, followed by a tuple of integers.
The tuple specifies the extents of the tensor's dimensions and hence the type of the declared variable.
For example, a tensor of rank 3 whose dimensions contain 300, 400, and 500 elements respectively is declared in Figure <ref>.
The degenerate case where a variable is declared to denote a scalar is shown in Figure <ref>.
In this case, the scalar type is indicated by an empty tuple.



0.4
	

	: [300 400 500]
	

	

	figureTensor declaration.
	


0.4
	

	: []
	

	

	figureScalar declaration.
	




A statement in the model language assigns a tensor expression to a previously declared variable.
Variables and tensor expressions are written without indices, as in <cit.>.
The dimensions of tensor variables and expressions are implicitly numbered, from left to right, starting from one.

All of the tensor operations introduced in Section <ref> can be expressed in the model language.
The hash operator (#) denotes the outer product of its operands, and contraction is expressed by a period (.) followed by a pair of integers that specifies the dimensions to be contracted.
The code that expresses the matrix multiplication from Equation (<ref>) is shown in Figure <ref>.
First, the outer product of matrices and is formed with the hash operator, and then the second and third dimension are contracted over. 
In Figure <ref>, the resulting matrix product is assigned to the variable , which is declared with appropriate dimensions.



[t]0.38
	
		: [300 400] 

		: [400 500] 

		: [300 500] 
 

		= (# ) . [2 3]
	
	figureContraction.
	


[t]0.48
	
		: [300 400] 

		: [400 300] 

		: [] 
 

		= ((# ) 
				. [2 3])
				. [1 2]
	
	figureTrace of matrix product.
	




Figure <ref> demonstrates how multiple contractions can be expressed: 
the trace of the matrix product of and , cf. Equation (<ref>), is computed.
The result of the first contraction has type [300 300], and both dimensions are contracted in the second contraction.
Hence, the final result is a scalar and is assigned to the variable .
Note that rather than expressing multiple contractions by a sequence of periods as in Figure <ref>, one could introduce syntax for writing multiple contractions more compactly.
Such syntax is indeed used in existing frameworks and DSLs for tensors <cit.>.
Since contractions over multiple pairs of dimensions can always be reduced to a sequence of contractions over single pairs of dimensions, no generality is lost in the model language by restricting the period operator to only one pair of dimensions.

Finally, transposition is expressed by the caret operator ().
Thus, the code for Equation (<ref>) is as in Figure <ref>.
Again, an arbitrary permutation of a tensor's dimensions can be expressed as a sequence of transpositions.
Hence, the model language's caret operator is completely general, while existing languages will typically include syntax for expressing general permutations more compactly.




[t]0.4
	
	0.4mm: [200 300 400 500 600] 

	0.4mm: [200 500 400 300 600] 
 

	=̌ u  [2 4]
	
	figureTransposition.
	




The production for in the grammar in Figure <ref> does not specify any precedence order for the operations between expressions.
For the purpose of this report, no precedence order is required, and it may be assumed that all operations between expressions associate to the left.
Hence, parentheses must be used to indicate the order in which operations are to be performed.
[
	An alternative convention could be to assign higher precedence to those operators that appear further towards the right in the production for .
	This convention is in agreement with the usual precedence order of the arithmetic operators +, -, *, and /.
]




 §.§ Typing and evaluation



In this section we formally define the semantics of the model language.
We also establish some simple properties of model language programs.
Before we can do this, we need to set up a number of preliminary definitions.



Let k∈_0.

	
  * A multi-index ı is a tuple ı∈^k. 
	By convention, ^0 = {()}, i.e. the set containing only the empty tuple.
	Multi-indices are written in bold face.
	
	
  * 
	Let ı = (i_1,…,i_k) ∈^k and ȷ = (j_1,…,j_k) ∈^k.
	The partial order ≤_k is defined by
	
    ı≤_k ȷ ⇔ ∀_1≤ l≤ k  i_l ≤ j_l .

	The subscript k is usually omitted, i.e. instead of ≤_k we simply write ≤.
	
	
  * 
	Let ı, ȷ, ∈̨^k.
	A pair of multi-indices is denoted as (ı,ȷ).
	Mildly abusing notation, we write ∈̨(ı,ȷ) iff ≰̨ı and ≤̨ȷ. 
	
	
  * The elements of a tensor x can be accessed using multi-indices,
	
    x_ı = x_i_1⋯ i_k,

	where ı = (i_1,…,i_k) ∈^k.
	
	
  * 
	For all l∈ such that 1≤ l≤ k, 
	the l-th projection π_l is defined as the map 
	π_l : ^k →, π_l(ı) = i_l, for ı = (i_1,…,i_k) ∈^k.
	
	 



Multi-indices are also used to specify the type of a tensor.
However, our presentation will be clearer if we can distinguish tensor types from general multi-indices.
Hence, the following definition of tensor types.



A tensor type  (or simply type) is a multi-index ∈^k, k∈_0.
For ∈^k, k is the rank of the tensor type .


Note that the rank of a tensor may be zero (since k∈_0), which accounts for the degenerate case when a tensor is in fact a scalar, as in Figure <ref>.
The extent of any tensor dimension, however, must be positive since the components of a multi-index are taken from = {1,2,…}.

The essential ingredients in typing and evaluating model language programs are two distinct maps.
The first map, denoted Γ, maps identifiers to tensor types.
This map is used during the typing of model language programs to access the types of declared variables.
Since typing is a static program analysis, we refer to the map Γ as the static context.

The second map, denoted μ, maps subscripted identifiers to an appropriately chosen value domain, typically , , or a machine-representable subset thereof.
Thus, the map μ stores the values corresponding to elements of tensors.
During program evaluation, the map μ is typically updated.
Hence, μ is referred to as the dynamic store.
When a model language program has terminated, the state of the store μ is considered the program's result since μ then contains the values computed for all the tensors involved in the program.

The next definition summarizes the previous paragraphs.



 


	
  * 
	A static context (or simply context) is a map Γ from identifiers to tensor types of arbitrary rank.
	Formally, for an identifier , if ∈Γ, then
	
    Γ()∈⋃_k=0^∞^k.

	
	
  * 
	The symbol ∙ denotes the special value undefined.
	
	
  * 
	A dynamic store (or simply store) is a map μ from subscripted identifiers to values, including the undefined value ∙.
	Formally, for an identifier and multi-index ı∈^k, 
	if _ı∈μ, then
	
    μ(_ı) ∈∪{∙},

	where  is the value domain of interest.

 



We admit ∙ in the image of the store μ for two reasons.
First, this allows us to reason about variables that are in the domain of μ but have not been initialized.
Second, by allowing undefined values, we do not need to take extra care in handling division by zero.
Extensions of the usual arithmetic operators to ∪{∙} are defined below.



Let v∈ and w∈∖{0}.
Then, 

	
  * v ⊙∙ = ∙⊙ v = ∙, for ⊙∈{+,-,*},
	
	
  * v / ∙ = ∙ / w = ∙, and 
	v / 0 = ∙ / 0 = ∙.

 



Since we allow maps to take the undefined value, we must distinguish carefully between the constant map that takes the value ∙ everywhere and the map  that is not defined anywhere.
Hence, we define the map  by virtue of its empty domain.



The symbol  denotes the map that has an empty domain, i.e. =∅.








  §.§.§ Typing and well-formed programs




	
	Now we are finally in a position to discuss the rules for forming valid model language programs.

The inference rules in Figures <ref>–<ref> specify what constitutes a correct program in the model language.
The declarations at the beginning of a program are used to form a static context Γ, cf. Figure <ref>.
Initially, the context is empty, which is expressed by the appearance of  in the rule .
Subsequently, rule states that every declaration of a variable adds the variable's identifier to the context Γ, such that Γ maps the identifier to its tensor type.
The notation Γ{↦…} means that the domain of the map Γ is augmented by .
Note that because of ∉Γ in the premise of rule , variables may not be re-declared in the model language.

Figure <ref> lists the inference rules for judging whether a program is well-formed.
Rule says that in order to decide whether a program is well-formed, the static context Γ must first be formed from the declarations that appear in the program.
This context is then used to decide whether the statements in the program are well-formed.
By the rule , an empty sequence of statements is well-formed.
By , an assignment statement is well-formed if the type of the variable and the type of the expression on the right-hand side agree.
Note that ∈Γ in the premise of rule ensures that variables have been declared when expressions are assigned to them.

The rule relies on the typing of an expression  in the context Γ.
Expression typing is specified in Figure <ref>.
The typing rules and are straightforward.
The rule says that the type of an outer product is formed by concatenating the types of the operands.
A transposition swaps two dimensions in a tensor type, cf. rule .
For a tensor contraction to be well-typed, the contracted dimensions must have the same extent, which is ensured by the premise d_m=d_n of rule .
The contracted dimensions are then dropped from the resulting type, 
which is indicated by the hats in (d_1, …, d_m, …, d_n, …, d_k).

Rule allows element-wise application of the usual arithmetic operators (+, -, *, and /) if the types of the operands match.
Rule further allows multiplication by a scalar from the left, and rule analogously allows division by a scalar.

	
	Neither of these scalar operations change the type of their tensor operands.


Note that the formation of programs can fail in essentially five ways:

	
  * re-declaration of a variable, violating the premises of rule ;
	
	
  * assignment to an undeclared variable, violating the premises of ;
	
	
  * mismatch of types in an assignment, violating the premises of rule ;
	
	
  * use of an undeclared variable in an expression, violating the premises of ;
	
	
  * mismatch of types in an expression, violating the premises of rules , , , or .
	








  §.§.§ Evaluation of model language programs



The model language is intended to capture only part of an ambient numerical application, namely the part that deals with manipulating tensors.
Hence, when a model language program is started, it is assumed that memory has been allocated for variables by the ambient application.
The initial store is thus populated with values for all variables declared in the model language program.
Values may be undefined (∙), which models the situation where the ambient application has allocated memory but has not initialized it.
Uninitialized variables may of course be assigned to during the execution of a model language program.
As already explained, the state of the store μ after executing a model language program is considered the result of the program.
[
	The interface between the ambient application and a program written in the model language is further discussed in Section <ref>.
]

The rules in Figure <ref> specify the state of the store when execution of a model language program begins.
Rule captures the requirement that memory has been allocated by the ambient application.
The values x_ı (written in italics) are assumed to have been fixed by the ambient application, including the possibility of uninitialized values, which is why the x_ı are chosen from ∪{∙}.
Note that since re-declaration of variables is not allowed, each application of augments the domain of μ with _ı for all multi-indices ı≤.

The evaluation of statements and programs is specified by the inference rules in Figure <ref>.
Rule formalizes the fact that the final state of the dynamic store is considered the result of program evaluation: 
the relation ⇓ relates a program, which is a purely syntactic entity, to a dynamic store.
The way in which assignment statements manipulate the store is defined by the relation →_Γ.
It should be stressed that rule updates the store μ with new values for all _ı with ı≤.

It may seem surprising that the evaluation relation →_Γ, which governs the dynamic behavior of programs, depends explicitly on the static context Γ.
This can be understood by considering how one would implement the rule .
Due to the universal quantifier in the conclusion of the rule, a new value is assigned to each element of the tensor .
In practice, this would be done inside a loop nest that iterates over all values that can be taken by the indices of , i.e. a loop nest that iterates over all multi-indices ı≤.
Since the type  is statically known, the machine code produced by a model language compiler would contain constant loop bounds corresponding to the entries in the tuple , 
and the loop bounds, of course, determine the dynamic behavior of program execution.
Note further that the evaluation of expressions in the premise of rule also depends on the static context, as is explained below.

The notation →_Γ^0,1 in the premise of rule means that the relation →_Γ is applied zero or one times.
Hence, a program that does not contain any statements evaluates to the initial store, 
i.e. ⟨μ, ∅⟩ = ⟨μ, ∅⟩ implies ^* ⇓μ.

Figure <ref> gives denotational semantics for the evaluation of expressions.
The evaluation function depends on both the dynamic store μ and the static context Γ.
Equation (<ref>) explains why the store is required for evaluation: 
the values bound to variables must be looked up in the store.
The static context Γ appears in Equations (<ref>) and (<ref>), both of which require type information for correct evaluation of expressions.
Once again, a model language compiler would encode this type information in the machine code it produces:
in implementing Equation (<ref>), π_m() would become a loop bound;
and the actual value of the operator variable ⊙ in Equation (<ref>) would be turned into an appropriate machine instruction.
In Equation (<ref>), and henceforth, we use ≡ to denote an identity between syntactic entities.

Program evaluation can get stuck if identifiers are not in the domain of the store μ 
or if the function is not defined for a given argument.
The following sections show, however, that this cannot happen in well-formed programs.
(“Well-type[d] programs cannot go wrong.” <cit.>)




  §.§.§ Properties of well-formed programs



In this section, we establish simple properties of well-formed programs, culminating in Corollary <ref>, which states that the evaluation function is well-defined for expressions that appear in well-formed programs.
This already goes a long way towards establishing progress and safety of well-formed programs, which will be done in Section <ref>.

The rules for forming the context Γ (in Figure <ref>) and the rules for forming the store μ (in Figure <ref>) have very similar structure.
Therefore, a given context Γ uniquely determines the corresponding store μ.
This is formally established by the following Lemma <ref>, which assumes that the values x_ı in the inference rule are uniquely determined by the ambient application (cf. the discussion at the beginning of Section <ref>).



Let ^* ⊢_sΓ. 
There exists a unique store μ
such that

	
  * 
	^* ⊢_dμ, and
	
	
  * 
	for all ∈Γ, 
	with = Γ(),
	the following holds:
	∀_ı≤ _ı∈μ.


By induction on the length of ^*, which we denote as N. 

 

N=0: 
The rules and imply that Γ= and μ= respectively.
Therefore, Γ = μ = ∅ 
and part (<ref>) holds trivially. 

 

N+1: Let 

    ^N+1≡^N     :
    		[d_1,…,d_k]

such that ^N ⊢_sΓ_N, 
and let μ_N be the corresponding store that exists by the induction hypothesis, i.e. ^N ⊢_dμ_N.
Then, letting = (d_1,…,d_k), Γ = Γ_N{↦}.
By the rule, 

    ^N+1⊢_dμ,   where  μ = μ_N{∀_ı≤ _ı↦ y_ı}.

Clearly, Γ = Γ_N∪{}.
For ∈Γ_N, _ı∈μ holds by the induction hypothesis since μ_N⊆μ.
For , part (<ref>) of the lemma holds by construction of μ.





If ^* ⊢_sΓ, then the corresponding dynamic store that exists by Lemma <ref> is denoted as μ(Γ).


In the light of Lemma <ref>, the evaluation rule can be simplified.
Instead of relying on the relation ⊢_d to form the initial store, one can directly use the store μ(Γ):

    []
    	^* ^* ⇓μ'^* ⊢_sΓ  μ = μ(Γ)   ⟨μ, ^*⟩→_Γ^0,1⟨μ', ∅⟩




Second, the condition _ı∈μ in the rule can be phrased in terms of the domain of μ(Γ),

    []
    	⟨μ',  = ⟩→_Γ⟨μ'{∀_ı≤ _i_1… i_k↦
    	 r_i_1… i_k}, ∅⟩[                     ∈Γ   = Γ(); μ(Γ)⊆μ'  ∀_ı≤ 
    		 r_ı=Γ,μ(Γ)_ı ]  .



We could now proceed to proving that Γ,μ(Γ)· is well-defined.
However, the proof does not rely on the details of the store μ(Γ), and only the domain of the store matters.
Therefore, the following slightly more general lemma holds.



Assume ^* ⊢_sΓ.
The following hold:

	
  * 
	Let μ' be a store such that μ(Γ)⊆μ'.
	If Γ⊢ :,
	then Γ,μ'_ı is well-defined for all ı≤.
	(Note that Γ,μ'_ı∈∪{∙}.)
	
	
  * 
	If Γ⊢^*,
	then ∈Γ for all statements = in ^*.
	
	
  * 
	If Γ⊢^*,
	then Γ⊢ :, where =Γ(),
	for all statements = that occur in ^*.


Part (<ref>) is proved by induction on the structure of the expression . 

 

Case ≡: 
Since Γ⊢ :, inverting rule implies that 
∈Γ and = Γ().
By Lemma <ref>, _ı∈μ(Γ)⊆μ' for all ı≤.
It thus follows from Equation (<ref>) in Figure <ref> that Γ,μ'_ı is well-defined. 

 

Case e ≡ #: 
By inverting rule , Γ⊢ : _0 and Γ⊢ : _1.
Thus, by the induction hypothesis, Γ,μ'_ı and Γ,μ'_ȷ are well-defined for ı≤_0 and ȷ≤_1.
It follows from Equation (<ref>) in Figure <ref> that Γ,μ'_ is well-defined 
for ≤̨(d_01,…,d_0l_0,d_11,…,d_1l_1), where 
(d_01,…,d_0l_0) = _0 and (d_11,…,d_1l_1) = _1. 

 

The remaining cases are handled analogously.
The division operator that occurs in Equation (<ref>) in Figure <ref> poses no difficulty since is allowed to take the value ∙ (cf. Definition <ref>).
The only interesting case is that of contraction. 

 

Case ≡ . [m n]: 
By inverting rule , 
Γ⊢ : _0, 
_0 = (d_0,…,d_k), 
and d_m = d_n.
Hence, Γ,μ'_ȷ is well-defined for all ȷ≤_0 by the induction hypothesis.
On the right-hand side of Equation (<ref>) in Figure <ref>, the summation index l takes values from {1, …, d_m}.
It is obvious from this that Γ,μ'_ı is well-defined 
for ı≤(d_1,…,d_m,…,d_n,…,d_k). 

 

Parts (<ref>) and (<ref>) are proved by induction on the length of ^*.
The proofs use the inversions of rules and .



As an immediate consequence of Lemma <ref>, we obtain the result that is well-defined on all expressions that occur in a well-formed program.



Let ^* ^*, 
let Γ be the static context for which ^*⊢_sΓ,
and let μ' be a store such that μ(Γ)⊆μ'.
Then, for all = that occur in ^*, the following hold:

	
  * Γ⊢ :, where = Γ(),
	
	
  * Γ,μ'_ı is well-defined for all ı≤.



Corollary <ref> implicitly says that in a well-formed program there are no out-of-bounds read accesses to the store.
To see this, note that a read access occurs precisely when Equation (<ref>) from Figure <ref> is used in evaluating an expression.
Since Corollary <ref> guarantees that evaluation is well-defined, the store on the right-hand side of Equation (<ref>) can never be accessed outside of its domain.

The absence of out-of-bounds write accesses will follow from the key result of the next section, namely that well-formed programs can be fully evaluated.




 §.§ Progress and safety



We now establish the central result that the execution of well-formed programs 


cannot get stuck.
This means that for a well-formed program there always exists a store μ such that the program and μ are related by ⇓.

Thus, evaluation of programs in the model language according to Figure <ref> carries the flavor of big-step semantics.
However, for a well-formed program P, the rules , and , also guarantee that a program P' that is formed of the same declarations as P but contains only a subset of the statements in P can also be fully evaluated.
[
	Since the programs P and P' contain the same declarations, the same static context Γ is used in establishing that P and P' are well-formed.
	Hence, Corollary <ref> yields that evaluation of expressions is well-defined for both P and P'.
]
This observation lets program evaluation appear closer to small-step semantics.
We therefore use the terms program evaluation and progress interchangeably.



Let ^* ^*, and let Γ be the static context for which ^*⊢_sΓ.
Then, there exists a unique store μ' such that ^* ^* ⇓μ' and μ' = μ(Γ).

By induction on the length of ^*, which we denote as N. 

 

N=0: 
Since ⟨μ(Γ), ∅⟩→^0_Γ⟨μ(Γ),∅⟩, rule can be applied and μ'=μ(Γ).
(Note that →^0_Γ is the same as equality =.) 

 

N+1: 
Assume that ^* ^N  =.
By the induction hypothesis,

    ^* ^N ⇓μ_N, 
       μ_N = μ(Γ).

By Lemma <ref>(<ref>), 
∈Γ.
Thus, let = Γ().
It follows from Lemma <ref> 
that _ı∈μ(Γ) = μ_N for all ı≤.
Moreover, Corollary <ref> implies 
that Γ,μ_N_ı is well-defined for ı≤.
Therefore, we can apply rule to obtain

    ⟨μ_N,  = ⟩→_Γ⟨μ',∅⟩ ,   where  μ' = μ_N{∀_ı≤ _ı↦ r_ı} , 
       and   r_ı = Γ,μ_N_ı.

Since _ı∈μ_N for all ı≤, 
also μ' = μ_N = μ(Γ).
Furthermore, rule can now be applied to deduce 

    ⟨μ(Γ), ^N  = ⟩→_Γ⟨μ',∅⟩
    	.

From this, an application of yields 
^* ^N  =  ⇓ μ'.
Note that μ' is unique by construction.



The fact that well-formed programs can be fully evaluated almost immediately implies that programs are safe, 
in the sense that there are no out-of-bounds accesses.
This is because out-of-bounds accesses would evaluate the map μ outside of its domain, which in turn would cause program evaluation to become stuck.
The following corollary formalizes the absence of out-of-bounds accesses.



Let ^* ^*.
There are no out-of-bounds accesses to the store during the evaluation of ^*.

For read accesses to the store, the claim follows already from Corollary <ref>, as explained at the end of Section <ref>.
For write accesses, the claim is a consequence of Theorem <ref> since complete evaluation of ^* requires successive applications of the rule .
The premises of this rule ensure that the store μ is modified only in places that are already in μ.



It is important to stress that the progress and safety results establish the sanity of the defined model language.
Theorem <ref> implies that the evaluation scheme defined in Figures <ref>–<ref> is a sensible one: 
it is guaranteed that valid programs can be evaluated without getting stuck.
Corollary <ref> is of particular importance since the model language provides an index-free way of manipulating tensor expressions.
Hence, accesses to elements of tensors, via multi-indices, are only inserted by an implementation of the model language, e.g. by a model language compiler.
Corollary <ref> guarantees that an implementation of the evaluation scheme from Figures <ref>–<ref> introduces no memory accesses that are out-of-bounds.






 §.§ Applicability and limitations of the model language




The model language is not intended for specifying entire numerical applications.
Instead, it focuses on expressing those parts of an application that specifically manipulate tensors using the previously defined operations, e.g. contraction, transposition etc.
From a practical perspective, the model language should be thought of as a DSL or intermediate language that facilitates, for example, the generation of efficient code for performance-critical parts of an application by exploiting domain knowledge, analogous to <cit.>.
This means that there must be an interface between programs written in the model language and the ambient application, usually written in a general-purpose programming language.
The variables declared in the model language collectively constitute this interface.

According to Section <ref>, it is assumed that the ambient application has allocated memory for the variables that are declared in the model language.
Thus, variables can be used to pass values between model language programs and the ambient application.
As already mentioned in Section <ref>, the ambient application may (but need not) initialize variables before a model language program is executed; 
and the values that are assigned to variables in the model language can subsequently be accessed by the ambient application.

The model language supports only a single, global scope since it is only intended to model parts of a numerical application that are limited in size.
Moreover, allowing scopes to be nested would unnecessarily complicate the simple interface between model language programs and ambient applications since it is not obvious if and how variables declared in nested scopes should correspond to variables in the ambient application.

The control flow in numerical applications is typically highly structured: 
loop nests iterate over the possible values that can be taken by the indices of tensors.
The loop bounds that appear in these loop nests are precisely the tensor dimensions, which are typically specified as constants at compile time since this aids compilers in generating more efficient machine code, cf. <cit.>.
Hence, the model language's requirement that tensor dimensions be specified as (compile-time) constants is not a practically relevant limitation.
[
	If this is seen to be a limitation, it can be overcome by deferring the compilation of model language programs until the ambient numerical application is run and tensor dimensions are known, cf. <cit.>.
]
Of course, general control flow, beyond the structured control flow that is implicit in tensor evaluation and assignment, cannot be expressed in the model language since there are no syntactic constructs for branching or loops.
Once again, this is completely aligned with the separation between ambient applications and model language programs.
Control flow and any complex logic beyond tensor expressions must be specified in the ambient application, which is assumed to be written in a general-purpose programming language.










§ PADDING AND ALIGNMENT



In this section we study an alternative implementation of the model language, namely we introduce padding in the memory layout of tensors.
Here, padding means that the memory allocated for any dimension of a tensor is rounded up to a multiple of a fixed value ∈.
Padding can positively affect performance, for example when the architecture of the targeted machine supports vector or SIMD instructions, cf. <cit.>.
By padding, the dimensions of tensors can be made multiples of the machine's vector length or SIMD width.
Vectorizing compilers can then produce more efficient machine code.
[
	This is due to the absence of scalar loop iterations that result from vectorization if tensor dimensions are not multiples of the vector length or SIMD width.
]
Another advantage of padding arises in conjunction with alignment: 
aligned memory accesses are usually faster than non-aligned ones, and 
if the memory allocated for a tensor is aligned, then padding can ensure that nested (sub-)tensors are also aligned, cf. <cit.>.

The advantage of having formalized the semantics of the model language in Section <ref> is that an implementation with padding can be proven correct.
This, of course, also requires a formal specification of the implementation with padding, 
which relies on the following Definitions <ref> and <ref>.

Henceforth, we refer to the constant  as the vector length.
This terminology derives from choosing the value of  based on the target machine's vector length or SIMD width.
The following definition introduces notation for rounding up natural numbers to the nearest multiple of .



Let ∈ be the vector length.

	
  * For d∈_0, 
	let d_ = min{n· : n∈_0 , n·≥ d}.
	
	
  * For k∈ and ı = (i_1,…,i_k)∈^k, 
	let ı_M = (i_1_,…,i_k_).
	
	
  * For ()∈^0, let ()_ = (). 

	(Recall that, by convention, ^0={()}.)
	
	
  * For a static context Γ, let Γ_ be defined point-wise, i.e.
	
    Γ_() = Γ()_,
		
	for all ∈Γ.

 



Subsequently,  is assumed fixed.
Hence, we omit the subscript on ·_, and simply write ·.
Definition <ref> immediately leads to the next lemma, which will be used in the subsequent formal analysis.



Let Γ be a static context.
If Γ⊢ :, then Γ⊢ :.

	Straightforward structural induction on the expression .
	The proof uses the fact that the rules for expression typing in Figure <ref> are syntax-directed.



The equivalence of the model language implementation from Section <ref> and the implementation with padding discussed in this section relies on the combination of two facts: 
(1) the operations in Figure <ref> are linear, and 
(2) padded memory can be filled with zeros.
The only place where linearity does not hold is in the denominator of division.
This motivates the introduction of the following controlled division operation.
[
	We say that the introduced division operation is controlled since dividing zero by zero does not lead to an uncontrolled singularity.
]



The controlled division operation is defined on ∪{∙} as in Definition <ref> except that

	
  * 0/0 = 0,
	
	
  * 0/∙ = 0.

 




	
	
	This division operation is controlled since 0/0 = 0 holds generally in the limit where both the numerator and denominator approach zero, but the denominator does so in a more controlled way than the numerator.

From now on we assume that division, as it appears, for example, in Figure <ref>, is always controlled division.
The results from previous sections are not affected by this assumption.







 §.§ Program evaluation with padding



The inference rules in Figures <ref> and <ref> formally define how model language programs are evaluated when the dimensions of tensors are padded with zeros.
As before, it is assumed that an ambient numerical application allocates memory for tensors.
Allocations are further assumed to include padded memory, and rule captures these assumptions.
Note that, also as before, memory may be left uninitialized by the ambient application.
However, memory that has only been allocated for the purpose of padding must be initialized to zero, which is captured by the requirement x_ı = 0 for ı∈(,) in rule .
(Recall from Definition <ref>(<ref>) the meaning of “∈” in this context.)

As in Section <ref>, we assume that the values x_ı in the premises of rule are uniquely determined by the ambient application.


We then obtain the following uniqueness lemma for a well-formed store μ with padding.



Let ^* ⊢_sΓ. 
There exists a unique store μ
such that

	
  * ^* ⊢_pdμ, and
	
	
  * for all ∈Γ,
	with = Γ(),
	
		
  * ∀_ı≤ _ı∈μ,
		
		
  * ∀_ı≤ μ(_ı) = μ(Γ)(_ı),
		
		
  * ∀_ı∈(,) μ(_ı) = 0,
	
	where μ(Γ) is the uniquely defined store from Definition <ref>.

 



The proof is completely analogous to that of Lemma <ref>.	


As before, we are compelled to afford a special symbol to the uniquely defined padded store.



If ^* ⊢_sΓ, then the corresponding padded store that exists by Lemma <ref> is denoted as μ(Γ).


The rules for the evaluation of statements and programs in Figure <ref> are almost identical to the ones from Figure <ref>.
The key difference is that the rounded type  and context Γ appear in rule .
In Figure <ref>, the function was defined for an arbitrary context Γ and dynamic store μ.
Using the context Γ on in lets us reuse the definitions from Figure <ref>.
The relevance of using Γ,μ· in will become apparent in the proofs of subsequent results.




 §.§ Progress and safety with padding



We now establish the progress and safety properties for the model language with padding.
Both are properties of the relation ⇓_p, and we establish these properties by following the same route as for the relation ⇓ in Sections <ref> and <ref>.
Hence, the progress and safety results in the current section, and their proofs, are analogous to Theorem <ref> and Corollary <ref>.



Assume ^* ⊢_sΓ.
Let μ' be a store such that 

	
  * 
	μ(Γ)⊆μ', and
	
	
  * 
	for all ∈Γ, with =Γ(), we have μ'(_ı) = 0 if ı∈(,).

Then, Γ⊢ : implies

	
  * 
	Γ,μ'_ı is well-defined for all ı≤, and
	
	
  * 
	Γ,μ'_ı = 0 for all ı∈(,).


We proceed by structural induction on the expression .
The proof is very similar to the proof of Lemma <ref>, 
part (<ref>). 

 

Case ≡: 
The lemma follows directly from the definition of in Equation (<ref>), Figure <ref>.
Note that the requirement <ref>. is needed to establish part (<ref>). 

 

Case e ≡ #: 
Part (<ref>) follows as in the proof of Lemma <ref>.
Part (<ref>) follows directly from the induction hypothesis since for ı∈(,) one of the factors on the right-hand side of Equation (<ref>) in Figure <ref> is equal to zero. 

 

Case e ≡ /: 
The same reasoning applies as in the proof of Lemma <ref>, 
i.e. Γ,μ'_ı is well-defined since it may take the value ∙.
For ı∈(,), part (<ref>) follows from the property 0/0 = 0 of controlled division.
When Γ⊢ : (), i.e. in the case of division by a scalar, the property 0/∙ = 0 of controlled division is also required to establish part (<ref>). 

 

Case ≡ . [m n]: 
By inverting rule , 
Γ⊢ : _0, 
_0 = (d_0,…,d_k), 
and d_m = d_n.
Again, the fact that Γ,μ'_ı is well-defined follows as in the proof of Lemma <ref>, but bear in mind that on the right-hand side of Equation (<ref>) in Figure <ref>, the summation index l now takes values from {1, …, d_m}. 

 

The remaining cases are straightforward.



Note that the proof of part (<ref>) of Lemma <ref> relies on the linearity of the arithmetic operations that occur in the definition of in Figure <ref> 
(and on controlled division from Definition <ref>).

The following progress theorem is analogous to Theorem <ref>. It also says that the final store is still suitably padded with zeros.



Let ^* ^*, and let Γ be the static context for which ^*⊢_sΓ.
Then, there exists a unique store μ' such that ^* ^* ⇓_pμ' and μ' = μ(Γ).
Moreover, μ'(_ı) = 0 
if ∈Γ, = Γ(), and ı∈(,).

The proof is similar to that of Theorem <ref>. 
Hence, this proof also proceeds by induction on the length of ^*, which we denote as N. 

 

N=0: 
Since ⟨μ(Γ), ∅⟩^0_Γ⟨μ(Γ),∅⟩, it can be concluded from that μ'=μ(Γ).
Lemma <ref> then implies μ'(_ı) = 0 for ∈Γ, = Γ(), and ı∈(,). 

 

N+1: 
Assume that ^* ^N  =.
By the induction hypothesis,

    ^* ^N ⇓_pμ_N, 
       μ_N = μ(Γ).

By Lemma <ref>(<ref>), 
∈Γ.
Thus, let = Γ().
It follows from Lemma <ref> 
that _ı∈μ(Γ) = μ_N for all ı≤.
Also by the induction hypothesis, μ_N satisfies the requirements of Lemma <ref>.
We can therefore apply rule to obtain

    ⟨μ_N,  = ⟩_Γ⟨μ',∅⟩ ,   where  μ' = μ_N{∀_ı≤ _ı↦ r_ı} , 
       and   r_ı = Γ,μ_N_ı.

Since _ı∈μ_N for all ı≤, 
also μ' = μ_N = μ(Γ).
Applications of the rules and now yield the desired

    ^* ^N  =  ⇓_p μ'
    	.

Finally, let ∈Γ and _1 = Γ().
If ≢, then μ'(_ı) = μ_N(_ı) = 0 
for ı∈(_1,_1) by the induction hypothesis.
If ≡ and ı∈(_1,_1), then μ'(_ı) = μ'(_ı) = r_i = 0 
follows by the construction of μ' and Lemma <ref>(<ref>).



As previously, this progress result also implies that model language programs implemented with a padded store are safe, in the sense that there are no out-of-bounds memory accesses.



Let ^* ^*.
There are no out-of-bounds accesses to the padded store during the evaluation of ^* as defined by the rules in Figure <ref>.





 §.§ Simulation with padding



In this section we finally arrive at the central result that program evaluation with a padded dynamic store simulates the original program evaluation from Figure <ref>.
In other words, evaluation with a padded store produces the same values as the original evaluation, and is therefore equivalent to the original evaluation.
As a first step towards this equivalence result, the next lemma relates evaluation in the context Γ to evaluation in the original context Γ.



Let ^*⊢_sΓ.
Let μ_1 and μ_2 be stores such that

	
  * 
	μ(Γ)⊆μ_1 and 
	μ(Γ)⊆μ_2,
	
	
  * 
	for all x∈Γ with _ = Γ(x),
	
    μ_2(_ı) = {[  μ_1(_ı)  ,     if  ı≤_;        0  , if  ı∈(_,_) ].
    			 .


If Γ⊢ :, 
then Γ,μ_1_ı = Γ,μ_2_ı 
for all ı≤.

The proof proceeds by structural induction on . 

 

Case ≡: 
Requirement <ref>. guarantees that the claim of the lemma holds. 

 

Case ≡⊙: 
If ⊙≡ * and Γ⊢ : (), 
then Γ⊢ : () by Lemma <ref>, 
and the claim follows from the induction hypothesis.
Similarly for ⊙≡ / and Γ⊢ : ().
The remaining cases follow at once from the induction hypothesis. 

 

Case ≡ . [m n]: 
By Γ⊢ : and inversion of , we have Γ⊢ : _0.
It then follows from Lemma <ref> that Γ⊢ : _0.
Thus, if π_m(_0) = d_m, then π_m(_0) = d_m.
Therefore,

    Γ,μ_2 . [m  n]
    		_i_1…i_m…i_n… i_k
        = 
    	∑_l=1^d_mΓ,μ_2
    		_i_1… i_m-1 l i_m+1… i_n-1 l i_n+1… i_k
        =
    	∑_l=1^d_mΓ,μ_2
    		_i_1… i_m-1 l i_m+1… i_n-1 l i_n+1… i_k ,

where the second identity holds by Lemma <ref>(<ref>),
which, in turn, is applicable by virtue of requirements <ref>., <ref>.
The desired result now follows from the induction hypothesis. 

 

The remaining cases are straightforward.





Let ^* ^*, and let Γ be the static context for which ^*⊢_sΓ.
Let μ_1 and μ_2 be the uniquely determined stores from Theorems <ref> and <ref> respectively, 
i.e. ^* ^* ⇓μ_1 
and ^* ^* ⇓_pμ_2.
Then, if ∈Γ, = Γ(), 

    μ_2(_ı) = {[ μ_1(_ı)  ,     if  ı≤;       0  ,  if  ı∈(,) ].
    	.


By induction on the length of ^*, which we denote as N. 

 

N=0: 
In this case, μ_1=μ(Γ) and μ_2=μ(Γ), 
by Lemmata <ref> and <ref> respectively.
The desired relationship between μ_1 and μ_2 also follows from Lemma <ref>. 

 

N+1: 
Let 

    ^N+1≡^N   =  .

By the induction hypothesis, 

    ^* ^N ⇓μ_N,1  , 
       ^* ^N ⇓_p μ_N,2  , 
       μ_N,2(_ı) = {[ μ_N,1(_ı)  ,      if  ı≤_;         0  ,  if  ı∈(_,_) ].
    	,

for ∈Γ, _ = Γ().
Moreover, by inversion of and (using the uniqueness of μ_N,1 and μ_N,2),

    ⟨μ_N,1,  = ⟩→_Γ⟨μ_1, ∅⟩, 
       ⟨μ_N,2,  = ⟩_Γ⟨μ_2, ∅⟩.

Hence, by and respectively,

    μ_1 = μ_N,1{∀_ı≤_ _ı↦Γ,μ_N,1_ı} , 
       μ_2 = μ_N,2{∀_ı≤_ _ı↦Γ,μ_N,2_ı} ,

where _ = Γ().
For ≢ the claim of the theorem holds by the induction hypothesis.
For ≡ and ı≤_, we have

    μ_2(_ı) 
    	= Γ,μ_N,2_ı
    	= Γ,μ_N,1_ı
    	= μ_1(_ı) ,

by Lemma <ref>.
For ≡ and ı∈ (_, _), we have

    μ_2(_ı) 
    	= Γ,μ_N,2_ı
    	= 0 ,

by Lemma <ref>(<ref>).
	


Note that for a minimal simulation result, it would suffice that the dynamic stores μ_1 and μ_2 from Theorem <ref> agree on the intersection of their domains.
Theorem <ref> is slightly stronger in that it also states that the store μ_2 takes the value zero outside of the domain of μ_1.
This additional strength was used in the above proof to yield a strong enough induction hypothesis.




§ EXTENSIONS



As described in Sections <ref> and <ref>, a model language program interfaces with the ambient application through the variables declared in the model language program.
Memory for variables is assumed to have been allocated by the ambient application.
This interface is rather crude in that it does not allow one to express which variables are intended to be used for communication with the ambient application or how variables are intended to be used (for input, output, or both).
An easy way to improve this interface is to add qualifiers to variable declarations that indicate how a variable is to be used.
This is analogous to the storage qualifiers in and out in the OpenGL shading language <cit.>.
The Fortran programming language <cit.> allows a similar qualification of procedure arguments with the intent attribute.

An input qualifier on the declaration of a variable in the model language could be used to indicate that is intended to communicate data from the ambient application into the model language program.
This would imply that none of the elements of the tensor can be undefined when execution of the model language program begins.
Thus, the rules for forming the dynamic store in Figure <ref> would have to be modified.
Figure <ref> gives the modified inference rules.
Note that rule must be applied when a variable declaration with an input qualifier is met, 
and this rule disallows the undefined value ∙.



Extending the model language with an input qualifier also enables a static program analysis that detects uses of uninitialized variables.
By Figure <ref>, only variables declared as input are guaranteed to be initialized when program execution begins.
Thus, if uses of uninitialized variables are to be avoided, all expressions evaluated by a model language program can ultimately only depend on input variables.
Due to the absence of explicit control flow in the model language, analyzing the dependencies between expressions is straightforward.

Similarly, an output qualifier can be used to enable further program analysis, and even optimization.
The output qualifier indicates which variables are live-out of a model language program, i.e. which variables are used to communicate results of the program back to the ambient application, after the model language program has completed.
Any expressions in a model language program that do not affect the value of an output variable can be eliminated from the program.
This is a form of an optimization known as dead code elimination, cf. <cit.>.
Note that the language implementation in <cit.> supports input and output qualifiers.

Generally, the simple structure of the model language should simplify many program analyses and optimizations.
For example, detecting common subexpressions is straightforward, facilitating common subexpression elimination.
The absence of explicit control flow turns reaching definition analysis into a simple backwards search: 
each use of a variable is reached by the last definition of , i.e. the last assignment to .
(See again <cit.> for descriptions of the mentioned analyses and optimizations.)

Lastly, it should be noted that many tensor operations are inherently parallel since they independently operate on tensor elements corresponding to different multi-indices.
An advanced implementation of the model language could exploit this parallelism, especially when a GPU architecture is targeted for program execution.
However, a few subtleties must be considered when designing such a parallel implementation.
The rule is written such that evaluation of the function for different multi-indices ıcan proceed in parallel, and the result of is assigned to the temporary tensor variable r.
Only then is the store μ updated with the values of the elements of r.
A direct implementation of this is rather wasteful since additional memory must be allocated to hold the temporary tensor r.
This is likely to lead to less than optimal performance of the memory system, especially caches.
A more sensible implementation would avoid allocating memory for the temporary r and directly commit the result of to the store μ.
However, proceeding like this in parallel, i.e. for different multi-indices ıat the same time, may lead to incorrect results if the variable that is assigned to also occurs in the expression from the rule .
Thus, non-trivial program analysis is required to exploit parallelism correctly and efficiently in evaluating tensor expressions.







§ SUMMARY



In the present report, we have introduced a language for manipulating tensor expressions.
The language serves to model any DSL or tensor library API that supports common tensor operations, e.g. element-wise arithmetic, contraction, transposition.
Formal semantics of our model language have been specified, and a number of properties have been established formally.

The key properties of our model language definition can be summarized as progress and safety.
By progress we mean that a well-formed program in the model language can be fully evaluated, without getting stuck.
The property of safety, in the sense that there are no out-of-bounds memory accesses during the evaluation of a model language program, was established almost as a by-product of our progress proof.

We have also formally specified an alternative implementation of the model language in which tensor dimensions are padded up to multiples of the targeted machine's vector length or SIMD width.
In a practical implementation, padding may have a positive impact on performance.
The benefit of having defined formal language semantics is that the original language definition and the implementation with padding can formally be proven equivalent.

A number of extensions of our model language have been discussed, leading to discussions also of (a) the applicability of standard program analyses and optimizations to model language programs and (b) the possibility of exploiting parallelism in tensor operations in a language implementation.
Hence, future work could look into (a) formalizing program analyses and optimizations in the context of the model language and (b) formalizing parallel evaluation semantics for model language programs.








§ ACKNOWLEDGMENTS


The author would like to thank 
Sebastian Ertel and 
Andres Goens
for general discussions on formal language semantics.

This work was partially supported by the German Research Council (DFG) through the Cluster of Excellence `Center for Advancing Electronics Dresden' (cfaed).






