Properties of Normalization for a math based intermediate representation

TL;DR

This paper provides a formal analysis of the normalization transformation in Diderot program compilation, proving it preserves types, values, and terminates, thereby increasing confidence in its correctness.

Contribution

It introduces a formal proof that the normalization rewriting system is type-preserving, value-preserving, and terminating, enhancing reliability in the compiler.

Findings

Normalization is type-preserving

Normalization preserves tensor values

The rewriting system terminates

Abstract

The Normalization transformation plays a key role in the compilation of Diderot programs. The transformations are complicated and it would be easy for a bug to go undetected. To increase our confidence in normalization part of the compiler we provide a formal analysis on the rewriting system. We proof that the rewrite system is type preserving, value preserving (for tensor-valued expressions), and terminating.