Rioli, Alessandro
(2016)

*Coinductive Techniques on a Linear Quantum λ-Calculus*, [Dissertation thesis], Alma Mater Studiorum Università di Bologna.
Dottorato di ricerca in

Informatica, 27 Ciclo. DOI 10.6092/unibo/amsdottorato/7341.

Documenti full-text disponibili:

## Abstract

In this thesis, it is examined the issue of equivalence between linear terms in higher order languages, that is, in languages which allow to use functions as variables, and where variables which appear in the terms must be used exactly once.
The work is developed focusing on the bisimulation method, with the purpose to compare this technique with that which has become the standard for the comparison between the terms of a language, i.e. the context equivalence.
The thesis is divided into three parts: in the first one, the introduction of the bisimulation and context equivalence techniques takes place within a deterministic linear and typed language.
In the second part, the same techniques are reformulated for a language that, while preserving the linearity, loses the deterministic connotation, allowing the terms to evaluate to a set of values each one having a certain probability to appear in the end of calculation. In the last part, a quantum language is examined, discussing the advantages of quantum computation, which allows to speed-up many of the algorithms of computation. Here one gives the concept of quantum program, which is inextricably linked to the (quantum) register where the qubits used in the computation are stored, entailing a more complex notion of equivalence between terms.
The techniques to demonstrate that bisimulation is a congruence are not standard and have been used for the first time by Howe for untyped languages: within the thesis, one shows that bisimulation is a congruence in all considered languages but it coincides with the context equivalence relation only for the deterministic one. Indeed, extending the techniques already used by Howe to the probabilistic and quantum environment, it is shown, as non trivial result, that in probabilistic and quantum linear languages the bisimulation is contained in context equivalence relation.

Abstract

In this thesis, it is examined the issue of equivalence between linear terms in higher order languages, that is, in languages which allow to use functions as variables, and where variables which appear in the terms must be used exactly once.
The work is developed focusing on the bisimulation method, with the purpose to compare this technique with that which has become the standard for the comparison between the terms of a language, i.e. the context equivalence.
The thesis is divided into three parts: in the first one, the introduction of the bisimulation and context equivalence techniques takes place within a deterministic linear and typed language.
In the second part, the same techniques are reformulated for a language that, while preserving the linearity, loses the deterministic connotation, allowing the terms to evaluate to a set of values each one having a certain probability to appear in the end of calculation. In the last part, a quantum language is examined, discussing the advantages of quantum computation, which allows to speed-up many of the algorithms of computation. Here one gives the concept of quantum program, which is inextricably linked to the (quantum) register where the qubits used in the computation are stored, entailing a more complex notion of equivalence between terms.
The techniques to demonstrate that bisimulation is a congruence are not standard and have been used for the first time by Howe for untyped languages: within the thesis, one shows that bisimulation is a congruence in all considered languages but it coincides with the context equivalence relation only for the deterministic one. Indeed, extending the techniques already used by Howe to the probabilistic and quantum environment, it is shown, as non trivial result, that in probabilistic and quantum linear languages the bisimulation is contained in context equivalence relation.

Tipologia del documento

Tesi di dottorato

Autore

Rioli, Alessandro

Supervisore

Dottorato di ricerca

Scuola di dottorato

Scienze e ingegneria dell'informazione

Ciclo

27

Coordinatore

Settore disciplinare

Settore concorsuale

Parole chiave

λ-Calculus, Quantum computing, Bisimulation, Context equivalence, Howe's relation.

URN:NBN

DOI

10.6092/unibo/amsdottorato/7341

Data di discussione

13 Maggio 2016

URI

## Altri metadati

Tipologia del documento

Tesi di dottorato

Autore

Rioli, Alessandro

Supervisore

Dottorato di ricerca

Scuola di dottorato

Scienze e ingegneria dell'informazione

Ciclo

27

Coordinatore

Settore disciplinare

Settore concorsuale

Parole chiave

λ-Calculus, Quantum computing, Bisimulation, Context equivalence, Howe's relation.

URN:NBN

DOI

10.6092/unibo/amsdottorato/7341

Data di discussione

13 Maggio 2016

URI

## Statistica sui download

Gestione del documento: