Expressionse,b,f,a∷=xVariable∣x⇒bAbstraction∣f←aApplicationVariablesx∈k,x,y,…Numbersn∈0,1,2,… \small\begin{array}{lrcll} \mathrm{Expressions}\quad & e,b,f,a & {\Coloneqq} & x & \quad\mathrm{Variable} \\ & & {\mid} & x\Rightarrow b & \quad\mathrm{Abstraction} \\ & & {\mid} & f\leftarrow a & \quad\mathrm{Application} \\ \mathrm{Variables} & x & {\in} & \mathsf{k}, \mathsf{x}, \mathsf{y}, \dots \\ \mathrm{Numbers} & n & {\in} & 0, 1, 2, \dots \end{array} ExpressionsVariablesNumbers​e,b,f,axn​::=∣∣∈∈​xx⇒bf←ak,x,y,…0,1,2,…​VariableAbstractionApplication​