λ-račun#
Najpomembnejše mesto v teoriji programskih jezikov zaseda λ-račun, ki tvori jedro vsakega funkcijskega programskega jezika.
Sintaksa#
Za razliko od IMPa sintaksa λ-računa vsebuje le eno vrsto izrazov:
Vsak izraz lahko predstavlja:
spremenljivko,
abstrakcijo (oziroma lambdo), ki predstavlja funkcijo s parametrom
in telesom , teraplikacijo, ki funkcijo, predstavljeno z
, uporabi na argumentu, predstavljenim z izrazom .
Na primer:
predstavlja identično funkcijo, predstavlja funkcijo, ki sprejme argument in vrne konstantno funkcijo, ki vedno vrne , predstavlja kompozitum, ki sprejme funkciji in ter vrne funkcijo, ki na najprej uporabi , nato pa še .
Če bi želeli, bi lahko izraze razširili še z drugimi konstrukti, na primer aritmetičnimi operacijami ali pogojnimi izrazi, vendar bomo videli, da jih načeloma ne potrebujemo, zato zaenkrat počakajmo z njimi.
Parameter abstrakcije je vezana spremenljivka, zato na primer izraza
Funkcije bomo uporabili tako, da bomo vse pojavitve parametra v telesu zamenjali z argumentom. V ta namen rekurzivno definiramo substitucijo
Kot vidimo, moramo paziti, da pri substituciji abstrakcij ne bi zamenjali vezane spremenljivke. Na primer (saj
Operacijska semantika#
Ukazi v IMPu so zaključili izvajanje, ko so prispeli do ukaza
Ker lahko izrazi v lambda računu divergirajo, bomo tako kot v IMPu tudi tu podali semantiko malih korakov
Prvo pravilo govori o tem, da najprej do vrednosti izračunamo prvi člen. Ko je ta izračunan, lahko uporabimo drugo pravilo in izračunamo še drugi člen. Če sta oba vrednosti (in je prvi funkcija), lahko funkcijo s pomočjo substitucije uporabimo na argumentu. Zadnji korak ima posebno ime in sicer β-redukcija.
Izbrana pravila niso edini način, na katerega lahko podamo semantiko λ-računa. V lenih funkcijskih jezikih, kot je Haskell, argumenta pred β-redukcijo ne gremo računati, saj ga morda ne bomo nikoli potrebovali. Takemu načinu računanja pravimo leno izvajanje, oziroma call-by-name ali CBN. Načinu izvajanja, ki smo ga spoznali prej, pravimo neučakano izvajanje, oziroma call-by-value. Leno izvajanje bi podali samo s praviloma:
Churchevo kodiranje#
Izkaže se, da lahko s pomočjo funkcij predstavimo tudi ostale vrednosti, ki jih običajno srečamo v programskih jezikih.
Naravna števila#
Na primer naravno število
Na primer
lahko pa tudi kot
da najprej
Podobno lahko definiramo tudi seštevanje in množenje:
Pri seštevanju
Logične vrednosti#
Logični vrednosti predstavimo s funkcijama, ki vzameta dva argumenta, vrneta pa prvega oziroma drugega:
Predikat, ki ugotovi, ali je naravno število nič, lahko definiramo kot:
Torej,
Rekurzija#
Recimo, da bi radi definirali:
Za razliko do prejšnjih definicij se ta ne sklicuje samo na poprej definirane izraze, temveč tudi sama nase. Ciklične definicije se lahko znebimo tako, da problem prevedemo na iskanje fiksne točke. Definirajmo:
Vse je tako kot v definiciji
Pri izračunu fiksne točke si pomagamo z Y-kombinatorjem:
Definicija Y-kombinatorja je malo nenavadna, zato si najprej oglejmo, kako se izvaja izraz
Da ne bo zmešnjave, pred tem v drugi abstrakciji preimenujmo
Velja torej
Dobili smo izraz, ki intuitivno predstavlja fiksno točko
Poglejmo, zakaj
Na tej točki se izvajanje ustavi, saj smo dobili funkcijo. Če jo uporabimo na številu
Sedaj je izvajanje odvisno od vrednosti