päänormaali

Päänormaali (head normal form, HNF) on käsite lambda-laskennassa. Se kertoo, millaisessa muodossa termi esiintyy, kun ei voida suorittaa beta- reduktiota pään kohdasta. Toisin sanoen päänormaali on tila, jossa ulkokuoren pääosa ei ole lambda-abstraktioilla aloitettu redexi, tai termi on lambda-abstraktio, jonka sisällä voi olla reduktioita, mutta joidenkin ulkona näkyvien muotojen reducointi on pysäytetty.

Määritelmä voidaan esittää seuraavasti: termi on päänormaali, jos se on joko lambda-abstraktio λx. M, tai sovellus, jonka pääosa on muuttuja tai vakio (ei lambda) ja jonka alaosat ovat itsessään päänormaaleja. Tämä tarkoittaa käytännössä, että ulkoinen rakenne ei ala beta-reduktiolla, vaikka termissä sisällä voikin esiintyä reduktioita.

Päänormaali ja beta-normaali muoto eroavat: jokainen beta-normaali termi on päänormaali, mutta ei päinvastoin. Esimerkiksi λx. x on sekä päänormaali että beta-normaali. Toisaalta termi λx. (λy. y) x on päänormaali, mutta ei beta-normaali, sillä sisäpuolella oleva (λy. y) x on beta-reduktio.

Käyttö ja sovellukset: päänormaaliin evaluoinnissa korostuvat erityisesti vasemmanlaiskaiset (leftmost-outermost) vähentämiset sekä lazy-evaluaatioissa värähtelyä kuvaavat neutrals-luokat. Päänormaali on hyödyllinen käsite analyysissä, kun tarkastellaan, miten termiä voidaan vähentää tai miten sen päämuoto pysyy vakaana evaluoinnin aikana.