Feebly not weakly


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 λβη-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).