INVESTIGADORES
DÍAZ CARO Alejandro
artículos
Título:
Confluence via strong normalisation in an algebraic λ-calculus with rewriting
Autor/es:
BUIRAS, PABLO; DÍAZ-CARO, ALEJANDRO; JASKELIOFF, MAURO
Revista:
Electronic Proceedings in Theoretical Computer Science
Editorial:
Open Publishing Association
Referencias:
Año: 2012 vol. 81 p. 16 - 29
Resumen:
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.