Redukcja beta w rachunku lambda za pomocą Haskella

Question

Zdefiniowałem następujące funkcje redukcji beta, ale nie jestem pewien, jak wziąć pod uwagę przypadek, w którym zmienne wolne są ograniczone.

data Term = Variable Char | Lambda Char Term | Pair Term Term deriving (Show,Eq) 
--substition 
s[M:x]= if (s=x) then M else s 
AB[M:x]= (A[M:x] B [x:M]) 
Lambda x B[M:x] = Lambda x B 
Lambda y P[M:x]= if x=y then Lambda y P else Lambda y P (M:x) 



--beta reduction 
Reduce [s]= s 
Reduce[Lambda x B]M = B[M:x] 
Reduce[L1 L2] = (Reduce [L1] Reduce [L2]) 

Answer 1

Link hammar dał w komentarzu opisuje rozwiązanie w szczegółach.

Chciałbym zaproponować inne rozwiązanie. Nicolaas Govert de Bruijn, holenderski matematyk, wymyślił alternative notation for lambda terms. Chodzi o to, że zamiast używać symboli dla zmiennych, używamy liczb. Zastępujemy każdą zmienną liczbą reprezentującą liczbę lambd, które musimy przekroczyć, aż znajdziemy abstrakcję, która wiąże zmienną. Abstrakcja nie potrzebuje wtedy żadnych informacji. Np

λx. λy. x 

przekształca się

λ λ 2 

lub

λx. λy. λz. (x z) (y z) 

przekształca się

λ λ λ 3 1 (2 1) 

Zapis ten ma kilka znaczących zalet. W szczególności, ponieważ nie ma zmiennych, nie ma zmiany nazwy zmiennych, nie ma konwersji α. Chociaż musimy zmienić numerację indeksów odpowiednio podczas podstawiania, nie musimy sprawdzać konfliktów nazw i dokonywać jakichkolwiek zmian nazwy. Powyższy artykuł Wikipedii podaje przykład tego, jak działa β-redukcja z tym zapisem.