Pages: 1 2 3 [4]   Go Down
Print
Author Topic: Aiuto esercizio Lambda-calcolo  (Read 10112 times)
0 Members e 1 Utente non registrato stanno visualizzando questa discussione.
golvellius
Apprendista Forumista
**
Offline Offline

Posts: 124


« Reply #45 on: 16-04-2013, 10:27:01 »

Ti ringrazio sei stato gentilissimo.
I miei unici dubbi riguardano in pratica la parte dove si effettua la sostituzione e l'unione delle basi, che ancora non ho ben chiari (ma non a causa tua, tu sei stato chiarissimo  ;-) ) , devo applicarmi un altro po e ne verrò fuori :-)

Grazie mille.
Logged
golvellius
Apprendista Forumista
**
Offline Offline

Posts: 124


« Reply #46 on: 16-04-2013, 12:20:25 »

Solo un piccolo chiarimento, se avessimo avuto entrambe le basi non nulle, come avrei dovuto procedere per effettuare l'unione tra le due basi?

Logged
golvellius
Apprendista Forumista
**
Offline Offline

Posts: 124


« Reply #47 on: 16-04-2013, 14:53:48 »

Ho iniziato a esercitarmi con qualche altro esercizio dello stesso tipo, se qualcuno ha voglia, tempo e pazienza potrebbe gentilmente dirmi se procedo bene o sto sbagliando?

\x.(\y.x) voglio trovare la coppia principale

Caso \x.M

Trovo il tipo più generale di M
    
   \y.x

determino prima

PP(x) = <{x:a}, a>

x è una variabile libera
pertanto

PP(\y.x)= <{0}, a-->a>

Se non dico fesserie (concedetemele sono agli inizi :-) )

abbiamo \x.(\y.x) con x variabile legata

quindi

PP(\x.(\y.x))= <{0}, b-->(a-->a)>


Ha senso tutto quello che ho scritto? :-)

Grazie e buona giornata.
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 3.072



WWW
« Reply #48 on: 16-04-2013, 17:53:31 »

x è una variabile libera
pertanto

PP(\y.x)= <{0}, a-->a>


NO, l'algoritmo ti chiede di controllare se la variabile che astrai sia libera nel corpo
dell'astrazione.

FB
Logged
golvellius
Apprendista Forumista
**
Offline Offline

Posts: 124


« Reply #49 on: 17-04-2013, 10:52:16 »

x è una variabile libera
pertanto

PP(\y.x)= <{0}, a-->a>


NO, l'algoritmo ti chiede di controllare se la variabile che astrai sia libera nel corpo
dell'astrazione.

FB


Grazie per la risposta professore.

Ammetto di essermi un po' arenato da ieri sera :-(
C'è qualche piccolo meccanismo che non mi è chiaro e non mi fa venir fuori da questo esercizio.

Vediamo se il ragionamento in parte fila:

\x.(\y.x)

utilizzo il caso b) dell'algoritmo

Consideriamo un'astrazione \x.M devo trovare la tipizzazione più generale per M (dagli appunti utilizzando ricorsivamente l'algoritmo stesso)
if pp(M) = <P,p> then...

quindi cerco la tipizzazione più generale di M ovvero di \y.x 
la posso trovare applicando a sua volta la b) dell'algoritmo a \y.x?


in pratica considero la x di \y.x come termine M
 poiché PP(x) = < {x:a},a>
x in questo caso la considero libera, quindi caso i) del punto b)
PP(\y.x)= <{0},a-->a>


questo mi ha permesso di trovarmi la tipizzazione più generale di M in \x.(\y.x)

e adesso pensavo di applicare nuovamente la b avendo trovato già il tipo più generale di \y.x che è la mia M in \x.(\y.x)

Dal suo commento però capisco di stare sbagliando quando dico che x è libera, solo che non riesco a raccapezzarmi, potrebbe gentilmente darmi qualche altro suggerimento e correzione?

Grazie e buonagiornata.
Logged
Acicatena86
Apprendista Forumista
**
Offline Offline

Gender: Male
Posts: 404


See full me now who neon


