Lambda-calcolo. Le basi

[Black27]

Buonasera! Mi sto preparando ad affrontare un esame di programmazione funzionale, nel quale vengono posti anche dei quesiti in lambda-calcolo dove viene chiesto di effettuare una riduzione.
Le forme più semplici e intuibili le ho capite, ad esempio:

(λx.xy)a -> ay

oppure

(λx.(λy.yx)z)w -> (λx.zx)w -> zw

Mi perdo però quando vengono presentati dei quesiti senza "argomenti" (non so se il termine è esatto, abbiate clemenza ma sono un profano del lambda-calcolo ) come ad esempio:

(λxy.xy)(λz.z)

Mi potete spiegare come si risolve quest'ultima tipologia? ho provato a spremere un po' le meningi ma proprio non ce la faccio

Inoltre un'altra cosa che non riesco a fare è risolvere equazioni un po' più complesse, come

(λx.x(xy))(λz.zx)

Vi ringrazio già in anticipo

[Black27]

nessuno può aiutarmi?

[hamming_burst]

Ciao,
questo argomento è un po' di informatica, ma va bene comunque

In base a quello che dici per te:

$(λx.x)w$ e $(λy.y)(λx.x)$ sono due formule con diversi metodi per gestirle.
Invece sono la stessa cosa, cioè hanno il nome di "applicazione", se vuoi sostituiscile con due nomi diversi:

$(λx.x)w$ viene:
$e = (λx.x)$
$d = w$

$(λy.y)(λx.x)$
$e = (λy.y)$
$d = (λx.x)$

$e\ d$
la sostituzione diverrà: $e'\{d \/ e\}$

entrambe gestite allo stesso modo.
Qua una riduzione, fatta da sostituzioni successive può portare a loop infiniti, per questo esisono delle strategie di riduzione (come quella scritta sotto) ma penso che non vedrai questi casi se hai visto solo qualche caso base e non hai visto le $beta$-riduzioni $alpha$-conversioni e via terminologia...

______
Avevo scritto prima questo messaggio sotto, ma ho riletto il tuo post, e ho visto che sicuramente non saprai di cosa parlo, perciò ti ho riscritto sopra in base al tuo dubbio.
______
Se devi ridurre, quello che devi applicare è una strategia di "riduzione" a forma normale. Ci sono basi teoriche sotto, ma puoi applicarle senza problemi, se il tuo scopo è ridurre la formula.
Puoi utilizzare la strategia "leftmost-outermost" (più a sinistra - più interno) che ti da sempre una forma normale, ce ne sono altre, ma questa è più meccanica e vai sul sicuro.

In termini semplici, devi "sostituire" (sai come si sostituisce?) l'applicazione al posto della variabile legata più a sinistra possibile.

Es:

l'applicazione (λxy.xy)(λz.z) la sostituisci alla variabile legata più a sinsitra (dell'astrazione) (λxy.xy).

(λxy.xy){λz.z/x} -> (λy.(λz.z)y) -> (λy.(λz.z){y/z}) -> λy.y $-=$ I

ed ecco ridotta.

Non so se hai visto le $beta$-$eta$-riduzioni o equivalenze, ecc... se così fosse dovresti creare l'albero delle derivazioni, se hai visto solo qualche riduazione fatta da sostituzioni allora quella che vedi sopra va bene...

Se hai dubbi chiedi pure

EDIT:
aggiornate le formule

[Black27]

Ti ringrazio davvero tanto della risposta, stavo iniziando a disperare (ho pochissimo materiale sul lambda-calcolo, e online si trova davvero poco)! Visto che vedo che sei stato molto chiaro nella risposta, voglio sfruttare ancora il tuo aiuto

Prima vorrei fare un veloce riassunto della mia attuale situazione:
Il prof è entrato in classe e ha messo una slide con un esercizio, e ha detto "provate a risolverlo!" senza dare alcuna base teorica. Ovviamente nessuno (o pochissimi) son riusciti a fare qualcosa, al che ha iniziato ad andare avanti con esempi e esercizi senza spiegare nulla di teoria! Risultato: fra 4 giorni ho l'esame, e mi viene richiesto di fare delle riduzioni in lambda-calcolo senza alcuna base teorica! Questo penso che spieghi in parte la mia approssimazione sui termini e la mia poca preparazione

Ritorniamo al dunque:

Volevo chiederti una cosa: All'inizio ho visto che hai sostituito le varie parti con $ e,d $. Non mi è chiaro a cosa corrisponda $ e' $.

In verità la seconda parte mi risulta più chiara (cioè quella che hai scritto per prima).
Il modo in cui hai risolto l'esempio mi è chiaro, ma trovo difficoltà ad applicarla ad altri esercizi. Ad esempio, provo a risolvere il seguente esercizio:

(λx.x(xy)) (λz.zx)

per prima cosa sostituisco il termine piu a destra a λx. Quindi ottengo

