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"
}