Small-Step-Semantik des Lambda-Kalküls

Basis-Operation ist A[x/B]:

ersetze jedes freie Vorkommen von x in A durch B

• β-Konversion:

  (λx.A)B→_βA[x/B]

  wobei $\mathsf {FV}$(B) disjunkt zu $\mathsf {BV}$(A)

• α-Konversion: gebundene Umbenennung

  (λx.A)→_α(λy.A[x/y])

...und Abschluß unter Kontext (Inferenz-System?)

Bemerkungen:

• warum ist die Bedingung bei →_β nötig? (Beispiele)