((λz.zx)(xy))

E, applicando quindi xy al termine a sinistra, ottengo

xyx

Che secondo il mio ragionamento dovrebbe essere la soluzione. In realtà la soluzione corretta è la seguente:

(λz.zx)((λz.zx)y)
(λz.zx)(yx)
(yx)x

Il procedimento col quale è stato risolto mi è chiaro, ma mi fa porre delle domande: Esiste commutatività? Cioè xyx è uguale a yxx ? Oppure il modo in cui ho sostituito io è sbagliato? (quindi esiste un solo modo per trovare una soluzione).

Sempre riguardo la commutatività, c'è un altro esericizio risolto, che è il seguente:

(λx.xy)(λz.zx)(λz.zx)
((λz.zx)y))(λz.zx)
yx(λz.zx)

E qui si ferma. Io però risolvendolo automaticamente mi è venuto spontaneo da scambiare i vari termini, quindi (la prossima parte la aggiungo io)

(λz.zx)yx
(yx)x

Come risultato. Quindi sono andato automaticamente avanti fino alla fine. è sbagliato del tutto? (già mi aspetto un si, ma vorrei capire il motivo)

Grazie davvero di cuore dell'aiuto, non saprei dove rivolgermi altrimenti >.<

[hamming_burst]

Vediamo un po'.

Per il materiale in internet ce ne è parecchio, in inglese la maggior parte, in italiano c'è:

- http://it.wikipedia.org/wiki/Lambda_calcolo che è completo di tutte le regole.
- https://www.matematicamente.it/forum/pos ... tml#479143 quarda "lambda calcolo non tipato" c'è di tutto

Per i tuoi dubbi. Le regole del lamda calcolo (non tipato) sono poche, se le capisci scrivi un intero linguaggio.
Prima di tutto:
- le formule NON sono commutative, sono associative.
- l'astrazione ($lambda$x.M) con M variabili, associa a destra
- l'applicazione ($lambda$x.M)N associa a sinistra.

per fare una sostituzione e una riduzione (Beta-riduzione) ci sono dei vincoli e dei sottocasi, sono spiegati su wiki.

per l'esercizio, te secondo me non hai ben presente la definizione di "scope" di un'astrazione.
Un'astrazione la puoi vedere un po' come una funzione con i parametri formali.

(λx.x) è uguale a

function f x -> x;;

spero l'esempio spiegi l'idea.

(λx.x(xy)) (λz.zx) se sostituisci (stando attento ai vincoli) -> (λx.x(xy)) {(λz.zx)/x} -> (λz.zx)((λz.zx)y) hai un doppio passaggio lo scope di (λx.x(xy)) è tutto quello che c'è dopo il punto fino alla partentesi chiusa (informalmente).
Perciò:

(λx.x(xy)) (λz.zx) -> (λx.x(xy)) {(λz.zx)/x} -> (λz.zx)((λz.zx)y)
(λz.zx)((λz.zx)y) -> (*) (λz.zx) {(λz.zx)y)/z} -> strategia leftmost ((λz.zx)y)x
((λz.zx)y)x -> (yx)x

l'esercizio invece utilizza la strategia leftmost-outermost
cioè (*) ((λz.zx){y/z}) -> (λz.zx)(yx)

ricordandoti che non esiste commutatività, al massimo puoi parlare di $alpha$-conversioni. E' una questione di stare attenti all'ordine di sostituzione e riduzione, ma visto che non conosci le beta, eta ecc.. non hai una base sui passi da fare, ma se vai di "strtegie" puoi cavartela

se hai dubbi chiedi pure.

PS: penso che vedrai questi argomenti in corsi più avanzati, adesso penso siano solo infarinature

[Black27]

Perfetto! Ora è davvero molto più chiaro (prima brancolavo nel buio).
Se poi mi verranno ancora dei dubbi prima dell'esame ne approfitterò a chiederti di nuovo aiuto! Ti ringrazio tantissimo

[hamming_burst]

Prego, questa parte dell'informatica teorica è una di quelle che preferisco, ti aiuto volentieri

[nepotu1]

ciao io non riesco proprio a capire alcune cose.. per esempio non capisco quale sia l ordine di sostituzione, quando va usata valutazione per valore e quando per nome.

per esempio per questo esercizio:
(λx. ((λz.zwz) ( ((λxyx.y)(λx.y)(λy.x)) ((λx.xx)(λy.yyy)) ) ))t

dovrebbe risultare t( \y.t)
invece a me mi da computazione divergente.. perché
(λx.xx)(λy.yyy) = (λy.yyy)(λy.yyy) = (λy.yyy)(λy.yyy)(λy.yyy) = (λy.yyy)(λy.yyy)(λy.yyy)(λy.yyy) = ......

cosa sbaglio?? sono in panico:( tra qualche giorno ho l esame .. heeelp me plssss