Programming Language Theory Flashcard

What is the untyped calculus of booleans and numbers?

Books

Decklanguage theory

Question

Answer

A simple language with only natural numbers and booleans as primitives.

Terms:

\begin{matrix} t & : = & tru \\ | & fls \\ | & if t then t else t \\ | & 0 \\ | & succ t \\ | & pred t \\ | & iszero t \end{matrix}

Values:

\begin{matrix} v & : = & tru \\ | & fls \\ | & n v \\ n v & : = & 0 \\ | & succ n v \end{matrix}

Evaluation relation:

\frac{t_{1} \to t_{1}^{'}}{if t_{1} then t_{2} else t_{3} \to if t_{1}^{'} then t_{2} else t_{3}} if tru then t_{1} else t_{2} \to t_{1} if fls then t_{1} else t_{2} \to t_{2} \frac{t \to t^{'}}{succ t \to succ t^{'}} pred 0 \to 0 pred (succ t) \to t \frac{t \to t^{'}}{iszero t \to iszero t^{'}} iszero 0 \to tru iszero (succ n v) \to fls