Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search

TL;DR

This paper investigates redundancies in dependently typed lambda calculi like LF, identifying syntactic criteria to eliminate unnecessary typing information, thereby improving proof search efficiency and expression compactness.

Contribution

It introduces the concept of 'rigidity' in LF types, providing formal criteria to recognize and remove redundant typing, enhancing translation and execution of specifications.

Findings

Identified 'rigidity' as a key property for redundancy detection.

Proposed a translation approach exploiting rigidity to optimize proof search.

Discussed implications for compact representation of dependently typed expressions.

Abstract

Dependently typed lambda calculi such as the Logical Framework (LF) are capable of representing relationships between terms through types. By exploiting the "formulas-as-types" notion, such calculi can also encode the correspondence between formulas and their proofs in typing judgments. As such, these calculi provide a natural yet powerful means for specifying varied formal systems. Such specifications can be transformed into a more direct form that uses predicate formulas over simply typed lambda-terms and that thereby provides the basis for their animation using conventional logic programming techniques. However, a naive use of this idea is fraught with inefficiencies arising from the fact that dependently typed expressions typically contain much redundant typing information. We investigate syntactic criteria for recognizing and, hence, eliminating such redundancies. In particular, we identify a property of bound variables in LF types called "rigidity" and formally show that checking that instantiations of such variables adhere to typing restrictions is unnecessary for the purpose of ensuring that the overall expression is well-formed. We show how to exploit this property in a translation based approach to executing specifications in the Twelf language. Recognizing redundancy is also relevant to devising compact representations of dependently typed expressions. We highlight this aspect of our work and discuss its connection with other approaches proposed in this context.