Beispiel: S.R. und Term-Ersetzung

Regeln für symbolisches Differenzieren (nach t):

 D(t) -> 1         D(constant) -> 0
 D(+(x,y)) -> +(D(x),D(y))
 D(*(x,y)) -> +(*(y,D(x)),*(x,D(y)))
 D(-(x,y)) -> -(D(x),D(y))

Robert Floyd 1967, zitiert in: Nachum Dershowitz: 33 Examples of Termination, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.9447

• Korrektheit? Termination? Komplexität?
• Strategie (Auswahl von Regel und Position)?
• ausreichend? angemessen?