Inleiding tot Lambda Calculus 2
Type HOC
Class Logica en formele systemen
Les 13
Vrije en gebonden variabelen
Definitie 2
Voor een λ-expressie van de vorm
λx.M
zegt men dat
λx een binding is van x in M
het bereik van de binding is M, dit wil zeggen dat alle (nog niet gebonden) voorkomens van x in λx.M
gebonden zijn.
In een λ-expressie heten alle voorkomens van variabelen die niet gebonden zijn vrij.
We defini¨eren nu de verzameling V V (M) die alle variabelen uit M bevat die minstens ´e´en keer vrij
voorkomen in M.
Definitie 3
Weze M ∈
Λ. De verzameling V V (M) van vrije variabelen van
M wordt gedefinieerd door:
∀∈
• x V : V V (x) = {x}
Substitutie
β-Gelijkheid
Rekenen
De zogenaamde Church getallen cn (n ∈ IN)worden gedefinieerd als volgt: cn λ.f.λ.x.(f)n x
Inleiding tot Lambda Calculus 2 1
Type HOC
Class Logica en formele systemen
Les 13
Vrije en gebonden variabelen
Definitie 2
Voor een λ-expressie van de vorm
λx.M
zegt men dat
λx een binding is van x in M
het bereik van de binding is M, dit wil zeggen dat alle (nog niet gebonden) voorkomens van x in λx.M
gebonden zijn.
In een λ-expressie heten alle voorkomens van variabelen die niet gebonden zijn vrij.
We defini¨eren nu de verzameling V V (M) die alle variabelen uit M bevat die minstens ´e´en keer vrij
voorkomen in M.
Definitie 3
Weze M ∈
Λ. De verzameling V V (M) van vrije variabelen van
M wordt gedefinieerd door:
∀∈
• x V : V V (x) = {x}
Substitutie
β-Gelijkheid
Rekenen
De zogenaamde Church getallen cn (n ∈ IN)worden gedefinieerd als volgt: cn λ.f.λ.x.(f)n x
Inleiding tot Lambda Calculus 2 1
