Forum Informatica Unict

LAUREA TRIENNALE (D.M. 270/04) => Fondamenti di Informatica, 9 CFU => Topic started by: Dott.V on 13-06-2017, 20:35:13



Title: Esercizio Lamba calcolo 46
Post by: Dott.V 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?


Title: Re:Esercizio Lamba calcolo 46
Post by: Franco Barbanera 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


Title: Re:Esercizio Lamba calcolo 46
Post by: Dott.V 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)


Title: Re:Esercizio Lamba calcolo 46
Post by: Franco Barbanera on 15-06-2017, 19:21:09
E' diversa dal lambda-calculator


Title: Re:Esercizio Lamba calcolo 46
Post by: Franco Barbanera on 15-06-2017, 19:22:56
E dove sono i passaggi da
(λx.(w(xy)))(λa.(a(λx.(w(xy)))))

a

w(xy)

?


Title: Re:Esercizio Lamba calcolo 46
Post by: Dott.V 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)


Title: Re:Esercizio Lamba calcolo 46
Post by: Franco Barbanera 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.


Title: Re:Esercizio Lamba calcolo 46
Post by: Franco Barbanera 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



Title: Re:Esercizio Lamba calcolo 46
Post by: Franco Barbanera on 06-07-2017, 13:38:51
Sto ancora aspettando la soluzione....

FB


Title: Re:Esercizio Lamba calcolo 46
Post by: Dott.V 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)))
??


Title: Re:Esercizio Lamba calcolo 46
Post by: Franco Barbanera 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))))


Title: Re:Esercizio Lamba calcolo 46
Post by: Dott.V 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.


Title: Re:Esercizio Lamba calcolo 46
Post by: Franco Barbanera 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



Title: Re:Esercizio Lamba calcolo 46
Post by: Dott.V 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


Title: Re:Esercizio Lamba calcolo 46
Post by: Franco Barbanera on 04-10-2017, 11:12:33
 :-OK