Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search
Abstract
A new, comprehensive approach to inhabitation problems in simply-typed lambda-calculus is shown, dealing with both decision and counting problems. This approach works by exploiting a representation of the search space generated by a given inhabitation problem, which is in terms of a lambda-calculus for proof search that the authors developed recently. The representation may be seen as extending the Curry-Howard representation of proofs by lambda-terms, staying within the methods of lambda-calculus and type systems. Our methodology reveals inductive descriptions of the decision problems, driven by the syntax of the proof-search expressions, and the end products are simple, recursive decision procedures and counting functions.
Keywords
Cite
@article{arxiv.1604.02086,
title = {Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search},
author = {José Espírito Santo and Ralph Matthes and Luís Pinto},
journal= {arXiv preprint arXiv:1604.02086},
year = {2017}
}
Comments
16 pages + 3 pages appendix (an error in the original version was detected, the proofs are very different and are based on new definitions)