Definiowanie struktury danych stosu i jego głównych operacji w rachunku lambda

Question

Próbuję zdefiniować strukturę danych stack w rachunku lambda, używając kombinatorów punktów stałych. Próbuję zdefiniować dwie operacje, insertion i removal elementów, czyli push i pop, ale jedyne, które udało mi się zdefiniować, wstawienie, nie działa poprawnie. Usunięcie nie mogłem dowiedzieć się, jak zdefiniować.

To jest moje podejście do pracy push, a moja definicja stack:

Stack definition: 
STACK = \y.\x.(x y) 
PUSH = \s.\e.(s e) 

Moi stosy są zainicjować z elementem wskazania dno; Używam 0 tutaj:

stack = STACK 0 = \y.\x.(x y) 0 = \x.(x 0)  // Initialization 
stack = PUSH stack 1 = \s.\e.(s e) stack 1 =  // Insertion 
    = \e.(stack e) 1 = stack 1 = \x.(x 0) 1 = 
    = (1 0) 

Ale teraz, gdy próbuję wstawić inny element, to nie działa, jak moja pierwsza konstrukcja ma być rozebrany.

Jak naprawić definicję STACK lub definicję PUSH i jak zdefiniować operację POP? Sądzę, że będę musiał zastosować kombinator, aby umożliwić rekursję, ale nie mogłem wymyślić, jak to zrobić.

odniesienia: http://en.wikipedia.org/wiki/Combinatory_logic

dalszych wyjaśnień lub przykład na określenie struktury danych w lambda rachunku będą bardzo cenione.

Answer 1

Stos w rachunku lambda to tylko pojedynczo połączona lista. I pojedynczo związane lista jest w dwóch formach:

nil = λz. λf. z 
cons = λh. λt. λz. λf. f h (t z f) 

To Church encoding z listą reprezentowane jako catamorphism. Co ważne, w ogóle nie potrzebujesz stałego kombinatora punktowego. W tym widoku stos (lub lista) jest funkcją pobierającą jeden argument dla przypadku nil i jeden argument dla przypadku cons. Na przykład, lista [a,b,c] jest reprezentowana następująco:

cons a (cons b (cons c nil)) 

Pusta stos nil jest równoważna K combinator z rachunku nart. Konstruktorem cons jest operacja push. Biorąc pod uwagę element głowicy h i inny stos t dla ogona, wynikiem jest nowy stos z elementem h z przodu.

Operacja pop po prostu rozdziela listę na jej głowę i ogon.Można to zrobić z parą funkcji:

head = λs. λe. s e (λh. λr. h) 
tail = λs. λe. s e (λh. λr. r nil cons) 

Gdzie e jest coś, co zajmuje pustego stosu, ponieważ pojawiały pusty stos jest niezdefiniowany. Mogą być one łatwo przekształcone jedną funkcję, która zwraca parę head i tail:

pop = λs. λe. s e (λh. λr. λf. f h (r nil cons)) 

Ponownie, para jest Church zakodowane. Para to tylko funkcja wyższego rzędu. Para (a, b) jest reprezentowana jako funkcja wyższego rzędu λf. f a b. Jest to tylko funkcja, która, biorąc pod inną funkcję f, ma zastosowanie f zarówno do a i b.

Answer 2

Definiując COMBINATOR, który:

jest zdefiniowany jako termin lambda bez zmiennych wolnych, więc z definicji każdy syntezatora jest już termin lambda,

można określić, na Przykładowo, struktura lista, pisząc:

Y = (list definition in lambda calculus) 
Y LIST = (list definition in lambda calculus) LIST 
Y LIST = (element insertion definition in lambda calculus) 

intuicyjnie i stosując operator paradoksalny, możliwa jest definicja - rozważyć \ = lambda:

• lista jest pusta, a następnie element końcowy, na przykład 0;
• lub lista jest utworzona przez element x, który może być inną listą w obrębie poprzedniej.

Ponieważ został zdefiniowany przez kombinator - kombinator punktowy stały - nie ma potrzeby wykonywania dalszych aplikacji, poniższa abstrakcja jest terminem lambda.

Y = \f.\y.\x.f (x y) 

Teraz nazywania jej listy:

