Lambda kalkul: Porovnání verzí

Smazaný obsah Přidaný obsah
Řádek 11:
Mějme dány nejvýše spočetné množiny C resp. V (konstant resp. proměnných). Množinou všech lambda výrazů rozumíme množinu Λ (velká lambda) řetězů obsahujících symboly z <code>C ∪ V ∪ {(, ), λ}</code> takových, že:
<code>
# c ∈ C, => c ∈ Λ
# v ∈ V => v ∈ Λ
# M,N ∈ Λ → (M N) ∈ Λ
# x ∈ V, M ∈ Λ → (λ x . M) ∈ Λ
</code>
V dalším budeme označovat konstanty písmeny ''c, d, e, …'', proměnné odzadu tj. ''z, y, x, …'' a obecné λ-výrazy velkými písmeny latinky. Budeme také vynechávat závorky, tj. místo (''λ x.x'') budeme psát ''λ x.x'' (nebo jen ''λ xx''). Podobně výraz ''λx (x, y, z)'' budeme značit jako ''λx . x, y, z''.
(Tečka odděluje "argumenty" λ od těla λ-výrazu a umožňuje zkrácený zápis ''λ xy.y'' ve významu ''λ x (λ y (y))''. Jinými slovy, tečka nahrazuje levou závorku, ke které je pravá závorka co nejvíce vpravo - tj. u další pravé závorky)