10. Rewriting Flashcards
What restrictions must a rewrite rule (a => b) satisfy?
- a is not a variable
- vars(b) ⊆ vars(a)
What does this mean?
Zero or more rewrite rule application
What does this mean?
(should be and)
What does this mean?
What is a redex?
Any subexpression that can be rewritten (reducible expression)
When is a set of rewrite rules terminating?
Starting with any expression, successively apply rewrite rules eventually brings us to a state where no rule applies
What is terminating also called?
(strongly) normalizing or noetherian
What is normal form?
An expression were no rewrite rules apply is called a normal form (w.r.t. a set of rewrite rules)
How can you prove termination?
1. Define natural number measure on expressions
- Show that each rule application reduces the measure
Measure cant go bellow zero, so any sequence will terminate
What is canonical normal form?
If all normal forms for s are identical, s has a canonical normal form
What does it mean for a set of rewrite rules to be confluent?
For every r, s1, s2
What does it mean for a rewrite set that is confluent and terminating?
Any expression will rewrite to a canonical normal form
What does it mean for a set of rewrite rules to be locally confluent?
For every r, s1, s2
What is newmans lemma (rewriting)?
local confluence + termination = confluence
What is the Knuth-Bendix (KB) completion algorithm?
- Take a critical pair [1, s2 ] in R
- Normalize s1 to s1’ and s2 to s2’
- If R union {s1’ => s2’} is termination add it to R, otherwise if R union {s2’ => s1’} is terminating add it to R otherwise fail
What is the rewrite rule of inference?
What conditions does isabelle apply a rewrite rule in the form
[| P_1, …, P_n |] ==> s = t