Y LIST = (*\f*.\y.\x.*f* (x y)) *LIST* -- applying function name 
LIST = \y.\x.LIST (x y), and adding the trailing element "0" 
LIST = (\y.\x.LIST (x y)) 0 
LIST = (*\y*.\x.LIST (x *y*)) *0* 
LIST = \x.LIST (x 0), which defines the element insertion abstraction. 

operator paradoksalny Y, lub po prostu COMBINATOR, pozwala rozważyć definicję LISTA już ważny element, bez zmiennych wolnych, tak , bez potrzeby redukcji.

Następnie można dołączyć/wstawić elementy, powiedzmy 1 i 2, wykonując:

LIST = (\x.LIST (x 0)) 1 2 = 
    = (*\x*.LIST (*x* 0)) *1* 2 = 
    = (LIST (1 0)) 2 = 

Ale tutaj, wiemy definicji listy, więc go rozwinąć:

= (LIST (1 0)) 2 = 
    = ((\y.\x.LIST (x y)) (1 0)) 2 = 
    = ((*\y*.\x.LIST (x *y*)) *(1 0)*) 2 = 
    = (\x.LIST (x (1 0))) 2 = 

teraz, wstawianie elemenet 2:

= (\x.LIST (x (1 0))) 2 = 
    = (*\x*.LIST (*x* (1 0))) *2* = 
    = LIST (2 (1 0)) 

który może zarówno zostać rozszerzona, w przypadku nowego wkładania, o r po prostu pozostaje tak, jak jest, ze względu na to, że LISTA jest terminem lambda, zdefiniowanym przez kombinator.

Rozszerzenie dla przyszłych wstawkami:

= LIST (2 (1 0)) = 
    = (\y.\x.LIST (x y)) (2 (1 0)) = 
    = (*\y*.\x.LIST (x *y*)) *(2 (1 0))* = 
    = \x.LIST (x (2 (1 0))) = 
    = (\x.LIST (x (2 (1 0)))) (new elements...) 

Cieszę się, że udało mi się wyprowadzić ten sam, ale jestem pewien, że musi być jakiś dobry grono dodatkowych warunków, przy definiowaniu stos, kupa lub jakaś bardziej wyszukana struktura.

Próbuje wyprowadzić abstrakcji dla wstawiania/usuwania stos - bez wszystko krok po kroku:

Y = \f.\y.\x.f (x y) 
Y STACK 0 = \x.STACK (x 0) 
STACK = \x.STACK (x 0) 

Aby wykonać operację na nią, nazwijmy pustego stosu - przypisanie zmiennej (:

stack = \x.STACK (x 0) 

// Insertion -- PUSH STACK VALUE -> STACK 
PUSH = \s.\v.(s v) 
stack = PUSH stack 1 = 
    = (\s.\v.(s v)) stack 1 = 
    = (\v.(stack v)) 1 = 
    = (stack 1) = we already know the steps from here, which will give us: 
    = \x.STACK (x (1 0)) 

stack = PUSH stack 2 = 
    = (\s.\v.(s v)) stack 2 = 
    = (stack 2) = 
    = \x.STACK x (2 (1 0)) 

stack = PUSH stack 3 = 
    = (\s.\v.(s v)) stack 3 = 
    = (stack 3) = 
    = \x.STACK x (3 (2 (1 0))) 

a my po raz kolejny imię ten wynik, dla nas do pop elementy:

stack = \x.STACK x (3 (2 (1 0))) 

// Removal -- POP STACK -> STACK 
POP = \s.(\y.s (y (\t.\b.b))) 
stack = POP stack = 
    = (\s.(\y.s y (\t.\b.b))) stack = 
    = \y.(stack (y (\t.\b.b))) = but we know the exact expansion of "stack", so: 
    = \y.((\x.STACK x (3 (2 (1 0)))) (y (\t.\b.b))) = 
    = \y.STACK y (\t.\b.b) (3 (2 (1 0))) = no problem if we rename y to x (: 
    = \x.STACK x (\t.\b.b) (3 (2 (1 0))) = 
    = \x.STACK x (\t.\b.b) (3 (2 (1 0))) = someone guide me here, if i'm wrong 
    = \x.STACK x (\b.b) (2 (1 0)) = 
    = \x.STACK x (2) (1 0) = 
    = \x.STACK x (2 (1 0)) 

Na co, mamy nadzieję, mamy element 3.

Próbowałem sam to wyprowadzić, więc jeśli istnieją jakiekolwiek ograniczenia z rachunku lambda, których nie śledziłem, proszę, wskazuj to.