On Statman's Finite Completeness Theorem

TL;DR

This paper provides a comprehensive proof of Statman's finite completeness theorem and explores its implications for the lambda-definability and higher-order matching conjectures.

Contribution

It offers a complete, self-contained proof of a key theorem in lambda calculus and clarifies the relationship between two important conjectures.

Findings

Proof of Statman's finite completeness theorem

Establishment that lambda-definability implies higher-order matching conjecture

Clarification of the relationship between key conjectures in lambda calculus

Abstract

We give a complete self-contained proof of Statman's finite completeness theorem and of a corollary of this theorem stating that the $\lambda$-definability conjecture implies the higher-order matching conjecture.