LTIQ Un Calcolo Lineare per Q#

Il teorema di non duplicazione della meccanica quantistica afferma che uno stato quantistico non possa mai essere duplicato o cancellato. Diversi linguaggi di programmazione quantistici, ovvero basati sui principi della meccanica quantistica, garantiscono a tempo di compilazione, grazie ai sistemi di tipi lineari, che i loro programmi non violino mai il teorema di non duplicazione. Non è questo il caso del linguaggio specifico di dominio Microsoft Q#: l’esecuzione di un programma Q# può portare ad errori a tempo di esecuzione dovuti a violazioni del teorema di non duplicazione causando uno spreco di risorse quantistiche. Per ovviare a questo problema, in questo lavoro di tesi viene formalizzato il core computazionale di Q# introducendo il calcolo fondazionale Linearly Typed Idealized Q# (abbreviato in LTIQ). Dopo aver provvisto LTIQ di una sintassi e una semantica operazionale viene definitio un sistema di tipi lineare per esso. Il risultato principale di questo elaborato, assieme alla definizione del sistema di tipi, è la dimostrazione del teorema di sicurezza rispetto ai tipi (type safety). Da questo segue che in un programma ben tipato nessun dato tipato linearmente verrà duplicato o cancellato durante l’esecuzione del programma. Avendo i dati quantistici tipo lineare, nessun programma ben tipato violerà quindi il teorema di non duplicazione durante la sua esecuzione.