Skip to Main content Skip to Navigation
Reports

Encoding rewriting strategies in lambda-calculi with patterns

Germain Faure 1, 2
2 TYPICAL - Types, Logic and computing
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
Abstract : 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.
Document type :
Reports
Complete list of metadata

Cited literature [4 references]  Display  Hide  Download

https://hal.inria.fr/inria-00413178
Contributor : Germain Faure <>
Submitted on : Thursday, September 3, 2009 - 5:23:15 PM
Last modification on : Thursday, March 5, 2020 - 6:20:15 PM
Long-term archiving on: : Saturday, November 26, 2016 - 12:09:28 PM

File

rapport.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00413178, version 2

Collections

Citation

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

Share

Metrics

Record views

299

Files downloads

166