Pages: 1 [2]   Go Down
Print
Author Topic: Re:esercizio esempio beta-Riduzione  (Read 996 times)
0 Members e 1 Utente non registrato stanno visualizzando questa discussione.
ɹǝǝuıƃuǝsɹǝʌǝɹ
Administrator
God of the Forum
*****
Offline Offline

Gender: Male
Posts: 4.467


Più grande è la lotta, e più è glorioso il trionfo


WWW
« Reply #15 on: 08-01-2018, 19:39:13 »

Non sono il professore, ma mi permetto comunque di rispondere...

Evidenzio il penultimo passaggio, e la sua correzione:
professore, abbiamo provato a fare l'esercizio numero 43 e ora posto la soluzione, mi può dire se è corretto??

           (λxxxx.xx)(λx.xx)(λx.x)y((λx.x)x)

->beta   (λxxxx.xx)(λx.xx)(λx.x)yx
=alpha   (λa.(λb.(λc.(λx.xx))))(λx.xx)(λx.x)yx
->beta   (λb.(λc.(λx.xx)))(λx.x)yx
->beta   (λc.(λx.xx))y
x
->beta      λx.xx  (?) testate   boh <diventa in realtà:> (λx.xx)
x
->beta   xx

« Last Edit: 09-01-2018, 20:08:12 by Franco Barbanera » Logged

La grande marcia della distruzione mentale proseguirà. Tutto verrà negato. Tutto diventerà un credo. È un atteggiamento ragionevole negare l'esistenza delle pietre sulla strada; sarà un dogma religioso affermarla. È una tesi razionale pensare di vivere tutti in un sogno; sarà un esempio di saggezza mistica affermare che siamo tutti svegli. Accenderemo fuochi per testimoniare che due più due fa quattro. Sguaineremo spade per dimostrare che le foglie sono verdi in estate. Non ci resterà quindi che difendere non solo le incredibili virtù e saggezze della vita umana, ma qualcosa di ancora più incredibile: questo immenso, impossibile universo che ci guarda dritto negli occhi. Combatteremo per i prodigi visibili come se fossero invisibili. Guarderemo l'erba e i cieli impossibili con uno strano coraggio. Saremo tra coloro che hanno visto eppure hanno creduto.

In tutto, amare e servire.

  
                            ن                           
I can deal with ads,
I can deal with buffer,
but when ads buffer
I suffer...

...nutrimi, o Signore, "con il pane delle lacrime; dammi, nelle lacrime, copiosa bevanda...

   YouTube 9GAG    anobii  S  Steam T.B.o.I. Wiki [univ] Lezioni private  ʼ  Albo d'Ateneo Unicode 3.0.1
Usa "Search" prima di aprire un post - Scrivi sempre nella sezione giusta - Non spammare - Rispetta gli altri utenti - E ricorda di seguire il Regolamento
luca98
Matricola
*
Offline Offline

Posts: 78



« Reply #16 on: 08-01-2018, 19:51:14 »

.ora è più comprensibile?

poco piu'.

            (\a.(\b.(\x.((\xx.x)(xx)(\x.x)))))x(xx)

-->beta   (\b.(\x.((\xx.x)(xx)(\x.x))))(xx)

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

=alpha   (\x.((\a.\x.x)(xx)(\x.x)))     

-->beta  (\x.((\x.x)(\x.x)))         

-->beta    \x.(\x.x)   



ha ragione...ho dimenticato a scrivere per ogni passaggio cosa stavo facendo testate

per il resto l'esercizio risulta corretto, giusto?
Logged
luca98
Matricola
*
Offline Offline

Posts: 78



« Reply #17 on: 08-01-2018, 21:29:00 »

Esercizio 46
Qual e' la formal normale del seguente termine?
((λw.(xw))(λy.(yx)))[λx.(w(xy))/x]

             
              ((λw.(xw))(λy.(yx)))[λx.(w(xy))/x]

-->beta   x(\y.(yx))[λx.(w(xy))/x] = (\x.(w(xy)))(\y.(y(\x.(w(xy)))))

=alpha   (\x.(w(xy)))(\m.(m(\x.(w(xy)))))

-->beta   (w((\m.(m(\x.(w(xy)))))y))       

-->beta   (w(y(\x.(w(xy)))))   forma normale

