Closed combination of context-embedding iterative strategies

Walid Belkhir (1, 2) , Nicolas Ratier (1) , Duy Duc Nguyen (1) , Michel Lenczner (1)

1 FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174)
2 CASSIS - Combination of approaches to the security of infinite states systems

This work is motivated by the challenging problem of the computer-aided generation of approximations (viewed as a series of transformations) of partial derivative equations. In this framework, the approximations posed over complex settings are incrementally constructed by extending an approximation posed on a simple setting and combining these extensions. In order to formalize these extensions and their combination, we introduce a class of rewriting strategies, called context-embedding iterative strategies (CE-strategies, for short). Roughly speaking, the class of CE-strategies is constructed by means of adding contexts and an iteration operator allowing the definition of recursive strategies. We show that the class of CE-strategies is closed under combination with respect to a correctness-completeness criterion. It turns out that the class CE-strategies enjoy nice algebraic properties, namely, the combination is associative, has a neutral element, and all the elements are idempotents.

Mots clés: Strategies; Combination; Unification; Fixed-point

Domaines: Informatique [cs]; Informatique et langage [cs.CL]

Walid Belkhir, Nicolas Ratier, Duy Duc Nguyen, Michel Lenczner. Closed combination of context-embedding iterative strategies. [Technical Report] LORIA - Université de Lorraine; FEMTO-ST. 2016. ⟨hal-01277395v2⟩