lambda-calcolo e beta-riduzioni

[ben100]

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

[ben100]

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]

[fields]

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 \( \displaystyle {v} \) e' un termine che contiene dentro di se' \( \displaystyle {\left(\lambda{x}{u}\right)}{t} \) si puo' sostituire quest'ultimo con \( \displaystyle {u}{\left[{t}/{x}\right]} \) (\( \displaystyle {t} \) sostituisce \( \displaystyle {x} \) in \( \displaystyle {u} \), stando attenti alla cattura di variabili) lasciando invariato il resto di \( \displaystyle {v} \). Questa e' la applicazione di un passo di \( \displaystyle \beta \)-riduzione.