The notation $A^T$ stands for the transpose of a matrix. It is not specific to machine learning, but rather standard notation in linear algebra. Other notations are sometimes used, for example $A'$.
A related operation is the adjoint $A^*$. The transpose and adjoint are equal for real matrices.
This may take the form of a quantity which is asserted to decrease continually and vanish when the machine stops.
Lambda calculus evaluation is a sequence of beta reduction steps. So for the lambda calculus (with or without types: types don't affect evaluation), you want a quantity (a positive integer) that decreases at each reduction step.
Such a quantity ...
After some research, I think I can answer this question by myself now.
Wikipedia is correct, that is
If the $\lambda $-calculus uses call by value reduction strategy, the term $(\lambda x.x)(y y)$ is a normal form.
Standard $\lambda $-calculus does not distinguish reduction strategies. It only gives you some Reduction Rules (e.g. $\...