Definizione di una struttura di dati stack e delle sue operazioni principali nel calcolo lambda

Question

Sto provando a definire una struttura dati stack nel calcolo lambda, utilizzando i combinatori a virgola fissa. Sto cercando di definire due operazioni, insertion e removal di elementi, quindi, push e pop, ma l'unico che ho potuto definire, l'inserimento, non funziona correttamente. La rimozione non riuscivo a capire come definire.

Questo è il mio approccio sul funzionamento push, e la mia definizione di un stack:

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

mie pile sono inizializzare con un elemento per indicare il fondo; Io sto usando un 0 qui:

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) 

Ma ora, quando provo ad inserire un altro elemento, non funziona, come la mia struttura iniziale è essere decostruito.

Come si risolve la definizione STACK o la definizione PUSH e come si definisce l'operazione POP? Credo che dovrò applicare un combinatore, per consentire la ricorsione, ma non sono riuscito a capire come farlo.

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

Qualsiasi ulteriore spiegazione o esempio sulla definizione di una struttura di dati in lambda calcolo sarà molto apprezzato.

Answer 1

Una pila nel calcolo lambda è solo una lista concatenata. E una lista concatenata semplice è disponibile in due forme:

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

Questo è Church encoding, con una lista rappresentato come il suo catamorphism. È importante sottolineare che non è necessario un combinatore a virgola fissa. In questa vista, una pila (o un elenco) è una funzione che accetta un argomento per il caso nil e un argomento per il caso cons. Ad esempio, l'elenco [a,b,c] è rappresentata in questo modo:

cons a (cons b (cons c nil)) 

Lo stack vuoto nil equivalente alla K combinatore del calcolo SCI. Il costruttore cons è l'operazione push. Dato un elemento di testa h e un altro stack t per la coda, il risultato è una nuova pila con l'elemento h nella parte anteriore.

L'operazione pop separa semplicemente l'elenco in testa e in coda.È possibile farlo con un paio di funzioni:

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

Dove e è qualcosa che gestisce lo stack vuoto, dal momento che spuntando la pila vuota non è definito. Questi possono essere facilmente trasformati in una funzione che restituisce la coppia di head e tail:

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

Nuovamente, la coppia è Chiesa codificato. Una coppia è solo una funzione di ordine superiore. La coppia (a, b) è rappresentata dalla funzione di ordine superiore λf. f a b. È solo una funzione che, data un'altra funzione f, applica f a entrambi a e b.

Answer 2

Definendo un combinatore, che:

è definito come un termine lambda senza variabili libere, quindi, per definizione, qualsiasi combinatore è già un termine lambda,

è possibile definire, per esempio, una struttura della lista, scrivendo:

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

Intuitivamente, e utilizzando un combinatore punto fisso, una possibile definizione è - considerare \ = lambda:

• un elenco è vuoto, seguito da un elemento finale, ad esempio 0;
• o una lista è formata da un elemento x, che potrebbe essere un'altra lista all'interno della precedente.

Poiché è stato definito con un combinatore - combinatore di punti fissi -, non è necessario eseguire ulteriori applicazioni, la seguente astrazione è un termine lambda stesso.

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

Ora, chiamandolo una lista:

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. 

Il punto fisso combinatore Y, o semplicemente Combinator, permette di prendere in considerazione la definizione di LIST già un utente valida, senza variabili libere, in modo da , senza necessità di riduzioni.

Quindi, è possibile aggiungere/inserire elementi, diciamo 1 e 2, facendo:

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

Ma qui, sappiamo la definizione di lista, così abbiamo espanderlo:

= (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 = 

ora, inserendo elemenet 2:

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

che possono sia essere ampliato, in caso di un nuovo inserimento, o r semplicemente lasciato come è, a causa del fatto che LIST è un termine lambda, definito con un combinatore.

espansione per inserimenti futuri:

= 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...) 

Sono davvero contento sono stato in grado di ricavare questo me stesso, ma sono abbastanza sicuro che ci deve essere qualche buon gruppo di condizioni di troppo, quando si definisce una stack, un heap o una struttura più elaborata.

Cercando di ricavare l'astrazione di inserimento pila/rimozione - senza tutto il passo-passo:

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

Per eseguire l'operazione su di essa, chiamiamolo uno stack vuoto - allocare una variabile (:

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))) 

E noi, ancora una volta, il nome di questo risultato, per noi per far apparire i elementi:

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)) 

Per cosa, si spera, abbiamo spuntato l'elemento 3.

Ho provato a ricavarlo da solo, quindi, se c'è qualche restrizione dal calcolo lambda, non l'ho seguito, per favore, segnalalo.