Kapitola 2. Lambda kalkul

Obsah

2.1. Operační sémantika lambda kalkulu

Lambda kalkul je teorie funkcí založená na velmi jednoduchém jazyce. Základní prvky tohoto jazyka (tzv. lambda výrazy) jsou pouze tři: proměnná, aplikace a abstrakce.

Pokud se některá proměnná x vyskytuje v kontextu abstrakce \x -> e, říkáme, že je ve výrazu e vázaná. Není-li proměnná vázaná, pak ji označujeme jako volnou.

Příklad 2.1.
Mějme lambda výraz \f -> (f x). Potom v podvýrazu (f x) je proměnná f vázaná a proměnná x volná.