VSL 2014: VIENNA SUMMER OF LOGIC 2014

Feebly not weakly

Author: Vincent Van Oostrom

PapersPapers with AbstractsAuthor IndexKeyword Index

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:
Disclaimer | Powered by EasyChair Smart Program