Pages: [1]   Go Down
Print
Author Topic: Dubbio su ese Lambda-Calcolo  (Read 840 times)
0 Members e 1 Utente non registrato stanno visualizzando questa discussione.
Frugalitas
Matricola
*
Offline Offline

Posts: 7


« on: 22-02-2017, 16:50:06 »

Buonasera a tutti! Svolgendo l'esercizio 102 mi è sorto un dubbio relativo alla forma normale di un lambda - termine .
Riporto per comodità l'esercizio di seguito:

Calcolare la forma normale (mostrando la computazione eseguita) del lambda-termine
and T T
dove
and e' λab.abF
T e' λxy.x
F e' λxy.y

Non ho incontrato nessuna difficoltà nel risolverlo e confrontando la mia soluzione con quella proposta dal prof, mi sono accorto che era corretta. Il dubbio è sorto solo dopo aver dato in pasto l'esercizio al secondo risolutore che il prof ha messo a disposizione nella pagina del corso. L'output del programma applicando qualsiasi metodo di valutazione è sempre lo stesso (come tra l'altro è giusto che sia) ed è il seguente :\y.y. Peccato che questo non corrisponda ne con la mia soluzione ne tanto meno con quella del prof, ovvero λxy.x. A questo mistero ci sono solo due possibili soluzioni o quella proposta sia da noi che dal programma non è la forma normale del l-termine oppure o sbagliamo noi o sbaglia il programma. Così sono andato a riguardarmi la definizione di redex, ovvero redesso, e reduct ovvero, ridotto. Un termine è in forma normale se non è possibile applicare ulteriori passi di B-riduzione, quindi se, e qui traduco dal testo [PS], non è possibile trovare all'interno della l-espressione ulteriori redessi da sostituire con i corrispettivi ridotti.
Un redex di conseguenza è una particolare stuttura sintattica caratterizzata dalla presenza di un' applicazione di una l-astrazione, quindi una beta riduzione è una particolare applicazione che ha come operando destro un'applicazione di una l-astrazione e come operando sinistro un qualsiasi lambda termine.
A questo punto se consideriamo (\xy.x) un redex e (\xy.x)(nulla) una B-riduzione otteniamo \y e quindi niente , stesso discorso vale per \y.y quindi le due soluzioni in questo caso sarebbero entrambe corrette. Questo però cozza con la definizione di B-riduzione infatti nulla non è un lambda termine.
Se invece consideriamo (\xy.x) e (\y.y) due forme normali contestiamo la validità del teorema di Church-Rosser(mai sia).  
Spero di non aver detto troppe cose oscene e se così dovesse essere mi scuso in anticipo.
Colgo l'occasione per far notare che il programma sopra citato non digerisce (o meglio calcola male) le espressioni di questo tipo (\x.xy)(\z.zi) , per ottenere una corretta valutazione è sufficiente "staccare" le variabili che seguono il punto.

Grazie in anticipo per la risposta.
« Last Edit: 23-02-2017, 23:04:20 by Franco Barbanera » Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.779



WWW
« Reply #1 on: 22-02-2017, 22:04:17 »

 
Quote
particolare applicazione che ha come operando destro un'applicazione di una l-astrazione e come operando sinistro un qualsiasi lambda termine.

Come operando sinistro una lambda-astrazione e come  operando destro un qualsiasi lambda termine
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.779



WWW
« Reply #2 on: 22-02-2017, 22:06:04 »

Quote
se consideriamo (\xy.x) un redex
(\xy.x) NON e' un redex

(\xy.x) e' un modo compatto di indicare (\x.(\y.x))
cioe' una lambda-astrazione il cui corpo e' una lambda-astrazione.


Quote
e (\xy.x)(nulla) una B-riduzione otteniamo \y

Cos'e' "nulla"??  sicuramente, come dici tu, non e' un lambda-termine.
\y inoltre NON e' un lambda termine.
« Last Edit: 22-02-2017, 22:08:15 by Franco Barbanera » Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.779



WWW
« Reply #3 on: 22-02-2017, 22:09:26 »

Quote
Spero di non aver detto troppe cose oscene

Beh... qualcuna si...   

Ma tra di noi non ci scandalizziamo. 
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.779



WWW
« Reply #4 on: 22-02-2017, 22:11:12 »

Mi sembra di aver indicato in qualche punto del programma (o in qualche esercizio)
che il valutatore di lambda-termini ha dei bug.
Non sapevo pero' che "cannasse" anche una espressione relativamente semplice
come quella da te indicata.

Logged
Frugalitas
Matricola
*
Offline Offline

Posts: 7


« Reply #5 on: 23-02-2017, 14:28:03 »

Ne sono consapevole ma è un rischio che devo correre. Per quanto riguarda la definizione di B-riduzione non ho riletto il messaggio e deve essermi sfuggito il fatto di aver invertito gli operandi. Quindi nel caso in questione un redex è \x.M dove M=\y.g  e l'altro è M giusto?? un l-termine \x.x è in forma normale ? L'ho svolto correttamente così??

((\ab.ab)(\xy.y))( (\xy.x)(\xy.x) ) ->B
( (\ab.ab)(\xy.y) )(\y.\xy.x) ->B
( (\b. (\y.\xy.x) b )(\y.y) ->B
( (\y.\xy.x )(\y.y) ->B
\xy.x

Sol. programma:

(λab.a b) (λxy.y) ((λxy.x) (λxy.x)))
→((λb.(λxy.y) b) ((λxy.x) (λxy.x)))
→((λb.(λxy.y) b) (λyxy.x))
→((λxy.y) (λyxy.x))
→λy.y

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

Posts: 2.779



WWW
« Reply #6 on: 23-02-2017, 14:34:49 »

 
Quote
un redex è \x.M dove M=\y.g  e l'altro è M giusto??

A parte che non e' la definizione di redex,
e' una frase priva di senso.

Dove hai studiato la definizione di redex?

FB
Logged
Frugalitas
Matricola
*
Offline Offline

Posts: 7


« Reply #7 on: 23-02-2017, 14:55:18 »

A term of the form (λx.M)N, which consists of a lambda
abstraction applied to another term, is called a β-redex.
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.779



WWW
« Reply #8 on: 23-02-2017, 15:15:02 »

A term of the form (λx.M)N, which consists of a lambda
abstraction applied to another term, is called a β-redex.

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

Posts: 2.779



WWW
« Reply #9 on: 23-02-2017, 15:17:07 »

Quote
((\ab.ab)(\xy.y))( (\xy.x)(\xy.x) ) ->B ( (\ab.ab)(\xy.y) )(\y.\xy.x)

Se scriviamo

and T T

le parentesi implicite sono

((and T) T)

e NON

(and (T T))
Logged
Frugalitas
Matricola
*
Offline Offline

Posts: 7


« Reply #10 on: 23-02-2017, 15:51:42 »

Grazie mille adesso mi è chiaro.
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 2.779



WWW
« Reply #11 on: 23-02-2017, 21:20:50 »

Il problema del valutatore automatico era dovuto alle parentesi errate?

FB
Logged
Frugalitas
Matricola
*
Offline Offline

Posts: 7


« Reply #12 on: 24-02-2017, 16:20:45 »

Si . L'unico problema si verifica con le l-astrazioni che presentano nel loro body più di una variabile. Per esempio in \x.yx  yx vengono  considerate dal programma come un un'unica variabile. Per una valutazione corretta bisogna scrivere (\x.y x).
« Last Edit: 24-02-2017, 16:33:00 by Frugalitas » Logged
Pages: [1]   Go Up
Print
Jump to: