Come "costruire" la base nel λ-calcolo tipato a' la Curry

[andyusa83]

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.

[Franco Barbanera]

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

[andyusa83]

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?

[Franco Barbanera]

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

[andyusa83]

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.

[Franco Barbanera]

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

[andyusa83]

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.

[Franco Barbanera]

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

[andyusa83]

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.