Forum Informatica Unict

LAUREA MAGISTRALE => Linguaggi di Programmazione, 9 CFU => Topic started by: andyusa83 on 15-05-2014, 18:57:18



Title: Come "costruire" la base nel λ-calcolo tipato a' la Curry
Post by: andyusa83 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.


Title: Re:Come "costruire" la base nel λ-calcolo tipato a' la Curry
Post by: Franco Barbanera 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


Title: Re:Come "costruire" la base nel λ-calcolo tipato a' la Curry
Post by: andyusa83 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?


Title: Re:Come "costruire" la base nel λ-calcolo tipato a' la Curry
Post by: Franco Barbanera 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


Title: Re:Come "costruire" la base nel λ-calcolo tipato a' la Curry
Post by: andyusa83 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.


Title: Re:Come "costruire" la base nel λ-calcolo tipato a' la Curry
Post by: Franco Barbanera 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


Title: Re:Come "costruire" la base nel λ-calcolo tipato a' la Curry
Post by: andyusa83 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.


Title: Re:Come "costruire" la base nel λ-calcolo tipato a' la Curry
Post by: Franco Barbanera 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


Title: Re:Come "costruire" la base nel λ-calcolo tipato a' la Curry
Post by: andyusa83 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.