rachunek lambda.pdf

(110 KB) Pobierz
Zbiór Λ termów rachunku lambda konstruue się indukcyjnie
jako zbiór słów nad alfabetem
Var

,
,
�½
, gdzie Var jest
przeliczalnym zbiorem zmiennych. Do zbioru Λ należą tylko
termy skonstruowane w następujący sposób:
-Dowolna zmienna ze zbioru Var jest termem rachunku
lambda, czyli jeżeli
x
Var
, to
x
 
.
-Jeżeli weźmiemy dowolny term M ze zbioru Λ oraz dowolną
zmienną x ze zbioru Var, to wyrażenie postaci
x.M
jest
termem rachunku lambda, czyli jeżeli
M
 
i
x
Var
, to
x.M
 
. Powyższy sposób tworzenia termów
nazywamy abstrakcją.
-Inna metoda to metoda aplikacji, czyli jeżeli
M
 
i
N
 
,
to
MN
 
.
Wolnym wystąpieniem zmiennej x nazywamy tylko takie
wystąpienie tej zmiennej, które nie jest w zasięgu żadnego
x
.
Zbiór zmiennych wolnych termu M-oznaczany przez FV(M)
zdefiniowany jest w zależności od budowy termu M w
następujący sposób:
-Jeżeli M jest pojedynczą zmienną tzn. M=x, to zmienna ta jest
wolna, a zatem FV(M)={x}.
-Jeżeli M jest postaci
x
.M '
, to
x
wiąże wszystkie wolne
wystąpienia zmiennej x w termie M’, a zatem
FV(M)=FV(M’)-{x}.
-Jeżeli M jest postaci PQ, to zmiennymi wolnymi termu M są
wszystkie zmienne wolne występujące w termach P i Q, czyli
FV(M)=FV(P)
FV(Q).
Zmienna jest zmienną wolną termu M, jeżeli należy do zbioru
FV(M), a zmienną związaną w przeciwnym wypadku.
Term M jest domknięty wtw gdy FV(M) jest zbiorem pustym.
α-konwersja to zamiana nazw zmiennych związanych
x
.
M
y
.
M
x
/
y
, gdzie
y
FV
(M )
, a M[x/y]
oznacza wynik podstawienia zmiennej y za każde wolne
wystąpienie zmiennej x w termie M.
Będziemy używać oznaczenia
T
1
�½
T
2
, aby powiedzieć,
że termy
T
1
i
T
2
są równe modulo α-konwersja tzn. że mogą
być zredukowane do tego samego termu dzięki zastosowaniu
skończonej liczby α-konwersji.
β-redukcja –obliczenia wykonywane przez procedurę
symulowane są w rachunku lambda poprzez proces zwany
β-redukcją. Aplikujemy procedurę
x.M
do argumentu N:
x
.
M
N
M
x
/
N
w taki sposób, że każda zmienna wolna termu N pozostaje
wolna po podstawieniu. Jest to możliwe do osiągnięcia po
ewentualnym wcześniejszym zastosowaniu α-konwersji.
Używamy oznaczenia
T
1
�½
T
2
, aby powiedzieć, że termy
T
2
są równe modulo β-konwersja tzn. że mogą być
zredukowane do tego samego termu dzięki zastosowaniu
skończonej liczby β-konwersji.
T
1
i
Aplikację PQ nazywamy β-redeksem, jeżeli term P jest w
postaci λ-abstrakcji. Term M jest w postaci normalnej, jeżeli
nie zawiera β-redeksów tzn. żaden podterm termu M nie jest
Β-redeksem.
Własność Churcha-Rossera
Jeżeli term M poprzez pewne ciągi β-redukcji redukuje się do
termów
N
1
i
N
2
, to istnieje term M’ taki, że zarówno
N
1
jak i
N
2
można zredukować do M’ (poprzez ciągi β-redukcji).
Term T jest normalizowalny, jeżeli można go zredukować do
postaci normalnej, a jest silnie normalizowalny, jeżeli każda
droga redukcji prowadzi do postaci normalnej.

Plik z chomika:

Inne pliki z tego folderu:

Inne foldery tego chomika:

Zgłoś jeśli naruszono regulamin