  Parsing Expression Grammars (PEGs) are a recognition-based formalism which
allows to describe the syntactical and the lexical elements of a language. The
main difference between Context-Free Grammars (CFGs) and PEGs relies on the
interpretation of the choice operator: while the CFGs' unordered choice e | e'
is interpreted as the union of the languages recognized by e and e, the PEGs'
prioritized choice e/e' discards e' if e succeeds. Such subtle, but important
difference, changes the language recognized and yields more efficient parsing
algorithms. This paper proposes a rewriting logic semantics for PEGs. We start
with a rewrite theory giving meaning to the usual constructs in PEGs. Later, we
show that cuts, a mechanism for controlling backtracks in PEGs, finds also a
natural representation in our framework. We generalize such mechanism, allowing
for both local and global cuts with a precise, unified and formal semantics.
Hence, our work strives at better understanding and controlling backtracks in
parsers for PEGs. The semantics we propose is executable and, besides being a
parser with modest efficiency, it can be used as a playground to test different
optimization ideas. More importantly, it is a mathematical tool that can be
used for different analyses.
