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