Guerra, Andrea
(2021)
LTIQ Un Calcolo Lineare per Q#.
[Laurea magistrale], Università di Bologna, Corso di Studio in
Informatica [LM-DM270]
Documenti full-text disponibili:
![[img]](http://amslaurea.unibo.it/style/images/fileicons/application_pdf.png) |
Documento PDF (Thesis)
Disponibile con Licenza: Salvo eventuali più ampie autorizzazioni dell'autore, la tesi può essere liberamente consultata e può essere effettuato il salvataggio e la stampa di una copia per fini strettamente personali di studio, di ricerca e di insegnamento, con espresso divieto di qualunque utilizzo direttamente o indirettamente commerciale. Ogni altro diritto sul materiale è riservato
Download (344kB)
|
Abstract
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.
Abstract
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.
Tipologia del documento
Tesi di laurea
(Laurea magistrale)
Autore della tesi
Guerra, Andrea
Relatore della tesi
Correlatore della tesi
Scuola
Corso di studio
Indirizzo
CURRICULUM A: TECNICHE DEL SOFTWARE
Ordinamento Cds
DM270
Parole chiave
Q#,sistemi di tipi,calcolo fondazionale,semantica operazionale,computazione quantistica,sistemi di tipi lineari,LTIQ
Data di discussione della Tesi
18 Marzo 2021
URI
Altri metadati
Tipologia del documento
Tesi di laurea
(NON SPECIFICATO)
Autore della tesi
Guerra, Andrea
Relatore della tesi
Correlatore della tesi
Scuola
Corso di studio
Indirizzo
CURRICULUM A: TECNICHE DEL SOFTWARE
Ordinamento Cds
DM270
Parole chiave
Q#,sistemi di tipi,calcolo fondazionale,semantica operazionale,computazione quantistica,sistemi di tipi lineari,LTIQ
Data di discussione della Tesi
18 Marzo 2021
URI
Statistica sui download
Gestione del documento: