Extending critical pairs advances analysis of higher-order rewriting
Extending Higher-Order Critical Pairs
Logic in Computer Science
Summary
When computer programs can be written in many different ways, it’s important to make sure different versions still give the same result. The authors work on improving a key tool—called critical pairs—that helps check if different rewriting steps conflict. They extend this tool to cover more complex kinds of rewriting used in advanced programming and transformations. This helps computer scientists better analyze and trust program changes and computations.
What this means in practice
- •For programming language designers: Analyze and certify correctness of language transformations involving complex higher-order rewriting rules.
- •For software refactoring engineers: Improve tools that verify correctness of automated code refactoring by capturing complex rewrite conflicts.
A theory result. No direct application yet.
Authors
Johannes Niederhauser, Aart Middeldorp
Abstract
Confluence is a fundamental property of computation which implies that the nondeterminism of a system does not affect its outcomes. A key concept of confluence research in rewriting theory is the notion of critical pairs which captures the potential local sources of non-confluence. In this paper, we lift the definition of higher-order critical pairs to a more expressive class of higher-order rewrite systems. Thereby, we facilitate confluence analysis of rewrite systems which can express complex one-step computations as well as program transformations from functional programming.