- Regel (l, r)
, Schreibweise (l→r)
, mit
l, r∈Term(Σ, V)
- Regel (l→r)
an Position p
in
t∈Term(Σ)
anwenden,
um s
zu erhalten, Schreibweise
t→(l→r), ps
∃σ : V→Term(Σ) : t|p = lσ∧t[p : = rσ] = s
Beispiel: Regel
(l, r) = (f (x), g(x, x))
, Term
t = h(1, f (f (2)))
.
Position
p = [2]∈Pos(t)
, Teilterm
t|p = f (f (2))
,
Substitution
σ : x f (2)
mit
t|p = lσ
,
auf r
anwenden:
rσ = g(f (2), f (2))
,
in t
einsetzen:
s = t[p : = rσ] = h(1, rσ) = h(1, g(f (2), f (2)))
.
Johannes Waldmann
2015-12-11