A Formal System for the Universal Quantification of Schematic Variables

TL;DR

This paper introduces a typed lambda-calculus with a universal quantifier for schematic variables, combining features from pure type systems and Automath, ensuring desirable logical invariants and including a machine-checked specification.

Contribution

It presents a novel typed lambda-calculus with a universal quantifier for schematic variables, extending the $ ext{lambda} ightarrow$ calculus with desirable logical properties and a formal machine-checked specification.

Findings

The calculus achieves confluence, strong normalization, and type preservation.

It extends earlier systems in the $ ext{lambda} ext{delta}$ family with new features.

A machine-checked formalization of the calculus is provided.

Abstract

We advocate the use of de Bruijn's universal abstraction $\lambda^\infty$ for the quantification of schematic variables in the predicative setting and we present a typed $\lambda$-calculus featuring the quantifier $\lambda^\infty$ accompanied by other practically useful constructions like explicit substitutions and expected type annotations. The calculus stands just on two notions, i.e., bound rt-reduction and parametric validity, and has the expressive power of $\lambda\rightarrow$. Thus, while not aiming at being a logical framework by itself, it does enjoy many desired invariants of logical frameworks including confluence of reduction, strong normalization, preservation of type by reduction, decidability, correctness of types and uniqueness of types up to conversion. This calculus belongs to the $\lambda\delta$ family of formal systems, which borrow some features from the pure type systems and some from the languages of the Automath tradition, but stand outside both families. In particular, the calculus includes and evolves two earlier systems of this family. Moreover, a machine-checked specification of its theory is available.