Pages: [1]   Go Down
Print
Author Topic: Esercizio Lamba calcolo 46  (Read 752 times)
0 Members e 1 Utente non registrato stanno visualizzando questa discussione.
Dott.V
Matricola
*
Offline Offline

Posts: 38


« on: 13-06-2017, 20:35:13 »

Buonasera.
Ho provato a portare in forma normale il seguente lambda-termine ottenendo un risultato diverso da quello che potrebbe fornire un lambda-calculator like this http://www.cburch.com/lambda/index.html .

Testo:

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

MIO svolgimento:

((λw.(xw))(λy.(yx)))
x(λy.(yx)){a/y}
x(λa.(ax))[λx.(w(xy))/x]
(λx.wxy)(λa.a(λx.wxy))
w(λa.a(λx.wxy))y
w(λa.a(wyy))
wwyy

Risultato del Lambda Calculator
wxy


Cosa sbaglio?
« Last Edit: 13-06-2017, 20:38:23 by Dott.V » Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.776



WWW
« Reply #1 on: 14-06-2017, 10:20:51 »

C'e' un errore nel passaggio da

x(λa.(ax))[λx.(w(xy))/x]

a

(λx.wxy)(λa.a(λx.wxy))

Scrivere w(xy)  e wxy  NON e' la stessa cosa!

FB
Logged
Dott.V
Matricola
*
Offline Offline

Posts: 38


« Reply #2 on: 14-06-2017, 15:58:40 »

E allora non avevo ben capito come funzionasse lo scope dei lambda-termini. Propongo allora la seguente soluzione:

((λw.(xw))(λy.(yx)))
x(λy.(yx)){a/y}
x(λa.(ax))[λx.(w(xy))/x]
(λx.(w(xy)))(λa.(a(λx.(w(xy)))))
w(xy)
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.776



WWW
« Reply #3 on: 15-06-2017, 19:21:09 »

E' diversa dal lambda-calculator
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.776



WWW
« Reply #4 on: 15-06-2017, 19:22:56 »

E dove sono i passaggi da
(λx.(w(xy)))(λa.(a(λx.(w(xy)))))

a

w(xy)

?
« Last Edit: 15-06-2017, 21:28:18 by Franco Barbanera » Logged
Dott.V
Matricola
*
Offline Offline

Posts: 38


« Reply #5 on: 15-06-2017, 19:28:25 »

(λx.(w(xy)))(λa.(a(λx.(w(xy)))))
(λf.(w(xy)){f/x})(λa.(a(λx.(w(xy))))) //qua passo a λf.M come parametro attuale (λa.(a(λx.(w(xy)))))
w(xy) //ottengo questo in un solo passaggio


Comunque il lambda-calculator mi da come risultato w xy che penso significhi w(xy)
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.776



WWW
« Reply #6 on: 15-06-2017, 21:29:43 »

(λf.(w(xy)){f/x})(λa.(a(λx.(w(xy))))) //qua passo a λf.M come parametro attuale (λa.(a(λx.(w(xy)))))
w(xy) //ottengo questo in un solo passaggio


Incomprensibile.
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.776



WWW
« Reply #7 on: 15-06-2017, 21:42:30 »

Per il lambda calculator, se scrivi xy
lui intende una variabile che si chiama xy.
Se vuoi indicare il termine corrispondente all'applicazione della variabile x alla variabile y
allora devi scrivere x y

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

Posts: 2.776



WWW
« Reply #8 on: 06-07-2017, 13:38:51 »

Sto ancora aspettando la soluzione....

FB
Logged
Dott.V
Matricola
*
Offline Offline

Posts: 38


« Reply #9 on: 20-09-2017, 09:53:09 »

Sto ancora aspettando la soluzione....

FB
Riproviamo da zero. Ho consultato un nuovo lambda-calculator https://www.easycalculation.com/analytical/lambda-calculus.php.

((\w.(xw))(\y.(yx)))[\x.(w(xy))/x]    //per semplicità di lettura ogni lettera identificherà una singola variabile
Per evitare collisioni tra variabili libere e variabili legate effettuo la ridenominazione del lambda-termine che andra a sostituire le x;

