5109637055

a-równoważność i konwencja Barendregta

►    A-abstrakcja Ax.t wiąże zmienną x w termie t

►    zmienne wolne

FV(x) = {x}

FV(Ax.t) = FV(t)-{x}

FV(t₀ ti) = FV(to)UFV(tx)

►    termy t i u są a-równoważne, jeżeli różnią się wyłącznie nazwami zmiennych związanych

►    a-równoważność jest relacją równoważności - utożsamiamy a-równoważne termy

►    konwencja Barendregta

zakładamy, że zmienne wolne są różne od zmiennych związanych w rozważanych termach (zmienne związane można zawsze odpowiednio przemianować)