zbMATH — the first resource for mathematics

A \(\rho\)-calculus of explicit constraint application. (English) Zbl 1272.68172
MartĂ­-Oliet, N. (ed.), Proceedings of the fifth international workshop on rewriting logic and its applications (WRLA 2004), Barcelona, Spain, March 27–28, 2004. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 117, 51-67 (2005).
Summary: Theoretical presentations of the \(\rho\)-calculus often treat the matching constraint computations as an atomic operation although matching constraints are explicitly expressed. Actual implementations have to take a much more realistic view: computations needed in order to find the solutions of a matching equation can be really important in some matching theories and the substitution application usually involves a term traversal.
Following the works on explicit substitutions in the \(\lambda\)-calculus, we propose, study and exemplify a \(\rho\)-calculus with explicit constraint handling, up to the level of substitution applications. The approach is general, allowing the extension to various matching theories. We show that the calculus is powerful enough to deal with errors. We establish the confluence of the calculus and the termination of the explicit constraint handling and application sub-calculus.
For the entire collection see [Zbl 1271.68050].

68Q42 Grammars and rewriting systems
Full Text: Link