Name
Abstract | ||
|---|---|---|
Affine terms are lambda terms in which no variable occurs twice, and linear terms are affine terms in which each bound variable occurs exactly once. The principal type of a term is the most general type which is assignable to the term. Hirokawa gave characterisations of the principal types of linear terms and of beta-normal affine terms. Shouji gave a characterisation of the principal types of beta-eta-normal linear terms. The proofs of these three theorems are parallel, but independent to each other. This paper points out that by using Berardi's pruning, the theorem on beta-normal affine terms is obtained from the theorem on linear terms. This is the first result. And also this paper shows a characterisation of principal types of beta-eta-normal affine terms. Its proof is obtained from the theorem on beta-eta-normal linear terms by Berardi's pruning. This is the second result. Besides, this paper gives other proofs of the the theorems on eta-normal terms. This is the third result. |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1016/S1571-0661(05)80336-6 | Electr. Notes Theor. Comput. Sci. |
Field | DocType | Volume |
Affine transformation,Discrete mathematics,Principal type,Mathematical proof,Mathematics,Pruning,Lambda | Journal | 31 |
ISSN | Citations | PageRank |
Electronic Notes in Theoretical Computer Science | 0 | 0.34 |
References | Authors | |
1 | 1 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Izumi Takeuti | 1 | 16 | 4.73 |