Indexed Streams: A Formal Intermediate Representation for Fused Contraction Programs
summary
A formal operational IR called index streams models sparse tensors and relations as transition systems with index, value, ready and skip functions; multiplication is implemented as a merge-like intersection so composite streams fuse into a single traversal. A Lean proof shows eval(product)=product(eval) and similar homomorphisms under mild lawfulness conditions. A 540-line prototype, ET compiler, generates code comparable to TACO and outperforms SQL by up to 24× and DuckDB by about 1.5× on selected benchmarks, demonstrating product-as-merge fusion.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:46Positive algebra in Lean
- 4:15Index Streams as IR
- 5:42What is an Index Stream
- 8:48Stream multiplication and merge sort
- 11:59Compiling to code
- 12:42Performance vs Taco and DuckDB
- 13:47Correctness proof
- 15:12Q&A
related talks
16mA Compiler for Fused Relational Operations on Multisets
16mCompile-Time Java Stream Fusion via mapMulti
19mCompile-Time Java Stream Fusion via mapMulti
01h 05mAll the Languages Together
29mGeneralized Arrays for Stainless Frames
18mDBSP: A unified (practical) theory of databases, streams, and incremental computation
40mSuperfusion: Eliminating Intermediate Data Structures via Inductive Synthesis
33mTeIL: a type-safe imperative Tensor Intermediate Language