Encoding rewriting strategies in lambda-calculi with patterns

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