[Lambda Calcolo] Loop o forma normale?
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?
è 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?
Risposte
Ciao Benvenuto,
non è molto complicato, anzi è banale.
xxxx è il nome del parametro della $\lambda$-astrazione, è una free-variable perchè non è legata a nessun termine/applicazione. difatti \(xxxx \neq x\). In pratica è una beta-riduzione/sostituzione vuota, basta vedere la definizione (oppure può esser vista come una eta-beta riduzione).
(\xxxx.xx) (\x.x x) -> x{(\x.x x)|xxxx} x{(\x.x x)|xxxx} -> x x
"andrePa":
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?
non è molto complicato, anzi è banale.
xxxx è il nome del parametro della $\lambda$-astrazione, è una free-variable perchè non è legata a nessun termine/applicazione. difatti \(xxxx \neq x\). In pratica è una beta-riduzione/sostituzione vuota, basta vedere la definizione (oppure può esser vista come una eta-beta riduzione).
(\xxxx.xx) (\x.x x) -> x{(\x.x x)|xxxx} x{(\x.x x)|xxxx} -> x x
Ah, in pratica considerando "xxxx" come unico parametro, non c'è nulla da sostituire e si lasciano gli altri termini. Grazie, ma quindi se invece di quattro x, ce ne fosse stata solamente una nell'astrazione (parte bound)? in quel caso gli avrei passato il parametro, oppure sarebbe stata vuota?
E un'altra cosa, perché si considera come unico parametro, e non come 4? (ad esempio \xyzw.yz ha 4 parametri in ingresso)
E un'altra cosa, perché si considera come unico parametro, e non come 4? (ad esempio \xyzw.yz ha 4 parametri in ingresso)
"andrePa":
Ah, in pratica considerando "xxxx" come unico parametro, non c'è nulla da sostituire e si lasciano gli altri termini.
per arrivare alla conclusione che hai mostrato quella è l'unica situzione possibile di spiegazione.
Se intendi le x come variabili "distinte", considerando la paranterizzazione destra della lambda-astrazione e sinistra delle applicazioni, sarebbe:
$(\lambdax.(\lambdax.(\lambdax.(\lambdax.(x x))))) (\lambdax.x x)$
ma c'è un problema formale di fondo, molto importante. $x$ in $\lambda x. ....$ è legata, non più utilizzabile (nel lambda calcolo classico, i passaggi sono per nome, non per valore od altro). La seconda variabile è formalmente sbagliata. In un sistema formale di controllo semantico avresti un errore.
Quindi se provi a valutare tale espressione avresti una terminazione od un'eccezione con un risultato parziale.
Grazie, ma quindi se invece di quattro x, ce ne fosse stata solamente una nell'astrazione (parte bound)? in quel caso gli avrei passato il parametro, oppure sarebbe stata vuota?
intendi: (\x.x x) (\x.x x)?
E un'altra cosa, perché si considera come unico parametro, e non come 4? (ad esempio \xyzw.yz ha 4 parametri in ingresso)
questo è il caso standard e non c'entra con il caso sopra che è un caso molto particolare.
\xyzw.yz è una compressione per intendere: \x.\y.\z\.w.(y z)
quattro parametri distinti e non puoi utilizzare la stessa variabile nei parametri (sai cosa è una alpha-conversione?).
Si, appunto per quello chiedevo!
Se si considerano parametri distinti, in quel caso si potrebbe cambiare il nome della variabile, od almeno, così ho sempre fatto quando ce n'era una legata, mentre in quel caso, sono tutte x, ed anche sostituendo, cosa vado a sostituire?
Quella era la domanda di fondo, ed anche l'impossibilità dell'applicazione dell'aplha-conversione mi ha creato qualche problema a capire come trovare la forma normale.
Se si considerano parametri distinti, in quel caso si potrebbe cambiare il nome della variabile, od almeno, così ho sempre fatto quando ce n'era una legata, mentre in quel caso, sono tutte x, ed anche sostituendo, cosa vado a sostituire?
Quella era la domanda di fondo, ed anche l'impossibilità dell'applicazione dell'aplha-conversione mi ha creato qualche problema a capire come trovare la forma normale.
"andrePa":
Si, appunto per quello chiedevo!
Se si considerano parametri distinti, in quel caso si potrebbe cambiare il nome della variabile, od almeno, così ho sempre fatto quando ce n'era una legata, mentre in quel caso, sono tutte x, ed anche sostituendo, cosa vado a sostituire?
nel caso esteso che ti ho riscritto?
(\x.\x.\x.\x. x x) (\x.x x)
Se sì, ti ritrovi in una forma non consistente e dipende tutto dalla semantica cosa ti risponde, è un po' aleatoria la questione.
"andrePa":
Quella era la domanda di fondo, ed anche l'impossibilità dell'applicazione dell'aplha-conversione mi ha creato qualche problema a capire come trovare la forma normale.
diciamo che è un caso degenere quello che hai proposto.
La regola è semplice, ogni parametro di un'astrazione (i $\lambda$-termini) devono essere distinti. Ogni ambiente valutato avrà corrispondenza solo se ci sono variabili distinte, se sono uguali allora ci sarà inconsistenza dei dati ed un errore formale.
Proporre che \xxxx sia la variabile xxxx è solo per spiegare la tua conclusione iniziale, ed un interprete potrebbe risponderti sia come ho fatto io, sia provare ad interpretare separatamente le variabili, ma in questo caso è tutto lasciato alla semantica dell'interprete e non al lambda calcolo classico.
L'insieme delle variabili è numerabile quindi ha cardinalità $NN$, perchè complicarsi la vita e sceglierle uguali?
Eh, ma all'appello non posso scegliermi le variabili...
Era un testo d'esame, ecco perché insistevo tanto. Grazie infinite comunque!
Era un testo d'esame, ecco perché insistevo tanto. Grazie infinite comunque!
"andrePa":
Eh, ma all'appello non posso scegliermi le variabili...
Era un testo d'esame, ecco perché insistevo tanto. Grazie infinite comunque!
ok, se hai altre domande posta pure
Per curiosità, di che esame si tratta? semantica,progr. funzionale, fondamenti, ...?
semantica!
xx(\x.x)y((\x.x)x)
avendo una cosa del genere, invece, come vado a lavorarci?
Grazie!
avendo una cosa del genere, invece, come vado a lavorarci?
Grazie!
"andrePa":
xx(\x.x)y((\x.x)x)
la parentesizzazione è corretta?
se si ci vuole una strategia normalizzante. Con la leftmost-outermost mi pare puoi fare solo uno step:
x x (\x.x) y ((\x.x) x) -> x x (\x.x) y ({x/x}x) -> x x (\x.x) y x
questo perchè lo scoping dell'applicazione è a sinistra.
cioè partendo da:
(\xxxx.xx)(\x.xx)(\x.x)y((\x.x)x)
(\xxxx.xx)(\x.xx)(\x.x)y((\x.x)x)
"hamming_burst":
[quote="andrePa"]xx(\x.x)y((\x.x)x)
la parentesizzazione è corretta?
se si ci vuole una strategia normalizzante. Con la leftmost-outermost mi pare puoi fare solo uno step:
x x (\x.x) y ((\x.x) x) -> x x (\x.x) y ({x/x}x) -> x x (\x.x) y x
questo perchè lo scoping dell'applicazione è a sinistra.[/quote]
allora, l'esempio era quello appena postato.
dando per scontato che i primi due si riducono con xx, rimane xx, oppure finisce come dici tu? x x (\x.x) y x
"hamming_burst":
[quote="andrePa"]xx(\x.x)y((\x.x)x)
la parentesizzazione è corretta?
se si ci vuole una strategia normalizzante. Con la leftmost-outermost mi pare puoi fare solo uno step:
x x (\x.x) y ((\x.x) x) -> x x (\x.x) y ({x/x}x) -> x x (\x.x) y x
questo perchè lo scoping dell'applicazione è a sinistra.[/quote]
si, è proprio la parentesizzazione che fatico a comprendere.
cioè ad intuito, faccio l'ultima identità, perché ci sono le parentesi, ma applicando LO, come ci si arriva?
Scusami per i post di seguito, all'inizio stavo scrivendo e poi ho notato la risposta.
"hamming_burst":
[quote="andrePa"]xx(\x.x)y((\x.x)x)
la parentesizzazione è corretta?
se si ci vuole una strategia normalizzante. Con la leftmost-outermost mi pare puoi fare solo uno step:
x x (\x.x) y ((\x.x) x) -> x x (\x.x) y ({x/x}x) -> x x (\x.x) y x
questo perchè lo scoping dell'applicazione è a sinistra.[/quote]
Per favore potresti spiegarmi come mai non posso ridurre anche (\x.x)y a y in modo da ottenere xxyx come forma normale? Mi faresti un grande piacere
"andrePa":
Scusami per i post di seguito, all'inizio stavo scrivendo e poi ho notato la risposta.
riformula il tuo dubbio che non l'ho capito.
"~Rose":
Per favore potresti spiegarmi come mai non posso ridurre anche (\x.x)y a y in modo da ottenere xxyx come forma normale? Mi faresti un grande piacere
Ciao ~Rose, da un po' un passavi da queste parti
attenta che gli spazi sono importanti, soprattutto per marcare l'applicazione: $xy \ne x\ y$. una è la variabile xy l'altra l'applicazione da y a x.
In questo caso lo scope delle astrazioni sono vincolati da parentesi quindi non c'è ambiguità. Queste sono tutte da considerare espressioni singole. Prova sostituire:
z $\equiv$ (\x.x)
t $\equiv$ ((\x.x) x)
utilizzando l'associazione sinistra (la convenzione) inserisci parentesi partendo da sinistra a destra:
x x z y t -> ((x x z y) t) -> (((x x z) y) t) -> ((((x x) z) y) t)
più chiaro? in tal caso non si sono riduzioni da fare perchè è già in forma canonica.
"hamming_burst":
In questo caso lo scope delle astrazioni sono vincolati da parentesi quindi non c'è ambiguità. Queste sono tutte da considerare espressioni singole. Prova sostituire:
z $ \equiv $ (\x.x)
t $ \equiv $ ((\x.x) x)
utilizzando l'associazione sinistra (la convenzione) inserisci parentesi partendo da sinistra a destra:
x x z y t -> ((x x z y) t) -> (((x x z) y) t) -> ((((x x) z) y) t)
più chiaro? in tal caso non si sono riduzioni da fare perchè è già in forma canonica.
Buondì hamming_burst, mi intrufolo anch'io nella conversazione
(semantica è imminente).Leggendo le regole di inferenza qui a me verrebbe da applicare la (3) visto che M (x) è in forma normale. Allora mi trovo sulla seconda x, applico di nuovo la (3) essendo M di nuovo in forma normale. Dopodiché mi troverei ad applicare (\x.x) y essendo M un'astrazione, ottenendo $ y $, e avanti così. Dove sbaglio nell'applicazione delle regole?
dicevo:
(\xxxx.xx)(\x.xx)(\x.x)y((\x.x)x)
come fa a venire xx?
(\xxxx.xx)(\x.xx)(\x.x)y((\x.x)x)
come fa a venire xx?
Salve a tutti! Mi aggrego anch'io alla conversazione. Sto facendo anch'io questo esercizio, ma non riesco a capire come abbia fatto ad arrivare al risultato xx.
utilizzate tutti le regole di una semantica operazionale come quella proposta da Black27? con inclusa anche l'$\alpha$-congruenza e l'$\alpha$-conversione? oppure nelle vostre semantiche sono state introdotte regole particolari, oppure usate altre semantiche?
se utilizzate tutti quelle di Black27, rispondo una sola volta per tutti.
PS: ciao Black
se utilizzate tutti quelle di Black27, rispondo una sola volta per tutti.
PS: ciao Black
"hamming_burst":
utilizzate tutti le regole di una semantica operazionale come quella proposta da Black27? con inclusa anche l'$\alpha$-congruenza e l'$\alpha$-conversione? oppure nelle vostre semantiche sono state introdotte regole particolari, oppure usate altre semantiche?
se utilizzate tutti quelle di Black27, rispondo una sola volta per tutti.
Usiamo la semantica proposta da Black27.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo