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

with Pablo Buiras and Alejandro Díaz-Caro. LSFA 2011.PDF

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 interpretation in System F.

BibTeX

@InProceedings{BuirasDiazcaroJaskelioffLSFA11,
    author = "Pablo Buiras and Alejandro D{\'\i}az-Caro and Mauro Jaskelioff,
    title = "Confluence via strong normalisation in an algebraic $\lambda$-calculus with rewriting",
    pages = "16--29",
    year = "2012",
    editor = "Simona {Ronchi della Rocca} and Elaine Pimentel",
    booktitle = "Proceedings of the 6th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2011)",
    series = "Electronic Proceedings in Theoretical Computer Science",
    volume = "81",
    publisher = "Open Publishing Association"
}