Substitutionen (Definition)

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

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

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

  Definitionsbereich: domσ mathend000#, Bildbereich: imgσ mathend000#.

• Substitution σ mathend000# auf Term t mathend000# anwenden: tσ mathend000#

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