Reduceri

In orice sistem algebric de calcul, scriem calcule sub forma unor siruri de egalitati intre formule echivalente, din ce in ce mai simple, de obicei.

Exemplu din aritmetica:

	(2+2)*(3+2)
=	4 * (3+2)
=	4 * 5
=	20

Observati ca termii se transforma in termi mai simpli (la fel si subtermii lor) iar numarul de operatii de facut se reduce. Acest proces il intalnim si in lambda calcul si se numeste reducere, avand de altfel reguli precise privind SENSUL in care se fac conversiile beta si eta. Alfa conversia nu are o alfa reducere deoarece ea practic nu simplifica expresia, doar o rescrie la fel de complicat dar cu alte nume la niste variabile.

Procedeul reducerii conduce la cea mai simpla forma a unei expresii, in aritmetica o numim valoarea iar in lambda calcul o numim forma normala.

Atentie: Spre deosebire de aritmetica unde toate operatiile aveau rezultat (exceptand x/0, impartirea prin zero) si realizarea unei operatii reducea formula, in lambda calcul e altfel: Exista formule care nu se pot reduce deloc, nu au forma normala, se comporta cam ca in gluma cu zmeul e la x. Exista si formule care se pot reduce doar cu anumite strategii de reducere, operand reducerile doar in anumita ordine. Aici forma normala exista, dar unele drumuri catre ea sunt inchise.

Exemple pagina in dezvoltare