Lista nr 2 zadań z rachunku lambda 7 marca 2019
Może raz jeszcze dwa zadania z listy 1.
Zad. 1. Znajdź w algebrze kombinatoryjnej termy stałe B i C spełniające prawa
Bxyz = x(yz) oraz Cxyz = xzy.
Zad. 2. Trochę modyfikujemy definicję algebry kombinatoryjnej (nie zmieniając nazwy). Jest to teraz algebra z czterema stałymi S, I, B, C spełniającymi prawa
Sxyz = xz(yz), Ix = x, Bxyz = x(yz) oraz Cxyz = xzy.
Pokaż, że dla każdego termu t(x1, . . . , xn), w którym występują zmienne x1, . . . , xn
(wszystkie wymienione), istnieje wyrażenie stałe F takie, że w tej algebrze zachodzi równość F x1 . . . xn = t(x1, . . . , xn).
Zad. 3. Udowodnij, że jeżeli x 6∈ F V (M ) (a więc na przykład, jeżeli M jest termem stałym), to M [x := N ] = M .
Zad. 4. Udowodnij, że jeżeli x 6= y oraz x, y 6∈ F V (L), to
M [x := N ][y := L] = M [y := L][x := N ][y := L].
Zad. 5. Udowodnij, że jeżeli x 6= y, x 6∈ F V (L), a także term N jest podstawialny za x w M , to
M [x := N ][y := L] = M [y := L][x := N [y := L]].
Zad. 6. Pokaż, że N jest podtermem termu M ∈ Λ wtedy i tylko wtedy, gdy M = C[N ] dla pewnego kontekstu C.
Zad. 7. Pokaż, że relacja → (w zbiorze termów Λ) jest zgodna z działaniami wtedy i tylko wtedy, gdy dla dowolnych M, N ∈ Λ i dla dowolnego kontekstu warunek M → N pociąga za sobą, że C[M ] → C[N ].
Zad. 8. Pokaż, że zwrotne i przechodnie domknięcie relacji symetrycznej jest rela- cją symetryczną.
Zad. 9. Pokaż, że zwrotne i przechodnie domknięcie relacji zgodnej z działaniami jest zgodne z działaniami.
Zad. 10. Pokaż, że relacja α-redukcji →α jest symetryczna.
Zad. 11. (Numerały Churcha w algebrach kombinatoryjnych). Przyjmijmy, że Cn= (S(S(KS)K))n(KI). Udowodnij, że w algebrach kombinatoryjnych zachodzą rów- ności Cnf x = fn(x). Udowodnij także, że w każdej algebrze kombinatoryjnej o przynajmniej dwóch elementach termy Cn oznaczają parami różne elementy.
Zad. 12. Pokaż, że żadna para różnych zmiennych nie jest w relacji α-konwersji.
Def. 1. Kontekstem nazywamy napis otrzymany zgodnie z następującymi regułami
1) [ ] jest kontekstem,
2) jeżeli M ∈ Λ i C jest kontekstem, to CM i M C są kontekstami, 3) jeżeli C jest kontekstem i x ∈ V , to λx C jest kontekstem.
Def. 2. Podstawienie C[N ] termu N w kontekscie C definiujemy rekurencyjnie następującymi wzorami
1) [ ][N ] = N ,
2) (CM )[N ] = C[N ]M oraz (M C)[N ] = M C[N ], 3) (λx C)[N ] = λxC[N ].
Def. 3. Relacja → w zbiorze λ-termów jest zgodna z działaniami, jeżeli dla do- wolnych termów M1, M2 i N , i dla dowolnej zmiennej x ∈ V warunek M1 → M2 implikuje, że N M1 → N M2, M1N → M2N oraz λxM1 → λxM2.
Def. 4. α-redukcją nazywamy najmniejszą relację →α w zbiorze λ-termów, która jest zgodna z działaniami i spełnia warunek
λx M →α λy M [x := y]
dla wszystkich termów M i zmiennych x i y takich, że y nie jest wolne w M i jest w M podstawialne za zmienną x.
Def. 5. Dla danych termów M, N ∈ Λ i liczby naturalnej n symbolem Mn(N ) będziemy oznaczać term zdefiniowany rekurencyjnie wzorami M0(N ) = N oraz Mn+1(N ) = M (Mn(N ))
