tipo

tipo

tipo termine che assume significati diversi in informatica e in logica.

☐ In informatica, con il termine tipo o tipo di dato si indica la caratteristica comune dei valori che possono essere assunti da un certo termine di un linguaggio di programmazione o di un qualsiasi linguaggio formale. Per esempio, se un termine può assumere come valore un numero intero (compreso nei limiti propri dell’automa) allora si dice che il termine in questione è un dato di tipo semplice → integer; se invece il termine può assumere anche valori numerici non interi, allora si tratta di un dato di tipo semplice → real. Oltre ai tipi di dato semplici numerici, esistono altri tipi di dati, anch’essi semplici, ma non numerici perché comprendono lettere, segni di interpunzione ecc.: un tipico esempio è il tipo di dato char (i cui elementi sono caratteri alfanumerici) o il tipo di dato → boolean (che ha due soli elementi, interpretabili come «vero» e «falso»). Vi sono inoltre tipi più complessi (tipi di dato strutturati) quali il tipo vettore o → array, e il → record. Alcuni linguaggi formali sono non tipati (o non tipizzati) poiché i loro termini non hanno tipo. Un esempio di linguaggio siffatto è il → lambda-calcolo puro, i cui termini non sono tipati e possono essere trattati tutti nello stesso modo: si può applicare una variabile x a un termine t creando il termine (x)t o viceversa applicare t a x creando il termine (t)x.

☐ In logica, con il termine teoria dei → tipi si indica il tentativo portato avanti da B. Russell, successivamente in collaborazione con A.N. Whitehead, di apportare una correzione alla teoria ingenua degli → insiemi in modo da metterla al riparo da contraddizioni e antinomie.