Programming Language Theory Concept

Pure untyped lambda calculus church numeral

Journey Statuslearning

\begin{matrix} 𝐭𝐞𝐫𝐦 \\ t & : : = & x \\ λ x . t \\ t t \\ 𝐯𝐚𝐥𝐮𝐞 \\ v & : : = & λ x . t \\ 𝐞𝐯𝐚𝐥𝐮𝐚𝐭𝐢𝐨𝐧 \\ \frac{t_{1} \to t_{1}^{'}}{t_{1} t_{2} \to t_{1}^{'} t_{2}} \\ \frac{t_{2} \to t_{2}^{'}}{v t_{2} \to v t_{2}^{'}} \\ (λ x . t_{1}) t_{2} \to [x \to t_{2}] t_{1} \end{matrix}