What is a Term?
The most usual terms we all know are arithmetic expressions built
on operators (or symbols) +, *, - , on numbers and on variables x, y, z,
etc. For instance, 1+2 is a term, (x+y)*2 is a term, (x+y) is a term and
it is a subterm of (x+y)*2 .
What are Term Rewriting Systems?
A Term Rewriting System is a set of rewrite rules, i.e. transformation rules on terms. For instance, x+0 -> x is a rewrite rule. Applying this rule to the term (1+0)+(0+0), can be done in the following way:
(1+0)+(0+0) -> 1 + (0 + 0)
where the rule x+0 -> x has been applied on the subterm (1+0) of (1+0)+(0+0), and the variable x has taken the value 1. Replacing x by 1 in the rule x+0 -> x, we obtain the instanciated rule 1+0 -> 1 meaning that we can replace subterm 1+0 by 1, hence thus:
(1+0)+(0+0) -> 1 + (0 + 0)
Similarly 1+(0+0) can be rewritten, and so on, until we get 1 which cannot be rewritten. It is a normal form.
(1+0)+(0+0) -> 1 + (0 + 0) -> 1 + 0 -> 1
Note that there is in fact another way to rewrite (1+0)+(0+0), where we first rewrite the second subterm (0+0):
(1+0)+(0+0) -> (1 + 0) + 0 -> 1 + 0 -> 1
What are reachable terms (or descendants)?
From term (1+0)+(0+0), with the term rewriting system R={x+0 -> x}, the set of reachable terms R*( (1+0)+(0+0) ) is equal to:
What is reachability analysis on term rewriting
systems?
Given a Tern Rewriting System R and two terms s and t,
reachability analysis consists in proving that, either
Why reachability analysis on Term Rewriting Systems well adapted for program verification?
Reachability analysis and the Timbuk tool are currently used for
verifying cryptographic protocols,
verifying Java applications, and verifying
higher-order functional programs.
How to experiment?
The Timbuk software
implements term rewriting systems, tree automata and reachability analysis.