Conventions Body of n extends as far to the right as possible nx MN means Ax(M N, not(x M)N 入X.fx=λx.(fx) 入X.f.fx=x.(ffx) Function applications are left-associative MNP means(M N)P, not M(N P (入X.y.X-y)53=(x.y.x-y)5)3 (fx.fx)(X.X+1)2=((千.AX.fx)(^x,X+1))2Conventions • Body of  extends as far to the right as possible x. M N means x. (M N), not (x. M) N • x. f x = x. ( f x ) • x. f. f x = x. ( f. f x ) • Function applications are left-associative M N P means (M N) P, not M (N P) • (x. y. x - y) 5 3 = ( (x. y. x - y) 5 ) 3 • (f. x. f x) (x. x + 1) 2 = ( (f. x. f x) (x. x + 1) ) 2