Programming Language Theory Flashcard

What are the syntax/values/evaluation relation for the untyped lambda calculus?

Books

Concepts

Deckpure-lambda-calculus

Question

What are the syntax/values/evaluation relation for the untyped lambda calculus?

Answer

Syntax:

\begin{matrix} t & : = & λ x . t \\ | & t t \end{matrix}

Values:

\begin{matrix} v & : = & λ x . t \end{matrix}

Evaluation rules, assuming call by value:

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