Compiling index notation to sums of products: a verified functional pearl

Abstract

Index notation writes a repeated index name for a summation, and any implementation must turn it into explicit loops. The translation is a small functional program, yet it has a classic trap: reusing the name of a contracted index as the name of the loop variable captures free occurrences of that name elsewhere in a product. We present a compiler from a calculus of named indices to sums of products (the plans of an einsum), written in a few lines of Lean 4 and proved correct. Bound names come from a counter, so capture cannot happen; typing is erased, so the correctness proof does not use it; and the whole proof rests on three small lemmas about summation, renaming and fresh names. Composed with a verified inference of the contracted names, the compiler turns an unannotated expression such as A^i_j B^j_k into the plan "ac,cb->ab". The development is about 600 lines, uses only the Lean core library, and is executable.

The record contains the manuscript (PDF and LaTeX sources, in the format of the Journal of Functional Programming) and the Lean 4 artifact (tic_lean_v1.0.zip), which builds with "bash build.sh" using Lean 4.35.0.

A mechanized calculus for index notation with automatic contraction
Luca Eliseo Pavesi
Submitted to Annals of Formalized Mathematics21 Oct 2026PreprintCC BY 4.0Full textZenodo
Model Counting as a Sum of Products: Verified Translation and Variable Elimination in Lean 4
Luca Eliseo Pavesi
Zenodo21 Oct 2026PreprintCC BY 4.0Full textZenodo
Home-based telerehabilitation after CABG: higher objectively verified adherence and 12-week functional outcomes in a single-center observational cohort
Yan Liu, Xugang Wang, Cuihua Wang +5
Frontiers in Cardiovascular Medicine15 Oct 2026Peer-reviewedCC BY 4.0Full textCardiovascular medicineCrossrefEurope PMCEurope PMCPMC
The flag major index on conjugacy classes of wreath products
Harel Rozenfeld
arXiv26 Oct 2026PreprintarXiv licenceFull textCombinatorics & discrete mathematicsarXiv
S_n-equivariant L-classes of Cartesian powers of Witt spaces and the Hodge index conjecture for symmetric products
Mohammadali Aligholi
arXiv2 Nov 2026PreprintCC BY 4.0Full textAlgebra & number theory Geometry & topologyarXiv

Cite

BibTeX RIS

BibTeX

@misc{pavesi2026compiling,
  title = {{Compiling index notation to sums of products: a verified functional pearl}},
  author = {Luca Eliseo Pavesi},
  howpublished = {Zenodo},
  year = {2026},
  month = oct,
  doi = {10.5281/zenodo.23544752},
  url = {https://zenodo.org/records/23544752},
  note = {CC BY 4.0},
}

RIS

TY  - UNPB
TI  - Compiling index notation to sums of products: a verified functional pearl
AU  - Luca Eliseo Pavesi
PY  - 2026
DA  - 2026/10/21
PB  - Zenodo
DO  - 10.5281/zenodo.23544752
UR  - https://zenodo.org/records/23544752
AB  - Index notation writes a repeated index name for a summation, and any implementation must turn it into explicit loops. The translation is a small functional program, yet it has a classic trap: reusing the name of a contracted index as the name of the loop variable captures free occurrences of that name elsewhere in a product. We present a compiler from a calculus of named indices to sums of products (the plans of an einsum), written in a few lines of Lean 4 and proved correct. Bound names come from a counter, so capture cannot happen; typing is erased, so the correctness proof does not use it; and the whole proof rests on three small lemmas about summation, renaming and fresh names. Composed with a verified inference of the contracted names, the compiler turns an unannotated expression such as A^i_j B^j_k into the plan "ac,cb->ab". The development is about 600 lines, uses only the Lean core library, and is executable.  The record contains the manuscript (PDF and LaTeX sources, in the format of the Journal of Functional Programming) and the Lean 4 artifact (tic_lean_v1.0.zip), which builds with "bash build.sh" using Lean 4.35.0.
ER  -

Abstract

Related

Cite