[Lambda Calcolo] Loop o forma normale?

[andrePa1]

Salve a tutti,
è il mio primo messaggio, a causa di una beta-riduzione in lambda calcolo che non mi viene.

(\xxxx.xx)(\x.xx) -> xx

Come si arriva a questa conclusione?

[hamming_burst]

Se è vero quanto scritto nei post precedenti, che dipende tutto dalla semantica come comportarsi nei casi particolari come questo, lasciando perdere il primo esempio che è un caso degenere dovuto al fatto che non mi è stato dato l'esercizio completo (è corretto cmq quella risoluzione); è anche vero che è possibile risoverlo utilizzando un po' allegramente i costrutti classici, sfociando quindi per implicazione in quelle che sono vere regole semantiche.

Pensavo di mostrarvi i vari passi inferenziali, ma lascio a voi quel tedioso passaggio, vi mostro solo lo step semantico vero.

(\xxxx.xx)(\x.xx)(\x.x)y((\x.x)x) =
= (\x.\x.\x.\x.x x) (\x.x x) (\x.x) y ((\x.x) x) = (((((\x.\x.\x.\x.x x) (\x.x x)) (\x.x)) y) ((\x.x) x))
utilizzando la normalizzazione leftmost-outermost (che penso conosciate tutti visto che è quella classica), cioè più a sinistra ed esterno, partiamo dal passo rosso (utilizzando altre normalizzazione il risultato cambierà).
Si può risolvere e spiegare in alcuni modi, passando per le FV e BV, attravero alpha-conversione preventiva, ma forse è più semplice passare per una delle varie forme di sostituzione (di beta-riduzione):

Sia (\y.M) N -> M{N/y}

if M=\x.M' e x=y allora \x.M'{N/y} = \x.M'

quindi in pratica non avviene nessuna beta-riduzione (è un'analogia con il primo caso del post, ma ci sono differenze):

(\x.\x.\x.\x.x x) (\x.x x) -> (\x.\x.\x.x x){(\x.x x)/x} = (\x.\x.\x.x x)
(\x.\x.\x.x x) (\x.x) -> (\x.\x.x x) {(\x.x)/x} = (\x.\x.x x)
(\x.\x.x x) y -> (\x.x x) {y/x} = (\x.x x)
(\x.x x) ((\x.x) x) -> x{((\x.x) x)/x} x{((\x.x) x)/x} = ((\x.x) x) ((\x.x) x)
((\x.x) x) ((\x.x) x) ->* left-right = x x

il tutto sarebbe da formalizzare secondo le regole inferenziali.

[Black27]

"hamming_burst":Se è vero quanto scritto nei post precedenti, che dipende tutto dalla semantica come comportarsi nei casi particolari come questo, lasciando perdere il primo esempio che è un caso degenere dovuto al fatto che non mi è stato dato l'esercizio completo (è corretto cmq quella risoluzione); è anche vero che è possibile risoverlo utilizzando un po' allegramente i costrutti classici, sfociando quindi per implicazione in quelle che sono vere regole semantiche.

Pensavo di mostrarvi i vari passi inferenziali, ma lascio a voi quel tedioso passaggio, vi mostro solo lo step semantico vero.

(\xxxx.xx)(\x.xx)(\x.x)y((\x.x)x) =
= (\x.\x.\x.\x.x x) (\x.x x) (\x.x) y ((\x.x) x) = (((((\x.\x.\x.\x.x x) (\x.x x)) (\x.x)) y) ((\x.x) x))
utilizzando la normalizzazione leftmost-outermost (che penso conosciate tutti visto che è quella classica), cioè più a sinistra ed esterno, partiamo dal passo rosso (utilizzando altre normalizzazione il risultato cambierà).
Si può risolvere e spiegare in alcuni modi, passando per le FV e BV, attravero alpha-conversione preventiva, ma forse è più semplice passare per una delle varie forme di sostituzione (di beta-riduzione):

Sia (\y.M) N -> M{N/y}

if M=\x.M' e x=y allora \x.M'{N/y} = \x.M'

quindi in pratica non avviene nessuna beta-riduzione (è un'analogia con il primo caso del post, ma ci sono differenze):

(\x.\x.\x.\x.x x) (\x.x x) -> (\x.\x.\x.x x){(\x.x x)/x} = (\x.\x.\x.x x)
(\x.\x.\x.x x) (\x.x) -> (\x.\x.x x) {(\x.x)/x} = (\x.\x.x x)
(\x.\x.x x) y -> (\x.x x) {y/x} = (\x.x x)
(\x.x x) ((\x.x) x) -> x{((\x.x) x)/x} x{((\x.x) x)/x} = ((\x.x) x) ((\x.x) x)
((\x.x) x) ((\x.x) x) ->* left-right = x x

il tutto sarebbe da formalizzare secondo le regole inferenziali.

Ottimo, grazie mille, chiarissimo come sempre