Buongiorno, con un certo ritardo ho corretto i vostri esami della scuola estiva BISS 2005, corso STT. Dovreste avere già ricevuto la lista degli studenti che hanno validato l'esame. In questo mail vi mando alcuni commenti sui vostri esercizi. La soluzione dell'esame si trova online: http://moscova.inria.fr/~zappa/teaching/stt05/bertinoro05.html - Domanda 4, punto 4. Il termine t = (\x.xx)(\x.xx) non è tipabile in nessuno dei sistemi di tipi studiati. È semplice vedere che non è tipabile nè nel sistema di tipi monomorfo, nè nel sistema di tipi polimorfo. Come accennato nell'introduzione dell'esame, il sistema di tipi interesezione che studiamo ha la proprietà di tipare tutti e soltanto i termini fortemente normalizzanti (ossia che non hanno riduzioni infinite). Il termine t non ha forma normale, e pertanto non può essere tipato con il sistema di tipi intersezione proposto. (Uno di voi cita Barendregt e dice che con i tipi intersezione si tipano tutti i lambda-termini. Barendregt però considera le intersezioni di zero tipi, che noi escludiamo.) - Domanda 5. Diversi di voi rispondono alla domanda 5 considerando la riduzione --> (ossia --epsilon--> chiusa per contesti di riduzione). L'esercizio chiedeva di considerare soltanto --epsilon--> (ossia solo la beta-riduzione). Altri considerano le delta-regole, ma il fun-language non contiene delta-regole. - C'è una certa confusione sulla definizione di "type preserving translation". Eccovi la definizione precisa. Sia S un linguaggio tipato, con a_s denotiamo i termini, con t_s i tipi. Sia T un secondo linguaggi tipato, con a_t denotiamo i termini, con t_t i tipi. Sia [[ ]]_a : a_s --> a_t una funzione che traduce termini di S in termini di T, e sia [[ ]]_t : t_s --> t_t una funzione che traduce i tipi di S in tipi di T. La traduzione si estende nel modo ovvio agli ambienti di tipaggio. Si dice che la traduzione [[ ]] preserva i tipi se Gamma |- a_s : t_s implica [[ Gamma ]] |- [[ a_s ]]_s : [[ t_s ]]_t (nel primo giudizio si considera il sistema di tipi di S, nel secondo quello di T). Vi invito a riguardare le risposte che avete dato alle domande 8 e 9. - L'esercizio di programmazione numero 2 aveva una parte volutamente lasciata alla vostra creatività: i termini del linguaggio source non avevano abbastanza informazioni di tipo per chiamare ricorsivamente la funzione translate passando il tipo della sottoespressione. Varie soluzioni erano possibili. Nella correzione ho introdotto esplicitamente un linguaggio intermedio in cui tutte le sottoespressioni sono esplicitamente tipate, la funzione annotate aggiunge a un termine nel linguaggio source le informazioni sui tipi delle sottoespressioni (facile perché le variabili astratte sono esplicitamente tipate), e la tcc è fatta a partire da questa rappresentazione intermedia (come è sempre il caso nei compilatori che propagano i tipi attraverso la compilazione). - Quando risolvete degli esercizi di programmazione, non cambiate arbitrariamente le interfacce delle funzioni richieste (in particolare il tipo della funzione "translate"). Spero che questo esame vi abbia insegnato cosa è una chiusura (grazie allo studente che durante il corso mi ha fatto la domanda per avermi suggerito l'esercizio). Ho alcuni commenti più precisi per alcuni di voi, ve li invierò separatamente. Se avete domande, è il momento di farle. Se passate nelle fredde brughiere del nord (ahem, a Parigi) non esitate a contattarmi, per una discussione informatica o una birra. Amicalmente, Francesco Zappa Nardelli