# Unification and combination of a class of traversal strategies made with pattern matching and fixed-points

## TL;DR

This paper introduces a formal framework for combining traversal strategies and context insertions in term transformations, demonstrating their algebraic properties and correctness, with applications in deriving asymptotic PDE models.

## Contribution

It defines unification and combination operations for traversal strategies, proving their algebraic properties and correctness, advancing formal methods in term transformation techniques.

## Key findings

- Unification and combination operations are associative and congruent.
- These operations have neutral elements, forming algebraic structures.
- Operations are proven correct for complex term transformations.

## Abstract

Motivated by an ongoing project on computer aided derivation of asymptotic models governed by partial differential equations, we introduce a class of term transformations that consists of traversal strategies and insertion of contexts. We define unification and combination operations on this class which amount to merging transformations in order to obtain more complex ones. We show that the unification and combination operations enjoy nice algebraic properties like associativity, congruence and the existence of neutral elements. The main part of this paper is devoted to proving that the unification and combination operations are correct.