8299308022

nazywa sią związana. Pozostałe zmienne, niewystępujące pod lambdą, są wolne. Wartość wyrażenia zależy tylko od wartości zmiennych wolnych.

W zapisie A-wyrażeń przyjmuje się umowy, że

•    z dwóch wyrażeń, stojących obok siebie, pierwsze oznacza funkcję a drugie argument, na którym ta funkcja działa; np. / x oznacza zastosowanie funkcji / do argumentu x;

•    zastosowanie funkcji wiąże do lewej; tak więc f gx oznacza (/g)x ;

•    funkcja ma zawsze tylko jeden argument, ale za to wynikiem jej działania może znowu być funkcja; więc właściwie nie powinniśmy pisać 3 • 4 tylko raczej -34 — i to oznacza zastosowanie funkcji • do liczby 3; a następnie zastosowanie wynikowej funkcji • 3, mnożącej swój argument przez 3, do liczby 4.

Podstawowym działaniem na A-wyrażeniach jest t.zw. 0-konwersja — zamiana zastosowania do argumentu wyrażenia zaczynającego się od A (czyli funkcji) na ciało funkcji z argumentem wstawionym w miejsce wystąpień zmiennej spod A:

/3-konwersja:    (Ax.e)e^/ ■—* e[e'/x\

Przez e[e'/x\ rozumie się wyrażenie e z e' wstawionym za X¹.

Przykład 1.20

Oto kilka przykładów zastosowania /9-konwersji:

1.    (Ax. x • x) 3 •—> 3-3

Wynikiem zastosowania funkcji, podnoszącej do kwadratu, do liczby 3 jest wyrażenie •33.

2.    (A/. \y. f (/ y)) (Ax. x • x) 3

i—► (Xy. (Ax. x • x) ((Ax.x • x) y)) 3 * * {Xy. (Ax.x ■ x)(y ■ y)) 3 i-* (Ay. (y-y)-(y- y)) 3 -> (3 • 3) • (3 • 3)

Tutaj funkcja wyższego rzędu¹², polegająca na złożeniu swojego funkcyjnego argumentu z sobą samym, zostaje zastosowana do funkcji „kwadrat”, a wynik zostaje zastosowany do liczby 3.

3.    (Ax. / (xx)) (Ax. / (xx))

/((Ax./(xx))(Ax./(xx)))

•-* /(/((Az-/(«)) (Az. / («))))

Jak widać, /3-konwersja może doprowadzić do wyrażenia, które dalej daje się przekształcać przez /^-konwersję, i ten ciąg przekształceń może być nieskończony. W tym przykładzie, jeśli wprowadzimy oznaczenie Fix / = (Ax. / (xx)) (Ax. / (xx)) to otrzymamy ciąg przekształceń

Fix/ ~/(Fix/) ~/(/(Fix/)) - ...

□

15

1

Dokładniej: e' wstawia się tylko za wolne wystąpienia zmiennej x w e; i to w taki sposób, żeby nie doprowadzić do związania żadnej zmiennej wolnej z e'. W razie konfliktu nazw należy zastosować a-konwersję, czyli przenazwować jakieś zmienne związane.

¹²Czyli biorąca funkcję za argument.