Rewriting Modulo \beta in the \lambda\Pi-Calculus Modulo

TL;DR

This paper introduces rewriting modulo beta in the lambda-Pi-calculus Modulo, ensuring key logical properties under broader conditions by encoding it into Higher-Order Rewrite Systems.

Contribution

It extends the lambda-Pi-calculus Modulo with a notion of rewriting modulo beta, enabling confluence and logical properties without requiring full confluence of the combined system.

Findings

Rewriting modulo beta ensures subject reduction and uniqueness of types.

Encoding into Higher-Order Rewrite Systems allows leveraging existing confluence results.

The approach broadens the applicability of the lambda-Pi-calculus Modulo in logical frameworks.

Abstract

The lambda-Pi-calculus Modulo is a variant of the lambda-calculus with dependent types where beta-conversion is extended with user-defined rewrite rules. It is an expressive logical framework and has been used to encode logics and type systems in a shallow way. Basic properties such as subject reduction or uniqueness of types do not hold in general in the lambda-Pi-calculus Modulo. However, they hold if the rewrite system generated by the rewrite rules together with beta-reduction is confluent. But this is too restrictive. To handle the case where non confluence comes from the interference between the beta-reduction and rewrite rules with lambda-abstraction on their left-hand side, we introduce a notion of rewriting modulo beta for the lambda-Pi-calculus Modulo. We prove that confluence of rewriting modulo beta is enough to ensure subject reduction and uniqueness of types. We achieve our goal by encoding the lambda-Pi-calculus Modulo into Higher-Order Rewrite System (HRS). As a consequence, we also make the confluence results for HRSs available for the lambda-Pi-calculus Modulo.