Substitutionen (Definition)

• Signatur Σ = Σ₀∪…Σ_k,
• Term(Σ, V) ist kleinste Menge T mit V⊆T und ∀0≤i≤k, f∈Σ_i, t₁∈T,…, t_i∈T : f (t₁,…, t_i)∈T.

  (hier Anwendung für Terme, die Typen beschreiben)

• Substitution: partielle Abbildung σ : V→Term(Σ, V),

  Definitionsbereich: domσ, Bildbereich: imgσ.

• Substitution σ auf Term t anwenden: tσ

• σ heißt pur, wenn kein v∈domσ als Teilterm in imgσ vorkommt.