Aiuto con il lambda calcolo

[teasel]

salve! allora anche dopo aver letto svariati documenti su codesto argomento non credo di averci capito tanto, avendo trovato su google un'altra persona nella mia stessa situazione in questo identico forum spero quindi di poter trovare aiuto qui, vi chiedo scusa in anticipo nel caso stia scrivendo nella sezione sbagliata

da quello che ho capito io il lambda calcolo e un modo per rappresentare funzioni, ergo

λx.x rappresenta una funzione che prende in entrata x e restituisce x (ovvero la funzione identita)

λx.y rappresenta una funzione che prende in entrata x e restituisce y

la cosa che pero comincia a confondermi e che quando vedo gli esercizi trovo robba del tipo

(λxxxx.xx)(λx.xx)(λx.x)y((λx.x)x)

cosa diamine sto rappresentando con λxxxx.xx? una funzione che prende 4 x e restituisce 2 x? una robba del tipo λxλxλxλx? se scrivessi λxy.zw cosa starei scrivendo esattamente?

come si esegue esattamente una riduzione, nell esempio banale di λx.y la riduzione sarebbe in pratica y visto che e quello che restituisce la funzione rappresentata dal calcolo?

per forma normale intendiamo semplicemente un termine in cui abbiamo eseguito tutte le possibili riduzioni no?

come facciamo a trovare quali sono le variabili libere? (qui credo sia piu un problema della mia confusione riguardo alla sintassi del lambda calcolo) un esercizio ad esempio mi chiede di trovare le variabili libere di questo termine

λz.( ((λx.λx.yx)x)(vλz.λw.v) )

come lo fareste?

[onlyReferee]

Ciao teasel
Allora, andiamo con ordine cercando di fare chiarezza sui tuoi vari punti. Il lambda calcolo è un sistema di riscrittura e la sua maggiore importanza è dovuta al fatto che permette di studiare proprietà delle funzioni in maniera abbastanza semplice grazie alla sua potenza di astrazione. Vi è poi un importante collegamento con l'informatica grazie alla corrispondenza di Curry-Howard in cui si fanno corrispondere i tipi della programmazione ai lambda termini nel lamba calcolo.
Venendo al tuo primo esempio, $\lambda x x x x.x x$ rappresenta una funzione con quattro input il cui risultato è ottenuto calcolando la lambda espressione $x x$ (non è dunque corretto affermare che ci sono due output). L'espressione $\lambda xy.zw$ che hai scritto te non è sintatticamente corretta poiché la variabile $w$ non appartiene allo scope della funzione (non è un parametro di ingresso) ne allo scope di eventuali funzioni più esterne che richiamano questa e che in tale esempio non sono presenti. Lo scope di una funzione ha per alcuni versi la corrispondenza di quello delle funzioni nella programmazione imperativa (anche se ovviamente bisognerebbe essere più precisi in questa affermazione). Diciamo che è come se dichiarassi una funzione dentro una funzione e dalla funzione più interna cercassi di richiamare una variabile presente nella mia funzione più esterna. Tornando al tuo esempio se avessi scritto invece $\lambda xyw.zw$ la tua espressione sarebbe stata corretta e corrisponde (usando una scrittura alternativa ma del tutto equivalente) a: $\lambda x.\lambda y.\lambda w.zw$.
Per non appesantire troppo il discorso e voler affrontare subito le riduzioni, dimmi pure se ti è chiaro questo intanto.

[teasel]

ciao, scusa se ti rispondo solo ora ma ieri ho avuto una giornataccia piena

che intendi per variabile che non appartiene allo scope della funzione? pensavo che dentro un espressione di lambda calcolo ci potessi scrivere quello che volevo

nell'espressione λxyw.zw z non c'e a sinistra quindi non capisco perche z può essere assente da sinistra ma w deve essere da entrambi i lati

la funzione λx.λy.λw.zw. a cosa corrisponderebbe volendola descrivere a parole?

se ho capito bene dovrebbe essere una funzione che preso x restituisce una funzione che preso y restituisce una funzione che preso w restituisce zw?

[onlyReferee]

ciao, scusa se ti rispondo solo ora ma ieri ho avuto una giornataccia piena
[...]

Ciao
Nessun problema, ieri la giornata piena ce l'ho avuta io e così ti rispondo adesso . Vedo di andare con ordine.

[...]
che intendi per variabile che non appartiene allo scope della funzione? pensavo che dentro un espressione di lambda calcolo ci potessi scrivere quello che volevo
[...]

