Elaboration of tensor trees

• Syntax in Lean allows us to represent tensor expressions in a way close to what we expect to see on pen-and-paper.
• The elaborator turns this syntax into a tensor tree.

Examples

• Suppose T and T' are tensors S.F (OverColor.mk ![c1, c2]).
• {T | μ ν}ᵀ is tensorNode T.
• We can also write e.g. {T | μ ν}ᵀ.tensor to get the tensor itself.
• {- T | μ ν}ᵀ is neg (tensorNode T).
• {T | 0 ν}ᵀ is eval 0 0 (tensorNode T).
• {T | μ ν + T' | μ ν}ᵀ is addNode (tensorNode T) (perm _ (tensorNode T')), where here _ will be the identity permutation so does nothing.
• {T | μ ν = T' | μ ν}ᵀ is (tensorNode T).tensor = (perm _ (tensorNode T')).tensor.
• If a ∈ S.k then {a •ₜ T | μ ν}ᵀ is smulNode a (tensorNode T).
• If g ∈ S.G then {g •ₐ T | μ ν}ᵀ is actionNode g (tensorNode T).
• Suppose T2 is a tensor S.F (OverColor.mk ![c3]). Then {T | μ ν ⊗ T2 | σ}ᵀ is prodNode (tensorNode T1) (tensorNode T2).
• If T3 is a tensor S.F (OverColor.mk ![S.τ c1, S.τ c2]), then {T | μ ν ⊗ T3 | μ σ}ᵀ is contr 0 1 _ (prodNode (tensorNode T1) (tensorNode T3)). {T | μ ν ⊗ T3 | μ ν }ᵀ is contr 0 0 _ (contr 0 1 _ (prodNode (tensorNode T1) (tensorNode T3))).
• If T4 is a tensor S.F (OverColor.mk ![c2, c1]) then {T | μ ν + T4 | ν μ }ᵀis addNode (tensorNode T) (perm _ (tensorNode T4)) where _ is the permutation of the two indices of T4. {T | μ ν = T4 | ν μ }ᵀ is (tensorNode T).tensor = (perm _ (tensorNode T4)).tensor is the permutation of the two indices of T4.

Comments

• In all of theses expressions μ, ν etc are free. It does not matter what they are called, Lean will elaborate them in the same way. In other words, {T | μ ν ⊗ T3 | μ ν }ᵀ is exactly the same to Lean as {T | α β ⊗ T3 | α β }ᵀ.
• Note that compared to ordinary index notation, we do not rise or lower the indices. This is for two reasons: 1) It is difficult to make this general for all tensor species, 2) It is a redundancy in ordinary index notation, since the tensor T itself already tells you this information.

Indices

def TensorTree.indexExpr.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.indexExpr : Category

A syntax category for indices of tensor expressions.

Equations

• Lean.Parser.Category.indexExpr = { }

def TensorTree.indexExpr_ : Lean.ParserDescr

A basic index is a ident.

Equations

• TensorTree.indexExpr_ = Lean.ParserDescr.node `TensorTree.indexExpr_ 1022 (Lean.ParserDescr.const `ident)

def TensorTree.indexExpr__1 : Lean.ParserDescr

An index can be a num, which will be used to evaluate the tensor.

Equations

• TensorTree.indexExpr__1 = Lean.ParserDescr.node `TensorTree.indexExpr__1 1022 (Lean.ParserDescr.const `num)

def TensorTree.«indexExprτ(_)» : Lean.ParserDescr

Notation to describe the jiggle of a tensor index.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.indexExprIsNum (stx : Lean.Syntax) : Bool

Bool which is true if an index is a num.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.indexToNum (stx : Lean.Syntax) : Lean.Elab.TermElabM ℕ

If an index is a num - the underlying natural number.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.indexToIdent (stx : Lean.Syntax) : Lean.Elab.TermElabM Lean.Ident

When an index is not a num, the corresponding ident.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.indexPosEq (a b : Lean.TSyntax `indexExpr × ℕ) : Lean.Elab.TermElabM (Option (ℕ × ℕ))

Takes a pair a b : ℕ × TSyntax `indexExpr. If a.1 < b.1 and a.2 = b.2 then outputs some (a.1, b.1), otherwise none.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.indexToDual (stx : Lean.Syntax) : Bool

Bool which is true if an index is of the form τ(i) that is, to be dualed.

Equations

• One or more equations did not get rendered due to their size.

Manipulation of lists of indexExpr

def TensorTree.evalAdjustPos (l : List ℕ) : List ℕ

Adjusts a list List ℕ by subtracting from each natural number the number of elements before it in the list which are less than itself. This is used to form a list of pairs which can be used for evaluating indices.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.getEvalPos (ind : List (Lean.TSyntax `indexExpr)) : Lean.Elab.TermElabM (List (ℕ × ℕ))

For list of indexExpr e.g. [α, 3, β, 2, γ], getEvalPos returns a list of pairs ℕ × ℕ related to indices which are numbers. The second element of each pair is the number corresponding to that index. The first element is the position of that number in the list of indices when all other numbered indices before it are removed. Thus for the example given getEvalPos outputs [(1, 3), (2, 2)].

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.getContrPos (ind : List (Lean.TSyntax `indexExpr)) : Lean.Elab.TermElabM (List (ℕ × ℕ))

For list of indexExpr e.g. [α, 3, β, α, 2, γ], getContrPos first removes all indices which are numbers (e.g. [α, β, α, γ]). It then outputs pairs (a, b) in ℕ × ℕ of positions of this list with a < b such that the index at a is equal to the index at b. It checkes whether or not an element is contracted more then once.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.withoutContrEval (ind : List (Lean.TSyntax `indexExpr)) : Lean.Elab.TermElabM (List (Lean.TSyntax `indexExpr))

The list of indices after contraction or evaluation.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.toPairs (l : List ℕ) : List (ℕ × ℕ)

Takes a list and puts consecutive elements into pairs. e.g. [0, 1, 2, 3] becomes [(0, 1), (2, 3)].

Equations

• TensorTree.toPairs (x1 :: x2 :: xs) = (x1, x2) :: TensorTree.toPairs xs
• TensorTree.toPairs [] = []
• TensorTree.toPairs [x] = [(x, 0)]

def TensorTree.contrListAdjust (l : List (ℕ × ℕ)) : List (ℕ × ℕ)

Adjusts a list List (ℕ × ℕ) by subtracting from each natural number the number of elements before it in the list which are less than itself. This is used to form a list of pairs which can be used for contracting indices.

Equations

• One or more equations did not get rendered due to their size.

Permutations of indices

def TensorTree.getPermutation (l1 l2 : List (Lean.TSyntax `indexExpr)) : Lean.Elab.TermElabM (List ℕ)

Given two lists of indices, all of which are indent, returns the List (ℕ) representing the how one list permutes into the other.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.stringToTerm (str : String) : Lean.Elab.TermElabM Lean.Term

The construction of an expression corresponding to the type of a given string once parsed.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.getPermutationTerm (l1 l2 : List (Lean.TSyntax `indexExpr)) : Lean.Elab.TermElabM Lean.Term

Given two lists of indices returns the permutation between them based on finMapToEquiv.

Equations

• One or more equations did not get rendered due to their size.

Syntax for tensor expressions.

def TensorTree.tensorExpr.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.tensorExpr : Category

A syntax category for tensor expressions.

Equations

• Lean.Parser.Category.tensorExpr = { }

def TensorTree.«tensorExpr_|__» : Lean.ParserDescr

The syntax for a tensor node.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.«tensorExpr_=_» : Lean.TrailingParserDescr

Equality.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.«tensorExpr_⊗_» : Lean.TrailingParserDescr

The syntax for tensor prod two tensor nodes.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.«tensorExpr_+_» : Lean.TrailingParserDescr

The syntax for tensor addition.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.«tensorExpr(_)» : Lean.ParserDescr

Allowing brackets to be used in a tensor expression.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.«tensorExpr_•ₜ_» : Lean.ParserDescr

Scalar multiplication for tensors.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.«tensorExpr_•ₐ_» : Lean.ParserDescr

group action for tensors.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.«tensorExpr-_» : Lean.ParserDescr

Negation of a tensor tree.

Equations

• TensorTree.«tensorExpr-_» = Lean.ParserDescr.node `TensorTree.«tensorExpr-_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "-") (Lean.ParserDescr.cat `tensorExpr 0))

Syntax of tensor expressions to indices.

def TensorTree.getNumIndicesExact (stx : Lean.Syntax) : Lean.Elab.TermElabM ℕ

For syntax of the form T where T is S.F.obj (OverColor.mk c) this returns the value of TensorSpecies.numIndices T. That is, the exact number of indices associated with that tensor.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.getAllIndices (stx : Lean.Syntax) : Lean.Elab.TermElabM (List (Lean.TSyntax `indexExpr))

For syntax of the form T | α β 2 β, getAllIndices returns a list [α, β, 2, β] of all indexExpr.

Equations

• One or more equations did not get rendered due to their size.

partial def TensorTree.getProdIndices (stx : Lean.Syntax) : Lean.Elab.TermElabM (List (Lean.TSyntax `indexExpr))

The function getProdIndices is defined for the following syntax:

1. For e.g. T | α β 2 β, it returns all uncontracted and unevaluated indices e.g.[α]
2. For e.g. T1 | α β 2 β ⊗ T2 | α γ δ δ it returns all unevaluated indices which are not contracted in either tensor e.g. [α, α, γ].
3. For e.g. (T1 | α β 2 β ⊗ T2 | α γ δ δ) ⊗ T3 | γ it does 2 recursively e.g. [γ, γ]

partial def TensorTree.getIndicesFull (stx : Lean.Syntax) : Lean.Elab.TermElabM (List (Lean.TSyntax `indexExpr))

Returns the remaining indices of a tensor expression after contraction and evaulation. Thus every index in the output of getIndicesFull is ident and there are no duplicates. Examples are:

1. T | α β 2 β gives [α]
2. T1 | α β 2 β ⊗ T2 | α γ δ δ gives [γ]
3. (T1 | α β 2 β ⊗ T2 | α γ δ δ) ⊗ T3 | γ gives []
4. T1 | α β 2 β + T2 | α 4 δ δ gives [α]

def TensorTree.getIndicesLeft (stx : Lean.Syntax) : Lean.Elab.TermElabM (List (Lean.TSyntax `indexExpr))

Gets the indices associated with the LHS of an addition.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.getIndicesRight (stx : Lean.Syntax) : Lean.Elab.TermElabM (List (Lean.TSyntax `indexExpr))

Gets the indices associated with the RHS of an addition.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.getIndicesLeftEq (stx : Lean.Syntax) : Lean.Elab.TermElabM (List (Lean.TSyntax `indexExpr))

Gets the indices associated with the LHS of an equality.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.getIndicesRightEq (stx : Lean.Syntax) : Lean.Elab.TermElabM (List (Lean.TSyntax `indexExpr))

Gets the indices associated with the RHS of an equality.

Equations

• One or more equations did not get rendered due to their size.

Modifying terms to tensor trees

def TensorTree.nodeTermMap (T : Lean.Term) : Lean.Term

For a term of the form T where T is S.F.obj (OverColor.mk c), tensorTermToTensorTree returns the term corresponding to the tensorNode T

Equations

• TensorTree.nodeTermMap T = Lean.Syntax.mkApp { raw := (Lean.mkIdent `TensorTree.tensorNode).raw } #[T]

def TensorTree.evalTermMap (l : List (ℕ × ℕ)) (T : Lean.Term) : Lean.Term

Given a list l of pairs ℕ × ℕ and a term T corresponding to a tensor tree, for each (a, b) in l, evalSyntax applies TensorTree.eval a b to T recursively. Here a is the position of the index to be evaluated and b is the value it is evaluated to.

For example, if l is [(1, 2), (1, 4)] and T is a tensor tree then evalSyntax l T is TensorTree.eval 1 4 (TensorTree.eval 1 2 T).

The list l is expected to be the output of getEvalPos.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.contrTermMap (l : List (ℕ × ℕ)) (T : Lean.Term) : Lean.Term

For each element of l : List (ℕ × ℕ) applies TensorTree.contr to the given term.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.prodTermMap (T1 T2 : Lean.Term) : Lean.Term

The syntax associated with a product of tensors.

Equations

• TensorTree.prodTermMap T1 T2 = Lean.Syntax.mkApp { raw := (Lean.mkIdent `TensorTree.prod).raw } #[T1, T2]

def TensorTree.negTermMap (T1 : Lean.Term) : Lean.Term

The syntax associated with a product of tensors.

Equations

• TensorTree.negTermMap T1 = Lean.Syntax.mkApp { raw := (Lean.mkIdent `TensorTree.neg).raw } #[T1]

def TensorTree.smulTermMap (c T : Lean.Term) : Lean.Term

The syntax associated with the scalar multiplication of tensors.

Equations

• TensorTree.smulTermMap c T = Lean.Syntax.mkApp { raw := (Lean.mkIdent `TensorTree.smul).raw } #[c, T]

def TensorTree.actionTermMap (c T : Lean.Term) : Lean.Term

The syntax associated with the group action of tensors.

Equations

• TensorTree.actionTermMap c T = Lean.Syntax.mkApp { raw := (Lean.mkIdent `TensorTree.action).raw } #[c, T]

def TensorTree.addTermMap (permSyntax T1 T2 : Lean.Term) : Lean.Elab.TermElabM Lean.Term

The syntax for a equality of tensor trees.

Equations

• One or more equations did not get rendered due to their size.

def TensorTree.equalTermMap (permSyntax T1 T2 : Lean.Term) : Lean.Elab.TermElabM Lean.Term

The syntax for a equality of tensor trees.

Equations

• One or more equations did not get rendered due to their size.

Syntax to tensor tree

partial def TensorTree.syntaxFull (stx : Lean.Syntax) : Lean.Elab.TermElabM Lean.Term

Takes a syntax corresponding to a tensor expression and turns it into a term correspondnig to a tensor tree.

Elaboration

def TensorTree.elaborateTensorNode (stx : Lean.Syntax) : Lean.Elab.TermElabM Lean.Expr

Takes a syntax corresponding to a tensor expression and turns it into an expression corresponding to a tensor tree.

Equations

• TensorTree.elaborateTensorNode stx = do let __do_lift ← TensorTree.syntaxFull stx let tensorExpr ← Lean.Elab.Term.elabTerm __do_lift.raw none pure tensorExpr

def TensorTree.tensorExprSyntax : Lean.ParserDescr

The tensor tree corresponding to a tensor expression.

Equations

• One or more equations did not get rendered due to their size.

Test cases