Conservativity of embeddings in the lambda Pi calculus modulo rewriting (long version)

TL;DR

This paper proves that embeddings of pure type systems into the lambda Pi calculus with rewriting are conservative without requiring the target system to be normalizing, broadening the framework's applicability.

Contribution

It establishes a conservative embedding result for lambda Pi calculus modulo rewriting without assuming normalization of the source or target systems.

Findings

Proves a relative form of normalization for embeddings

Shows the embedding is conservative without normalizing assumptions

Validates lambda Pi calculus modulo rewriting as a logical framework

Abstract

The lambda Pi calculus can be extended with rewrite rules to embed any functional pure type system. In this paper, we show that the embedding is conservative by proving a relative form of normalization, thus justifying the use of the lambda Pi calculus modulo rewriting as a logical framework for logics based on pure type systems. This result was previously only proved under the condition that the target system is normalizing. Our approach does not depend on this condition and therefore also works when the source system is not normalizing.