Pages: [1]   Go Down
Print
Author Topic: Come "costruire" la base nel λ-calcolo tipato a' la Curry  (Read 1909 times)
0 Members e 1 Utente non registrato stanno visualizzando questa discussione.
andyusa83
Apprendista Forumista
**
Offline Offline

Gender: Male
Posts: 232



« on: 15-05-2014, 18:57:18 »

Salve a tutti,
sto cercando di svolgere esercizi del tipo:
Code:
Fornire una derivazione nel sistema di tipi a' la Curry per il termine
λbc.((λy.c)(bc))

C'è la soluzione per l'esercizio indicato (n° 11) ma non riesco a capire come vengono "costruite" le basi da cui partire per dare i giudizi sui vari sottotermini. Ad esempio la soluzione inizia così:
Code:
b:t1->t2,c:t1, y:t2 |- c:t1      b:t1->t2,c:t1 |- b:t1->t2   b: t1->t2, c: t1 |- c: t1
------------------------------    -------------------------------------------------------
b:t1->t2, c:t1 |- λy.c:t2->t1                b: t1->t2, c: t1 |- (bc): t2
e i passaggi sono banali ma come si determinano le basi? Ad occhio? (Non penso proprio.)

E poi, perché la b compare nella base a sinistra nonostante non sia necessaria all'inizio mentre la y non compare a destra? È solo una scelta arbitraria per averla più avanti quando si dovrà dare un giudizio sul termine più esterno?

Ringrazio anticipatamente chiunque risponda.
Saluti.
« Last Edit: 15-05-2014, 19:01:45 by andyusa83 » Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 3.062



WWW
« Reply #1 on: 16-05-2014, 14:53:27 »

Quote
E poi, perché la b compare nella base a sinistra nonostante non sia necessaria all'inizio mentre la y non compare a destra? È solo una scelta arbitraria per averla più avanti quando si dovrà dare un giudizio sul termine più esterno?

Si.

FB
Logged
andyusa83
Apprendista Forumista
**
Offline Offline

Gender: Male
Posts: 232



« Reply #2 on: 16-05-2014, 16:53:30 »

Quote
E poi, perché la b compare nella base a sinistra nonostante non sia necessaria all'inizio mentre la y non compare a destra? È solo una scelta arbitraria per averla più avanti quando si dovrà dare un giudizio sul termine più esterno?

Si.

FB

Grazie, professore, ma tornano alla questione principale, come faccio a determinare le basi di partenza?
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 3.062



WWW
« Reply #3 on: 19-05-2014, 17:33:53 »

Nelle basi di partenza debbono esserci le variabili libere del termine finale
piu' quelle che verranno via via legate nei punti in cui si utilizzera' la regola
di (--> I).

FB
Logged
andyusa83
Apprendista Forumista
**
Offline Offline

Gender: Male
Posts: 232



« Reply #4 on: 19-05-2014, 21:57:32 »

Nelle basi di partenza debbono esserci le variabili libere del termine finale
piu' quelle che verranno via via legate nei punti in cui si utilizzera' la regola
di (--> I).

FB

Ma come si stabiliscono i tipi delle variabili (libere o legate che siano) da mettere nelle basi iniziali? È questo che non riesco a capire.
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 3.062



WWW
« Reply #5 on: 20-05-2014, 10:52:22 »

Se segui pedissequamente l'algoritmo pp, e' lui che le costruisce man mano.
Ma per termini semplici si puo' ovviamente fare ad occhio.
Per esempio, se il termine e' xyz e' ovvio che x deve avere come tipo una freccia
che ha come codominio una freccia.
Quindi occorre (cosa per cui si fanno gli esercizi) quel minimo di dimestichezza
con il sistema di assegnamento di tipi per riuscire a capire quali tipi utilizzare.

FB
Logged
andyusa83
Apprendista Forumista
**
Offline Offline

Gender: Male
Posts: 232



« Reply #6 on: 21-05-2014, 17:48:37 »

Se segui pedissequamente l'algoritmo pp, e' lui che le costruisce man mano.
Ma per termini semplici si puo' ovviamente fare ad occhio.
Per esempio, se il termine e' xyz e' ovvio che x deve avere come tipo una freccia
che ha come codominio una freccia.
Quindi occorre (cosa per cui si fanno gli esercizi) quel minimo di dimestichezza
con il sistema di assegnamento di tipi per riuscire a capire quali tipi utilizzare.

FB

Grazie Prof, ho applicato l'algoritmo pp (sul quale tra l'altro ho alcuni dubbi) ma continuo a non capire: non si dovrebbe iniziare con tipi semplici per tutte le variabili e via via eliminare dalla base quelle che si legano e assegnare i tipi alle varie applicazioni e lambda-astrazioni che si presentano? Lo chiedo perché nella soluzione dell'esempio citato si parte già con un tipo freccia per la variabile b: t1->t2.
Mi sembra strano infatti alla fine il risultato proposto è: (t1->t2)->t1->t1, quando ad occhio, considerando che il termine che il termine λbc.((λy.c)(bc)) è riducibile a λbc.c, dovrebbe venire t2->t1->t1, o una sua sostituzione.
Sicuramente la soluzione proposta è giusta e mi sta sfuggendo qualcosa ma al momento non capisco cosa.
Logged
Franco Barbanera
Moderator
Forumista Eroico
*****
Offline Offline

Posts: 3.062



WWW
« Reply #7 on: 22-05-2014, 15:12:43 »

L'esercizio chiede il tipo principale di
λbc.((λy.c)(bc))
NON di
λbc.c

Nel termine
λbc.((λy.c)(bc))
il tipo del dominio (il tipo di b) deve essere per forza una freccia,
poiche' all'interno del termine la variabile b viene applicata a c
e questo si puo' fare solo se b ha un tipo freccia.

FB
Logged
andyusa83
Apprendista Forumista
**
Offline Offline

Gender: Male
Posts: 232



« Reply #8 on: 22-05-2014, 23:05:42 »

L'esercizio chiede il tipo principale di
λbc.((λy.c)(bc))
NON di
λbc.c

Nel termine
λbc.((λy.c)(bc))
il tipo del dominio (il tipo di b) deve essere per forza una freccia,
poiche' all'interno del termine la variabile b viene applicata a c
e questo si puo' fare solo se b ha un tipo freccia.

FB

Grazie per il chiarimento, Prof. Adesso penso di aver capito.
Saluti.
Logged
Pages: [1]   Go Up
Print
Jump to: