Name
Abstract | ||
|---|---|---|
A rewrite system is called uniformly normalising if all its steps are perpetual, i.e. are such that if s → t and s has an infinite reduction, then t has one too. For such systems termination (SN) is equivalent to normalisation (WN). A well-known fact is uniform normalisation of orthogonal non-erasing term rewrite systems, e.g. the λI-calculus. In the present paper both restrictions are analysed. Orthogonality is seen to pertain to the linear part and non-erasingness to the non-linear part of rewrite steps. Based on this analysis, a modular proof method for uniform normalisation is presented which allows to go beyond orthogonality. The method is shown applicable to biclosed first- and second-order term rewrite systems as well as to a λ-calculus with explicit substitutions. |
Year | Venue | Keywords |
|---|---|---|
2001 | Lecture Notes in Computer Science | modular proof method,uniform normalisation,orthogonal non-erasing term,present paper,second-order term,infinite reduction,non-linear part,linear part,explicit substitution,systems termination,second order |
Field | DocType | ISBN |
Discrete mathematics,Normalisation by evaluation,Automated theorem proving,Algorithm,Orthogonality,Critical pair,Fundamental theorem,Modular design,Mathematics | Conference | 3-540-42117-3 |
Citations | PageRank | References |
4 | 0.46 | 12 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Zurab Khasidashvili | 1 | 307 | 25.40 |
| Mizuhito Ogawa | 2 | 135 | 23.17 |
| Vincent van Oostrom | 3 | 505 | 38.41 |