von C-Otto » 22.02.10 10:17
Mit dem Zeichen "=" wird hier eine Substitution angedeutet (die ich sonst immer mit "/" schreibe). In diesem Kontext ist "=" also nicht die übliche Gleichheitsrelation, insbesondere folgt aus X=Y und Y=a nicht X=a. Im Folgenden verwende ich lieber "/", um Substitutionen anzudeuten.
Hier zwei Beispielsubstitutionen, um den Unterschied klarzumachen:
sigma1:
X/a
Y/f(X)
term: g(X, Y)
sigma1(term) = g(a, f(X))
sigma2:
X/a
Y/f(a)
sigma2(term) = g(a, f(a))
Es gilt aber sigma1(sigma1(term)) = sigma2(term) = g(a, f(a)).
Ein mgu muss aber schon nach einmaliger Anwendung "passen", es gibt hier keine Fixpunktberechnung oder ähnliches.
PS: Ich meinte jeweils a statt A
EDIT: Da stand oben mal komischer Kram zu "=". Jetzt passt es.
Dr. rer. nat. Carsten Otto
http://verify.rwth-aachen.de/otto/