il lamda calculator presente nel sito mi da invece come risulato: w xy

non capisco dove sbaglio...
Logged
Gerasia
Matricola
*
Offline Offline

Posts: 31


« Reply #18 on: 08-01-2018, 21:29:42 »

Non sono il professore, ma mi permetto comunque di rispondere...

Evidenzio il penultimo passaggio, e la sua correzione:
professore, abbiamo provato a fare l'esercizio numero 43 e ora posto la soluzione, mi può dire se è corretto??

           (λxxxx.xx)(λx.xx)(λx.x)y((λx.x)x)

->beta   (λxxxx.xx)(λx.xx)(λx.x)yx
=alpha   (λa.(λb.(λc.(λx.xx))))(λx.xx)(λx.x)yx
->beta   (λb.(λc.(λx.xx)))(λx.x)yx
->beta   (λc.(λx.xx))y
x
->beta      λx.xx  (?) testate   boh <diventa in realtà:> (λx.xx)
x
->beta   xx



chiedo perdono, mi è sfuggita completamente di testa quella x  pray
ma apparte quello risulta corretto il procedimento??
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.928



WWW
« Reply #19 on: 08-01-2018, 22:43:03 »

tenete presente che per il lambda-calulator (che e' pieno di bug...)
l'espressione xy non rappresenta x applicato ad y, ma una unica variabile
di nome "xy".

Logged
MoonlightLucrix
Matricola
*
Offline Offline

Gender: Male
Posts: 2



« Reply #20 on: 09-01-2018, 18:03:14 »

Scusi prof. ho un dubbio su quest'esercizio:
(λx.xxy)(λxy.xyy)  il risultato dovrebbe essere -> yyy

riducendo ottengo

((λxy.xyy)(λxy.xyy)y) dopo questo punto non so come procedere, andando avanti mi vengono cose diverse dal risultato 
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.928



WWW
« Reply #21 on: 09-01-2018, 19:57:57 »

  

   (λx.xxy)(λxy.xyy)

-->beta ((λxy.xyy)(λxy.xyy)y)

a questo punto, anche se non e' indispensabile, facciamo una alpha conversione,
in modo da non rischiare di confonderci

=alpha ((λab.abb)(λxy.xyy)y)

ricordiamoci ora che in realta' questo termine (per le convenzioni sulla notazione) e'

 (((λa.(λb.(abb)))(λx.λy.xyy))y)

a questo punto esiste un unico redex in questo termine, che e'

(((λa.(λb.(abb)))(λx.λy.xyy))y)

[Fin qui e' chiaro?]

riducendo il redex sottolineato  si ottiene.... [CONTINUARE]






« Last Edit: 09-01-2018, 20:07:22 by Franco Barbanera » Logged
jeremy_sapienza
Matricola
*
Offline Offline

Posts: 11


« Reply #22 on: 09-01-2018, 23:24:26 »

mi perdoni professore ma quindi se facessi invece in questo modo..

(\x.xxy)(\xy.xyy) xxy[\xy.xyy / x]

-->beta ((\xy.xyy)(\xy.xyy)y)  xyy[\xy.xyy / xy]

-->beta ((\xy.xyy)(yy)) xyy[yy / xy]

yyy

ho comesso un errore già dall'inizio appena stavo per ridurre? visto che \x. e il secondo lambda termine non sono uguali(\xy.)?   non ho capito il perchè del primo passo che lei ha scritto

« Last Edit: 10-01-2018, 12:18:05 by jeremy_sapienza » Logged
josura
Matricola
*
Offline Offline

Gender: Male
Posts: 29


Ho paura.


« Reply #23 on: 09-01-2018, 23:34:36 »

(((λa.(λb.(abb)))(λx.λy.xyy))y)
-->beta ((λb.((λx.λy.xyy)bb))y)
-->beta ((λb.((λy.byy)b))y)
-->beta (λb.(bbb)y)
-->beta yyy

Forse?
Sono stato battuto sul tempo?  
Ma in teoria nella beta riduzione si dovrebbero sostituire/ridurre solo variabili libere, o almeno è quello che ho capito dal testo, si possono sostituire pure applicazioni?
Sono confuso dal risultato del mio collega.
« Last Edit: 09-01-2018, 23:51:26 by josura » Logged

A.K.A. voglio morire/vivere
jeremy_sapienza
Matricola
*
Offline Offline

Posts: 11


« Reply #24 on: 09-01-2018, 23:49:57 »

(((λa.(λb.(abb)))(λx.λy.xyy))y)
-->beta ((λb.((λx.λy.xyy)bb))y)
-->beta ((λb.((λy.byy)b))y)
-->beta (λb.(bbb)y)
-->beta yyy

Forse?
Sono stato battuto sul tempo?  
Ma in teoria nella beta riduzione si dovrebbero sostituire solo variabili libere, o almeno è quello che ho capito dal testo, si possono sostituire pure applicazioni?
Sono confuso dal risultato del mio collega.

io sinceramente, vedendo questa congruenza

(MP)[N/x] =congruo (M[N/x])(P[N/x])

ho pensato che una cosa del genere si possa fare.. , però non ne sono sicuro, perchè difatti la sostituzione si occupa di sostituire le variabili libere..
« Last Edit: 09-01-2018, 23:51:32 by jeremy_sapienza » Logged
josura
Matricola
*
Offline Offline

Gender: Male
Posts: 29


Ho paura.


« Reply #25 on: 09-01-2018, 23:55:12 »

Sono perplex 
Logged

A.K.A. voglio morire/vivere
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.928



WWW
« Reply #26 on: 10-01-2018, 14:56:14 »

Quote
mi perdoni professore ma quindi se facessi invece in questo modo..

(\x.xxy)(\xy.xyy) xxy[\xy.xyy / x]

-->beta ((\xy.xyy)(\xy.xyy)y)  xyy[\xy.xyy / xy]

Cosi' e' scritto male.

Puoi scrivere, se vuoi:

              (\x.xxy)(\xy.xyy)

-->beta    xxy[\xy.xyy / x]
                che per definizione di sostituzione, questo corrisponde a
                 ((\xy.xyy)(\xy.xyy)y)

[e poi continuare]
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.928



WWW
« Reply #27 on: 10-01-2018, 14:58:24 »

(((λa.(λb.(abb)))(λx.λy.xyy))y)
-->beta ((λb.((λx.λy.xyy)bb))y)
-->beta ((λb.((λy.byy)b))y)
-->beta (λb.(bbb)y)
-->beta yyy

Forse?
Sono stato battuto sul tempo?  
Ma in teoria nella beta riduzione si dovrebbero sostituire/ridurre solo variabili libere, o almeno è quello che ho capito dal testo, si possono sostituire pure applicazioni?
Sono confuso dal risultato del mio collega.

Se io scrivessi  "yytbbooughbssnnllsii",
ti confonderesti?
Credo di si. Perche'?
Perche' ho scritto una cosa priva di senso..

FB
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.928



WWW
« Reply #28 on: 10-01-2018, 15:02:00 »

Quote
io sinceramente, vedendo questa congruenza

(MP)[N/x] =congruo (M[N/x])(P[N/x])

ho pensato che una cosa del genere si possa fare..

Quella che hai fornito e' una parte della definizione di sostituzione,
che dice che la sostituzione di N al posto della variabile libera in neltermine (MP)
si ottiene sostiotuendo N al posto di x in M e applicando il risultato alla sostituzione
di N al posto di x in P  (in soldoni, sostituendo N al posto di x sia in M che in P)
Logged
MoonlightLucrix
Matricola
*
Offline Offline

Gender: Male
Posts: 2



« Reply #29 on: 10-01-2018, 18:42:41 »

(((λa.(λb.(abb)))(λx.λy.xyy))y)
-->beta ((λb.((λx.λy.xyy)bb))y)
-->beta ((λb.((λy.byy)b))y)
-->beta (λb.(bbb)y)
-->beta yyy

Forse?
Sono stato battuto sul tempo?  
Ma in teoria nella beta riduzione si dovrebbero sostituire/ridurre solo variabili libere, o almeno è quello che ho capito dal testo, si possono sostituire pure applicazioni?
Sono confuso dal risultato del mio collega.

Io allora sbagliavo perché al passaggio:

((λb.((λx.λy.xyy)bb))y)
-->beta((λb.((λy.bbyy)))y)

gli portavo entrambe le b pensando fossero un blocco unico…
Logged
Pages: 1 [2]   Go Up
Print
Jump to: