Linguagens de Programação Quântica Juliana Vizzotto e Antonio Costa

Prévia do material em texto

Linguagens de Programac¸a˜o Quaˆntica: Um
Apanhado Geral
Juliana Kaizer Vizzotto
ESIN/UCPel
Antoˆnio Carlos da Rocha Costa
PPGINF/UCPel
10 Workshop-Escola de Computac¸a˜o e Informac¸a˜o Quaˆntica
Outubro 2006
Roteiro
Motivac¸a˜o
Arquiteturas para Computac¸a˜o Quaˆntica
Propriedades dos dados quaˆnticos
Linguagens com dados quaˆnticos e controle cla´ssico
QCL - Bernhard O¨mer, 1998
QPL - Peter Selinger, 2004
Propriedades do controle quaˆntico
Linguagens com dados e controle quaˆnticos
QML - Altenkirch e Grattage, 2005
QHaskell - Vizzotto e Rocha Costa, 2006
Motivac¸a˜o I - Computac¸a˜o Quaˆntica
Computac¸a˜o quaˆntica e´ uma a´rea jovem!
(Feynman & Benioff, 1982) - Sistema quaˆntico pode ser
utilizado para executar computac¸o˜es
(Deutsch, 1985) - Ma´quina de Turing quaˆntica
(Shor, 1994) - Algoritmo quaˆntico para fatorac¸a˜o de nu´meros
inteiros
(Grover, 1996) - Algoritmo quaˆntico para procura
1. Evideˆncia que computadores quaˆnticos podem realmente
executar algumas tarefas mais eficientemente que os computadores
cla´ssicos!
2. Desenvolvimento de esquemas experimentais para execuc¸a˜o de
tais algoritmos!
Motivac¸a˜o II - Programac¸a˜o Quaˆntica
Programac¸a˜o quaˆntica → Linkar 1. e 2.
Estudar algoritmos quaˆnticos do ponto de vista de programac¸a˜o
(Knill, 1996) - primeira proposta de pseudo-co´digo para
programac¸a˜o quaˆntica
Programac¸a˜o quaˆntica:
Compreensa˜o das estruturas de dados e controle quaˆnticos
Entendimento da lo´gica de programac¸a˜o quaˆntica
Impulsionar o desenvolvimento de algoritmos quaˆnticos
Motivac¸a˜o III - Programac¸a˜o Quaˆntica
Mesmo que a implementac¸a˜o de computadores quaˆnticos ainda
seja muito limitada: poucos qubits em laborato´rios!
Acredita-se que a pesquisa na a´rea de linguagens de
programac¸a˜o quaˆntica e´ consideravelmente importante!
tanto para o desenvolvimento de algoritmos
quando para fundamentos de linguagens quaˆnticas
Ale´m disso:
Em computac¸a˜o cla´ssica o trabalho em linguagens de
programac¸a˜o e´ datado va´rios anos antes do desenvolvimento
de dispositivos computacionais pra´ticos na de´cada de 50.
Church, 1936 - Ca´lculo lambda
Turing, 1936 - Ma´quina de Turing Universal
Arquiteturas para Programac¸a˜o Quaˆntica
(Knill, 1996): QRAM - Dados quaˆnticos e controle cla´ssico
...
representacao fisica 
dos recursos quanticos
hardware e software 
 classicos
Codigo para operacoes 
quanticas
Resultados de 
Medidas
Memoria Quantica
Entrada
classica
saida 
classica
Arquiteturas para Programac¸a˜o Quaˆntica
QRAM - Dados quaˆnticos e controle cla´ssico
Ma´quina cla´ssica controla a memo´ria quaˆntica (recursos
quaˆnticos)
Recursos quaˆnticos: colec¸a˜o de qubits
Instruc¸o˜es:
Inicializac¸o˜es
Evoluc¸o˜es unita´rias
Medidas
Operadores quaˆnticos como componentes pre´-definidos:
codificam a definic¸a˜o de um circuito quaˆntico
Arquiteturas para Programac¸a˜o Quaˆntica
(Deutsch, 1985): Ma´quina de Turing Quaˆntica (MTQ) - Dados e
Controle quaˆnticos
Arquiteturas para Programac¸a˜o Quaˆntica
(Deutsch, 1985): Ma´quina de Turing Quaˆntica (MTQ) - Dados e
Controle quaˆnticos
Estado da fita e´ uma colec¸a˜o de qubits, possivelmente em
superposic¸a˜o.
Como o controle da fita tambe´m e´ quaˆntico, tambe´m pode
estar em superposic¸a˜o.
A MTQ evolui em direc¸o˜es diferentes simultaneamente.
Propriedades dos Dados Quaˆnticos
Paralelismo quaˆntico: estado quaˆntico pode estar em uma
superposic¸a˜o dos seus estados ba´sicos:
α|0〉 + β|1〉
Exemplo: versa˜o do algoritmo de Deutsch
Considerando uma func¸a˜o f : B → B
Queremos saber se f e´ constante ou balanceada
Classicamente: duas aplicac¸o˜es de f
Em uma linguagem quaˆntica: f pode ser aplicada uma u´nica vez!
f (α|0〉 + β|1〉)
Propriedades dos Dados Quaˆnticos
Emaranhamento: estado quaˆntico e´ GLOBAL
Evoluc¸a˜o unita´ria global do estado!
Exemplo: considerando um estado de dois qubits como:
α|00〉 + β|11〉
Problema 1. Na˜o temos como separar o primeiro qubit do segundo!
Problema 2. A na˜o ser fazendo uma medida!
O que causa um efeito colateral no estado quaˆntico!
meas(α|00〉 + β|11〉) 7→ {|00〉, |11〉}
Propriedades dos Dados Quaˆnticos
Non-clonning: dado quaˆntico na˜o pode ser copiado
Exemplo: considerando um estado como
α|0〉 + β|1〉
Na˜o temos como saber os valores de α e β!
Se tentamos, medimos!! Colapsando o estado e perdendo o
estado original!
Linguagens com Dados Quaˆnticos e Controle Cla´ssico
QCL - Bernhard O¨mer, 1998
Extensa˜o de uma linguagem cla´ssica estruturada como C.
Possui dados cla´ssicos e estruturas de controle (comandos)
cla´ssicos.
Parte quaˆntica da linguagem:
Essencialmente trata a manipulac¸a˜o de registradores quaˆnticos
atrave´s de estruturas de controle cla´ssicas!
Dado quaˆntico e´ manipulado atrave´s de refereˆncias a um vetor
de dados quaˆnticos.
QCL
Estado da ma´quina quaˆntica
O estado da ma´quina com n qubits e´ dado por Hn
Exemplo: ma´quina quaˆntica com 4 qubits
qcl> dump;
: STATE : 4 qubits free
1 |0000>
Registradores quaˆnticos
Qubits: registradores quaˆnticos de tamanho 1.
qcl> qureg a[1]; qureg b[1] // alocando 2 qubits
qcl> Rot(−pi/3,a) // rotando o primeiro qubit
qcl> Had(b) // hadamard no segurndo qubit
QCL
Estado da ma´quina quaˆntica apo´s alocac¸a˜o:
|Ψ〉 = |00〉 ⊗ (H|0〉) ⊗ (Rx(pi/3)|0〉)
qcl> dump;
: STATE : 2 / 4 qubits allocated, 2 / 4 qubits free
0.612372 |0000> + 0.612372 |0010> +
0.353553 |0001> + 0.353553 |0011>
Considera-se um conjunto universal de portas elementares!
Portas elementares sa˜o as primitivas fundamentais para manipular
o estado da ma´quina quaˆntica! Como atribuic¸o˜es em computac¸a˜o
cla´ssica!
QCL
Operadores sobre registradores quaˆnticos
Dado um operador unita´rio agindo sobre m qubits
U : Hm →Hm, a ac¸a˜o de U sobre um registrador em uma
ma´quina quaˆntica com n qubits e´ dada por:
U(s) = Π†s(U ⊗ I (n −m))Πs
Todos os operadores quaˆnticos em QCL sa˜o definidos dessa
maneira!
O tamanho do registrador operando e´ passado como
paraˆmetro.
QCL
Operadores sobre registradores quaˆnticos
Portas elementares sa˜o tratadas como subrotinas externas
extern operator H(qureg q)
extern operator RotX(real theta, qureg q)
extern qufunct CNOT(qureg q, quconst c)
Chamadas a` portas elementares podem ser invertidas:
qcl> qureg a[1];
[1/4] 1.0 |0000>
qcl> H(a);
[1/4] 0.7071 |0000> + 0.7071 |0001>
qcl> !H(a);
[1/4] 1.0 |0000>
QCL
Operadores sobre registradores quaˆnticos
Condicionais
extern cond Not(qureg q) // not condicional
O registrador de controle e´ passado como um paraˆmetro
impl´ıcito se o operador e´ utilizado no corpo de um condicional.
Exemplo:
qcl> qureg s[1]; qureg e[2];
qcl> if e {Not(s);} // invert s para e = 11
QCL
Operadores sobre registradores quaˆnticos
Medidas
Observa´veis sa˜o restritos a` base computacional
Retorna um valor cla´ssico
Reduz o estado
qcl> qureg q[2];
qcl> int m;
qcl> H(q);
[2/4] 0.5 |0000> + 0.5 |0001> +
0.5 |0010> + 0.5 |0011>
qcl> measure q,m;
[2/4] 0.5 |0011>
qcl> print m;
: 3 // 2 ** 0 + 2 ** 1
QCL
Operadores sobre registradores quaˆnticos
Registradores, portas elementares e medidas sa˜o suficientes para
implementac¸a˜o de algoritmos quaˆnticos
QCL apresenta subrotinas quaˆnticas!
Exemplo:
operator U(qureg x,qureg y){
H(x);
Not(y);
}
QCL
Copiando dado quaˆntico?
Duplicac¸a˜o de uma refereˆncia a um qubit
qcl> qureg x[1];
qcl> CNOT(x,x)
HUMMMM???
Sintaticamente permitido escrever!
Erro detectado em tempo de execuc¸a˜o somente!
QCL
Algoritmo de Deutsch
Algoritmo probabil´ıstico: com uma aplicac¸a˜o da func¸a˜of : B → B consegue-se calcular f (0)⊕ f (1) com probabilidade
1/2 com uma u´nica aplicac¸a˜o de f .
boolean g(boolean x) { ..}
qufunct G(qureg x, qureg y){...}
operator U(qureg x, qureg y) {
H(x);
G(x,y);
H(x & y);
}
QCL
Algoritmo de Deutsch
procedure deutsch(){
qureg x[1];
qureg y[1];
int m
{ reset ;
U(x,y);
measure y,m
} until m ≡ 1;
measure x,m;
print "g(0) xor g(1) = ",m;
reset;
}
Linguagens com Dados Quaˆnticos e Controle Cla´ssico
QPL - Peter Selinger, 2004
Primeira linguagem funcional quaˆntica!
Cada operac¸a˜o transforma um conjunto espec´ıfico de entradas
em sa´ıdas.
A primeira versa˜o de QPL tinha uma sintaxe baseada em
diagramas de fluxo com operac¸o˜es para inicializac¸a˜o,
atribuic¸a˜o (u´nica), condicional (medida), permutac¸o˜es, etc
Semaˆntica denotacional baseada em matrizes de densidade e
superoperadores.
Sistema de tipos esta´tico.
QPL
Diagramas de fluxo quaˆnticos
input p,q :qbit
measure p
output p,q :qbit
q *= N p *= N
p,q:qbit
p,q:qbit
p,q:qbit
p,q:qbit
p,q:qbit
p,q:qbit
B
DC
A
D 0
00
0
00
A
input p,q :qbit
measure p
output p,q :qbit
q *= N p *= N
p,q:qbit
p,q:qbit
p,q:qbit
p,q:qbit
p,q:qbit
D
0 0
0
0
00
NAN*
0
00
p,q:qbit NAN*+D
QPL
Diagramas ba´sicos:
A 0
00
q:qbit,Gamma = 
new qbit q := 0
Gamma = A
Alocando qubit
q:qbit,Gamma = 
A
C
B
D
discard q
Descartando qubit
Gamma = A + D
QPL
Diagramas ba´sicos:
A B
DC
measure p
q:qbit, Gamma = 
q:qbit, Gamma = q:qbit, Gamma = 
A
D
0 10
00
0 0
0
q *= S
q:qbit, Gamma = A
q:qbit, Gamma = (SXI)A(SXI)*
Medida Transformacao unitaria
QPL
Copiando dado quaˆntico?
Em QPL a co´pia de dados quaˆnticos e´ proibida via sintaxe!
Sistema de tipos (esta´tico)!!
Em qualquer contexto de tipos, varia´veis distintas se referem a
objetos distintos em tempo de execuc¸a˜o.
q representa uma lista de varia´veis distintas!
Isto satisfaz o requerimento que: operac¸o˜es agindo sobre
diversos qubits, precisam de locac¸o˜es f´ısicas diferentes.
Um programa bem tipado nunca causara´ erros em tempo de
execuc¸a˜o!
QPL
Exemplo: atirando uma moeda!
new qbit q := 0
A 0
00
A 0
00
Gamma = A
q *= H
p:qbit,Gamma = 
p:qbit,Gamma = 1/2 A A
A A
measure q
discard q discard q
q:qbit,Gamma= q:qbit,Gamma=
0 1 0
0
0
A
Gamma =1/2A Gamma =1/2A
QPL
Loops e Procedimentos
new qbit q := 0
A 0
00
A 0
00
Gamma = A
q *= H
p:qbit,Gamma = 
p:qbit,Gamma = 1/2 A A
A A
measure q
discard q discard q
q:qbit,Gamma= q:qbit,Gamma=
0 1 0
0
0
A
Gamma =1/2A Gamma =1/2A
coin toss
a:qbit
coin toss
input a
output1 b output2 a
a:qbitb:qbit
Lambda QPL
Ca´lculo Lambda para Computac¸a˜o Quaˆntica com Controle Cla´ssico
Peter Selinger & Benoˆıt Valiron, 2004.
A linguagem:
M,N, P := x | MN | λ x ⋅ M
| if M then N else P
| 0 | 1 | meas | new | U | *
| <M,N> | let <x,y> = M in N
Lambda QPL
Semaˆntica Operacional: sistema de reduc¸a˜o probabil´ıstico
Passos de reduc¸a˜o:
[Q,L,M]→p [Q
′,L′,M ′]
onde, [Q,L,M] e´ o estado de um programa dado por um
vetor Q, um termo lambda L e um ambiente M.
Lambda QPL
[α |Q0> + β |Q1>, meas pi] →|α|2 [|Q0>,0]
Exemplo de reduc¸a˜o:
[|0>,(λx ⋅ plus x x) ( meas (H p0))]
→1 [1/sqrt(2)(|0>+|1>),(λx ⋅ plus x x) ( meas p0)]
→1/2 { [|0>,(λx ⋅ plus x x) (0)],
[|1>,(λx ⋅ plus x x) (1)]}
→1/2 { [|0>, plus 0 0],
[|1>, plus 1 1] }
→1/2 { [|0>,0],
[|1>,0]}
Lambda QPL
Considera-se um conjunto U de portas ba´sicas universais
[Q, U<pi, ..., pj>] →1 [Q’,<pi, ..., pj>]
[Q,U<p0,p0>] ???
Sistema de Tipos!
Lambda QPL
Sistema de Tipos
Baseado na lo´gica linear!
Capturar quais termos podem ser duplicados!
Um termo do tipo A na˜o pode ser duplicado!
Um termo do tipo !A pode ser duplicado!
Lambda QPL
Exemplo: teleportac¸a˜o
EPR = λ x ⋅ CNOT<H (new 0), new 0>
BellMeasure =
λ q2 ⋅ λ q1 ⋅ ( let (p, p’) = CNOT<q1,q2>
in <meas H(p), meas p’>)
U = λ q⋅ λ <x,y> ⋅ if x then ( if y then
U11q else U10q)
else ( if y then U01q else U00q)
Lambda QPL
Exemplo: teleportac¸a˜o
Teleport = let <p,p’> = EPR *
in let f = BellMeasure p
in let g = U p’
in <f,g>
Linguagens com Dados e Controle Quaˆnticos
QML - Altenkirch & Grattage, 2004
Uma linguagem funcional de primeira ordem com dados
quaˆnticos e controle quaˆntico.
Semaˆntica operacional baseada em circuitos quaˆnticos
QML: Syntax
(Variables) x, y, ... ∈ Vars
(Prob⋅ Amplitudes) κ, ι, ... ∈ C
(Patterns) p,q ::= x | (x,y)
(Terms) t,u,e ::= x | () | (t,u)
| let p = t in u
| if◦ t then u else u’
| false | true |
−→
0 | κ*t | t+u
QML
Exemplo: Not quaˆntico
qnot x = if◦ x then false else true
qnot false = true
qnot (false + true) = if◦ false
then false
else true +
if◦ true
then false
else true
= true + false
QML
Exemplo: Not condicional
cnot c x = if◦ c
then (true, qnot x)
else (false, x)
Exemplo: Not condicional??
cnot c x = if◦ c
then (c, qnot x)
else (c, x)
QML
Exemplo: Not condicional
cnot c x = if◦ c
then (true, qnot x)
else (false, x)
Exemplo: Not condicional??
cnot c x = if◦ c
then (c, qnot x)
else (c, x)
QML
Copiando dados quaˆnticos.
let x = false + true
in (x,x) ≡ (false,false) + (true, true)
Descartando dados quaˆnticos weakening: na˜o e´ permitido nos
casos que informac¸a˜o pode ser perdida.
let (x,y) = (false,false) + (true,true)
in x
Dado quaˆntico ligado a y e´ descartado.
A expressa˜o na˜o e´ bem tipada!
QML
Copiando dados quaˆnticos.
let x = false + true
in (x,x) ≡ (false,false) + (true, true)
Descartando dados quaˆnticos weakening: na˜o e´ permitido nos
casos que informac¸a˜o pode ser perdida.
let (x,y) = (false,false) + (true,true)
in x
Dado quaˆntico ligado a y e´ descartado.
A expressa˜o na˜o e´ bem tipada!
QML
Sistema de Tipos
Regras de tipo baseadas na lo´gica linear estrita
Contrac¸o˜es sa˜o impl´ıcitas.
Weakenings na˜o sa˜o permitidos.
QML
Tipos: colec¸a˜o de qubits
σ = Q1 | Q2 | σ ⊗ τ
Contexto de tipos
Γ = • | Γ,x:σ
QML
Tipos: colec¸a˜o de qubits
σ = Q1 | Q2 | σ ⊗ τ
Contexto de tipos
Γ = • | Γ,x:σ
QML
Algumas regras do sistema de tipos
Γ ⊢ t : σ ∆, x : σ ⊢ u : τ
let
Γ⊗∆ ⊢ let x = t in u : τ
f-intro
• ⊢ false : Q2
t-intro
• ⊢ true : Q2
var
x : σ ⊢ x : σ
QML
Ortogonalidade
if◦ x then true else true
A expressa˜o retorna true sem realmente utilizar qualquer
informac¸a˜o sobre x .
A expressa˜o na˜o e´ bem-tipada.
if◦ x then t else u
A expressa˜o somente deve ser aceita se t e u sa˜o valores quaˆnticos
ortogonais (t ⊥ u).
t ⊥ u holds if 〈t|u〉 = 0
QML
Ortogonalidade
if◦ x then true else true
A expressa˜o retorna true sem realmente utilizar qualquer
informac¸a˜o sobre x .
A expressa˜o na˜o e´ bem-tipada.
if◦ x then t else u
A expressa˜o somente deve ser aceita se t e u sa˜o valores quaˆnticos
ortogonais (t ⊥ u).
t ⊥ u holds if 〈t|u〉 = 0
QML
Ortogonalidade
if◦ x then true else true
A expressa˜o retorna true sem realmente utilizar qualquer
informac¸a˜o sobre x .
A expressa˜o na˜o e´ bem-tipada.
if◦ x then t else u
A expressa˜o somente deve ser aceita se t e u sa˜o valores quaˆnticos
ortogonais (t ⊥ u).
t ⊥ u holds if 〈t|u〉 = 0
QML
Ortogonalidade
if◦ x then true else true
A expressa˜o retorna true sem realmente utilizar qualquer
informac¸a˜o sobre x .
A expressa˜o na˜o e´ bem-tipada.
if◦ x then t else u
A expressa˜o somentedeve ser aceita se t e u sa˜o valores quaˆnticos
ortogonais (t ⊥ u).
t ⊥ u holds if 〈t|u〉 = 0
QML
Altenkirch, Grattage, Vizzotto, Sabry, 2005 - Teoria equacional
Dada a seguinte definic¸a˜o para o porta de Hadamard:
H x = if◦ x
then ( false + (−1)*true )
else ( false + true )
Gostar´ıamos de verificar que H (H x) e´ observacionalmente
equivalente a` x.
QML: teoria equacional
As equac¸o˜es quaˆnticas sa˜o:
(if◦)
if◦ (λ*t0 + κ*t1) then u0 else u1
≡ λ*(if◦ t0 then u0 else u1) +
κ*(if◦ t1 then u0 else u1)
(superpositions)
t+u ≡ u+t
t +
−→
0 ≡ t
t+(u+v) ≡ (t+u)+v
λ*(t+u) ≡ λ*t + λ*u
λ*t+κ*t ≡ (λ+κ)*t
0*t ≡
−→
0
QML: teoria equacional
By definition of H
H(H x) = if◦ ( if◦ x
then ( false + (−1)*true )
else ( false + true ))
then ( false + (−1)*true )
else ( false + true )
QML: teoria equacional
By commuting conversion for if◦
= if◦ x
then if◦ ( false + (−1)*true )
then ( false + (−1)*true )
else ( false + true )
else if◦ ( false + true )
then ( false + (−1)*true )
else ( false + true )
QML: teoria equacional
By ifo
= if◦ x
then ( if◦ false
then (false + (−1)*true )
else ( false + true ) +
(−1) if◦ true
then (false + (−1)*true )
else ( false + true ) )
else ( if◦ false
then (false + (−1)*true )
else ( false + true ) +
(−1) if◦ true
then (false + (−1)*true )
else ( false + true ) )
QML: teoria equacional
By β
= if◦ x
then ( false − false + true + true )
else ( false + false + true − true )
By simplification and normalisation
= if◦ x then true else false
By η-rule for if o
= x
QML: teoria equacional
By β
= if◦ x
then ( false − false + true + true )
else ( false + false + true − true )
By simplification and normalisation
= if◦ x then true else false
By η-rule for if o
= x
QML: teoria equacional
By β
= if◦ x
then ( false − false + true + true )
else ( false + false + true − true )
By simplification and normalisation
= if◦ x then true else false
By η-rule for if o
= x
QHaskell: sintaxe
x, y, ... ∈ Vars
κ, ι ∈ C
d ::= false | true | κ * d | q + r
p ::= e | x | meas x
| if x then p1 else p2
| proc xl → do cl
| pr −< xl
| let x = p1 in p2
| x ← e
| p1;p2
| qif x then p1 else p2
| returnA −< xl
QHaskell: exemplos
qnot = proc x → do
qif x then x’ ← false
else x’ ← qtrue
returnA −< x’
hadamar = proc x → do
qif x then x’ ← (false + (−1) * true)
else x’ ← false + true
returnA −< x’
QHaskell: exemplos
qnot (κ false + ι true) =
x’ ← ι false +
x’ ← κ true =
x’ ← ι false + κ true
QHaskell: exemplos
cqnot = let qnot = proc x → do
qif x then x’ ← false
else x’ ← true
returnA −< x’
in proc (c,y) → do
qif c then y’ ← qnot −< x
else y’ ← y
returnA −< (c,y’)
QHaskell: teleportac¸a˜o
teleportation = proc (eprL,eprR,q) → do
(m1,m2) ← alice −< (eprL,q)
q’← bob −< (eprR,(m1,m2))
returnA −< q’
alice = let qnot = ...
hadamard = ...
in proc (eprL,q) → do
(q1,e1) ← qcnot −< (q,eprL)
q2 ← hadamard −< q1
(m1,m2) ← meas −< (e1,q2)
returnA −< (m1,m2)
QHaskell: teleportac¸a˜o
bob = proc (eprR,(m1,m2)) → do
if m1 then r’ ← qnot −< eprR
else r’ ← eprR
if m2 then r’’ ← z −< r’
else r’’ ← r’
returnA r’’
QHaskell
Sistema de tipos
Controlar o uso de varia´veis!!
Sistema de tipos baseado na lo´gica linear!
Tipos cla´ssicos:
σ = 1 | Bool | σ ⊗ τ
Tipos quaˆnticos:
θ = Q1 | QBool | θ ⊗ υ
QHaskell
Sistema de tipos
Valores cla´ssicos:
false
• ◭ Γ ⊢ false : Bool
true
• ◭ Γ ⊢ true : Bool
Varia´veis:
cvar
• ◭ x : σ,Γ ⊢ x : σ
qvar
x : θ ◭ Γ ⊢ x : θ
QHaskell
Sistema de tipos
Medida: transforma dado quaˆntico em cla´ssico
Θ ◭ x : |θ|,Γ ⊢ x
meas
x : θ ⊗Θ ◭ Γ ⊢ meas x
QHaskell
Sistema de tipos
returnA: todas e somente todas as varia´veis quaˆnticas
retornas em um procedimento quaˆntico devem ser provadas!
Θ ◭ Γ ⊢ (x ′1 : θ
′
1, . . . , x
′
n : θ
′
n)
returnA
Θ ◭ Γ ⊢ returnA(x ′1 : θ
′
1, . . . , x
′
n : θ
′
n) : θ
′
1 ⊗ . . .⊗ θ
′
n
QHaskell
Sistema de tipos
Procedimentos quaˆnticos:
x1 : θ1, . . . , xn : θn,Θ ◭ Γ ⊢ cl; returnA(x
′
1 : θ
′
1, . . . , x
′
n : θ
′
n) : t
Θ ◭ Γ ⊢ proc (x1:θ1, ...,xn:θn) do
pro
cl
returnA(x ′
1
: θ′
1
, . . . , x ′n : θ
′
n)
QHaskell
QHaskell: uma proposta para uma linguagem quaˆntica mista!
Sintaxe para manipulac¸a˜o de dados quaˆnticos possivelmente
emaranhados baseada na notac¸a˜o do para setas em Haskell.
Sistema de tipos baseado na lo´gica linear para controlar a
utilizac¸a˜o de varia´veis quaˆnticas.
Um dado quaˆntico que e´ medido se transforma em dado
cla´ssico!
Trabalho futuro: definic¸a˜o de uma semaˆntica de reescrita para
QHaskell utilizando o ca´lculo-ρ.
Fim
Obrigada!