Lambda-calcolo e beta-riduzioni

[emaema-votailprof]

Salve a tutti...In questi giorni mi sto trovando ad affrontare alcuni quesiti che riguardano gli argomenti espressi nel topic..Mi interesserebbe sapere perchè:
1) la confluenza del λ-calcolo garantisce l'esistenza di un β-ridotto comune per ogni coppia di termini che siano β-ridotti di uno stesso termine.
2) che relazione può avere l'α-convertibilità con la domanda 1.
3) non riesco a capire qual'è il criterio secondo il quale viene abblicata una β-riduzione.

Grazie a tutti per l'interesse!!!

[emaema-votailprof]

Up! help please!


[mod="Fioravante Patrone"]Blocco per 24 ore, per violazione della regola relativa agli "up".[/mod]
[mod="Martino"]Sbloccato. 24 ore passate.[/mod]

[fields1]

"ben100":Mi interesserebbe sapere perchè:
1) la confluenza del λ-calcolo garantisce l'esistenza di un β-ridotto comune per ogni coppia di termini che siano β-ridotti di uno stesso termine.

Perche' quella che citi e' esattamente la definizione di confluenza (detta anche proprieta' di Church-Rosser).

2) che relazione può avere l'α-convertibilità con la domanda 1.

L'alpha equivalenza intendi? Non c'entra nulla con la confluenza della beta riduzione, riguarda solo la ridenominazione delle variabili vincolate.

3) non riesco a capire qual'è il criterio secondo il quale viene abblicata una β-riduzione.

Se $v$ e' un termine che contiene dentro di se' $(\lambda x u)t$ si puo' sostituire quest'ultimo con $u[t \/x]$ ($t$ sostituisce $x$ in $u$, stando attenti alla cattura di variabili) lasciando invariato il resto di $v$. Questa e' la applicazione di un passo di $\beta$-riduzione.