Encoding rewriting strategies in lambda-calculi with patterns

Germain Faure (1, 2)

1 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
2 TYPICAL - Types, Logic and computing

We propose a patch to the pure pattern calculus: we claim that this is strictly more powerful to define the application of the match fail as the pure \lambda-term defining the boolean false instead of the identity function as it is done in the original version of the pure pattern calculus~\cite{JayK09}. We show that using non algebraic patterns we are able to encode in a natural way any rewriting strategies as well as the branching construct | used in functional programming languages. We close the open question (raised in~\cite{Cirstea00,CirsteaK01}) whether rewriting strategies can be directly encoded in lambda-calculi with patterns.

Domaines: Langage de programmation [cs.PL]

Germain Faure. Encoding rewriting strategies in lambda-calculi with patterns. [Research Report] RR-7025, INRIA. 2009. ⟨inria-00413178v2⟩