\x.(w(xy)){t/x} =α \t.(w(ty))

Adesso effettuo la ridenominazione del lambda-termine principale;
((\w.(xw))(\y.(yx))){l/y, n/w} =α ((\n.(xn))(\l.(lx)))

Procediamo a portare il tutto in forma normale
(\n.(xn))(\l.(lx))
x(\l.(lx))

Adesso effettuo la sostituzione [\t.(w(ty))/x]

x(\l.(lx)) [\t.(w(ty))/x]
\t.w(ty)(\l.l(\t.w(ty)))

Adesso entrambi i lambda-calculator mi fermano a questo punto. Ma perché non è possibile proseguire portandolo nell'ulteriore forma normale:

w(\l.l(\t.w(ty))y)
w(\l.l(w(yy)))
??
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.776



WWW
« Reply #10 on: 27-09-2017, 11:39:53 »

il risultato di questa sostituzione
x(\l.(lx)) [\t.(w(ty))/x]
e'
( \t.w(ty) )(\l.l(\t.w(ty)))

e non
 \t.w(ty)(\l.l(\t.w(ty)))

Infatti, se scrivi
\t.w(ty)(\l.l(\t.w(ty)))
e' come se scrivessi
\t.((w(ty))(\l.l(\t.w(ty))))
Logged
Dott.V
Matricola
*
Offline Offline

Posts: 38


« Reply #11 on: 27-09-2017, 17:09:02 »

il risultato di questa sostituzione
x(\l.(lx)) [\t.(w(ty))/x]
e'
( \t.w(ty) )(\l.l(\t.w(ty)))

e non
 \t.w(ty)(\l.l(\t.w(ty)))

Infatti, se scrivi
\t.w(ty)(\l.l(\t.w(ty)))
e' come se scrivessi
\t.((w(ty))(\l.l(\t.w(ty))))

Ah, ecco perché mi devo fermare. ( \t.w(ty) )(\l.l(\t.w(ty))) è la forma normale.
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.776



WWW
« Reply #12 on: 28-09-2017, 19:15:37 »

Il termine
( \t.w(ty) )(\l.l(\t.w(ty)))
NON e' in forma normale.

Il termine
\t.((w(ty))(\l.l(\t.w(ty))))
si

FB

Logged
Dott.V
Matricola
*
Offline Offline

Posts: 38


« Reply #13 on: 03-10-2017, 17:10:29 »

Sto ancora aspettando la soluzione....

FB
Riproviamo da zero. Ho consultato un nuovo lambda-calculator https://www.easycalculation.com/analytical/lambda-calculus.php.

((\w.(xw))(\y.(yx)))[\x.(w(xy))/x]    //per semplicità di lettura ogni lettera identificherà una singola variabile
Per evitare collisioni tra variabili libere e variabili legate effettuo la ridenominazione del lambda-termine che andra a sostituire le x;

\x.(w(xy)){t/x} =α \t.(w(ty))

Adesso effettuo la ridenominazione del lambda-termine principale;
((\w.(xw))(\y.(yx))){l/y, n/w} =α ((\n.(xn))(\l.(lx)))

Procediamo a portare il tutto in forma normale
(\n.(xn))(\l.(lx))
x(\l.(lx))

Adesso effettuo la sostituzione [\t.(w(ty))/x]

x(\l.(lx)) [\t.(w(ty))/x]
\t.w(ty)(\l.l(\t.w(ty)))

Adesso entrambi i lambda-calculator mi fermano a questo punto. Ma perché non è possibile proseguire portandolo nell'ulteriore forma normale:

w(\l.l(\t.w(ty))y)
w(\l.l(w(yy)))
??
Correggo.

...
...
Adesso effettuo la sostituzione [\t.(w(ty))/x]

x(\l.(lx)) [\t.(w(ty))/x]
(\t.(w(ty)))(\l.(l(\t.(w(ty)))))
(w((\l.(l(\t.(w(ty)))))y))
(w(y(\t.w(ty)))) ->forma normale
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.776



WWW
« Reply #14 on: 04-10-2017, 11:12:33 »

 ok
Logged
Pages: [1]   Go Up
Print
Jump to: