Research proof index

Injectivity for booleans.

Injectivity for Church numerals

Rice's theorem: no SKI term is a non-trivial predicate. More specifically, say a term P is a predicate if, for every term x, P · x reduces to either TT or FF. A predicate P is trivial if either it always reduces to true, or always to false. This version of Rice's theorem derives a contradiction from the existence of a predicate P and...

Commuting evaluation with contraction. Evaluating index k and then contracting the pair i j equals contracting the corresponding pair k.succAbove i, k.succAbove j and then evaluating the residual index, up to the identity reindexing IsReindexing.succAbove_succSuccAbove_comm.

Reconstruction of a tensor from the evaluations of its last index: every t : Tensor S c is the sum over basis indices i of the evaluation evalT (Fin.last n) i t tensored with the basis covector basis ![c (Fin.last n)] (single.symm i), with the appended index permuted back into the last slot.

Basis expansion of a one-index tensor: every t : Tensor S ![c] is the sum over basis indices i of its evaluation coefficient toField (evalT 0 i t) times the corresponding basis tensor.