THEORETICAL PEARLS: A bargain for intersection types: a simple strong normalization proof
| Autor: | Peter Møller Neergaard |
|---|---|
| Rok vydání: | 2005 |
| Předmět: | |
| Zdroj: | Journal of Functional Programming. 15:669 |
| ISSN: | 1469-7653 0956-7968 |
| DOI: | 10.1017/s0956796805005587 |
| Popis: | This pearl gives a discount proof of the folklore theorem that every strongly $\beta$-normalizing $\lambda$-term is typable with an intersection type. (We consider typings that do not use the empty intersection $\omega$ which can type any term.) The proof uses the perpetual reduction strategy which finds a longest path. This is a simplification over existing proofs that consider any longest reduction path. The choice of reduction strategy avoids the need for weakening or strengthening of type derivations. The proof becomes a bargain because it works for more intersection type systems, while being simpler than existing proofs. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|