Lambda calcolo

[BoG3]

Ciao a tutti,
vorrei fare una domanda sul lambda calcolo:
dato:
$(\lambdax.xy)(\lambdat.tz)((\lambdax.\lambdaz.xyz)yx)$ procedo:
$|->(\lambdax.xy)(\lambdat.tz)((\lambdaz.yyz)x)$
$|->(\lambdax.xy)(\lambdat.tz)(yyx)$ ora ho dei dubbi:
Se non sbaglio: la precedenza va a sinistra, quindi devo applicare $(\lambdax.xy)$ a $(yyx)$. Giusto?
quindi ottengo: $(yyx)y$ e sostituito nella mia riduzione ho:
$|->((yyx)y)(\lambdat.tz)$ ma dovrebbe essere $(\lambdat.tz)((yyx)y)$. Qualcuno puo spiegarmi per favore? Perchè $((yyx)y)$ finisce a destra? PEnso di no aver capito la bvase della semantica. Forse la risposta è che:
$f(g(x))$ in lambda calcolo si scrive $(\lambdax.y)(lambday.z) x$ ?? (l'ho sparata .... solo per far capire la mia domanda... spero serva)

Grazie mille

[el_brando]

Allora sono un pò arrugginito con il lambda calcolo, ma dovrebbe essere così:

\( (\lambda x .xy)(\lambda t.tz)((\lambda x.\lambda z.xyz)yx) \rightarrow \)
\( \rightarrow (\lambda x .xy)(\lambda t.tz)((\lambda z.yyz)x) \rightarrow \)
\( \rightarrow (\lambda x .xy)(\lambda t.tz)(yyx) \rightarrow \)
\( \rightarrow (\lambda t.tz)(yyx)y \)

Ricorda:
- l'applicazione associa a sinistra, cioè \( MNP \equiv (MN)P \)
- lo scope di \( \lambda \) estende il più a destra possibile, cioè \( \lambda x.MN \equiv \lambda x.(MN) \)

[el_brando]

Forse non ho chiarito il tuo dubbio...
L'applicazione finale è \( [(\lambda x.xy)][(\lambda t. tz)(yyx)] \)
quindi \( (\lambda t. tz)(yyx) \) viene sostituito alla \( x \) di \((\lambda x.xy) \)...

[BoG3]

Questo è i lpassaggio che non capisco:

"el_brando":Allora sono un pò arrugginito con il lambda calcolo, ma dovrebbe essere così:
\( \rightarrow (\lambda x .xy)(\lambda t.tz)(yyx) \rightarrow \)
\( \rightarrow (\lambda t.tz)(yyx)y \)

Io avrei fatto così:
\( \rightarrow (\lambda x .xy)(\lambda t.tz)(yyx) \rightarrow \)
\( \rightarrow (yyx)y (\lambda t.tz) \)

PErchè el_brando ha ragione?
è forse perchè è una funzione composta e $\lambdat.tz$ deve prendere in input il risultato di $\lambdax.xy(yyx)$

Spero la mia domanda sia chiara

[el_brando]

Nel mio secondo post c'è la risposta...
Il perchè deriva da: "lo scope di \( λ \) estende il più a destra possibile, cioè \( λx.MN≡λx.(MN) \)" come ho scritto nel primo post...

[onlyReferee]

E' esattamente come descritto da el_brando. Si valuta tutta l'espressione lambda da sinistra a destra ed in assenza partentesi si ha che lo scope di $\lambda$ è esteso quanto più a destra possibile,

[BoG3]

"el_brando":Nel mio secondo post c'è la risposta...
Il perchè deriva da: "lo scope di \( λ \) estende il più a destra possibile, cioè \( λx.MN≡λx.(MN) \)" come ho scritto nel primo post...

Scusami! non avevo proprio visto! Grazie mille, in effetti era molto semplice!