Egy funkcionális nyelven írt program függvénydefiníciókból
(melyek rekurzívak is lehetnek) és kiértékelendõ kezdeti
kifejezésbõl áll. A függvénydefiníció egy vagy több
egyenlõséget tartalmaz, melyek bal és jobb oldalból és az
egyenlõség jelbõl állnak.
A bal oldal definiálja a
függvény nevét és a formális argumentumait (paramétereit). A jobb
oldal (a törzs) specifikálja a függvény eredményét. A törzsben lévõ
kifejezés lehet egy érték, egy formális paraméter vagy egy
függvényhívás.
A kezdeti kifejezés az a kifejezés, melynek értékét
ki akarjuk számítani. A funkcionális program végrehajtása a
programban található függvénydefiníciók szövegében (az ún.
környezetben) található kezdeti kifejezések kiértékelésébõl
áll.
A kiértékelés redukciós lépések ismételt végrehajtása. Minden
redukciós lépésben (ezeket a -> jel indukálja) egy, a
kifejezésben található függvényhívás lecserélõdik
(redukálódik) a megfelelõ függvény törzsre (az egyenlõség
jobb oldalára) úgy, hogy közben a formális argumentumok helyébe az
aktuálisak helyettesítõdnek. Az olyan (al)kifejezést, melyben
található lecserélhetõ függvénydefiníció, redex-nek hívják
(lecserélhetõ kifejezés angol rövidítésébõl).
Az alap
elgondolás az, hogy a redukciós eljárás akkor áll le, amikor már
nincs a kifejezésben redex, és a kezdeti kifejezés a lehetõ
legegyszerûbb formában (ún. normál formában) van. Ekkor a
normál forma kiiratódik.
Egy kiértékelés lépései:
squareinc 7
|| ez a kezdeti kifejezés
-> square (inc
7)
-> square (7+1)
-> square 8
-> 8*8
->
64
Ha a kezdeti kifejezésnek nincs normál formája (pl. amikor
a kezdeti kifejezés kiértékelése nem terminál), akkor a nem véges
eredmény azon része nyomtatódik ki, mely már kiértékelõdött.
Mivel általában sok redex van egy kifejezésben, ezért a redukciós
lépéseket több különbözõ sorrendben is végre lehet hajtani.
A
kiértékelés sorrendjét az ún. redukciós stratégia határozza meg. A
mellékhatások hiányának követketében a kiértékelés eredménye nem
függ a redukciók sorrendjétõl. Ha minden redex eltûnik,
és a kezdeti kifejezés normál formában van, akkor a kiszámítás
eredménye (feltéve, ha a kiszámítás befejezõdik) mindig
ugyanaz lesz: vagyis a normálforma egyértelmû. De mégis a
sorrend nem teljesen lényegtelen. Néhány redukciós sorrend akkor sem
vezet normál formára, ha az létezik. Az ilyen esetekben a kiszámítás
nem fog terminálni, míg egy másik sorrend esetén igen. Néhány
nyelvben (Lisp, ML, Hpe) a függvény argumentumai mindig
redukálódnak, mielõtt a függvényhívást magát tekintenék, mint
redex-et. Az ilyen nyelveket hívják mohó (vagy szigorú)
programnyelveknek. Ezzel szemben a legtöbb funkcionális programnyelv
(mint a Miranda) esetében a redukálás lustán történik. A
lusta kiértékelést követõ nyelvekben a redex akkor és csak
akkor számítódik ki, ha értékét tudni kell egy redukciós lépés
elvégzéséhez.
A lusta kiértékelési sorrend mindig megtalálja a
normál formát, ha az létezik.