| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 427731 | Information Processing Letters | 2012 | 5 Pages |
Abstract
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 Böhm tree of the term.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
