| 释义 |
head normalisation theorem head normalisation theoremUnder the typed lambda-calculus, beta/delta reduction of theleft-most redex (normal order reduction) is guaranteed toterminate with a head normal form if one exists. See alsoChurch-Rosser theorem. |