Syntax 。入terms or入expressions: (Terms)M,N:=x入x.MMN ·pure入-calculus Add extra operations and data types ·2x.(X+1) ·入z.(x+2*y+z) ·(2×.(x+1)3=3+1 ·(2z.(X+2*y+z)5=X+2*y+5 Syntax •  terms or  expressions: (Terms) M, N ::= x | x. M | M N • pure -calculus • Add extra operations and data types • x. (x+1) • z. (x+2*y+z) • (x. (x+1)) 3 = 3+1 • (z. (x+2*y+z)) 5 = x+2*y+5