November 12, 2021

First, λ-calculus has three entities: variable, abstraction and application. These can be written into:

$$ \begin{align*}e &::= x \\  &| \lambda x. e \\  &| e_1~e_2 \\\end{align*}  $$

The according syntax of Scheme is

$$ \begin{align*}e &::= x \\  &| (\lambda ~(x)~ e) \\  &| (e_1~e_2) \\\end{align*}  $$

Second, we can introduce

$$ (\texttt{define}~ \textit{var-name}~ e) $$

which is used to give a name to an expression, we can write:

$$ (\texttt{define} ~\textit{add-one} ~(λ ~(x)~ (+ ~x ~1))) $$

Which can be sugared into:

$$ (\texttt{define} ~(\textit{add-one} ~x)~ (+ ~x ~1)) $$

Third, we then enrich the syntax with number, boolean, if-else, cond and let-binding:

$$ \begin{align*}e &::= x \\  &| (\lambda ~(x)~ e) \\  &| (e_1~e_2) \\  &| n \\                &| (+~e_1~e_2) \\  &| (if~e_1~e_2~e_3) \\  &| true \\  &| false \\  &| (cond ~(e_1~e_2) ~(e_3~e_4) ~...) \\  &~~| (let ~([x_1~e_1]~[x_2~e_2]...) ~e ~...) \\             \end{align*} $$

Fourth, pretend not to be scared by some strange symbols, they're just conventions: