Linguaggi di Programmazione I: Paradigmi (A.A. 2002-3)

Regolamento del torneo dei tipi

1. Ciascun contendente consegna all’avversario un foglio di carta con sopra scritto in chiara calligrafia un termine chiuso (ovvero senza variabili libere) del seguente sottoinsieme di ML:

M ::= k | x | fn x ⇒ M | M N | let x = M in N

dove la metavariabile x denota una generica variabile e k una generica costante intera o booleana (ovviamente il termine può contenere più variabili e costanti diverse). L’albero di sintassi astratta del termine deve avere al più 20 nodi. Attenzione: 20 nodi in tutto, non 20 foglie! Ad esempio, l’albero sintattico di

let x = fn x ⇒ fn y ⇒ yx in fn y ⇒ x y x

ha 16 nodi. Si assume che ciascun contendente creda nella tipabilità del termine che consegna all’avversario. Il foglio deve essere piegato in modo che il termine non sia immediatamente visibile.

2. Si fa: uno-due-tre-via!. Al via i contendenti leggono il foglio che gli ha dato l’avversario. In assoluto silenzio ciascun contendente tenta di trovare il tipo principale del termine consegnatogli (un tipo derivabile per quel termine, ma non principale, non verrà considerato corretto). Dopo aver scritto la risposta sul foglio, dice stop! L’altro contendente deve interrompersi. La risposta può cosistere in un tipo σ, oppure nella dichiarazione: nessun tipo! oppure troppi nodi!

3. Il contendente che ha detto stop! (chiamiamolo A) legge la sua risposta. L’altro contendente (B) può: i) confermare la risposta di A, nel qual caso A vince l’incontro; oppure, ii) contestare la risposta di A. A questo punto A può chiedere: e allora qual è la risposta giusta? B deve in tal caso dichiarare ciò che lui crede essere il tipo principale del termine consegnato ad A (oppure, se A ha protestato per i troppi nodi, dimostrare che il suo termine ha dimensioni regolamentari). Se lo fa correttamente vince B (anche se non è riuscito a tipare il termine di A); se invece B dichiara a sua volta un tipo sbagliato (per il termine scritto da lui stesso!), allora vince A con ludibrio per l’avversario (anche se la prima risposta di A era sbagliata!).