An alternate proof of Statman's finite completeness theorem

摘要

Statman's finite completeness theorem says that for every pair of non-equivalent terms of simply-typed lambda-calculus there is a model that separates them. A direct method of constructing such a model is provided using a simple induction on the Boehm tree of the term.