Feebly not weakly
Author: Vincent Van Oostrom
Paper Information
| Title: | Feebly not weakly |
| Authors: | Vincent Van Oostrom |
| Proceedings: | HOR 2014 Workshop Proceedings |
| Editor: | Kristoffer Rose |
| Keywords: | unification, pattern, linear, geometric, critical peak, orthogonalisation, feeble orthogonality, critically trivial |
| Abstract: | ABSTRACT. Some rewrite systems are not orthogonal, in that they do have critical peaks, but are very close to being orthogonal, in that for any given object there exists a partial function, called orthogonalisation, mapping the set of all redexes to an orthogonal subset and every multi-step to an equivalent one. Term rewrite systems having only trivial peaks, so-called weakly orthogonal systems with the lambda-beta-eta-calculus as prime example, are known to admit such an orthogonalisation. Here we characterise the term rewrite systems that admit orthogonalisation as those whose critical peaks are feeble, in that at least two out of the three terms in such a peak must be identical (generalising weak orthogonality). |
| Pages: | 0 |
| Talk: | Jul 12 11:15 |
| Paper: | ![]() |
