  which expresses the meaning of \(\lambda x.M\) as a function. We have used \(M[x:=N\)] as a notation for the value of the expression that results when \(N\) is substituted for the variable \(x\) in the matrix \(M\). One usually sees this equation as a rewrite rule \((\beta\)-reduction)