esercizi sul lambda calcolo

[Franco Barbanera]

e poi una cosa...

è possibile fare una sostituzione del genere?

\y.x [xy/x]

io credo di no perchè BV(\y.x) n FV(xy) != 0, però non sono convìnto di questa cosa

Scusi professore ma noi non avevamo detto che se si verifica

BV(\y.x) n FV(xy) != 0 NON si poteva sostituire?

Non ho capito molto bene questa cosa...

Abbiamo anche detto che quando la condizione non e' soddisfatta
si fa una alfa-conversione (cioe' una rinomina delle variabili legate)
in modo che la condizione risulti verificata.

[Franco Barbanera]

una sostituzione si può sempre svolgere

Forse e' meglio utilizzare il verbo "applicare".

[Franco Barbanera]

x luca98:
fai gli esercizi di alfa-conversione proposti sul forum

[luca98]

e poi una cosa...

è possibile fare una sostituzione del genere?

\y.x [xy/x]

io credo di no perchè BV(\y.x) n FV(xy) != 0, però non sono convìnto di questa cosa

Scusi professore ma noi non avevamo detto che se si verifica

BV(\y.x) n FV(xy) != 0 NON si poteva sostituire?

Non ho capito molto bene questa cosa...

Abbiamo anche detto che quando la condizione non e' soddisfatta
si fa una alfa-conversione (cioe' una rinomina delle variabili legate)
in modo che la condizione risulti verificata.

Ora ho capito! Grazie professore

[luca98]

Esercizio 33

Eseguire le seguenti sostituzioni:
(λx.yx)[yz/x]
(λy.xy)[yz/x]
(λz.(λx.yx)xz)[zx/x]
---------------------------------------------------------------------------
1 credo che nella prima non si possa sostituire dato che la x è legata(mi corregga se sbaglio)
2 \t.(yz)t
3 \p.(\x.yx)(zx)p)

la 1 non e' che non si possa fare,
e' che e' una sostituzione che non cambia nulla

Quindi se ho capito bene potrei scrivere...

(λx.yx)[yz/x] -> (λyz.yyz)

(λx.yx)[yz/x] -> (λyz.yyz)
Non ci va la freccia!
E abbiamo detto che si sostituiscono solo le variabili libere!
La x in (λx.yx) NON e' libera.

allora resta così no? \x.yx

avevo frainteso le sue parole "la 1 non e' che non si possa fare,
e' che e' una sostituzione ehe non cambia nulla"

Per questo ho sostituito, ma le assicuro che avevo ben chiaro il fatto che non si possono sostituire variabili legate come la X in questione 

[luca98]

x luca98:
fai gli esercizi di alfa-conversione proposti sul forum

Va bene professore, domani proverò a farli

[Franco Barbanera]

allora resta così no? \x.yx

Esatto.