« Reply #50 on: 17-04-2013, 11:24:15 »

Sbagli , (secondo me  Smiley ) qui

"in pratica considero la x di \y.x come termine M
 poiché PP(x) = < {x:a},a>
x in questo caso la considero libera, quindi caso i) del punto b)
PP(\y.x)= <{0},a-->a> "


Quando fai  PP(\y.x) , ottieni <y:b, b-->a> cioè devi dare un tipo più semplice a y.  Tu togli l'ipotesi sul tipo di x, ma devi mettere quella sul tipo di y.

Comunque spero di non aver detto una cavolata.
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 3.072



WWW
« Reply #51 on: 17-04-2013, 13:57:46 »

Sbagli , (secondo me  Smiley ) qui

"in pratica considero la x di \y.x come termine M
 poiché PP(x) = < {x:a},a>
x in questo caso la considero libera, quindi caso i) del punto b)
PP(\y.x)= <{0},a-->a> "


Quando fai  PP(\y.x) , ottieni <y:b, b-->a> cioè devi dare un tipo più semplice a y.  Tu togli l'ipotesi sul tipo di x, ma devi mettere quella sul tipo di y.

Comunque spero di non aver detto una cavolata.

l'errore e' infatti propio li'.

FB
Logged
golvellius
Apprendista Forumista
**
Offline Offline

Posts: 124


« Reply #52 on: 17-04-2013, 15:49:16 »

Grazie mille davvero, adesso è tutto molto più chiaro :-)

Logged
Joe
Apprendista Forumista
**
Offline Offline

Posts: 492


« Reply #53 on: 18-05-2013, 12:31:32 »

Salve a tutti, ho rifatto i seguenti esercizi, vi chiedo se sono corretti ed eventualmente quali correzioni devo apportare. (Tra parentesi tonde riporto lo stato della base B). Grazie infinite per le risposte.

Esercizio 3

Dare una derivazione formale nel sistema di assegnamento di tipi alla Curry per il seguente giudizio:
|--  \xy.yx :  a --> (a-->b) --> b

Soluzione

B|-- y : a -> b B|-- x : a                                    (B = {y : a -> b , x : a})
-------------
        B|-- yx : b


B|-- y : a -> b B|-- yx : b                                    (B = {x : a})
----------------
    B|-- \lambda y.yx : (a -> b) -> b

B|-- x : a B|-- \lambda y.yx : (a -> b) -> b                                    (B = \phi)
------------------
  \phi|-- \lambda x.\lambda y.yx : a -> (a -> b) -> b


Esercizio 3.5

Dimostrare formalmente che il seguente giudizio e' valido
z: b-->a |- \xy.x(zy) : (a-->c) --> (b-->c)

Soluzione

B|-- z : b -> a B|-- y : b                                    (B = {z : b -> a , y : b})
-------------
        B|-- zy : a


B, x : a -> c |-- zy : a                                    (B = {z : b -> a , y : b, x : a -> c})
-----------
    B|-- x(zy) : c

B|-- y : b B|-- x(zy) : c                                    (B = {z : b -> a , x : a -> c})
-------------
  B |-- \lambda y.x(zy) : b -> c


B|-- x : a -> c B|-- \lambda y.x(zy) : b -> c                                    (B = {z : b -> a})
----------------------
  B |-- \lambda x.\lambda y.x(zy) : (a -> c) -> (b -> c)


Esercizio 11


Fornire una derivazione nel sistema di tipi a' la Curry per il termine
\xz.((\y.z)(xz))

Soluzione


B|-- x : a -> b B|-- z : a                                    (B = {x : a -> b , z : a})
-------------
        B|-- xz : b


B, y : c |-- z : a                                    (B = {x : a -> b , z : a, y : c})
-----------
    B|-- \lambda y.z : c -> a

B|-- \lambda y.z : c -> a B|-- xz : b                                    (B = {x : a -> b , z : a})
-------------
  B |-- (\lambda y.z)(xz) : a


B|-- z : a B|-- (\lambda y.z)(xz) : a                                    (B = {x : a -> b})
----------------------
  B |-- \lambda z.((\lambda y.z)(xz)) : a -> a

