Programming Language Theory Concept

Full beta-reduction

Books

Journey Statusmastered Tags

In Pure/Untyped lambda calculus, this strategy is defined by the following rules:

$\frac{t_{1} \to t_{1}^{'}}{t_{1} t_{2} \to t_{1}^{'} t_{2}}$
$\frac{t_{2} \to t_{2}^{'}}{t_{1} t_{2} \to t_{1} t_{2}^{'}}$
$\frac{t_{2} \to t_{2}^{'}}{λ x . t_{2} \to λ x . t_{2}^{'}}$
$(λ x . t_{1}) t_{2} \to [x \to t_{2}] t_{1}$