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

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

2010-07-05

arxiv.org/abs/1007.0779v1

Computer Science

Logic in Computer Science

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-215682