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.





< Previous Terms Terms Containing head normalisation theorem Next Terms >
HDTV
hdx
Head Disk Assembly
header
Head Normal Form
 heads down
head-strict
heap
heartbeat
heatseeker