Lambda Calcolo

Question

Tutti,

Di seguito è l'espressione lambda, che mi sto trovando difficile ridurre vale a dire che non sono in grado di capire come fare per questo problema.

(λm λn λa λb m (nab) b.) (Λ f x x.) (Λ f x fx.)

Questo è quello che ho provato, ma mi sono bloccato:

Considerando precedente espressione come: (. λf x x) (λm.E) m equivale a
E = (. λn λa λb m (nab) b)
m = (. λ f x fx)

= > (λn λa λb. (λ f x. x) (λ f x. fx) (nab) b)

C considerando l'espressione sopra come (λn. E) M corrisponde a
E = (λa λb. (Λ f x. X) (λ f x. F x) (n a b) b)
M = ??

.. e io sono perso !!

Qualcuno può aiutarmi a capire che, per QUALSIASI espressione di calcolo lambda, quali dovrebbero essere i passaggi per eseguire la riduzione?

Answer 1

È possibile seguire le seguenti misure per ridurre le espressioni lambda:

1. Completamente parentesi l'espressione per evitare errori e rendere più evidente la posizione in cui si verifica l'applicazione dell'applicazione.
2. Trova un'applicazione di funzione, cioè trova un'occorrenza del modello (λX. e1) e2 dove X può essere un qualsiasi identificatore valido e e1 e e2 possono essere espressioni valide.
3. applicare la funzione sostituendo (λx. e1) e2 con e1' dove e1' è il risultato di sostituire ogni occorrenza libera di x in e1 con e2.
4. Ripetere 2 e 3 finché il motivo non si verifica più. Si noti che questo può portare ad un ciclo infinito di espressioni non normalizzare, così si dovrebbe smettere dopo 1000 iterazioni o giù di lì ;-)

Così, per il tuo esempio ci iniziare con l'espressione

((λm. (λn. (λa. (λb. (m ((n a) b)) b)))) (λf. (λx. x))) (λf. (λx. (f x))) 

Qui la sottoespressione (λm. (λn. (λa. (λb. (m ((n a) b)) b)))) (λf. (λx. x)) si adatta al nostro modello con X = m, e1 = (λn. (λa. (λb. (m ((n a) b)) b)))) e e2 = (λf. (λx. x)). Così, dopo la sostituzione otteniamo (λn. (λa. (λb. ((λf. (λx. x)) ((n a) b)) b))), che rende tutta la nostra espressione:

(λn. (λa. (λb. ((λf. (λx. x)) ((n a) b)) b))) (λf. (λx. (f x))) 

Ora possiamo applicare il modello per l'intera espressione con X = n, e1 = (λa. (λb. ((λf. (λx. x)) ((n a) b)) b)) e e2 = (λf. (λx. (f x))). Così, dopo aver sostituito otteniamo:

(λa. (λb. ((λf. (λx. x)) (((λf. (λx. (f x))) a) b)) b)) 

Ora ((λf. (λx. (f x))) a) si adatta il nostro modello di e diventa (λx. (a x)), che porta a:

(λa. (λb. ((λf. (λx. x)) ((λx. (a x)) b)) b)) 

Questa volta siamo in grado di applicare il modello a ((λx. (a x)) b), che si riduce a (a b), portando a :

(λa. (λb. ((λf. (λx. x)) (a b)) b)) 

Ora applicare il modello a ((λf. (λx. x)) (a b)), che si riduce a (λx. x) e ottieni:

(λa. (λb. b)) 

Ora che abbiamo finito.

Answer 2

dove stai andando male è che nella prima fase, non si può avere

M = (λf x. x)(λ f x. f x) 

perché l'espressione originale non include quell'espressione applicazione. Per chiarire questo punto, si può mettere tra parentesi implicite seguendo la regola che l'applicazione è lasciata-associativa (usando [e] per le nuove parentesi e mettendo in qualche manca s ""):

[ (λm . λn . λa . λb . m (n a b) b) (λ f x. x) ] (λ f x. f x) 

Da qui , trova un'espressione del modulo (λv.E) M alcuni all'interno e riduci sostituendo v con M in E. Fai attenzione che è davvero un'applicazione della funzione a M: non è se hai qualcosa come N (λv.E) M, da allora N è applicato alla funzione e M come due argomenti.

Se sei ancora bloccato, prova a inserire i paren per ogni lambda anche - fondamentalmente un nuovo "(" dopo ogni ".", E un matching ")" che va il più a destra possibile mentre è ancora . corrispondenti alla nuova "(" per fare un esempio, ho fatto uno qui (usando [e] per farli risaltare):

((λm . λn . λa . [λb . m (n a b) b]) (λ f x. x)) (λ f x. f x)