Name
Abstract | ||
|---|---|---|
Klop's Problem is finding a type for characterizing hereditary head normalizing terms, that is, lambda-terms whose Böhm trees do not contain the bottom. This paper proves that this problem does not have any solution by showing that the set of those terms is not recursively enumerable. This paper also gives a best-possible solution by providing an intersection type system with a countably infinite set of types such that typing in all these types characterizes hereditary head normalizing terms. By using the same technique, this paper also shows that the set of lambda-terms normalizing by infinite reduction is not recursively enumerable. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-78969-7_15 | FLOPS |
Keywords | Field | DocType |
recursively enumerable,hereditary head,best-possible solution,infinite reduction,hm tree,countably infinite,intersection type system | Countable set,Maximal set,Computer science,Recursively enumerable language,Algorithm,Recursive functions,Transitive closure | Conference |
Volume | ISSN | ISBN |
4989 | 0302-9743 | 3-540-78968-5 |
Citations | PageRank | References |
2 | 0.65 | 8 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Makoto Tatsuta | 1 | 111 | 22.36 |