You are here: irt.org | FOLDOC | head normalisation theorem
Under the typed lambda-calculus, beta/delta reduction of the left-most redex (normal order reduction) is guaranteed to terminate with a head normal form if one exists. See also Church-Rosser theorem.
Nearby terms: Head Disk Assembly « header « Head Normal Form « head normalisation theorem » heads down » head-strict » heap
FOLDOC, Topics, A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, ?, ALL