Confluence via strong normalisation in an algebraic λ-calculus with rewriting

BUIRAS, PABLO; DÍAZ-CARO, ALEJANDRO; JASKELIOFF, MAURO

Electronic Proceedings in Theoretical Computer Science

Open Publishing Association

Año: 2012 vol. 81 p. 16 - 29

The linear-algebraic λ-calculus and the algebraic λ-calculus are untyped λ-calculi extended witharbitrary linear combinations of terms. The former presents the axioms of linear algebra in the formof a rewrite system, while the latter uses equalities. When given by rewrites, algebraic λ-calculi arenot confluent unless further restrictions are added. We provide a type system for the linear-algebraicλ-calculus enforcing strong normalisation, which gives back confluence. The type system allows anabstract interpretation in System F.