10. Rewriting

Question 1

What restrictions must a rewrite rule (a => b) satisfy?

Answer 1

• a is not a variable
• vars(b) ⊆ vars(a)

Question 2

What does this mean?

Answer 2

Zero or more rewrite rule application

Question 3

What does this mean?

Answer 3

(should be and)

Question 4

What does this mean?

Answer 4

Question 5

What is a redex?

Answer 5

Any subexpression that can be rewritten (reducible expression)

Question 6

When is a set of rewrite rules terminating?

Answer 6

Starting with any expression, successively apply rewrite rules eventually brings us to a state where no rule applies

Question 7

What is terminating also called?

Answer 7

(strongly) normalizing or noetherian

Question 8

What is normal form?

Answer 8

An expression were no rewrite rules apply is called a normal form (w.r.t. a set of rewrite rules)

Question 9

How can you prove termination?

Answer 9

1. Define natural number measure on expressions

2. Show that each rule application reduces the measure
   Measure cant go bellow zero, so any sequence will terminate

Question 10

What is canonical normal form?

Answer 10

If all normal forms for s are identical, s has a canonical normal form

Question 11

What does it mean for a set of rewrite rules to be confluent?

Answer 11

For every r, s₁, s₂

Question 12

What does it mean for a rewrite set that is confluent and terminating?

Answer 12

Any expression will rewrite to a canonical normal form

Question 13

What does it mean for a set of rewrite rules to be locally confluent?

Answer 13

For every r, s₁, s₂

Question 14

What is newmans lemma (rewriting)?

Answer 14

local confluence + termination = confluence

Question 15

What is the Knuth-Bendix (KB) completion algorithm?

Answer 15

1. Take a critical pair [1, s₂ ] in R
2. Normalize s₁ to s₁’ and s₂ to s₂’
3. If R union {s₁’ => s₂’} is termination add it to R, otherwise if R union {s₂’ => s₁’} is terminating add it to R otherwise fail

Question 16

What is the rewrite rule of inference?

Answer 16

Question 17

What conditions does isabelle apply a rewrite rule in the form

[| P_1, …, P_n |] ==> s = t

Answer 17

Question 18

Advantages of rewritting?

Answer 18

• Efficent
• if confluent + termination: decision procedure for equational goals in the theory defined by the rules

Question 19

Disadvantages of rewritting?

Answer 19

• Not complete if non-confluent or non-terminating
• Knowledge and goals must often be represented in the form of equations