Some simple rippling examples

Claus-Peter Wirth

SEKI-Working-Paper SWP–2006–02

SEKI-Working-Paper ISSN 1860-5931 ^{UNIVERSITÄT DES SAARLANDES FACHRICHTUNG INFORMATIK D–66123 SAARBRÜCKEN GERMANY WWW: http://www.ags.uni-sb.de/}

This SEKI-Working-Paper was internally reviewed by: Erica Melis FR Informatik, Universität des Saarlandes, D–66123 Saarbrücken, Germany

E-mail: melis@activemath.org
WWW: http://www.activemath.org/~melis

Editor of SEKI series:

Claus-Peter Wirth Brandenburger Str. 42, D–65582 Diez, Germany

E-mail: wirth@logic.at
WWW: http://www.ags.uni-sb.de/~cp

Some simple rippling examples

Claus-Peter Wirth

July 18, 2008

Abstract

Keywords:

1 Simple Examples

Example 1.1

Given: rev(append(k, l)) = append(rev(l), rev(k)).

Note that all variables in this goal are sinks!

Goal: rev^{s}(append^{s}(cons^{↑}(x, k^{s}), l)) = append^{s}(rev^{s}(l), rev^{s}(cons^{↑}(x, k^{s}))). This goal is suggested by recursion analysis.

Wave-Rules:

(1)  rev^{s}(cons^{↑}(x, l^{s})) = append^{↑}(rev^{s}(l^{s}), cons(x, nil))
(2) append^{s}(cons^{↑}(x, k^{s}), l^{s}) = cons^{↑}(x, append^{s}(k^{s}, l^{s}))
(3) append^{s}(h^{s}, append^{↑}(k^{s}, l)) = append^{↑}(append^{s}(h^{s}, k^{s}), l)

Note that, when a wave-rule is applied, only variables marked as skeleton may be substituted by terms with a skeleton marker!

Reduction of left-hand side of goal:

rev^{s}(append^{s}(cons^{↑}(x, k^{s}), l))

Wave-rule (2) via {x ↦ x, k^{s} ↦ k^{s}, l^{s} ↦ l}:

rev^{s}(cons^{↑}(x, append^{s}(k^{s}, l)))

Wave-rule (1) via {x ↦ x, l^{s} ↦ append^{s}(k^{s}, l)}:

append^{↑}(rev^{s}(append^{s}(k^{s}, l)), cons(x, nil))

Fully rippled! Cross fertilization via {k ↦ k^{s}, l ↦ l} and removal of annotaton

append(append(rev(l), rev(k)), cons(x, nil))

Reduction of right-hand side of goal:

append^{s}(rev^{s}(l), rev^{s}(cons^{↑}(x, k^{s})))

Wave-rule (1) via {x ↦ x, l^{s} ↦ k^{s}}:

append^{s}(rev^{s}(l), append^{↑}(rev^{s}(k^{s}), cons(x, nil)))

Wave-rule (3) via {h^{s} ↦ rev^{s}(l), k^{s} ↦ rev^{s}(k^{s}), l ↦ cons(x, nil)}:

append^{↑}(append^{s}(rev^{s}(l), rev^{s}(k^{s})), cons(x, nil))

Fully rippled! After removal of annotation, this is equal to reduced form of left-hand side.

Example 1.2

Given: ¬Even(x), ¬Even(y), Even(x + y).

Note that all variables in this goal are sinks!

Goal: ¬Even^{s}(s^{↑}(s^{↑}(x^{s}))), ¬Even(y), Even^{s}(s^{↑}(s^{↑}(x^{s})) +^{s} y). This goal is suggested by recursion analysis.

Wave-Rules:

(4)  s^{↑}(x^{s}) +^{s} y^{s} = s^{↑}(x^{s} +^{s} y^{s})
(5) Even^{s}(s^{↑}(s^{↑}(x^{s}))) = Even^{s}(x^{s})

Note that, when a wave-rule is applied, only variables marked as skeleton may be substituted by terms with a skeleton marker!

Reduction of goal with wave-rule (5) via {x^{s} ↦ x^{s}}:

¬Even^{s}(x^{s}), ¬Even(y), Even^{s}(s^{↑}(s^{↑}(x^{s})) +^{s} y)

Wave-rule (4) via {x^{s} ↦ s^{↑}(x^{s}), y^{s} ↦ y}:

¬Even^{s}(x^{s}), ¬Even(y), Even^{s}(s^{↑}(s^{↑}(x^{s}) +^{s} y))

Wave-rule (4) via {x^{s} ↦ x^{s}, y^{s} ↦ y}:

¬Even^{s}(x^{s}), ¬Even(y), Even^{s}(s^{↑}(s^{↑}(x^{s} +^{s} y)))

Wave-rule (5) via {x^{s} ↦ x^{s} +^{s} y}:

¬Even^{s}(x^{s}), ¬Even(y), Even^{s}(x^{s} +^{s} y)

Fully rippled! Fertilization via {x ↦ x^{s}, y ↦ y}.

Example 1.3

Given: revtail(h, append(k, l)) = append(revtail(h, k), l).

Note that all variables in this goal are sinks!

Goal: revtail^{s}(cons^{↑}(x, h^{s}), append^{s}(k, l)) = append^{s}(revtail^{s}(cons^{↑}(x, h^{s}), k), l). This goal is suggested by recursion analysis.

Wave-Rules:

(6) revtail^{s}(cons^{↑}(x, k^{s}), l^{s}) = revtail^{s}(k^{s}, cons^{↓}(x, l^{s}))
(7) cons^{↓}(x, append^{s}(k^{s}, l^{s})) = append^{s}(cons^{↓}(x, k^{s}), l^{s})

Note that, when a wave-rule is applied, only variables marked as skeleton may be substituted by terms with a skeleton marker!

Reduction of left-hand side of goal:

revtail^{s}(cons^{↑}(x, h^{s}), append^{s}(k, l))

Wave-rule (6) via {x ↦ x, k^{s} ↦ h^{s}, l^{s} ↦ append^{s}(k, l)}:

revtail^{s}(h^{s}, cons^{↓}(x, append^{s}(k, l)))

Wave-rule (7) via {x ↦ x, k^{s} ↦ k, l^{s} ↦ l}:

revtail^{s}(h^{s}, append^{s}(cons^{↓}(x, k), l))

Fully rippled! Cross fertilization via {h ↦ h^{s}, k ↦ cons^{↓}(x, k), l ↦ l} and removal of annotaton

append(revtail(h, cons(x, k)), l)

Reduction of right-hand side of goal:

append^{s}(revtail^{s}(cons^{↑}(x, h^{s}), k), l)

Wave-rule (6) via {x ↦ x, k^{s} ↦ h^{s}, l^{s} ↦ k}:

append^{s}(revtail^{s}(h^{s}, cons^{↓}(x, k)), l)

Fully rippled! After removal of annotation, this is equal to reduced form of left-hand side.

Example 1.4

Given: Perm(l, l) = true.

Note that all variables in this goal are sinks!

Goal: Perm^{s}(cons^{↑}(x, l^{s}), cons^{↑}(x, l^{s})) = true.

This goal is suggested by recursion analysis.

Wave-Rules:

(8)  Perm(cons^{↑}(x, k^{s}), l^{s}) = Perm(k^{s}, delonce^{↓}(x, l^{s})) ⟵ mbp(x, l) = true
(9) Perm(cons^{↑}(x, k^{s}), l^{s}) = false ⟵ mbp(x, l) ≠ true
(10) delonce^{↓}(x, cons^{↑}(y, l^{s})) = l^{s}  ⟵ x = y
(11) delonce^{↓}(x, cons^{↑}(y, l^{s})) = cons^{↑}(y, delonce^{↓}(x, l^{s})) ⟵ x ≠ y

Note that, when a wave-rule is applied, only variables marked as skeleton may be substituted by terms with a skeleton marker!

Reduction of goal with wave-rule (8) via {x ↦ x, k^{s} ↦ l^{s}, l^{s} ↦ cons^{↑}(x, l^{s})}:

Perm^{s}(l^{s}, delonce^{↓}(x, cons^{↑}(x, l^{s}))) = true, mbp(x, cons(x, l)) ≠ true
Perm^{s}(cons^{↑}(x, l^{s}), cons^{↑}(x, l^{s})) = true, mbp(x, cons(x, l)) = true

First clause is reduced with wave-rule (10) via {x ↦ x, y ↦ x, l^{s} ↦ l^{s}}:

Perm^{s}(l^{s}, l^{s}) = true, x ≠ x, mbp(x, cons(x, l)) ≠ true

Perm^{s}(l^{s}, delonce^{↓}(x, cons^{↑}(x, l^{s}))) = true, x = x, mbp(x, cons(x, l)) ≠ true

The first clause is fully rippled and tautology by fertilization. The second clause is a reflexive tautology.

The remaining clause from above can be reduced with wave-rule (9) via {x ↦ x, k^{s} ↦ l^{s}, l^{s} ↦ cons^{↑}(x, l^{s})}:

false = true, mbp(x, cons(x, l)) = true

This simplifies to

mbp(x, cons(x, l)) = true

and then to the reflexive tautologies

true = true, x ≠ x mbp(x, l) = true, x = x