Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search

TL;DR

This paper introduces a novel method for solving inhabitation problems in simply-typed lambda-calculus by leveraging a specialized lambda-calculus for proof search, enabling decision and counting solutions.

Contribution

It develops a comprehensive approach that extends Curry-Howard representations, providing inductive descriptions and recursive procedures for inhabitation decision and counting problems.

Findings

Provides a recursive decision procedure for inhabitation problems.

Develops counting functions for inhabitation solutions.

Extends Curry-Howard representation within lambda-calculus.

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.