Alfa reducere

De fapt nu este vorba de o reducere ci in realitate este o conversie. Alpha conversia descrie o operatie foarte cunoscuta, aceea a schimbarii numelui unui parametru dintr-o functie.

Sunteti de acord ca functiile:

f(x) = x+1

si

f(y) = y+1

sunt una si aceeasi functie ?

Daca DA, atunci ati inteles ca prima poate fi alfa convertita in a doua si invers.

Nota:

Probleme mai complicate apar cand in functie exista si variabile libere si variabile legate

Exemplu:

f(x) = x + 1 + (\ x -> x*x) 10.

Aici f(x) se calculeaza sumand x cu 1 si cu ridicarea la patrat aplicata lui 10. Aceasta este echivalenta cu:

f(y) = y +1 + (\x -> x *x) 10.

cu

f(y) = y +1 + (\y -> y *y) 10.

dar nu cu:

f(y) = y +1 + (\x -> x *y) 10.

Problema provine din faptul ca nu am voie sa inlocuiesc o variabila libera cu una legata sau sa fac o alfa conversie care sa confuzioneze: de exemplu sa transforme o variabila libera punindu-i numele unei variabile legate sau invers.

Din acest motiv o definitie riguroasa a unei alfa conversii se bazeaza pe o definitie riguroasa a setului de variabile libere si legate dintr-un term (sau subterm). Aceste seturi de variabile se pot defini inductiv dupa structura, complexitatea, termului.

pagina in dezvoltare