Confluence via strong normalisation in an algebraic \lambda-calculus with rewriting
Pablo Buiras, Alejandro D\'iaz-Caro, Mauro Jaskelioff
TL;DR
This paper introduces a type system for the linear-algebraic lambda-calculus that enforces strong normalisation, ensuring confluence in a calculus extended with linear combinations of terms.
Contribution
It provides a novel type system that guarantees strong normalisation and confluence in an algebraic lambda-calculus with rewriting, enabling abstract interpretation in System F.
Findings
The type system enforces strong normalisation.
Ensures confluence in algebraic lambda-calculi with rewriting.
Allows abstract interpretation in System F.
Abstract
The linear-algebraic lambda-calculus and the algebraic lambda-calculus are untyped lambda-calculi extended with arbitrary linear combinations of terms. The former presents the axioms of linear algebra in the form of a rewrite system, while the latter uses equalities. When given by rewrites, algebraic lambda-calculi are not confluent unless further restrictions are added. We provide a type system for the linear-algebraic lambda-calculus enforcing strong normalisation, which gives back confluence. The type system allows an abstract interpretation in System F.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.