Abstract.
The ro-calculus
is a new calculus that integrates in a uniform and simple setting first-order rewriting,
ro-calculus and non-deterministic computations. The main design concept of the ro-calculus
is to make all the basic ingredients of rewriting explicit objects, in particular the
notions of rule application and multisets of results. This paper describes
the calculus from its syntax to its basic properties in the untyped case. The ro-calculus
embeds first-order conditional rewriting and ro-calculus and it can be used in order to
give an operational semantics to the rewrite based language ELAN. We show how the set-like
data structures are easily represented in ELAN and how this can be used in order to
specify the Needham-Scroeder public-key protocol.
Keywords: Rewriting, Strategy, Multisets, Matching. |