Cerco di spiegarti meglio con un esempio ciò che intendo con scope della funzione e variabile che appartiene allo stesso. Supponiamo di avere la seguente lambda espressione (di seguito per praticità parlerò sempre di espressione intendendo una lambda espressione, giusto per abbreviare): $\lambda xyz.\lambda w.wxyz$. Come vedi nell'espressione lambda più interna, ossia quella a destra, richiamo $x, y$ e $z$ anche se gli stessi non sono appartenenti all'espressione più interna ma solo a quella più esterna. Perché possiamo far ciò Perché l'espressione più interna mi "vede" le variabili presenti nelle espressioni in cui essa è contenuta. Viceversa sarebbe invece un errore scrivere ad esempio $\lambda xyz.((\lambda v.vxyz)w)$ (ho messo le parentesi giusto per farti capire meglio). Il $w$ in questo caso se volessimo effettuare una riduzione (di cui ti parlerò appena sarà chiaro questo aspetto) diventerebbe input dell'espressione $\lambda v.vxyz$ ma il problema è un altro: essa è presente nel corpo dell'espressione di livello superiore, ossia quella con $\lambda xyz$ ma non è uno dei suoi parametri in ingresso e pertanto non sappiamo dove "andare a pescarla"
Diverso e corretto è invece questo caso qui: $\lambda w. (\lambda xyz.((\lambda v.vxyz)w))$. Se noti infatti qui $w$ è visibile in quanto appartiene agli input (in tal caso ce n'è uno solo) di $\lambda w$ che è due livelli superiori rispetto all'espressione più interna.

[...]
nell'espressione λxyw.zw z non c'e a sinistra quindi non capisco perche z può essere assente da sinistra ma w deve essere da entrambi i lati
[...]

Difatti per quanto detto sopra tale espressione non è corretta perché scritta così il corpo della stessa non sa chi sia $z$. Detto in altre parole non è vero che $z$ può essere assente nella parte sinistra.

[...]
la funzione λx.λy.λw.zw. a cosa corrisponderebbe volendola descrivere a parole?

se ho capito bene dovrebbe essere una funzione che preso x restituisce una funzione che preso y restituisce una funzione che preso w restituisce zw?

Detta meglio a parole si può esprimere così: questa espressione corrisponde ad una funzione che preso $x$ restituisce il risultato di una funzione che preso $y$ restituisce il risultato di una funzione che preso $w$ ritorna il risultato dell'applicazione $zw$. Anche tale espressione comunque non è corretta sempre per quanto detto prima (chi è $z$ ).

[teasel]

vabbene spiegami questa cosa della riduzione

[onlyReferee]

[...]

come si esegue esattamente una riduzione, nell esempio banale di λx.y la riduzione sarebbe in pratica y visto che e quello che restituisce la funzione rappresentata dal calcolo?
[...]

Una riduzione è un procedimento che permette di semplificare la nostra espressione e vedere qual è il risultato dell'applicazione di un determinato input ad una delle funzioni presenti nella nostra espressione. In certi passaggi ci possono essere anche più riduzioni possibili applicabili ad un'espressione e pertanto si può scegliere la riduzione da eseguire. Ovviamente il risultato verrà lo stesso.
Per eseguire una riduzione bisogna, una volta scelto il termine che si può ridurre, applicare uno per volta allo stesso le espressioni alla sua destra. In questo modo di fatto applico un input alla funzione corrente sostituendo nel corpo della stessa cioè che viene "inputato" alla funzione.
Esempio: posso ridurre il termine: $(\lambda x y.x x y)w$ in $\lambda y.ww$. Come vedi nel secondo termine mi ritrovo così ad avere un input in meno e la $x$ che pertanto "scompare" in quanto nel corpo della funzione ho sostituito il mio input $w$ in corrispondenza della $x$.
Altro esempio: posso ridurre il termine: $\(lambda x y.x x y)(\lambda w.z)u$ in $\(lambda y.(\lambda w.z)(\lambda w.z)y)u$ col primo passaggio e poi da qui in $(\lambda w.z)(\lambda w.z)u$. Ora di fatto il prossimo passo di riduzione è quello di sostituire $(\lambda w.z)$ in $(\lambda w.z)$ ma di fatto nel corpo della mia espressione ($z$) non ho occorrenze di $w$ e pertanto magicamente il $\lambda w$ che c'è davanti "scompare" e rimango con $z$, a cui poi ovviamente accodo $u$. Questo è il mio risultato.

[...]
per forma normale intendiamo semplicemente un termine in cui abbiamo eseguito tutte le possibili riduzioni no?
[...]

Esatto: un termine tale per cui non si possono più eseguire riduzioni al fine di semplificarlo (ottenendo cioè un termine diverso da quello corrente) si dice in forma normale.

[...]
come facciamo a trovare quali sono le variabili libere? (qui credo sia piu un problema della mia confusione riguardo alla sintassi del lambda calcolo) un esercizio ad esempio mi chiede di trovare le variabili libere di questo termine

λz.( ((λx.λx.yx)x)(vλz.λw.v) )

come lo fareste?

Alla luce di quanto scritto in questi post, appare ora chiaro come le variabili libere nell'esercizio da te proposto sono $y$ e $v$ in quanto non compaiono come argomenti di nessuna tra le espressioni (nessuna espressione contiene $\lambda ...y...$ o $\lambda ...u...$ (dove ovviamente al posto dei punti ci potrebbero essere come no delle altre variabili).