Substitutionen: Produkt

Produkt von Substitutionen: t(σ₁oσ₂) = (tσ₁)σ₂ mathend000#

Beispiel 1:

σ₁ = {X $\mapsto$ Y}, σ₂ = {Y $\mapsto$ a}, σ₁oσ₂ = {X $\mapsto$ a, Y $\mapsto$ a} mathend000#.

Beispiel 2 (nachrechnen!):

σ₁ = {X $\mapsto$ Y}, σ₂ = {Y $\mapsto$ X}, σ₁oσ₂ = σ₂ mathend000#

Eigenschaften:

• σ mathend000# pur ⇒ mathend000# σ mathend000# idempotent: σoσ = σ mathend000#
• σ₁ mathend000# pur ∧ mathend000# σ₂ mathend000# pur impliziert nicht σ₁oσ₂ mathend000# pur

Implementierung:

import Data.Map 
type Substitution = Map Identifier Term
times :: Substitution -> Substitution -> Substition