B|-- x : a -> b B|-- \lambda z.((\lambda y.z)(xz)) : a -> a                                    (B = \phi)
------------------------
  \phi |-- \lambda x.\lambda z.((\lambda y.z)(xz)) : (a -> b) -> (a -> a)


Esercizio 12

Fornire una derivazione nel sistema di tipi a' la Curry per il termine
\x.((\y.z)(xz))

Soluzione

B|-- x : a -> b B|-- z : a                                    (B = {x : a -> b , z : a})
-------------
        B|-- xz : b


B, y : c |-- z : a                                    (B = {x : a -> b , z : a, y : c})
-----------
    B|-- \lambda y.z : c -> a

B|-- \lambda y.z : c -> a B|-- xz : b                                    (B = {x : a -> b , z : a})
-------------
  B |-- (\lambda y.z)(xz) : a


B|-- x : a -> b B|-- (\lambda y.z)(xz) : a                                    (B = {z : a})
------------------------
  B|-- \lambda x.((\lambda y.z)(xz)) : (a -> b) -> a
Logged
Acicatena86
Apprendista Forumista
**
Offline Offline

Gender: Male
Posts: 404


See full me now who neon


« Reply #54 on: 18-05-2013, 14:31:34 »

Negli ultimi due commetti un errore. La y deve avere il tipo di (xz) cioè b , se metti che ha tipo c non puoi applicare subito dopo la regola dell' arrow elimination (tu la applichi in maniera errata).
Infatti la regola dice

    B|- M:\sigma\rightarrow\tau B|-N:\sigma
-------------
     B|- MN:\tau

Per il resto ottengo i tuoi risultati, quindi dovrebbero essere corretti  yoh
Logged
Joe
Apprendista Forumista
**
Offline Offline

Posts: 492


« Reply #55 on: 18-05-2013, 14:39:05 »

Negli ultimi due commetti un errore. La y deve avere il tipo di (xz) cioè b , se metti che ha tipo c non puoi applicare subito dopo la regola dell' arrow elimination (tu la applichi in maniera errata).
Infatti la regola dice

    B|- M:\sigma\rightarrow\tau B|-N:\sigma
-------------
     B|- MN:\tau

Per il resto ottengo i tuoi risultati, quindi dovrebbero essere corretti  yoh

Adesso?

Esercizio 11



B|-- x : a -> b B|-- z : a                                    (B = {x : a -> b , z : a})
-------------
        B|-- xz : b


B, y : b |-- z : a                                    (B = {x : a -> b , z : a, y : b})
-----------
    B|-- \lambda y.z : b -> a

B|-- \lambda y.z : b -> a B|-- xz : b                                    (B = {x : a -> b , z : a})
-------------
  B |-- (\lambda y.z)(xz) : a


B|-- z : a B|-- (\lambda y.z)(xz) : a                                    (B = {x : a -> b})
----------------------
  B |-- \lambda z.((\lambda y.z)(xz)) : a -> a

B|-- x : a -> b B|-- \lambda z.((\lambda y.z)(xz)) : a -> a                                    (B = \phi)
------------------------
  \phi |-- \lambda x.\lambda z.((\lambda y.z)(xz)) : (a -> b) -> (a -> a)


Esercizio 12


B|-- x : a -> b B|-- z : a                                    (B = {x : a -> b , z : a})
-------------
        B|-- xz : b


B, y : b |-- z : a                                    (B = {x : a -> b , z : a, y : b})
-----------
    B|-- \lambda y.z : b -> a

B|-- \lambda y.z : b -> a B|-- xz : b                                    (B = {x : a -> b , z : a})
-------------
  B |-- (\lambda y.z)(xz) : a


B|-- x : a -> b B|-- (\lambda y.z)(xz) : a                                    (B = {z : a})
------------------------
  B|-- \lambda x.((\lambda y.z)(xz)) : (a -> b) -> a
Logged
Acicatena86
Apprendista Forumista
**
Offline Offline

Gender: Male
Posts: 404


See full me now who neon


« Reply #56 on: 18-05-2013, 15:42:53 »

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