Übung zu Termgleichungen

• sind die Substitutionen σ₁ = {X $\mapsto$ Y} mathend000# und σ₂ = {Y $\mapsto$ X} mathend000# vergleichbar bzgl. ≤ mathend000#?
• ≤ mathend000# auf Substitutionen ist keine Halbordnung.

  Die durch ≤ mathend000# definierte Äquivalenzrelation ist ...

• vervollständigen Sie den Unifikationsalgorithmus, vergleichen Sie mit http://dfa.imn.htwk-leipzig.de/cgi-bin/gitweb.cgi?p=ws11-cb.git;a=blob;f=kw56/Type/Constraint.hs;hb=master
• wenden Sie den Algorithmus an zur Lösung von
  f (X₁, f (X₂, f (X₃, a))) = f (f (X₂, X₂), f (f (X₃, X₃), f (a, a)))

  mathend000#