A simple proof of a theorem of Statman
| Autor: | Harry G. Mairson |
|---|---|
| Rok vydání: | 1992 |
| Předmět: | |
| Zdroj: | Theoretical Computer Science. 103:387-394 |
| ISSN: | 0304-3975 |
| DOI: | 10.1016/0304-3975(92)90020-g |
| Popis: | In this note, we reprove a theorem of Statman that deciding the βη-equality of two first-order typable λ-terms is not elementary recursive (Statman, 1982). The basic idea of our proof, like that of Statman's is the Henkin quantifier elimination procedure (Henkin, 1963). However, our coding is much simpler, and easy to understand. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|