Wiederholung: Operationale Semantik

(SOS - small step operational semantics)

Ein-Schritt-Relation

• β-Reduktion: (λx.M)N→_βM[x : = N]

falls bound-vars(M) und free-vars(N) disjunkt.

bei Bedarf gebundene Var. umbenennen

• α-Reduktion: λx.M→_αλy.M[x : = y]

Abschluß von →_β unter Kontexten:

• A₁→_βA₂⇒A₁B→_βA₂B, BA₁→_βBA₂, λxA₁→_βλxA₂

operationale Semantik (= Programmausführung)
ist reflexive transitive Hülle →_β^* (Mehr-Schritt-Relation)