Introducción a la computación cuántica y

fundamentos de lenguajes de programación

Materia optativa de la
Licenciatura en Ciencias de la Computación
con créditos para el doctorado
Universidad Nacional de Rosario

Alejandro Díaz-Caro
Instituto de Investigación en Ciencias de la Computación
(CONICET / Universidad de Buenos Aires)
& Universidad Nacional de Quilmes

version 2018-06-25
 Enfoque de este apunte

Estas notas están pensadas para estudiantes

de grado y posgrado de computación, no de fí-
sica. Es por ello que el enfoque que se da es casi
puramente matemático, con algún comentario
aquí y allá de la física que motiva el formalis-
mo, pero todos los razonamientos se realizan
exclusivamente desde el lado de la matemática.

Materia:
Introducción a la computación cuántica y fundamentos de lenguajes de programación

Departamento de Ciencias de la Computación

Facultad de Ciencias Exactas, Ingeniería y Agrimensura
Universidad Nacional de Rosario

CC 2015–2018 Creative Commons Attibution 4.0 Internacional.
Podés ver una copia de la licencia en http://creativecommons.org/licenses/by/4.0/.
Índice general

1. Introducción a la computación cuántica 7

1.1. Introducción . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.2. Preliminares: un poco de álgebra . . . . . . . . . . . . . . . . . . . . . . 9
1.2.1. Espacio de Hilbert . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.2.2. Productos tensoriales . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.2.3. Notación bra–ket . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.2.3.1. Notación bra y ket para vectores . . . . . . . . . . . . . 11
1.2.3.2. Notación bra y ket para matrices . . . . . . . . . . . . . 13
1.3. Bits cuánticos y operadores . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.3.1. Primera intuición . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.3.2. Bits cuánticos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.3.3. Operadores . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.4. Teorema del no-clonado . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.5. Estados de Bell . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
1.6. Usando los estados de Bell . . . . . . . . . . . . . . . . . . . . . . . . . . 19
1.6.1. Codificación superdensa . . . . . . . . . . . . . . . . . . . . . . . 19
1.6.2. Teleportación cuántica . . . . . . . . . . . . . . . . . . . . . . . . 20
1.7. Paralelismo Cuántico . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

2. Algoritmos cuánticos y aplicación a criptografía 23

2.1. Algoritmo de Deutsch . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.2. Algoritmo de Deutsch-Jotza . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.3. Algoritmo de Búsqueda de Grover . . . . . . . . . . . . . . . . . . . . . . 26
2.3.1. Oráculo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.3.2. Inversión sobre el promedio . . . . . . . . . . . . . . . . . . . . . 27
2.3.3. El algoritmo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.3.3.1. Paso 1: Se aplica Hadamard (H ⊗n ) . . . . . . . . . . . . 28
2.3.3.2. Paso 2: Se aplica el oráculo (U ) . . . . . . . . . . . . . . 28
2.3.3.3. Paso 3: Se aplica la inversión sobre el promedio (G) . . . 29
2.3.4. Cálculo del número óptimo de iteraciones . . . . . . . . . . . . . . 30
2.4. Aplicación criptográfica . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2.4.1. One-time pad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2.4.2. Criptosistema Cuántico QKD-BB84 . . . . . . . . . . . . . . . . . 32

3
3. Introducción a la mecánica cuántica 35
3.1. Postulados de la mecánica cuántica . . . . . . . . . . . . . . . . . . . . . 35
3.1.1. Medición proyectiva . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3.1.1.1. Preliminares . . . . . . . . . . . . . . . . . . . . . . . . 36
3.1.1.2. Medición proyectiva . . . . . . . . . . . . . . . . . . . . 38
3.1.2. Fase . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
3.2. Operador densidad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
3.2.1. Preliminares . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
3.2.2. Conjuntos de estados cuánticos . . . . . . . . . . . . . . . . . . . 40
3.2.3. Propiedades generales del operador densidad . . . . . . . . . . . . 42
3.2.4. El operador densidad reducido . . . . . . . . . . . . . . . . . . . . 44
3.2.4.1. Teleportación cuántica y el operador densidad reducido . 45

4. Introducción al lambda cálculo y a la teoría de tipos 47

4.1. PCF no tipado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
4.1.1. Primeras definiciones . . . . . . . . . . . . . . . . . . . . . . . . . 47
4.1.2. Gramática de PCF . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4.1.3. Semántica operacional . . . . . . . . . . . . . . . . . . . . . . . . 49
4.1.4. No terminación . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
4.1.5. Captura de variables . . . . . . . . . . . . . . . . . . . . . . . . . 50
4.2. Estrategias de reducción . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
4.2.1. Primeras definiciones . . . . . . . . . . . . . . . . . . . . . . . . . 51
4.2.2. Reducción débil . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
4.2.3. Call-by-name . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
4.2.4. Call-by-value . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
4.3. PCF tipado . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
4.3.1. Introducción . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
4.3.2. Gramática de PCF tipado . . . . . . . . . . . . . . . . . . . . . . 55
4.3.3. La relación de tipado . . . . . . . . . . . . . . . . . . . . . . . . . 56
4.3.4. Correctitud . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
4.3.5. Normalización fuerte . . . . . . . . . . . . . . . . . . . . . . . . . 58
4.4. Inferencia de tipos simples . . . . . . . . . . . . . . . . . . . . . . . . . . 62
4.4.1. Introducción . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
4.4.2. Algoritmo de Hindley . . . . . . . . . . . . . . . . . . . . . . . . . 63
4.4.3. Algoritmo de unificación de Robinson . . . . . . . . . . . . . . . . 64
4.5. Polimorfismo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
4.5.1. Introducción . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
4.5.2. Tipos polimórficos . . . . . . . . . . . . . . . . . . . . . . . . . . 66
4.6. Interpretación . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
4.6.1. Interpretación en CBN . . . . . . . . . . . . . . . . . . . . . . . . 68
4.6.2. Interpretación en CBV . . . . . . . . . . . . . . . . . . . . . . . . 69
4.7. Semántica denotacional . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
4.7.1. Primeras definiciones . . . . . . . . . . . . . . . . . . . . . . . . . 70
4.7.2. La semántica denotacional de PCF tipado . . . . . . . . . . . . . 71
4.8. Rapid(ísim)a descripción de la lógica lineal . . . . . . . . . . . . . . . . . 73
4.8.1. Introducción . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
 4.8.2. Cálculo de secuentes . . . . . . . . . . . . . . . . . . . . . . . . . 74
4.8.3. Un ejemplo simple de sistema de tipos lineal . . . . . . . . . . . . 75

5. Extensiones cuánticas al lambda cálculo 77

5.1. Control clásico, datos cuánticos . . . . . . . . . . . . . . . . . . . . . . . 77
5.1.1. El cálculo de Selinger y Valiron . . . . . . . . . . . . . . . . . . . 77
5.2. Control y datos cuánticos . . . . . . . . . . . . . . . . . . . . . . . . . . 82
5.2.1. El cálculo de van Tonder . . . . . . . . . . . . . . . . . . . . . . . 82
5.2.2. El lambda cálculo lineal algebraico . . . . . . . . . . . . . . . . . 84
5.2.3. Tipando superposiciones y mediciones proyectivas . . . . . . . . . 88
Capítulo 1

Introducción a la computación cuántica

I feel that a deep understanding of why quantum algorithms work is still lac-
king. Surely the power of quantum computers has something to do with entan-
glement, quantum parallelism, and the vastness of Hilbert space, but I think
that it should be possible to pinpoint more precisely the true essence of the
matter. John Preskill [1998]

1.1. Introducción
La computación cuántica, una rama de las ciencias de la computación teórica, tiene su
origen en la física, y más precisamente en el físico estadounidense Richard Feynman,
quien en 1981 dedicó una charla en el Massachusetts Institute of Technology (MIT) al
problema de la simulación de la física cuántica con computadoras clásicas. Sus ya célebres
palabras finales resumen su frustración de ese entonces:

And I’m not happy with all the analyses that go with just the classical theory,
because nature isn’t classical, dammit, and if you want to make a simulation of
nature, you’d better make it quantum mechanical, and by golly it’s a wonderful
problem, because it doesn’t look so easy. Thank you.
(ver, por ejemplo, [Brown, 2001, pp.100])

Esta provocación, lejos de plantear soluciones, abrió las puertas a interrogantes nunca
antes concebidos. ¿Qué ganancia se lograría si las computadoras fuesen regidas por las
leyes de la mecánica cuántica? Fueron los algoritmos de Grover [1996] y Shor [1997] los
cuales despertaron el gran interés desde las ciencias de la computación en este nuevo
paradigma. El primero es un algoritmo de búsqueda sobre registros desordenados, el cual
provee una ganancia cuadrática de complejidad temporal frente a cualquier algoritmo
clásico conocido. El segundo es un algoritmo para la factorización de números, con una
ganancia exponencial.
Actualmente existen muchas áreas de investigación dentro de la computación cuántica.
Por ejemplo, desde un punto de vista práctico se plantea el problema de construir el
hardware de una computadora cuántica. Desde sus orígenes, en las palabras de Feinmann,

7
8 1.1. Introducción

la idea es que un algoritmo cuántico sea una simulación cuántica en hardware que se
comporta de acuerdo a las leyes de la física cuántica. Es decir que un experimento cuántico
en un laboratorio, puede considerarse como un algoritmo. O dicho de otro modo: podemos
describir el comportamiento de un sistema cuántico a través de un algoritmo. La pregunta
es, ¿podemos realizar el experimento cuántico que describe un algoritmo dado? Allí es
donde se manifiesta el desafío técnico.
Otra área es la de desarrollar algoritmos que obtengan una ganancia con respecto a su
contraparte clásica. En general los algoritmos de Grover y Shor mencionados anterior-
mente se consideran como los ejemplos canónicos de aceleración obtenida gracias a la
computación cuántica. Muchos otros algoritmos cuánticos son derivados de ellos. La pre-
gunta aquí es ¿qué otros algoritmos podemos obtener que nos den una ganancia respecto
a los algoritmos clásicos?
Otra rama de investigación es la del diseño de lenguajes de programación que permitan
expresar los algoritmos cuánticos de una manera amigable, y quizá permitiendo descubrir
nuevos algoritmos al tener una herramienta de alto nivel para pensarlos.
Desde un punto de vista más fundamental, y como lo expresara Preskill en la cita que
abre este capítulo, los fundamentos lógicos detrás de la computación cuántica, siguen
siendo un misterio. Si bien existe una lógica cuántica [Birkhoff y von Neumann, 1936],
ésta fue propuesta muchos años antes de la computación cuántica, por lo que encontrar la
correspondencia entre computación y lógica cuántica no es trivial. Esta área tiene muchas
subáreas con metodologías diferentes. En particular, el estudio de semántica de lenguajes
de programación sigue este objetivo. En este caso no se persigue el estudio del lenguaje
en sí mismo, sino que el objetivo es el estudio de la lógica subyacente. Estudiar la lógica
detrás de la computación cuántica implica estudiar la lógica detrás de la física cuántica,
lo cual puede tener influencia en el desarrollo de nuevas teorías sobre el mundo que nos
rodea.

En esta materia nos interesan los dos últimos aspectos: lenguajes de programación que
permitan expresar el cómputo cuántico de una manera estructurada y amigable, y el
estudio de propiedades de lenguajes que nos acerquen hacia una lógica computacional de
la física cuántica.

Estructura de la materia y de estos apuntes En el primer encuentro, de dos días

(10hs en total), y se plantea la primera introducción a la computación cuántica. Esta es
una introducción para un sólo encuentro, para una introducción más extensa, se reco-
mienda el libro de Nielsen y Chuang [2010]. En el resto de este capítulo desarrollaremos
los rudimentos básicos de la computación cuántica, desde un enfoque puramente matemá-
tico (en contraposición con el enfoque físico). En el Capítulo 2 explicaremos algunos de
los algoritmos más conocidos y una aplicación a la criptografía. En el segundo encuentro
estudiaremos los postulados de la mecánica cuántica, desarrollados en el Capítulo 3, des-
de un punto de vista más físico, relacionándolo con el formalismo aprendido. En el tercer
encuentro estudiaremos el cálculo lambda tipado y el isomorfismo de Curry-Howard. Fi-
nalmente, en el cuarto y último encuentro, estudiaremos extensiones cuánticas al cálculo
lambda, en el paradigma de control clásico y datos cuánticos y en el paradigma de control
y datos cuánticos.
Capítulo 1. Introducción a la computación cuántica 9

1.2. Preliminares: un poco de álgebra

1.2.1. Espacio de Hilbert
TL;DR Cn con la suma (+) y el producto (·) usuales, y el producto escalar definido
por
n
X
h~v , wi
~ = h(v1 , v2 , . . . , vn ), (w1 , w2 , . . . , wn )i = vi∗ · wi
i=1
∗
donde v es el complejo conjugado de v, es un espacio de Hilbert.
En el resto de la sección se define formalmente qué es un espacio de Hilbert.

Definición 1.1 (Producto escalar). Sea E un espacio vectorial sobre el cuerpo K (R

o C). Un producto escalar (también llamado producto interno) definido sobre E es una
función h, i : E × E → K que verifica las siguientes propiedades.
~ ∈ E, a, b ∈ K, se cumple:
Para todo ~u, ~v , w

h~u, ~ui ≥ 0
(Definida positiva)
h~u, ~ui = 0 ⇔ ~u = ~0E
hw,
~ a~u + b~v i = ahw, ~ ~ui + bhw,
~ ~v i (Lineal por derecha)
∗ ∗
ha~u + b~v , wi
~ = a h~u, wi ~ + b h~v , wi
~ (Antilineal por izquierda)
∗
h~u, ~v i = h~v , ~ui (Hermítica)

Definición 1.2 (Espacio pre-Hilbert). Un espacio pre-Hilbert es un espacio vectorial

sobre K con producto escalar.

Observación. Todo espacio pre-Hilbert es un espacio vectorial normado con la norma

p
k~v k = h~v , ~v i

Definición 1.3 (Sucesión de Cauchy). Sea ~vn una sucesión de vectores del espacio E.
Si k~vn − ~vm k → 0 cuando n, m → ∞, entonces la sucesión ~vn es una sucesión de Cauchy.
(Esto quiere decir que puedo hacer distar entre sí los términos tan poco como quiera).

Observación. Toda sucesión convergente es de Cauchy, pero no toda sucesión de Cauchy

es convergente.

Definición 1.4 (Espacio completo). E es completo para la norma k · k, si y sólo si toda

sucesión de Cauchy converge con esa norma.

Definición 1.5 (Espacio de Hilbert). Un espacio pre-Hilbert completo en su norma se

denomina espacio de Hilbert.

1.2.2. Productos tensoriales

En esta sección consideramos espacios vectoriales equipados con una base canónica.
10 1.2. Preliminares: un poco de álgebra

Definición 1.6 (Producto tensorial). Sean E y F dos espacios vectoriales con bases
canónicas B = {~bi | i ∈ I} y C = {~cj | j ∈ J} respectivamente. El producto tensorial
E ⊗ F de E y F es el espacio vectorial de base canónica {~bi ⊗ ~cj | i ∈ I y j ∈ J}, donde
~bi ⊗ ~cj es el par ordenado formado por el vector ~bi y el vector ~cj . La operación ⊗ se
extiende a vectores de E y F bilinearmente:
X X X
( αi~bi ) ⊗ ( βj~cj ) = αi βj (~bi ⊗ ~cj )
i j ij

Definición 1.7 (Producto cartesiano entre dos subconjuntos de espacios vectoriales).

Sean E y F dos espacios vectoriales equipados con bases B y C, y sean S y T dos
subconjuntos de E y F respectivamente. Definimos el conjunto S × T , subconjunto del
espacio vectorial E ⊗ F , de la siguiente manera:

S × T = {~u ⊗ ~v | ~u ∈ S, ~v ∈ T }

Observación. E × F 6= E ⊗ F . Por ejemplo, si E = F = C2 , con base canónica {~i, ~j},

entonces E × F contiene a ~i ⊗ ~i y a ~j ⊗ ~j, pero no a ~i ⊗ ~i + ~j ⊗ ~j, que no es producto de
dos vectores de C2 .
Definición 1.8 (Generador). Sea E un espacio vectorial equipado con una base B, y
S ⊆ E. Escribimos G(S) al espacio vectorial sobre C generado por S, es decir, que
contiene todas las combinaciones lineales de elementos de S.
Observación. Si E y F son dos espacios vectoriales con bases B y C respectivamente,
entonces
E ⊗ F = G(B × C) = G(E × F )
La operación ⊗ introducida genéricamente en la Definición 1.6, puede ser definida más
precisamente para matrices (y vectores, tomando matrices columna o fila) de la siguiente
manera.
Definición 1.9 (Producto tensorial entre matrices). El producto tensorial de dos matri-
ces, P y Q se define como la matriz
 
p11 Q . . . p1m Q
P ⊗ Q =  ... .. 

. 
pn1 Q . . . pnm Q

Ejemplos 1.10.
      
5 6 5 6 5 6 10 12
    1 2
1 2 5 6 
7 8 7 8  7 8 14
  16
⊗ = = 
3 4 7 8  5 6 5 6  15 18 20 24
3 4
7 8 7 8 21 24 28 32
    
3 3
    1
1 3 
4 = 4
  
⊗ =
2 4  3  6
2
4 8
Capítulo 1. Introducción a la computación cuántica 11

Observación. El producto escalar, o producto interno, entre dos vectores nos da un nú-
mero. El producto tensorial, o producto externo, entre dos vectores nos da un vector de
mayor dimensión.
Como se dijo anteriormente, E × F 6= E ⊗ F , y por lo tanto:

Existen vectores de E ⊗ F que no son producto

tensorial entre uno de E y uno de F .
   
2 2 0 21
Ejemplo 1.11. Consideremos el espacio C ⊗ C . Una base de C es { , } Por lo
1 0
tanto         

 0 0 0 1 
0 0 1 0
        
C ⊗ C = Gen(   ,   ,   ,   ) = C4
2 2 

 0 1 0 0 
1 0 0 0
 

Tomemos ~v = (α, 0, 0, β)T , con α, β 6= 0. Es fácil verificar que ~v ∈ C4 . Sin embargo, no

existen ~v1 , ~v2 ∈ C2 tal que ~v = ~v1 ⊗ ~v2 .

Demostración. Supongamos que existen ~v1 y ~v2 tales que ~v1 ⊗ ~v2 = ~v , entonces
    
    ac α 
 ac = α
a c ad  0  ad = 0
    
⊗ = = ⇒
b d  bc  0 
 bc = 0
bd β bd = β


pero este es un sistema que no tiene solución.

1.2.3. Notación bra–ket

Notación introducida por Paul Dirac [1939] para describir estados cuánticos.

1.2.3.1. Notación bra y ket para vectores

En lugar de escribir los vectores como ~v la notación ket usa |vi.
En particular definimos:    
1 0
|0i = |1i =
0 1
Por lo tanto, cualquier vector de C2 puede escribirse como
     
α 1 0
=α +β = α|0i + β|1i
β 0 1

Podemos, por ejemplo, definir vectores como los siguientes

! !
1 √1 1 √1
|+i = √ (|0i + |1i) = √12 |−i = √ (|0i − |1i) = 2
2 2 2 − √12
12 1.2. Preliminares: un poco de álgebra

y como estos son dos vectores ortogonales (por ende, forman una base), ahora es posible
también escribir cualquier vector de C2 como combinación lineal de |+i y |−i.
Por ejemplo:
 
α 1 1
= α|0i + β|1i = √ (α + β)|+i + √ (α − β)|−i
β 2 2
Observación. Al menos que se indique lo contrario, en el resto del apunte consideraremos
n
el espacio complejo de dimensión N = 2n , CN = C2 .

Definición 1.12 (Bra y Ket). Llamamos ket a un vector de la forma

 
α1
 .. 
|ψi =  . 
αN

y bra a un vector de la forma

hψ| = (α1∗ , . . . , αN
∗
)
donde αi ∈ C y αi∗ denota el conjugado de αi .

Observaciones.
Haciendo un abuso de notación, podemos escribir vectores como el siguiente:

|α1 ψ1 + α2 ψ2 i = α1 |ψ1 i + α2 |ψ2 i

A partir la definición de bras y kets, llamamos “braket” al producto escalar:

 
β1
∗ ∗  .. 
hψ|φi = (α1 , . . . , αN )  .  = a ∈ C
βN

Recordatorio de álgebra: Una base ortonormal de un espacio vectorial normado es

una base donde todos los vectores tienen norma 1. Además, en una base, todos los
vectores son ortogonales entre sí (es decir, el producto escalar entre ellos es 0). Por
lo tanto:
Dado un conjunto B = {|u1 i, . . . , |uN i}, B es una base ortonormal de CN si y sólo
si para todo i, j tenemos hui |uj i = δij , donde δij es la delta de Kronecker (igual a
1 si i = j, y 0 en otro caso).

Entonces, todo Ket |ψi se puede expresar como |ψi = N

P
i=1 ai |ui i.

Si tomamos la base canónica de CN , con |ui i el vector i-ésimo de dicha base, pode-
mos calcular la componente i-ésima de un vector cualquiera de la siguiente manera:
N
X N
X
hui |ψi = hui | aj |uj i = aj hui |uj i = ai
| {z }
j=1 j=1
δij
Capítulo 1. Introducción a la computación cuántica 13

N
P
Teorema 1.13. Sea B = {|u1 i, . . . , |uN i} una base ortonormal, entonces |ui ihui | = I.
i=1
Demostración.
N
! N
! N
!
X X X
|ui ihui | |ψi = |ui ihui | aj |ui i
i=1 i=1 j=1
N X
X N N
X
= aj |ui i hui |uj i = ai |ui i = |ψi
| {z }
i=1 j=1 i=1
δij

Observaciones.
N
b∗i hui |.
P
Análogamente a los kets, todo bra hφ| puede ser descompuesto como hφ| =
i=1

Podemos ver que b∗i

= hφ|ui i ∈ C ya que
" N # N
X X
hφ| = hφ| |ui ihui | = hφ|ui ihui | ⇒ b∗i = hφ|ui i
| i=1 {z } i=1

Observación. De aquí en más, trabajaremos sólo con los vectores normalizados de CN (es
decir, vectores cuya norma es 1). Esto es
N
! N ! N N
X X X X
2 ∗ ∗
1 = kψk = hψ|ψi = aj huj | ai |ui i = aj ai huj |ui i = |ai |2 = 1
| {z }
j=1 i=1 i,j=1 i=1
δij

Es decir, trabajamos con vectores cuya suma de los módulos al cuadrado de sus compo-
nentes es 1.

1.2.3.2. Notación bra y ket para matrices

Para toda matriz cuadrada de dimensión N a coeficientes complejos A, tenemos la si-
guiente representación:
   
|vectori
X N   XN  N XN z }| { N X N
   X X
A= |ui ihui | A  |uj ihuj | = |ui i hui | A|uj i huj | = αij |ui ihuj |
  
 i=1   j=1  i=1 j=1 | {z }
i=1 j=1
| {z } | {z } αij
I I

donde αij es la componente ij de la matriz.

Con esta representación, podemos representar el producto de una matriz por un vector
de la siguiente manera:
N XN
! N !
X X
A|ψi = αij |ui ihuj | ak |uk i
i=1 j=1 k=1
N X
X N X
N N X
X N
= αij ak |ui i huj |uk i = αij aj |ui i
| {z }
i=1 j=1 k=1 i=1 j=1
δjk
14 1.3. Bits cuánticos y operadores

PN
Es decir, las componentes del vector A|ψi son bi = j=1 αij aj .

1.3. Bits cuánticos y operadores

1.3.1. Primera intuición
En computación clásica la unidad mínima de información es el bit, el cual puede estar en
un estado 0 o 1. Leer un bit es una operación que no conlleva ninguna particularidad. En
contraposición, un bit cuántico o qubit puede estar en un estado que sea una superposición
de los estados 0 y 1. Un qubit es un vector de C2 , por lo tanto lo podemos representar
como α|0i + β|1i, lo cual representa el estado que es 0 y en 1 a la vez. Leer un qubit en
cambio se produce a través de una operación llamada medición, y al medir un qubit, éste
colapsa, cambia su estado (dependiendo de la medición puede cambiar por ejemplo a |0i
o |1i, pero también podría usarse otro operador de medición que lo colapse a otra base).

1.3.2. Bits cuánticos

Definición 1.14 (Qubit). Un qubit o bit cuántico es un vector normalizado (es decir,
con norma 1) del espacio de Hilbert C2 .

Observación. Considerando la base {|0i, |1i} de C2 , cualquier qubit puede escribirse como
|ψi = α|0i + β|1i, con |α|2 + |β|2 = 1.

Definición 1.15 (n-qubits). Un sistema de n-qubits es un vector normalizado del espacio

n
n
C2 = C2 .
N
i=1

Observaciones.
En lugar de escribir |0i ⊗ |1i ⊗ · · · ⊗ |0i escribimos |01 . . . 0i.

De la misma manera, en ocasiones, en lugar de |0i ⊗ (α|0i + β|1i) escribimos sim-

plemente |0i(α|0i + β|1i).
n
La base canónica del espacio C2 es {|0 . . . 00i, |0 . . . 01i, . . . , |1 . . . 11i}.

1.3.3. Operadores
Definición 1.16 (Operador). Un operador de CN es una matriz cuadrada de dimensión
N a coeficientes complejos.

Definición 1.17 (Adjunto). El adjunto de un operador A se nota por A† y se define

como el operador transpuesto y conjugado de A. Es decir, si αij = hui |A|uj i son las
componentes de A, las componentes de A† son αji
∗
= huj |A|ui i∗ = hui |A† |uj i.

Propiedades. Sean A y B operadores de CN , a ∈ C y |ψi ∈ CN

Capítulo 1. Introducción a la computación cuántica 15

(A† )† = A (aA)† = a∗ A† hAψ| = hψ|A†

(A + B)† = A† + B † (AB)† = B † A†

Definición 1.18 (Proyector). A los operadores de la forma P = |φihφ| se les llama

proyectores, ya que proyecta ortogonalmente un ket |ψi cualquiera sobre el ket |φi:

P |ψi = |φi hφ|ψi = a|φi

| {z }
a∈C

   
1 0
Ejemplo 1.19. Tomemos la base {|0i, |1i}, con |0i = y |1i = . Un vector |ψi
0 1
cualquiera puede escribirse como |ψi = α|0i + β|1i. Por lo tanto

|0ih0|ψi = |0ih0|(α|0i + β|1i) = |0i(α h0|0i +β h1|0i) = α|0i

| {z } | {z }
1 0

Definición 1.20 (Operador hermítico). Un operador A es hermítico si A = A† .

Definición 1.21 (Operador unitario). Un operador U es unitario si U † U = U U † = I, o

lo que es lo mismo U † = U −1 .

Propiedades. Para cualquier operador U unitario vale:

U preserva el producto interno: hU φ|U ψi = hφ|U † U |ψi = hφ|ψi

U −1 es unitario.

Si {|ψ1 i, . . . , |ψN i} es base ortonormal, entonces {U |ψ1 i, . . . , U |ψN i} también lo es.

Definición 1.22 (Operador de medición). Un conjunto de proyectores {M1 , . . . , Mk } se

dice que es un operador de medición si satisface
k
X
Mi Mi† = I
i=1

Definición 1.23 (Compuertas cuánticas). A los operadores unitarios se les llama com-
puertas cuánticas, como analogía a las compuertas lógicas de la computación clásica, ya
que serán esos los que se utilizan para realizar el cómputo.

Observación. La mayoría de las compuertas cuánticas que usaremos a lo largo del curso
serán además de operadores unitarios, hermíticos, por lo que coinciden con su inversa.

Definición 1.24 (Evolución). Se dice que un sistema representado por un ket |ψi evo-
luciona al sistema |φi, cuando se realiza una de las siguientes operaciones:

Se premultiplica por una compuerta cuántica U :

|φi = U |ψi
16 1.3. Bits cuánticos y operadores

Se aplica un operador de medición M = {M1 , . . . , Mk } de la siguiente manera:

Mi |ψi
|φi = q para algún 1 ≤ i ≤ k
†
hψ|Mi Mi |ψi

La elección del Mi no se conoce de antemano, sólo se conoce la probabilidad para

cada i, la cual viene dada por la siguiente ley:

p(i) = hψ|Mi† Mi |ψi

Observaciones.
U M
Usaremos también la notación |ψi −
→ |φi o |ψi −→ |φi para indicar que el ket |ψi
evoluciona al ket |φi.
Cuando se quiera hacer evolucionar sólo un qubit de un sistema de n-qubits, digamos
el qubit i, se premultiplica tensorialmente i − 1 veces y se postmultiplica n − i − 1
veces la compuerta a aplicar por la matriz identidad. Ejemplo: U aplicada al segundo
qubit de un sistema de 2–qubits, será la compuerta I ⊗ U .
Ejemplo 1.25. Consideramos el operador medición de {M0 , M1 } con
   
1 0 0 0
M0 = |0ih0| = M1 = |1ih1| =
0 0 0 1

Podemos verificar que M0 M0† + M1 M1† = M0 + M1 = I, y por lo tanto es un operador de

medición.
Sea |ψi = α|0i + β|1i, entonces, la probabilidad de que el proyector que se aplique sea
M0 es

p(0) = hψ|M0† M0 |ψi

= (α∗ h0| + β ∗ h1|)M0 (α|0i + β|1i)
= |α|2 h0|M0 |0i + α∗ βh0|M0 |1i + αβ ∗ h1|M0 |0i + |β|2 h1|M0 |1i
= |α|2 h0|0i h0|0i + α∗ β h0|0i h0|1i +αβ ∗ h1|0i h0|0i +|β|2 h1|0i h0|1i
| {z } | {z } | {z } | {z } | {z } | {z } | {z } | {z }
1 1 1 0 0 1 0 0
2
= |α|

Análogamente, p(1) = hψ|M1† M1 |ψi = · · · = |β|2 .

Dado que el vector está normalizado, p(0) + p(1) = |α|2 + |β|2 = kψk = 1.
Luego de aplicar este operador de medición, la evolución es la siguiente. Si se aplicó el
proyector M0 , el sistema queda en el siguiente estado:
M0 |ψi M0 |ψi α
q =p = |0i
p(0) |α|
hψ|M0† M0 |ψi
 2
α |α|2
Este estado está normalizado ya que  |α|  = |α|2
= 1.
M1 |ψi β
Análogamente si se aplicó M1 se obtiene √ = |β|
|1i.
p(1)
Capítulo 1. Introducción a la computación cuántica 17

Definición 1.26 (Compuertas más comunes y operadores de Pauli). Las compuertas

cuánticas más importantes, por su utilidad en el diseño de algoritmos, son las siguientes:
La compuerta H de Hadamard:
H|0i = √1 (|0i + |1i)
 
2 √1
1 1
√1 (|0i
donde: H=
H|1i = 2
− |1i) 2 1 −1

La identidad I:  
I|0i = |0i 1 0
donde: I=
I|1i = |1i 0 1
La negación X:  
X|0i = |1i 0 1
donde: X=
X|1i = |0i 1 0
El cambio de fase Z:
 
Z|0i = |0i 1 0
donde: Z=
Z|1i = −|1i 0 −1

La No-controlada CN OT :
 
CN OT |0xi = |0xi I 0
donde: CN OT =
CN OT |1xi = |1i ⊗ X|xi 0 X

En particular, las matrices I, X, iXZ y Z son las llamadas matrices de Pauli en honor
a Wolfgang Pauli

1.4. Teorema del no-clonado

El teorema de no-clonado [Wootters y Zurek, 1982] dice que es imposible construir una
máquina universal de clonado. Es decir, no podemos copiar un qubit arbitrario, ya que no
existe ningún método que pueda copiarlo sin saber su estado preciso, y como la medición
cambia el qubit, no podemos saber su estado preciso. En consecuencia, no podemos copiar
un qubit arbitrario.
Teorema 1.27 (No-cloning). No existe ninguna compuerta cuántica U tal que para algún
|φi ∈ CN y ∀|ψi ∈ CN se cumpla U |ψφi = |ψψi.
Demostración. Supongamos que existe la operación U de la cual se habla en el teorema,
entonces, dados cualesquiera |ψi, |φi ∈ CN , se cumple
U |ψφi = |ψψi
U |ϕφi = |ϕϕi
Por lo tanto, hU ψφ|U ϕφi = hψψ|ϕϕi. Sin embargo, por un lado
hU ψφ|U φϕi = hψφ|U † U |ϕφi = hψφ|ϕφi = hψ|ϕihφ|φi = hψ|ϕi
Mientras por el otro hψψ|ϕϕi = hψ|ϕihψ|ϕi = hψ|ϕi2
Pero si hψ|φi = hψ|φi2 , entonces hψ|φi = 0 o hψ|φi = 1, lo cual es imposible: 0 implica
que los dos vectores tomados al azar son ortogonales, y 1 que son iguales.
18 1.5. Estados de Bell

1.5. Estados de Bell

Consideremos el siguiente circuito cuántico

|xi H •
βxy
|yi
Es decir, partiendo del estado inicial |xyi, se aplica H al primer qubit. Luego se aplica
CN OT a ambos, donde el primero es el de control (marcado con el punto negro). En
otras palabras, este circuito representa la siguiente ecuación:

βxy = CN OT (H ⊗ I)|xyi

Las posibles salidas de este circuito, cuando x e y varían entre 0 y 1 son las siguientes:
H(1) 1 1 CN OT (1,2) 1
|00i −−→ √ (|0i + |1i) |0i = √ (|00i + |10i) −−−−−−→ √ (|00i + |11i) = β00
2 2 2
H(1) 1 1 CN OT (1,2) 1
|01i −−→ √ (|0i + |1i) |1i = √ (|01i + |11i) −−−−−−→ √ (|01i + |10i) = β01
2 2 2
H(1) 1 1 CN OT (1,2) 1
|10i −−→ √ (|0i − |1i) |0i = √ (|00i − |10i) −−−−−−→ √ (|00i − |11i) = β10
2 2 2
H(1) 1 1 CN OT (1,2) 1
|11i −−→ √ (|0i − |1i) |1i = √ (|01i − |11i) −−−−−−→ √ (|01i − |10i) = β11
2 2 2
Observación. β00 = (X ⊗ I)β01 = (Z ⊗ I)β10 = (XZ ⊗ I)β11 .
A estos cuatro estados se les llama Estados de Bell, en honor a John S. Bell. Estos son
estados entrelazados, es decir, estados que no pueden representarse como el producto
tensorial de dos estados individuales.
A los estados entrelazados también se les llama estados EPR por Einstein, Podolsky, y
Rosen [1935] quienes detectaron, en pleno auge de las formulaciones de la teoría cuántica,
que existía una acción a distancia que parecía no razonable. Por muchos años se llamó la
“paradoja EPR”. Lo que determinaron es que cuando se tiene un par entrelazado (física-
mente el estado representa por ejemplo el spin en un par de electrones, o la polarización
de un par de fotones), sucede que cuando se colapsa (por acción de la medición) un estado
del par, el segundo también colapsará, incluso cuando físicamente se encuentren a años
luz de distancia. Con el tiempo se demostró experimentalmente que esto es exactamente
lo que sucede, y por lo tanto no hay paradoja. También se demuestra que esto no contra-
dice la teoría de la relatividad (que entre otras cosas determina que nada puede viajar
a mayor velocidad que la luz, ni siquiera la información), ya que no hay trasmisión de
información en este colapso a distancia.
Matemáticamente la acción de medir un estado de un par se ve con el siguiente ejemplo:
Ejemplo 1.28. Consideremos el siguiente operador de medición: M = {M0 , M1 } donde
M0 = |0ih0| y M1 = |1ih1|.
Aplicando este operador al primer qubit del estado β00 , se obtiene uno de los siguientes
resultados:
Capítulo 1. Introducción a la computación cuántica 19

Si se aplica el proyector M0 (el cual lo expresamos como M0 ⊗ I para que se aplique

M0 al primer qubit y la identidad al segundo), el estado resultante será

(M0 ⊗ I)β00 (|00ih00| + |01ih01|) √12 (|00i + |11i)

p =q
p(0) √1 (h00| + h11|)(|00ih00| + |01ih01|) √1 (|00i + |11i)
2 2
√1 (|00ih00|00i)
2
=q = |00i
1
2
h00|00ih00|00i

Análogamente, si se aplica M1 se obtiene |11i

Es decir, al medir el primer qubit del estado entrelazado β00 , se obntiene |00i o |11i, es
decir que ambos qubits colapsan.

1.6. Usando los estados de Bell

Como se mencionó en la sección anterior, el colapso de un par entrelazado no transmite
información (y por eso no viola la teoría de la relatividad), sin embargo, es posible utilizar
dicho colapso como canal de comunicación, el cual necesita también de un canal clásico
para terminar la transmisión (y por ende, el canal clásico implica todas las limitaciones
impuestas por la relatividad).
El algoritmo cuántico descripto en la sección 1.6.1, descripto por primera vez por Ben-
nett y Wiesner [1992], permite transmitir dos bit clásicos, enviando sólo un bit cuántico,
utilizando un par entrelazado como canal de comunicación. Es llamado “codificación su-
perdensa” ya que se trata de codificar dos bits de información en un bit cuántico, o dicho
de otro modo: dos bits de información en el estado de una partícula cuántica.
El algoritmo descripto en la sección 1.6.2, descripto por primera vez por Bennett, Bras-
sard, Crépeau, Jozsa, Peres, y Wootters [1993], permite enviar un bit cuántico enviando
dos bit clásicos y utilizando un par entrelazado como canal de comunicación. Es llamado
“teleportación cuántica” ya que se trata de mover el valor de un bit cuántico (recorde-
mos que un bit cuántico no puede ser copiado (ver Teorema 1.27)) a otro bit cuántico, o
dicho de otro modo: se trata de teletransportar el estado de una partícula a una nueva
partícula, destruyendo la primera.

1.6.1. Codificación superdensa

El objetivo de esta técnica es transmitir 2 bits clásicos enviando tan sólo 1 qubit.
Los pasos a seguir por el emisor (a quien llamaremos “Alice”) y el receptor (a quien
llamaremos “Bob”) son los siguientes.

1. Alice y Bob preparan un estado β00 .

2. Alice se queda con el primer qubit del par y Bob se lleva el segundo. Podemos
considerar que estos dos pasos son la preparación del canal cuántico.
20 1.6. Usando los estados de Bell

Observación. El estado entrelazado no se puede separar en el sentido de que no

puede considerarse matemáticamente como un qubit multiplicado tensorialmente
por otro qubit. Debemos considerarlos como un vector del espacio C2 ⊗ C2 , es decir,
un vector de dimensión 4. Pero físicamente son un par de electrones, o fotones
(u otra partícula elemental), las cuales sí pueden ser separadas físicamente (más
allá de que no es trivial el problema experimental que representa manipular dichas
partículas sin que interaccionen con el ambiente).

3. Alice aplica una transformación a su qubit, de acuerdo a los bits que quiere enviar:
Z b1 X b2 , donde C 0 = I y C 1 = C.

4. Alice envía su qubit a Bob.

5. Bob aplica CNOT a los dos elementos del par y luego Hadamard al primero.

6. Bob realiza una medición.

El circuito completo queda de la siguiente manera

Z b1 X b2 | • H |b1 i

β00 |

| |b2 i

donde la línea punteada determina el paso 4, en el que Alice envía su qubit a Bob.
Ejemplo 1.29. Se quiere enviar los bits 11. Por lo tanto se aplica (ZX ⊗ I) a β00 , con lo
que se obtiene β11 (en general, la aplicación de la compuerta Z b1 X b2 cambia el estado β00
a βb1 b2 ):

(ZX ⊗ I)β00 = (Z ⊗ I) ((X ⊗ I)β00 )

 
1
= (Z ⊗ I) (X ⊗ I) √ (|00i + |11i)
2
 
1
= (Z ⊗ I) √ (|10i + |01i)
2
1
= √ (−|10i + |01i) = β11
2
El resto del circuito (a partir de la línea punteada vertical) es el circuito inverso al de
Bell, y como toda compuerta unitaria es tal que U = U −1 , aplicando el circuito inverso
al de Bell se obtiene los estados iniciales. En este caso, |11i.

1.6.2. Teleportación cuántica

El objetivo de esta técnica es transmitir un qubit mediante el envío de dos bits clásicos.
Los pasos a seguir por Alice y Bob son los siguientes.

1. Alice y Bob preparan un estado β00 .

Capítulo 1. Introducción a la computación cuántica 21

2. Alice se queda con el primer qubit del par y Bob se lleva el segundo.
3. Alice aplica CNOT entre el qubit a transmitir y el primero del par β00 , y luego
Hadamard al primero.
4. Alice realiza una medición sobre los dos qubits en su posesión y envía el resultado
de la medición (2 bits clásicos) a Bob.
5. Bob aplica una transformación sobre su qubit, de acuerdo a los bits recibidos:
Z b1 X b2 .
El circuito completo queda de la siguiente manera
|ψi • H

β00

Z b1 X b2 |ψi
donde |ψi es el qubit a transmitir (o “teleportar”).
Ejemplo 1.30. Se quiere transmitir el qubit |ψi = α|0i + β|1i, entonces
 
1
|ψi ⊗ β00 = (α|0i + β|1i) √ (|00i + |11i)
2
1
= √ (α|0i(|00i + |11i) + β|1i(|00i + |11i))
2
CN OT (1,2) 1
−−−−−−→ √ (α|0i(|00i + |11i) + β|1i(|10i + |01i))
2
 
H(1) 1 1 1
−−→ √ α √ (|0i + |1i)(|00i + |11i) + β √ (|0i − |1i)(|10i + |01i)
2 2 2
1
= [|00i(α|0i+β|1i) + |01i(α|1i+β|0i) + |10i(α|0i−β|1i) + |11i(α|1i−β|0i)]
2
1 1
1XX
= |b1 b2 i(X b2 Z b1 )|ψi
2 b =0 b =0
1 2

Por lo tanto, aplicando Z b1 X b2 , Bob obtendrá el estado original |ψi. (Nótese que para
toda compuerta U , U = U −1 ).
Observación. Si se quiere escribir la compuerta Z b1 X b2 como dos dos compuertas,
b b b
debe escribirse b
X2 Z 1 , ya que en Z X primero se aplica la compuerta X 2 y
b 1 2

luego Z b1 .

1.7. Paralelismo Cuántico

Consideremos una función f : {0, 1} → {0, 1}. Clásicamente para obtener todos los
resultados posibles de esta función, es necesario evaluarla tantas veces como sea el cardinal
del dominio (2 en este caso, una evaluación para la entrada 0, y otra para la entrada 1).
22 1.7. Paralelismo Cuántico

Esta es una función que toma un bit y devuelve un bit. Si fuese un bit cuántico, sería
posible evaluar la función en una superposición de 0 y 1 (por ejemplo 12 (|0i + |1i)), lo
cual nos daría como resultado una superposición de f aplicada a 0 y a 1.
El método es el siguiente. Primero se debe construir una matriz unitaria Uf de C4 que
calcule la función, de la siguiente manera:

Uf |x, 0i = |x, f (x)i

En realidad, aunque vamos a usar la definición que acabamos de dar, se debe definir
también qué sucede cuando el segundo qubit es |1i, por lo que esta compuerta se define
más generalmente como Uf |x, yi = |x, y ⊕ f (x)i, donde ⊕ es la suma módulo 2.
Lo que se pretende es aplicar f a todas las entradas posibles, por lo que primero se aplicará
Hadamard al |0i, a fin de obtener una superposición, y luego se aplicará la compuerta
Uf . El circuito es el siguiente:

|0i H
|0,f (0)i+|1,f (1)i
Uf |ψi = √
2
|0i
Es decir:
H(1) 1 1 Uf 1
|00i −−→ √ (|0i + |1i)|0i = √ (|00i + |10i) −→ √ (|0, f (0)i + |1, f (1)i)
2 2 2
La salida de este circuito es un estado que es superposición de todos los resultados posibles
de la aplicación de la función f . Y la compuerta Uf fue utilizada una sola vez. El problema
ahora pasa porque el resultado es una superposición de todos los resultados posibles, y
al querer leerlo (es decir, al medirlo), éste colapsará a uno de los dos. El problema de
los algoritmos cuánticos pasa por utilizar la superposición de manera inteligente para
aprovechar el paralelismo, pero obteniendo el resultado buscado y no una superposición
de resultados sin utilidad.
En el siguiente capítulo mostraremos algunos de los algoritmos que, haciendo uso del
paralelismo, consiguen ganancias en complejidad respecto a su contrapartida clásica.
Capítulo 2

Algoritmos cuánticos y aplicación a

criptografía

En este capítulo veremos algunos de los algoritmos cuánticos más conocidos. En particu-
lar, los algoritmos de Deutsch [1985] y de Deutsch y Jozsa [1992], que pueden considerarse
como los primeros algoritmos cuánticos que hacen uso del paralelismo (ver Sección 1.7).
El algoritmo de Grover [1996], que es uno de los que motivó que los investigadores en
computación se interesaran en el área. No se incluye el algoritmo de Shor [1997], el otro
importante algoritmo que motivó a investigadores en computación a adentrarse en el área.
Finalmente, el último ejemplo es una aplicación directa de la física cuántica en cripto-
grafía, diseñado por Bennett y Brassard [1984], la cual no sigue el esquema de los otros
algoritmos cuánticos presentados, pero es también el puntapié de un área de investigación
activa dentro de la computación cuántica.

2.1. Algoritmo de Deutsch

El objetivo de este algoritmo es saber si una función que toma un bit y devuelve un bit,
es constante o no.
El algoritmo se resume en el siguiente circuito

|0i H H
Uf
|1i H

Observación. Uf es la compuerta definida en la Sección 1.7, la cual consideraremos que

existe sin dar más detalles de su construcción.

Uf |x, yi = |x, y ⊕ f (x)i

Las primeras dos compuertas Hadamard, aplicadas a |0i y |1i, producen lo siguiente:
H(1,2) 1 1 1 1
|01i −−−→ √ (|0i + |1i) √ (|0i − |1i) = |xi √ (|0i − |1i) = √ (|x, 0i − |x, 1i) (2.1)
2 2 2 2

donde |xi = √1 (|0i + |1i) es una abreviación introducida por comodidad.

2

23
24 2.2. Algoritmo de Deutsch-Jotza

La aplicación de Uf sobre el estado (2.1) produce el siguiente estado:

1
Uf ( √ (|x, 0i − |x, 1i))
2
1
= √ (Uf |x, 0i − Uf |x, 1i)
2
  (2.2)
1 1 1
=√ √ (|0, f (0)i + |1, f (1)i) − √ (|0, 1 ⊕ f (0)i + |1, 1 ⊕ f (1)i)
2 2 2
1
= (|0, f (0)i + |1, f (1)i − |0, 1 ⊕ f (0)i − |1, 1 ⊕ f (1)i)
2
Si f (0) 6= f (1), (2.2) es igual a
  
1 |0i − |1i |0i − |1i
± (|00i + |11i − |01i − |10i) = ± √ √
2 2 2

en cambio si f (0) = f (1),

  
1 |0i + |1i |0i − |1i
± (|00i + |10i − |01i − |11i) = ± √ √
2 2 2

Es decir, el primer qubit es ±|−i, si f (0) 6= f (1) y ±|+i si f (0) = f (1). Aplicando
Hadamard al primer qubit, obtenemos |1i si éste era |−i y |0i si éste era |+i.
 
|0i − |1i
Si f (0) 6= f (1), aplicando Hadamard se obtiene ± |1i √
2
 
|0i − |1i
Si f (0) = f (1), aplicando Hadamard se obtiene ± |0i √
2
es decir, aplicando Hadamard, se obtiene
 
|0i − |1i
±|f (0) ⊕ f (1)i √
2

Dado que el primer qubit es |0i o |1i, podemos medirlo y nos dará con probabilidad 1 el
valor 0 si f es constante y con probabilidad 1 el valor 1 si f no lo es.
Observación. Este algoritmo hace uso del paralelismo, ya que la evaluación de la función se
realiza una vez sobre el estado en superposición de 0 y 1. El algoritmo clásico equivalente
haría dos evaluaciones de la función y una comparación.

2.2. Algoritmo de Deutsch-Jotza

Este algoritmo es una generalización del anterior. Dada una función que toma n bits y
devuelve uno, el algoritmo permite distinguir si la función es constante o balanceada (o
sea, con la mitad de las entradas devuelve 0 y con la otra mitad 1). Sólo se distinguen
esos dos casos, el algoritmo no es útil para otro tipo de funciones.
Capítulo 2. Algoritmos cuánticos y aplicación a criptografía 25

El circuito es el siguiente:
|0i H H

|0i H H
Uf
.. ..
. .
|1i H
La entrada de este algoritmo son n + 1 qubits: |0i⊗n |1i = |0 . . . 01i.
Aplicando las n + 1 compuertas Hadamard sobre la entrada, se obtiene
 ⊗n   X |xi  |0i − |1i 
|0i + |1i |0i − |1i
√ √ = √ √ (2.3)
2 2 2n 2
x∈{0,1}n

La compuerta Uf que se utiliza es una generalización del caso anterior definida por
Uf |x, yi = |x, y ⊕ f (x)i
donde x son cadenas de n bits.
Es decir
Uf |x, 0i = |x, f (x)i Uf |x, 1i = |x, 1 ⊕ f (x)i
Por lo tanto, aplicando Uf sobre el estado (2.3) se obtiene
 
X |xi  |0i − |1i  X 1

|0i − |1i

Uf  √ √ = √ Uf |xi √
2n 2 2n 2
x∈{0,1}n x∈{0,1}n
X 1
= √ (Uf |x, 0i − Uf |x, 1i)
2n+1
x∈{0,1}n
(2.4)
X 1
= √ (|x, f (x)i − |x, 1 ⊕ f (x)i)
x∈{0,1}n
2n+1
 
X 1 |f (x)i − |1 ⊕ f (x)i
= √ |xi √
2n 2
x∈{0,1}n

Para simplificar la notación, la compuerta Hadamard puede expresarse como sigue

)
H|0i = √12 (|0i + |1i) 1 X
1 ⇒ H|xi = √ (−1)xy |yi
H|1i = √2 (|0i − |1i) 2 y∈{0,1}

De la misma manera, es posible generalizar la aplicación de H a n qubits como sigue:

   
1 X 1 X
H ⊗n |x1 . . . xn i =  √ (−1)x1 z1 |z1 i · · ·  √ (−1)xn zn |zn i
2 z ∈{0,1} 2 z ∈{0,1}
1 n

1 X
=√ (−1)x·z |zi
n
2 z∈{0,1}n

donde x · z = x1 z1 + . . . + xn zn .
26 2.3. Algoritmo de Búsqueda de Grover

Con esta notación, se aplica Hadamard a los primeros n qubits del estado (2.4) (es decir,
al ket |xi), obteniendo
 
 
X 1  1 X
x·z |f (x)i − |1 ⊕ f (x)i
√ √ (−1) |zi √
2n 2n 2
x∈{0,1}n z∈{0,1} n
(2.5)
X X (−1)x·z |zi  |f (x)i − |1 ⊕ f (x)i 
= √
n n
2n 2
x∈{0,1} z∈{0,1}

Casos:

Si f es constante, el estado (2.5) es

X X (−1)x·z |zi  |0i − |1i 
± √
2n 2
x∈{0,1}n z∈{0,1}
n

Cuando z = 0, los primeros n qubits son

X |0i⊗n 2n ⊗n
± n
= ± n
|0i = ±|0i⊗n
n
2 2
x∈{0,1}

Por lo tanto, dado que este vector tiene norma 1, el resto de los términos de la
suma deben anularse, debido a que el resultado tiene que ser forzosamente un vector
normalizado. Por lo tanto, cuando f es constante, el estado (2.5) es
 
⊗n |0i − |1i
±|0i √
2
Es decir, midiendo los primeros n qubits se obtiene 0 . . . 0 en este caso.

Si f es balanceada (50 % de las veces devuelve 0 y 50 % devuelve 1), entonces para

z=0
X |0i⊗n  |f (x)i − |1 ⊕ f (x)i  ⊗n
 
x |0i |0i − |1i
X
√ = (−1) √ =0
n
2n 2 n
2n 2
x∈{0,1} x∈{0,1}

Es decir que los primeros n qubits no incluyen al qubit |0i⊗n , y por lo tanto, al
medir los primeros n qubits no se puede obtener 0 . . . 0 en este caso.

Conclusión: Si se obtiene |0i⊗n a la salida de la medición, la función es constante, en otro

caso la función es balanceada.

2.3. Algoritmo de Búsqueda de Grover

Antes de analizar este algoritmo, son necesarias algunas compuertas extras: la compuerta
Oráculo (Sección 2.3.1), y la compuerta de inversión sobre el promedio (Sección 2.3.2).
Capítulo 2. Algoritmos cuánticos y aplicación a criptografía 27

2.3.1. Oráculo

Dada una función de un bit en un bit f , la compuerta Uf definida en la Sección 1.7, es

Uf |x, yi = |x, y ⊕ f (x)i.
Si se elije y = |−i = √12 (|0i − |1i), entonces

 
1
Uf |x, yi = Uf |xi √ (|0i − |1i)
2
1
= √ (Uf |x, 0i − Uf |x, 1i)
2
1
= √ (|x, f (x)i − |x, 1 ⊕ f (x)i)
2
1
= |xi √ (|f (x)i − |1 ⊕ f (x)i)
2
f (x)
= (−1) |x, yi

Dado que Uf no modifica el estado y, es posible omitirlo y tomarlo como parte de la

definición de la compuerta. Entonces, definimos la compuerta

U |xi = (−1)f (x) |xi

a la cual se le llama Oráculo.

2.3.2. Inversión sobre el promedio

√ P
Sea el estado |φi = 1/ 2n x∈{0,1}n |xi. Definimos la compuerta de Inversión sobre el
promedio como G = 2|φihφ| − I. Es decir

G = 2|φihφ| − I
 1 
√
2n
= 2  ... 
 
√1 · · · √12n −I
 
2n
2n
√1
2n 2n
 2 2 2

2n
−1 2n
··· 2n
2 2 2

2n 2n
− 1 ··· 2n

=
 
.. .. .. 
 . . . 
2 2 2
2n 2n
··· 2n
− 1 2n ×2n

P
La aplicación de G sobre un estado cualquiera |ψi = x∈{0,1}n ax |xi es la siguiente
28 2.3. Algoritmo de Búsqueda de Grover

 
a0
 .. 
G|ψi  . 
a2n −1
   
X 2ax
2 2     − a0 
2 n
− 1 ···
 
 2n x∈{0,1}n
2n
 
  
 .. ..
  .. 
 . .
  . 
2 2
     
··· − 1
 X 2ax 
 
2n 2n   − a2n −1 
n
2n
x∈{0,1}

Es decir:
    
X X X 2ay X
G ax |xi =   − ax  |xi = (2A − ax )|xi
2n
x∈{0,1}n x∈{0,1}n n
y∈{0,1} x∈{0,1}n

donde A es el promedio de los ax .

2.3.3. El algoritmo
El algoritmo de Grover es un algoritmo de búsqueda sobre una lista desordenada. Supo-
nemos una lista de tamaño N , con N = 2n (observar que siempre es posible aumentar
la lista con datos irrelevantes para cumplir la condición sobre N ). Los índices de la lista
son x ∈ 0, 1n , es decir x = 0 . . . 2n − 1.
El objetivo del algoritmo es localizar el x0 tal que f (x0 ) = 1, para una función booleana
f dada.
El input del circuito es |0i⊗n .

2.3.3.1. Paso 1: Se aplica Hadamard (H ⊗n )

El primer paso es generar una superposición en todos los qubits.

H ⊗n 1 X
|0i⊗n −−→ √ |xi (2.6)
2n x∈{0,1}n

Este estado es una superposición de todos los elementos de la lista. La idea del algoritmo
es subir la probabilidad de que al medir este estado obtengamos el elemento x0 .

2.3.3.2. Paso 2: Se aplica el oráculo (U )

Aplicar el oráculo es el equivalente a aplicar la función booleana f sobre la superposición.

U 1 X
→ √
(2.6) − (−1)f (x) |xi (2.7)
2n x∈{0,1}n
Capítulo 2. Algoritmos cuánticos y aplicación a criptografía 29

2.3.3.3. Paso 3: Se aplica la inversión sobre el promedio (G)

X  (−1)f (x) 
(2.7) = √ |xi
2n
n
x∈{0,1} | {z }
ax
G
X
−
→ (2A − ax )|xi
x∈{0,1}n
  
X X (−1)f (y) (−1) f (x)
= 2 √ − √  |xi
2n 2n 2 n
x∈{0,1}n y∈{0,1}n
   (2.8)

X  X (−1)f (y)  2(−1)f (x) (−1)f (x) 

= 2 √ + √ − √  |xi
 2n 2n  2n 2n 2n 
x∈{0,1}n y∈{0,1}n
y6=x
  
X  X (−1)f (y)  2 − 2n 
= 2 √  + √ (−1)f (x)  |xi
x∈{0,1}n

y∈{0,1}n
2n 2n  2n 2n 
y6=x

En el estado (2.8), el término x = x0 , con f (x0 ) = 1, el cual estamos buscando es el

siguiente:
  
 2n − 2  n
 
 X 1 2 n 2 − 2
2 √ + √  |x0 i = √ (2 − 1) + √ |x0 i
 2n 2n  2n 2n  2n 2n 2n 2n
y∈{0,1}n
y6=x0

2n+1 + 2n − 4
 
= √ |x0 i
2n 2n

mientras que los otros términos, donde x 6= x0 , son

  

n
    n+1 n

 X 1  2(−1) 2 − 2 2 − 2 − 4
2 √   + √ + √  |xi =
 √ |xi
 y∈{0,1}n 2n 2n  2n 2n 2n 2n  2n 2n

y6=x0
y6=x

El algoritmo ha cambiado las amplitudes del estado, aumentando la amplitud del estado
x0 y disminuyendo las otras.
Repitiendo este proceso (pasos 2 y 3) se va subiendo la amplitud del estado que se
quiere encontrar y disminuyendo las otras. Sin embargo es cíclico: pasado cierto número
de repeticiones, esa amplitud vuelve a decrecer. En la Sección 2.3.4 se calcula el número
optimo de repeticiones para obtener la amplitud máxima. Cuando la amplitud es máxima,
se realiza una medición, obteniendo el estado x0 con la máxima probabilidad. En la
Sección 2.3.4 se muestra que la probabilidad de error tiene cota máxima en 1/2n .
30 2.3. Algoritmo de Búsqueda de Grover

Ejemplo
Sea una lista de 24 = 16 elementos, de los que sólo uno, x0 , verifica la propiedad f (x0 ) = 1.
El algoritmo comienza por tomar el estado |0i⊗4 y aplicar H ⊗4 obteniendo,
1 X
|xi
4 4
x∈{0,1}

Inicialmente todas las amplitudes son iguales a 1/4. Se aplica el oráculo y se obtiene
1 X
(−1)f (x) |xi
4 4
x∈{0,1}

Luego se aplica la inversión sobre el promedio, y la nueva amplitud del estado x0 será
25 + 24 − 4 11
√ = = 0,6875
24 24 16
y para el resto de los x la amplitud será
25 − 24 − 4 3
√ = = 0,1875
24 24 16
Con las sucesivas repeticiones de la aplicación del oráculo y la inversión sobre el promedio,
se obtienen las siguientes amplitudes:
Repetición Amplitud de x0 Amplitud de x 6= x0 Probabilidad de error
1 0.6875 0.1875 0.527
2 0.953125 0.078125 0.092
3 0.98046875 -0.05078125 0.039
A partir de la iteración 4 la probabilidad de error comienza a subir, por lo tanto el número
óptimo de iteraciones es 3, con una probabilidad de error de 0,039.

2.3.4. Cálculo del número óptimo de iteraciones

Luego de k iteraciones x0 tendrá una amplitud bk y el resto tendrán todos una amplitud
mk . Es decir, el estado será X
bk |x0 i + mk |xi
x∈{0,1}n
x6=x0

En cada iteración se aplica el oráculo U , el cual cambia el signo de bk , y luego G. Es

posible definir recursivamente las amplitudes en la repetición k:

1
m0 = b0 = √
2n (2n − 1)mk − bk
mk+1 = 2Ak − mk donde Ak =
2n
bk+1 = 2Ak + bk
Capítulo 2. Algoritmos cuánticos y aplicación a criptografía 31

Las fórmulas cerradas para estas recursiones son

1
mk = √ n cos((2k + 1)γ)
2 −1
bk = sen((2k + 1)γ)
r n r
2 −1 1
donde cos(γ) = n
y sen(γ) = .
2 2n
Para conseguir la mínima probabilidad de error, se debe minimizar |mk |. Notar que mk =
π π 1
0 si y sólo si (2k + 1)γ = , es decir, si k = − .
2 4γ 2
Sin embargo, dado que k es el número de repeticiones, debe ser entero, por lo tanto, el
número óptimo de iteraciones es  
π
k̃ =
4γ
1
Para calcular una cota de la probabilidad de error, observar primero que que |k − k̃| ≤ ,
2
entonces
π
| − (2k̃ + 1)γ| = |(2k + 1)γ − (2k̃ + 1)γ| = |2γ(k − k̃)| ≤ γ
2
Con esto, podemos determinar que la probabilidad de error luego de k̃ iteraciones es
π 1
(2n − 1)(mk )2 = cos2 ((2k̃ + 1)γ) = sen2 ( − (2k̃ + 1)γ) ≤ sen2 (γ) = n
2 2
En el ejemplo anterior  
 
 π 
k̃ =  q =3
1
4asen( 16 )
1
y la probabilidad de error es 0,039 ≤ = 0,0625.
24

2.4. Aplicación criptográfica

2.4.1. One-time pad
Este es un método de criptografía clásica [Vernam, 1926] que consiste en compartir una
secuencia de bits (clave) del largo del mensaje a transmitir y aplicar la operación reversible
XOR para cifrar y descifrar. (Ver Figura 2.1). Las claves deben ser secretas y no deben
ser reutilizadas.
Este método es 100 % seguro: un 0 en el mensaje encriptado puede significar un 0 en el
mensaje original y un 0 en la clave, o un 1 en el mensaje y un 1 en la clave. Lo mismo
sucede con un 1 en el mensaje encriptado. Es decir que adivinar la clave tiene la misma
probabilidad que adivinar el mensaje original. La única debilidad de este método es la
predistribución de claves, ya que el canal que se use para distribuirla podría ser vulnerado.
El método cuántico que se describe a continuación, QKD-BB84 (por Quantum Key Dis-
tribution de Bennett y Brassard [1984]), es justamente un método para la distribución
segura de claves.
32 2.4. Aplicación criptográfica

Figura 2.1: One-Time pad

2.4.2. Criptosistema Cuántico QKD-BB84

La idea es transmitir una clave binaria por un canal inseguro.
Para transmitir el bit 0, Alice (el emisor) puede elegir, al azar, la base {|0i, |1i} (a la que
llamaremos esquema +) y considerar 0 ≡ |0i, o la base {|−i, |+i} (a la que llamaremos
esquema ×) y considerar 0 ≡ |−i. Análogamente al bit 1 lo codificamos como |1i en el
esquema + o como |+i en el esquema ×.
Bob realizará una medición sobre el estado recibido eligiendo al azar entre el esquema
+ y el esquema ×. Ver ejemplo en Figura 2.2. El paso final es intercambiar información
(por un canal abierto) de los esquemas utilizados, y sólo conservar los bits producidos
usando el mismo esquema.

1 |1i 1
(1) Alice Esquema + Esquema + Bob

1 |1i 1o0
(2) Alice Esquema + Esquema × Bob

Figura 2.2: Ejemplo: (1) Alice transmite un 1 codificado mediante el esquema + y Bob
elije al azar el esquema + obteniendo un 1 (2) si Bob elige el esquema × obtiene 0 ó 1
con probabilidad 1/2.

El algoritmo paso a paso:

1. Alice comienza a transmitir una secuencia de 0 y 1, elegidos aleatoriamente, alter-
nando los esquemas + y × también aleatoriamente.
Capítulo 2. Algoritmos cuánticos y aplicación a criptografía 33

2. Bob recibe la secuencia y va alternando las mediciones entre los esquemas + y ×

aleatoriamente.

3. Alice le transmite a Bob la sucesión de esquemas empleada.

4. Bob le informa a Alice en qué casos utilizó el mismo esquema.

5. Usando solamente los bits de los esquemas idénticos a dos puntas, ambos han defi-
nido una sucesión aleatoria de bits que servirá como one-time pad de encriptación
para transmisiones futuras por cualquier canal.

Esquemas de Alice × + + × × + × +
Valores de Alice |−i |0i |0i |+i |−i |0i |−i |1i
Esquemas de Bob + × + × + + × ×
Valores de Bob |0i |+i |0i |+i |1i |0i |−i |−i
√ √ √ √
Coincidencias
Clave 0 1 0 0

6. Alice y Bob intercambian hashes de las claves (en bloques) para aceptarla o descar-
tarla.

Inviolabilidad Este protocolo es, en teoría, inviolable. Supongamos que Cliff espía el
canal de comunicación entre Alice y Bob e intenta recuperar la clave. Cliff está en la
misma situación que Bob y no conoce cuál esquema es el correcto, + o ×. Por lo tanto
elige al azar y se equivocará, en promedio, la mitad de las veces.
En el paso 5 Alice y Bob se ponen de acuerdo en cuáles valores tomar en cuenta (las coin-
cidencias de la secuencia de esquemas). Esta información no le es útil a Cliff porque sólo
en la mitad de las veces habrá usado el detector correcto, de manera que mal interpretará
sus valores finales.
Además el QKD brinda el método para que Alice y Bob puedan detectar el potencial
espionaje de Cliff:
Imaginemos que Alice envió un 0 con el esquema × (es decir, el qubit |−i). Si Cliff usa el
esquema +, colapsará el qubit a |0i o |1i. Si Bob usa el esquema × y mide |−i coincide con
lo enviado por Alice, pero si mide |+i Alice y Bob descubrirán esa discrepancia durante
el intercambio de hashes, por lo tanto descartarán el bloque.
34 2.4. Aplicación criptográfica
Capítulo 3

Introducción a la mecánica cuántica

3.1. Postulados de la mecánica cuántica

En el Capítulo 1 vimos los postulados de la mecánica cuántica sin mencionarlo, desde
un punto de vista matemático formal. Revisitaremos los mismos postulados, nombrán-
dolos como tales. Estos cuatro postulados definen el entorno matemático conocido como
mecánica cuántica.
Postulado 1 (Espacio de estados). Todo sistema físico cuántico aislado tiene
asociado un espacio vectorial complejo con producto escalar conocido como el
espacio de estados del sistema. El sistema se describe completamente por un
vector de estado, el cual es un vector unidad en el espacio de estados.

Postulado 2 (Evolución). La evolución de un sistema físico cuántico aislado se

describe por una transformación unitaria. Es decir, el estado |ψi del sistema en
el tiempo t1 se relaciona con el estado |ψ 0 i del sistema en el tiempo t2 a través
del operador unitario U , el cual sólo depende de los tiempos t1 y t2 .

|ψ 0 i = U |ψi

El postulado anterior se puede tomar con tiempo continuo, para lo cual hace falta una
ecuación diferencial, y el postulado se transforma en el siguiente:
Postulado 20 . La evolución del estado de un sistema físico cuántico aislado es
descripta por la ecuación de Shcrödinger,

d|ψi
i~ = H|ψi
dt
En esta ecuación, ~ es una constante física conocida como constante de Planck
cuyo valor debe ser determinado experimentalmente. El valor exacto no es im-
portante, en la práctica es común absorber el valor ~ en H tomando ~ = 1. El
operador H no es la compuerta Hadamard vista anteriormente sino un operador
hermítico fijo conocido como el Hamiltoniano del sistema.

35
36 3.1. Postulados de la mecánica cuántica

Postulado 3 (Medición cuántica). La medición cuántica se describe por una

colección {Mm } de matrices de medición. Dichas matrices actúan en el espacio
de estados del sistema que se mide. El índice m refiere a los resultados posibles de
la medición. Si el estado del sistema es |ψi, inmediatamente antes de la medición,
entonces la probabilidad de que el resultado m ocurra viene dado por
†
p(m) = hψ|Mm Mm |ψi

y el estado del sistema luego de la medición es

Mm |ψi
q
†
hψ|Mm Mm |ψi

Las matrices satisfacen la ecuación de completitud,

X
†
Mm Mm = I
m

La ecuación de completitud expresa el hecho de que las probabilidades suman

uno: !
X X X
† †
1= p(m) = hψ|Mm Mm |ψi = hψ| Mm Mm |ψi
m m m

Postulado 4 (Sistema compuesto). El espacio de estados de un sistema físico

compuesto es el producto tensorial de los espacios de estados de los componentes.
Más aún, si tenemos sistemas enumerados de 1 a n, donde el sistema i está en el
estado |ψi i, el estado conjunto del sistema total es

|ψ1 i ⊗ |ψ2 i ⊗ · · · ⊗ |ψn i

3.1.1. Medición proyectiva

Un caso particular del postulado 3 es el conocido como medición proyectiva. De hecho, la
medición general es equivalente a las mediciones proyectivas más operaciones unitarias.
Por lo tanto, en general, usaremos sólo mediciones proyectivas.

3.1.1.1. Preliminares
Definición 3.1 (Autovectores y autovalores). Un autovector de un operador lineal A en
un espacio vectorial dado es un vector no-nulo |vi tal que A|vi = v|vi, donde v es un
número complejo conocido como autovalor de A correspondiente a |vi.

Observación. En la definición anterior, notar que v 6= |vi. De hecho, v ∈ C y |vi ∈ C2 .

La “v” que aparece en |vi es simplemente una etiqueta, un nombre, para el vector.
Capítulo 3. Introducción a la mecánica cuántica 37

Ejemplo 3.2. Consideremos la matriz de Pauli iXZ

iXZ = i(|0ih1| + |1ih0|)(|0ih0| − |1ih1|)
= i(|0ih1|0ih0| − |0ih1|1ih1| + |1ih0|0ih0| − |1ih0|1ih1|)
= i(|1ih0| − |0ih1|)
 
0 −i
O, en su notación matricial, iXZ =
i 0
Queremos buscar un vector |vi = α|0i + β|1i tal que iXZ|vi = v|vi, para algún v, y con
k|vik = 1. Es decir:
i(|1ih0| − |0ih1|)(α|0i + β|1i) = i(α|1i − β|0i) = −βi|0i + αi|1i
debe ser igual a v(α|0i + β|1i), con |α|2 + |β|2 = 1.
Por lo tanto,
  
  βi 2 
  + |β|2 = 1
 s
|v|

 v
  
 |α|2 + |β|2 = 1  |β| =

   

vα = −βi ⇒
βi
⇒ |v| + 1
α = −

vβ = αi

 v  
 α = −βi

 βi 
 2
v =1
 vβ = − i


v
 
1 1
 |β| = √  |β| = √

 

⇒ 2 o 2

 α = −βi 
 α = −βi
 v=1  v = −1
√ √
Tomando, por ejemplo, v = 1 y β = 1/ 2 tenemos α = −i/ 2, y por lo tanto 1 es un
√
autovalor de iXZ con autovector 1/ 2(|1i − i|0i).
Definición 3.3 (Función característica). La función característica de un operador lineal
A es c(x) = det |A − xI|.
Teorema 3.4. Las soluciones a la ecuación c(x) = 0 son los autovalores del operador
A.
Ejemplo 3.5. En el ejemplo anterior, podemos ver que
c(x) = det |iXZ − xI|
= det |i(|1ih0| − |0ih1|) − x(|0ih0| + |1ih1|)|
= det | − x|0ih0| − i|0ih1| + i|1ih0| − x|1ih1||
= (−x)2 − (−i2 )
= x2 − 1
Y tenemos c(x) = 0 ⇒ x2 − 1 = 0 ⇒ x = ±1.
Definición 3.6 (Autoespacio). El autoespacio correspondiente un autovalor v de un
operador linear A es el conjunto de vectores que tienen a v como autovalor.
Ejemplo 3.7. Siguiendo con el ejemplo anterior, el autoespacio correspondiente al auto-
valor 1 del operador iXZ es {β|1i − βi|0i | β ∈ C}.
Teorema 3.8. El autoespacio de un autovalor v de un operador lineal A en un espacio
vectorial V es un subespacio vectorial de V .
38 3.1. Postulados de la mecánica cuántica

3.1.1.2. Medición proyectiva

Definición 3.9. Una medición proyectiva es descripta por un observable, M , el cual es un
operador hermítico en el espacio de estados del sistema que es objeto de la observación.
El observable tiene descomposición espectral (es decir, factorización a forma canónica)
dada por: X
M= mPm
m
donde Pm es el proyector al autoespacio de M con autovalor m. Los posibles resultados
de la medición corresponden con los autovalores m del observable. Luego de medir |ψi,
la probabilidad de obtener el resultado m viene dada por
p(m) = hψ|Pm |ψi
Al obtener el resultado m, el estado del sistema inmediatamente luego de la medición es
P |ψi
pm
p(m)
Observación. La medición proyectiva se puede ver como un caso particular del Postula-
do 3. Si a las matrices que forman el operador medición del Postulado 3 le agregamos la
condición que los Mm son hermíticos y ortogonales, es decir Mm Mm0 = δm,m0 Mm , entonces
el Postulado 3 reduce a las mediciones proyectivas que acabamos de definir.
Ejemplo 3.10. Consideremos la medición del observable Z.
c(x) = det |Z − xI| = det |(1 − x)|0ih0| − (1 + x)|1ih1|| = (1 − x)(−1 − x) = −1 + x2
Por lo tanto, las soluciones a c(x) = 0 son 1 y −1, y esos son los autovalores de Z. Dichos
autovalores corresponden a los autovectores |0i y |1i respectivamente.
Los proyectores P0 y P1 sobre los autoespacios {α|0i | α ∈ C} y {β|1i | β ∈ C} respecti-
vamente son P0 = |0ih0| y P1 = |1ih1|. Notar que
Z = |0ih0| − |1ih1|
√
Entonces, la medición de Z sobre el estado |−i = (|0i+|1i)/ 2 da como resultado 1 con
probabilidad h−|0ih0|−i = 1/2. Similarmente, se obtiene resultado −1 con probabilidad
1/2.

3.1.2. Fase
Consideremos por ejemplo el estado eiθ |ψi¬ , donde |ψi es un vector de estado, y θ es un
número real. Decimos que el estado eiθ |ψi es igual a |ψi, excepto por la fase global eiθ .
La medición sobre ambos estados es la misma: Supongamos que Mm es una matriz de
un operador de medición. Entonces las probabilidades de aplicar esa matriz vienen dadas
†
por hψ|Mm Mm |ψi y por hψ|e−iθ Mm †
Mm eiθ |ψi = hψ|Mm†
Mm |ψi­ . Por lo tanto, desde un
punto de vista observacional, ambos estados son idénticos.
Por esta razón solemos ignorar las fases globales ya que son irrelevantes a las propiedades
observacionales de sistemas físicos.
¬ iθ
e = cos θ + i sin θ (aeiθ es la llamada notación exponencial de un número complejo, donde a su
módulo y θ su argumento).
­ −iθ iθ
e e = e−iθ+iθ = e0 = 1.
Capítulo 3. Introducción a la mecánica cuántica 39

3.2. Operador densidad

Hasta ahora hemos visto la mecánica cuántica en términos de vectores de estados. Una
formulación alternativa es usando el operador densidad (o matriz densidad). Esta presen-
tación es equivalente matemáticamente, pero provee un lenguaje más conveniente para
razonar en algunos escenarios comunes que se encuentran en la mecánica cuántica.

3.2.1. Preliminares
Definición P
3.11
P(Traza). La traza de una matriz es la suma de sus elementos diagonales.
Así, si A = i j αij |ui ihuj |, la traza se define por
X
tr(A) = αii
i

Teorema 3.12. Sea A = |ψihϕ|. Entonces, tr(A) = hϕ|ψi.

P P
Demostración. Sean |ψi = i ai |ui i y |ϕi = j bj |uj i. Entonces,
X X X X
tr(A) = tr(|ψihϕ|) = tr( ai |ui i b∗j huj |) = tr( ai b∗j |ui ihuj |) = ai b∗i = hϕ|ψi
i j ij i

Ejemplos 3.13.
√ √
1. Sea A = |0ih−|. Entonces, A = 1/ 2(|0ih0| − |0ih1|) y tr(A) = 1/ 2.
√ √
Por otro lado, siguiendo el teorema, tr(A) = h0|−i = 1/ 2(h0|0i − h0|1i) = 1/ 2.

2. Sea A = |+ih−| = 1/2(|0ih0| − |0ih1| + |1ih0| − |1ih1|).

Entonces, tr(A) = 1/2 − 1/2 = 0 = h+|−i.

El siguiente corollario es muy útil para evaluar la traza de un operador.

Corolario 3.14. Sea |ψi un vector normalizado y A un operador cuántico. Entonces

tr(A|ψihψ|) = hψ|A|ψi

Demostración. Ejercicio.
Ejemplo 3.15. tr(X|0ih0|) = h0|X|0i = h0|0ih1|0i + h0|1ih0|0i = 0.

Propiedades (de la traza de una matriz). Sean A y B matrices de la misma dimensión,

U un operador unitario y λ ∈ C. Entonces

1. tr(AB) = tr(BA) 3. tr(λA) = λtr(A)

2. tr(A + B) = tr(A) + tr(B) 4. tr(U AU † ) = tr(A)

Demostración. Sólo mostramos la propiedad 4, las otras se dejan como ejercicio. De la

propiedad 1 se tiene tr(U AU † ) = tr(U † U A), y como U es unitaria, tr(U † U A) = tr(A).
40 3.2. Operador densidad

3.2.2. Conjuntos de estados cuánticos

El operador densidad provee una manera conveniente de describir un sistema cuántico en
el cual el estado no se conoce del todo.

Definición 3.16 (Operador o matriz densidad). Supongamos que un sistema cuántico

está en uno de un número de estados |ψi i, donde la probabilidad de que el estado sea |ψi i
viene dada por pi .
Decimos que el conjunto {pi , |ψi i} es el conjunto de estados puros. El operador densidad
o matriz densidad para este estado viene dado por la ecuación
X
ρ= pi |ψi ihψi |
i

Ejemplo 3.17. El operador densidad del conjunto de estados puros {(1/4, |+i); (3/4, |1i)}
tiene operador densidad

ρ = 1/4|+ih+| + 3/4|1ih1| = 1/8|0ih0| + 1/8|0ih1| + 1/8|1ih0| + 7/8|1ih1|

Es decir  
1/8 1/8
ρ= 1/8 7/8

Observación. Todos los postulados de la mecánica cuántica se pueden reformular en tér-

minos del operador densidad, y haremos eso más adelante en esta sección.

Evolución Supongamos que la evolución de un sistema cuántico cerrado se describe por

el operador unitario U . Si el sistema estaba inicialmente en el estado |ψi i con probabilidad
pi , entonces, luego de la evolución el sistema estará en estado U |ψi i con probabilidad pi .
Por lo tanto, la evolución del operador densidad se describe por

U
X X
ρ= pi |ψi ihψi | −
→ pi U |ψi ihψi |U † = U ρU †
i i

Ejemplo 3.18. Siguiendo con el Ejemplo 3.17, tomemos U = H, entonces el conjunto de

estados puros original {(1/4, |+i); (3/4, |1i)} evolucionará a {(1/4, |0i); 3/4, |−i)} y su matriz
densidad puede calcularse de dos maneras equivalentes:

1. A partir del conjunto de estados puros:

 
0
5/8 −3/8
ρ = 1/4|0ih0| + 3/4|−ih−| = 5/8|0ih0| − 3/8|0ih1| − 3/8|1ih0| + 3/8|1ih1| =
−3/8 3/8

2. O utilizando la igualdad dada más arriba: ρ0 = HρH † = HρH.

Capítulo 3. Introducción a la mecánica cuántica 41

Medición Supongamos que realizamos una medición descripta por las matrices Mm . Si
el estado inicial era |ψi i, entonces la probabilidad de obtener el resultado m es

† Cor.3.14 †
p(m|i) = hψi |Mm Mm |ψi i = tr(Mm Mm |ψi ihψi |)

Usando la ley de probabilidades totales, la probabilidad de obtener el resultado m es

X
p(m) = p(m|i)pi
i
X
†
= pi tr(Mm Mm |ψi ihψi |)
i
X
†
= tr( pi Mm Mm |ψi ihψi |)
i
X
†
= tr(Mm Mm pi |ψi ihψi |)
i
†
= tr(Mm Mm ρ)

Si el estado inicial era |ψi i, el estado luego de obtener el resultado m será

Mm |ψi i
|ψim i = q
†
hψi |Mm Mm |ψi i

Por lo tanto, luego de una medición que de resultado m tendremos el conjunto de estados
|ψim i, con probabilidades p(i|m) respectivamente. Por lo tanto, el operador densidad ρm
correspondiente es
†
X X Mm |ψi ihψi |Mm
ρm = p(i|m)|ψim ihψim | = p(i|m) †
(3.1)
i i hψi |Mm Mm |ψi i

Pero, usando teoría de probabilidad condicional,

† †
p(m ∩ i) p(m|i)pi tr(Mm Mm |ψi ihψi |) hψi |Mm Mm |ψi i
p(i|m) = = = pi †
= p i †
p(m) p(m) tr(Mm Mm ρ) tr(Mm Mm ρ)

Substituyendo en (3.1), obtenemos

† †
X Mm |ψi ihψi |Mm Mm ρMm
ρm = pi †
= †
i tr(Mm Mm ρ) tr(Mm Mm ρ)

Ejemplo 3.19. Volviendo al conjunto de estados del Ejemplo 3.17, tenemos

ρ = 1/8|0ih0| + 1/8|0ih1| + 1/8|1ih0| + 7/8|1ih1|

que corresponde a la matriz densidad del conjunto de estados {( 41 , |+i); ( 34 , |1i)}.

Utilizaremos la medición proyectiva {P0 , P1 } con P0 = |0ih0| y P1 = |1ih1|.
42 3.2. Operador densidad

Entonces, la probabilidad de medir 0 viene dada por

tr(P0† P0 ρ) = |0ih0|(1/8|0ih0| + 1/8|0ih1| + 1/8|1ih0| + 7/8|1ih1|)

= tr(1/8|0ih0| + 1/8|0ih1|)
= 1/8 tr(|0ih0|) + 1/8 tr(|0ih0|)
= 1/8

Similarmente, la probabilidad de medir 1 por

tr(|1ih1|ρ) = 1/8 tr(|1ih0|) + 7/8 tr(|1ih1|) = 7/8

Podemos ver que el conjunto de estados está en el estado |1i con probabilidad 3/4. Si ese
es efectivamente el estado inicial, la probabilidad de medir 1 sería 1. Por otro lado, en el
estado |+i, la probabilidad de medir 1 es 1/2. De ahí que la probabilidad de medir 1 es

3/4 × 1 + 1/4 × 1/2 = 7/8

tal y como dedujimos con la traza.

Luego de realizar la medición, si se midió 1, el estado del sistema podrá ser descripto por
el operador siguiente:
P1 ρP1† 7/8|1ih1|
ρ1 = 7 = = |1ih1|
/8 7/8

Efectivamente, si se midió 1 y el estado inicial era |+i, el estado final será |1i, pero lo
mismo pasa si el estado inicial era |1i, por lo que la matriz densidad es la matriz densidad
del conjunto de estados {1, |1i}.

Definición 3.20. Un sistema cuántico donde el estado |ψi se conoce exactamente se dice
que está en un estado puro. En este caso, el operador densidad es simplemente ρ = |ψihψ|.
Si no es un estado puro, ρ está en un estado mixto (o mezcla), o que es una mezcla de
diferentes estados puros.

Teorema 3.21. Para todo operador densidad ρ se tiene tr(ρ2 ) ≤ 1.

Más aún, la igualdad se cumple si y sólo si ρ está en un estado puro

Demostración. Ejercicio.

Teorema 3.22. Un estado cuánticoP que está en estado ρi con probabilidad pi , puede ser
descripto por la matriz densidad i pi ρi .

Demostración. Supongamos que ρi viene de un conjunto {pij , |ψij i} de estados puros (con
i fijo). Por lo tanto, la probabilidadP estar en el estado |ψP
de P ij i viene dada por pi pij . Es
decir que la matriz densidad es ρ = i j pi pij |ψij ihψij | = i pi ρi .

3.2.3. Propiedades generales del operador densidad

Definición 3.23 (Operador positivo). Un operador A se dice positivo si para todo vector
|ψi, hψ|A|ψi ≥ 0. Si hψ|A|ψi > 0 para todo |ψi =
6 0, decimos que A es definido positivo.
Capítulo 3. Introducción a la mecánica cuántica 43

Teorema 3.24. Si A es un operador positivo, entonces existe una descomposición A =

+
P
j λj |jihj| donde los vectores |ji son ortonormales y λj ∈ R0 son autovalores de A.

Teorema 3.25 (Caracterización de operadores densidad). Un operador ρ es el operador

densidad de un conjunto {pi , |ψi i} si y sólo si satisface las siguientes condiciones:

1. tr(ρ) = 1

2. ρ es un operador positivo

Demostración.
P
⇒) Sea ρ = i pi |ψi ihψi | un operador densidad. Entonces,

P P
1. tr(ρ) = i pi tr(|ψi ihψi |) = i pi = 1.
2. Sea |ϕi un vector arbitrario en el espacio de estados. Entonces,
!
X X X
hϕ|ρ|ϕi = hϕ| pi |ψi ihψi | |ϕi = pi hϕ|ψi ihψi |ϕi = pi |hϕ|ψi i|2 ≥ 0
i i i

⇐) Sea ρ cualquier operador positivo

Pcon traza igual a 1. Como ρ es positivo, usando
el Teorema 3.24 tenemos ρ = j λj |jihj|, donde los vectores |ji son ortogonales
y λj ∈ R+
P
0 son autovalores de ρ. Por la condición de traza 1, tenemos j λj = 1.
Por lo tanto, un sistema en el estado |ji con probabilidad λj tendrá un operador
de densidad ρ.

El Teorema 3.25 nos permite reformular el Postulado 1 para no depender de vectores, y

podemos entonces escribir todos los postulados en términos del operador densidad.
Postulado 1. Todo sistema físico cuántico aislado tiene asociado un espacio
vectorial complejo con producto escalar conocido como el espacio de estados del
sistema. El sistema se describe completamente por su operador densidad, el cual
es un operador positivo ρ con traza 1, que actúa en el espacio de estados del
P en estado ρi con probabilidad pi , entonces el
sistema. Si un sistema cuántico está
operador densidad del sistema es i pi ρi .

Postulado 2. La evolución de un sistema físico cuántico aislado se describe por

una transformación unitaria. Es decir, el estado ρ del sistema en el tiempo t1
se relaciona con el estado ρ0 del sistema en el tiempo t2 a través del operador
unitario U , el cual sólo depende de los tiempos t1 y t2 .

ρ0 = U ρU †
44 3.2. Operador densidad

Postulado 3. La medición cuántica se describe por una colección {Mm } de

matrices de medición. Dichas matrices actúan en el espacio de estados del sistema
que se mide. El índice m refiere a los resultados posibles de la medición. Si
el estado del sistema es ρ, inmediatamente antes de la medición, entonces la
probabilidad de que el resultado m ocurra viene dado por
†
p(m) = tr(Mm Mm ρ)

y el estado del sistema luego de la medición es

†
Mm ρMm
†
tr(Mm Mm ρ)

Las matrices satisfacen la ecuación de completitud,

X
†
Mm Mm = I
m

Postulado 4. El espacio de estados de un sistema físico compuesto es el producto

tensorial de los espacios de estados de los componentes. Más aún, si tenemos
sistemas enumerados de 1 a n, donde el sistema i está en el estado ρi , el estado
conjunto del sistema total es ρ1 ⊗ ρ2 ⊗ · · · ⊗ ρn .

3.2.4. El operador densidad reducido

Uno de los usos más interesantes del operador densidad es para describir subsistemas
de un sistema cuántico compuesto. Tal descripción viene dada por el operador densidad
reducido.

Definición 3.26. Sean A y B dos sistemas físicos tales que su estado es descripto por el
operador densidad ρAB . El operador densidad reducido para A se define por

ρA = trB (ρAB )

donde trB es la traza parcial sobre el sistema B, y es un operador lineal definido por

trB (|a1 iha2 | ⊗ |b1 ihb2 |) = |a1 iha2 |tr(|b1 ihb2 |) = hb2 |b1 i|a1 iha2 |

para todo |a1 i, |a2 i en el espacio de estados de A y |b1 i, |b2 i en el espacio de estados de
B.

Ejemplos 3.27. Supongamos que tenemos un sistema cuántico en el estado ρAB = ρ ⊗ σ,

donde ρ es el operador densidad del sistema A y σ el del sistema B. Entonces,

ρA = trB (ρ ⊗ σ) = ρtr(σ) = ρ

Similarmente, ρB = σ.
Capítulo 3. Introducción a la mecánica cuántica 45

√
Un ejemplo menos trivial es el estado de Bell β00 = 1/ 2(|00i + |11i), que tiene el siguiente
operador densidad
  
|00i + |11i h00| + h11| |00ih00| + |11ih00| + |00ih11| + |11ih11|
ρ= √ √ =
2 2 2

Haciendo la traza sobre el segundo qubit obtenemos el operador densidad del primer
qubit:

ρ1 = tr2 (ρ)
tr2 (|00ih00|) + tr2 (|11ih00|) + tr2 (|00ih11|) + tr2 (|11ih11|)
=
2
tr2 (|0ih0| ⊗ |0ih0|) + tr2 (|1ih0| ⊗ |1ih0|) + tr2 (|0ih1| ⊗ |0ih1|) + tr2 (|1ih1| ⊗ |1ih1|)
=
2
h0|0i|0ih0| + h0|1i|1ih0| + h1|0i|0ih1| + h1|1i|1ih1|
=
2
|0ih0| + |1ih1|
=
2
I
=
2

Notar que este es un estado mixto, ya que tr((I/2)2 ) = 1/2 < 1. Es decir que al estar
enredados, por más que el estado de dos qubits sea un estado puro, el primer qubit sólo
está en un estado mixto: es decir, un estado que no conocemos completamente.

3.2.4.1. Teleportación cuántica y el operador densidad reducido

Podemos usar el operador densidad reducido para analizar el algoritmo de teleportación.

Cuando presentamos el algoritmo de teleportación (Sección 1.6.2) dijimos que no contra-
dice la teoría de la relatividad (que entre otras cosas determina que nada puede viajar a
mayor velocidad que la luz, ni siquiera la información), ya que no hay trasmisión de infor-
mación hasta que Alice no le envía (usando un canal clásico) el resultado de la medición
a Bob. Podemos hacer esta afirmación de manera más rigurosa utilizando el operador
densidad reducido.
Antes de que Alice haga la medición, el estado del sistema es

1
(|00i(α|0i + β|1i) + |01i(α|1i + β|0i) + |10i(α|0i − β|1i) + |11i(α|1i − β|0i))
2

por lo que al medir los dos primeros qubits, se obtendrá

|00i(α|0i + β|1i) con probabilidad 1/4

|01i(α|1i + β|0i) con probabilidad 1/4

|10i(α|0i − β|1i) con probabilidad 1/4

|11i(α|1i − β|0i) con probabilidad 1/4

46 3.2. Operador densidad

Por lo tanto, el operador densidad del sistema es

1
ρ = (|00ih00|(α|0i + β|1i)(α∗ h0| + β ∗ h1|)
4
+|01ih01|(α|1i + β|0i)(α∗ h1| + β ∗ h0|)
+|10ih10|(α|0i − β|1i)(α∗ h0| − β ∗ h1|)
+|11ih11|(α|1i − β|0i)(α∗ h1| − β ∗ h0|))

Por lo tanto, si hacemos la traza parcial sobre el sistema de Alice, obtenemos que operador
densidad del sistema de Bob es
1
ρB = ((α|0i + β|1i)(α∗ h0| + β ∗ h1|) + (α|1i + β|0i)(α∗ h1| + β ∗ h0|)
4
+ (α|0i − β|1i)(α∗ h0| − β ∗ h1|) + (α|1i − β|0i)(α∗ h1| − β ∗ h0|))
2(|α|2 + |β|2 )|0ih0| + 2(|α|2 + |β|2 )|1ih1|
=
4
|0ih0| + |1ih0|
=
2
I
=
2
Por lo tanto, el estado de Bob después de que Alice hizo la medición, pero antes de que
Bob obtuvo el resultado de esa medición es I/2. Este estado no depende del estado |ψi que
se transmitió, y por lo tanto, cualquier medición que haga Bob no contendrá información
sobre |ψi, lo que previene que Alice use la teleportación para enviar información a mayor
velocidad que la luz.
Capítulo 4

Introducción al lambda cálculo y a la

teoría de tipos

4.1. PCF no tipado

En lugar de comenzar con lambda cálculo, veremos PCF (Programming language for
computable functions ¬ ). PCF se puede ver como una extensión al lambda cálculo con
algunas construcciones prácticas como números naturales y el operador de punto fijo.
Dichas construcciones no son necesarias, ya que es posible codificar todas ellas en lambda
cálculo, sin embargo, harán el razonamiento más sencillo.
Gran parte del material de este capítulo ha sido tomado del libro de Dowek y Lévy [2011].

4.1.1. Primeras definiciones

Dos construcciones de base:

• Construcción explícita de función (sin nombre): λx.t.

• Aplicación de una función a un argumento: tu.

Una constante para cada número natural.

Operaciones: +, −, ×, /­ .

Test a cero: isZ(t)?u : v devuelve u si t es 0 y v si t es > 0.

Observaciones.

Todo es función: Una función tomando un argumento constante u otra función, es lo

mismo. Por ejemplo, la función que toma una función y la compone consigo misma,
es
λf.λx.f (f x)
¬
PCF es un lenguaje de programación para funciones computables, basado en la lógica de Scott para
funciones computables LCF [Plotkin, 1977].
­
Dado que sólo usamos naturales, consideraremos que n − m = 0 si m > n, y / representa la división
euclidiana (con resto), donde la división por 0 simplemente no está definida.

47
48 4.1. PCF no tipado

No existen funciones que tomen varios argumentos. Por ejemplo, f (x, y) = x2 + y 2 ,

en PCF se escribe
λx.λy.x × x + y × y
| {z }
F

F 3 es una función que espera un argumento para elevarlo al cuadrado y sumarle 9.

La aplicación asocia a la izquierda: F 34 = (F 3)4.

El punto (.) de la construcción λ y los dos puntos (:) de la construcción isZ()? : son
equivalentes a paréntesis de apertura que cierran lo más a la derecha posible.
Ejemplo: λx.(isZ(x)?t : rs)u es λx.((isZ(x)?t : (rs))u).

Recursión

¿Cómo escribiríamos la función factorial en PCF?

λn.isZ(n)?1 : n × (F act}(n − 1))

| {z
?

En PCF hay un símbolo (palabra clave) “µ” que liga una variable en su argumento tal
que µf.G es el punto fijo® de λf.G.

µf.G = (λf.G)(µf.G)

Por lo tanto,
F act = µf. λn.isZ(n)?1 : n × (f (n − 1))
| {z }
G

Ejemplo 4.1.

F act 2 = (µf.G)2
= ((λf.G)F act)2
= (λn.isZ(n)?1 : n × F act(n − 1))2
= isZ(2)?1 : 2 × F act 1
= 2 × F act 1
= 2 × (µf.G)1
= 2 × ((λf.G)F act)1
= 2 × (λn.isZ(n)?1 : n × F act(n − 1))1
= 2 × isZ(1)?1 : 1 × F act 0
=2×1
=2
®
En matemáticas, x es el punto fijo de f si y sólo si f (x) = x.
Capítulo 4. Introducción al lambda cálculo y a la teoría de tipos 49

Let
La construcción let no es necesaria, pero será útil más adelante y por lo tanto también la
vamos a considerar:
let x = t in u
es equivalente a (λx.u)t.

4.1.2. Gramática de PCF

Los términos válidos de PCF los podemos describir con una gramática formal:
t ::= x | λx.t | tt | n ∈ N | t + t | t − t | t ∗ t | t/t
| isZ(t)?t : t | µx.t | let x = t in t
PCF es Turing completo, es decir que todas las funciones de enteros computables son
programables en PCF.

4.1.3. Semántica operacional

La gramática nos dice qué términos podemos escribir sintácticamente. La semántica ope-
racional nos da el significado de los términos, al definir como operan.
Las siguientes reglas tienen la forma t → u, y se lee “t reduce a u”:
(λx.u)t → u[t/x] (β reducción)
pq →n Si p  q = n, con  = +, −, ∗ o /
isZ(0)?t : u → t
isZ(1)?t : u → u
µx.t → t[µx.t/x]
let x = t in u → u[t/x]
También tendremos reglas de congruencia que permitirán reducir un término dentro de
otro:
t→u t→u t→u t→u t→u
tv → uv vt → vu λx.t → λx.u tv →uv vt→vu
Ejercicio: escribir las que faltan.
Observación. La tercera regla, que permite reducir dentro de la función, corresponde a
la posibilidad de optimizar programas.

4.1.4. No terminación
Ejemplos 4.2.
1. µx.x → x[µx.x/x] = µx.x
2. Sin µ: Ω = (λx.xx)(λx.xx) → xx[λx.xx/x] = (λx.xx)(λx.xx) = Ω
Ejercicio:
(µf.λx.f x)0
¿Termina?
50 4.1. PCF no tipado

Fix sin µ

Y = λf.(λx.f (xx))(λx.f (xx))

Sea F una función cualquiera:

Y F → (λx.F (xx))(λx.F (xx)) → F (Y F )

¡Y F es el punto fijo de F !

µf.G → (λf.G)(µf.G)
| {z } | {z } | {z }
YF F YF

Ejercicio: escribir el factorial sin usar µ.

4.1.5. Captura de variables

Ejercicio: Reducir los siguientes términos
1. (λx.λx.x)23

2. (λx.λy.((λx.(x + y))x)54

3. let x = 4 in 


let f = λy.y + x in En las primeras versiones de Lisp, este
let x = 5 in 
 ejemplo daba 11 en lugar de 10.

f6


Tenemos que definir precisamente qué significa t[u/x]. Damos una definición inductiva:

x[u/x] = u
y[u/x] = y
(λx.t)[u/x] = λx.t
(λy.t)[u/x] = λy.t[u/x] Si y ∈
/ FV(u)
(λy.t)[u/x] = λz.t[z/y][u/x] Si y ∈ FV(u)
(tv)[u/x] = t[u/x]v[u/x]
n[u/x] = n
(t  v)[u/x] = t[u/x]  v[u/x]
(isZ(t)?v1 : v2 )[u/x] = isZ(t[u/x])?v1 [u/x] : v2 [u/x]
(µx.t)[u/x] = µx.t
(µy.t)[u/x] = µy.t[u/x] Si y ∈
/ FV(u)
(µy.t)[u/x] = µz.t[z/y][u/x] Si y ∈ FV(u)
(let x = t in v)[u/x] = let x = t[u/x] in v
(let y = t in v)[u/x] = let y = t[u/x] in v[u/x] Si y ∈
/ FV(u)
(let y = t in v)[u/x] = let y = t[u/x] in v[z/y][u/x] Si y ∈ FV(u)
Capítulo 4. Introducción al lambda cálculo y a la teoría de tipos 51

Ejercicio: Definir, por inducción sobre t, FV(t).

Ejercicio: Definir, por inducción sobre t, BV (t), es decir, el conjunto de variables ligadas
de t (“bounded variables”).

4.2. Estrategias de reducción

4.2.1. Primeras definiciones
Definición 4.3. Notamos →∗ al cierre reflexivo y transitivo de →. Es decir, si t →∗ u,
entonces, t = v0 → v1 → v2 → · · · → vn = u, con n ≥ 0. Notamos →+ al cierre transitivo
de →. Es decir, si t →∗ u, t = v0 → v1 → · · · → vn = u, con n ≥ 1.

Ejemplo 4.4. (λx.x + 2)1 →∗ 3 porque (λx.x + 2)1 → 1 + 2 → 3.

También, (λx.x + 2)1 →+ 3, ya que (λx.x + 2)1 6= 3.

Definición 4.5.

1. Un término t está en forma normal si no existe u tal que t → u.

2. Un término t es normalizable (o tiene forma normal) si existe u en forma normal

tal que t →∗ u.

3. Un término t es fuertemente normalizable si no existe una secuencia infinita v0 , v1 ,

. . . tal que t → v0 → v1 → . . . . Es decir, toda secuencia de reducción comenzada
en t debe ser finita y terminar en un término en forma normal.

Definición 4.6. Sea →R una relación binaria, y →∗R su cierre reflexivo y transitivo.

→R satisface la propiedad del diamante si t →R v1 y t →R v2 t

implica que v1 →R u y v2 →R u para algún u.
v1 v2

u
→R es Church-Rosser o confluente si →∗R satisface la propiedad del diamante. Es
decir, si t →∗R v1 y t →∗R v2 implica que v1 →∗R u y v2 →∗R u para algún u.

→R tiene formas normales únicas si t →∗R v1 y t →∗R v2 , para términos en forma

normal v1 y v2 , implica v1 = v2 .

Lema 4.7.

1. Si →R satisface la propiedad del diamante, entonces es Church-Rosser.

2. Si →R es Church-Rosser, entonces tiene formas normales únicas.

Demostración. Ejercicio.

Teorema 4.8. La relación definida en la Sección 4.1.3 (semántica operacional de PCF)

es Church-Rosser.
52 4.2. Estrategias de reducción

Ejemplo 4.9. (λx.((λy.x + y)2))3

(λx.x + 2)3 (λy,3 + y)2

2+3
Pero esta propiedad, cuando hay términos que no terminan, no es suficiente. Por ejemplo:

F act = µf. λn.isZ(n)?1 : n ∗ f (n − 1) = µf.G

| {z }
G

Entonces:

F act 0 = (µf.G)0
→ (G[F act/f ])0
→ (G[G[F act/f ]/f ])0
→ (G[G[G[F act/f ]/f ]/f ])0
→ ··· → ∞

F act 0 tiene un único resultado, pero no cualquier camino llega a él.

Solución (en este caso): cuando hay un ifz, reducir primero el ifz antes que sus ramas.
Ésto, como veremos luego, es una estrategia.
Otro ejemplo:

C0 = λx,0
b1 = (µf.λx.f x)0

Entonces,

b1 = (µf.λx.f x)0 → (λx.(µf.λx.f x)x)0 → (µf.λx.f x)0 = b1

| {z }
b2

Es decir,
b 1 → b2 → b1 → b2 → · · ·
Por lo tanto, tenemos el siguiente diagrama:

C 0 b1 0

C 0 b2 C 0 b1 C 0 b2 C 0 b1 ...

En Caml,

let rec f x = f x in
let g x = 0 in
g (f 0)
Capítulo 4. Introducción al lambda cálculo y a la teoría de tipos 53

no termina nunca.
Mismo ejemplo en Java:

class Omega {
static int f (int x) {return f(x);}
static int g (int x) {return 0;}
static public void main (String [] args) {
System.out.println (g(f(0)));
}
}

La noción de estrategia de reducción permite definir el orden en el cual se debe reducir

un término.

Definición 4.10. Llamamos redex (por Red ucible Ex pression) a un subtérmino de un

término que puede reducir.

4.2.2. Reducción débil

Ejemplo motivador:

(λx.x + (4 + 5))3 3 + (4 + 5) 3+9 12

(λx.x + 9)3

La dirección → dice qué sucede cuando se ejecuta el programa.

La dirección ↓ comienza a ejecutar el programa antes de recibir los argumentos, es

decir, no ejecuta el programa sino que lo optimiza.

Definición 4.11. Una estrategia de reducción es débil si no reduce nunca el cuerpo de

una función, es decir, si no reduce bajo λ.

Observación. La estrategia débil no optimiza programa, los ejecuta. Sólo hace falta para
ésto eliminar la regla
t→u
λx.t → λx.u

4.2.3. Call-by-name

C 0 b1 0

C 0 b2 C 0 b1 C 0 b2 C 0 b1 ...
54 4.3. PCF tipado

Definición 4.12. La estrategia call-by-name reduce siempre el radical más a la izquierda.

En caso de ser además débil, será el más a la izquierda que no esté debajo de un λ.
Teorema 4.13 (Estandarización). Si un término reduce a un término en forma normal,
entonces la estrategia call-by-name termina.
Una ventaja de ésta estrategia es el teorema de estandarización. Otra ventaja es que si
tenemos, por ejemplo (λx,0)(Fact 10) no necesitamos calcular el factorial de 10. Por otro
lado, si tenemos (λx.x + x)(Fact 10), tendremos que calcular el factorial de 10 dos veces.
De todas maneras, la mayoría de los lenguajes que usan call-by-name usan alguna manera
de “compartir” información (por ejemplo, con punteros que dicen que (λx.x + x)(Fact 10)
reduce a x + x, donde x es un puntero a Fact 10. A eso se le llama reducción lazy.
Ejercicio: Escribir las reglas de reducción y congruencia que implementan call-by-name.

4.2.4. Call-by-value
C 0 b1 0

C 0 b2 C0 b 1 C 0 b2 C 0 b1 ...

Definición 4.14. A los términos t de PCF tales que FV(t) = ∅ y que t esté en forma
normal, se les llaman valores.
Definición 4.15. La estrategia call-by-value consiste en evaluar siempre los argumentos
antes de pasarlos a la función. La idea es que
(λx.t)v
reduce sólo cuando v esté en forma normal (si la estrategia es débil, y sólo reducimos
términos cerrados, v es un valor).
En (λx.x + x)(Fact 10) comenzamos por reducir el factorial, obtenemos 3628800 y recién
ahí lo pasamos a la función. De esa manera el factorial es calculado una vez.
Ejercicio: Escribir las reglas que implementan call-by-value.
Observación. Un poco de pereza es necesaria: ifz siempre debe evaluar primero la condi-
ción, estemos en call-by-name o call-by-value.

4.3. PCF tipado

4.3.1. Introducción
Ejemplos motivadores:
(λx.x + 1)λx.x + 2 → (λx.x + 2) + 1
isZ(λx.x)?0 : 1 6→
(λx.x)1λx.x → 1λx.x
Capítulo 4. Introducción al lambda cálculo y a la teoría de tipos 55

¡Todo es aplicable a todo! Sin restricciones. Sumar 1 a una función no tiene sentido. Hacer
un ifz sobre algo que no es un número o pasarle un argumento a un número, tampoco.
Idea: detectar este tipo de errores sintácticamente. Por ejemplo:

λx.x recive un argumento y devuelve lo mismo 1 es una constante

(λx.x)1 es una constante

Es decir, deducimos que no tiene sentido pasarle un argumento a (λx.x)1, ya que es una
constante, y lo dedujimos sin tener que ejecutar el programa.

En matemáticas:

Función: Dominio Codominio

Cualquier conjunto

Ejemplo:

f : Pares → N
x
f (x) 7→
2
¿Está bien definido f (3 + (4 + 1))? Hay que determinar si 3 + (4 + 1) pertenece al dominio,
es decir, si es par.
En general, determinar si un objeto cualquiera pertenece a un conjunto cualquiera es un
problema indecidible.
De todas maneras, x2 lo podemos calcular si x es un número (y no, por ejemplo, una
función), y poco importa si es par o no. Así que vamos a restringir las clases de conjuntos
que se pueden utilizar como dominios. A estos conjuntos los llamamos tipos.

4.3.2. Gramática de PCF tipado

Definición 4.16. Los tipos de PCF los definimos inductivamente por:

nat (es decir N) es un tipo.

Si A y B son tipos, A ⇒ B es un tipo que representa las funciones de A en B.

Teniendo tipos, tendremos que escribir de qué tipo son cada una de las variables. Como
sólo nos vamos a interesar en términos sin variables libres (sólo los subtérminos tendrán
variables libres), es suficiente con escribir el tipo cuando se liga la variable. Por ejemplo,
en lugar de λx.x la función identidad es una para cada tipo:

λx : nat.x es la identidad sobre los naturales

λx : nat ⇒ nat.x es la identidad sobre las funciones de naturales en naturales.

56 4.3. PCF tipado

En µ y let también es necesario marcar el tipo de la variable ligada.

La gramática de PCF tipado la definimos con una gramática de tipos y una de términos,
de la siguiente manera:

A ::= nat | A ⇒ A
t ::= x | λx : A.t | tt | n | t  t | isZ(t)?t : t | µx : A.t | let x : A = t in t

donde  = +, −, ×, / y n ∈ N.

4.3.3. La relación de tipado

Queremos definir inductivamente la relación t : A (es decir, el término t tiene el tipo A).
Pero si hay variables libres en t, ¿cómo las tipo?¯ .
Por ejemplo:
λx : nat.yx
¿Qué tipo tiene y? Claramente tiene que ser una función de nat en algo, pero ¿cómo
defino ese algo?

Contextos Un contexto nos da tipos para variables, entonces, en vez de decir λx :

nat.yx : nat ⇒ nat, decimos, si y : nat ⇒ nat, entonces λx : nat.yx : nat ⇒ nat. La
notación que usamos es la siguiente:

y : nat ⇒ nat ` λx : nat.yx : nat ⇒ nat

| {z }
contexto

Genéricamente, queremos definir la relación Γ ` t : A que asocia un término t y un

contexto Γ a un tipo A.

Definición 4.17. La relación de tipado Γ ` t : A se define inductivamente por:

axv axc
Γ, x : A ` x : A Γ ` n : nat
Γ, x : A ` t : B Γ ` t : A ⇒ B Γ ` u : A ⇒e
⇒i
Γ ` λx : A.t : A ⇒ B Γ ` tu : B

Γ ` t : nat Γ ` u : nat  Γ ` t : nat Γ ` u : A Γ ` v : A

ifz
Γ ` t  u : nat Γ ` isZ(t)?u : v : A
Γ, x : A ` t : A Γ, x : A ` t : B Γ ` u : A
µ let
Γ ` µx : A.t : A Γ ` let x : A = u in t : B

Donde  son cuatro reglas, una para cada operación aritmética.

¯
Dijimos que sólo vamos a interesarnos por términos cerrados (sin variables libres), pero como busca-
mos una definición inductiva, necesitamos poder tipar cada subtérmino, y un subtérmino de un término
sin variables libres, puede perfectamente tener variables libres.
Capítulo 4. Introducción al lambda cálculo y a la teoría de tipos 57

Ejemplo 4.18. Tipar λx : nat ⇒ nat.x((λy : nat.y + 2)3).

Sean ∆ = x : nat ⇒ nat, y Γ = ∆, y : nat. Entonces,
axv axc
Γ ` y : nat Γ ` 2 : nat
+
Γ ` y + 2 : nat
⇒i axc
∆ ` λy : nat.y + 2 : nat ⇒ nat ∆ ` 3 : nat
axv ⇒e
∆ ` x : nat ⇒ nat ∆ ` (λy : nat.y + 2)3 : nat
⇒e
∆ ` x((λy : nat.y + 2)3) : nat
⇒i
` λx : nat ⇒ nat.x((λy : nat.y + 2)3) : (nat ⇒ nat) ⇒ nat

Ejercicio 1: tipar factorial.

Ejercicio 2: tipar λx : A.xx para algún A.

4.3.4. Correctitud
Si deducimos el tipo A para un término (usando la Definición 4.17), o sea, sin ejecutar
el programa, y luego ejecutamos el programa obteniendo u, entonces queremos que el
término u tienga el mismo tipo, ya que la intención fue desde el principio saber qué
tipo de resultado voy a tener al ejecutar un programa (un número, una función, etc). El
teorema de subject reduction o de conservación de tipos (Teorema 4.20) nos asegura eso
en el sistema que acabamos de definir. Para demostrar este teorema necesitaremos un
resultado previo (Lema 4.19).

Lema 4.19 (Substitución). Si Γ, x : A ` u : B y Γ ` t : A, entonces Γ ` u[t/x] : B.

Demostración. Procedemos por inducción estructural sobre u.

u = x. Es decir que Γ, x : A ` x : B, entonces B = A, y dado que x[t/x] = t, el caso

queda demostrado.

u = y. Es decir que Γ, x : A ` y : B. Pero como x 6= y, se puede demostrar por inducción

en la relación de tipado que Γ ` y : B. Dado que y[t/x] = y, el caso queda
demostrado.

u = λy:C.r. Es decir que Γ, x : A ` λy:C.r : B, por lo tanto B = C ⇒ D y Γ, y : C, x :

A ` r : D. Entonces, por hipótesis de inducción, Γ, y : C ` r[t/x] : D, y por la regla
⇒i , Γ ` λy:C.r[t/x] : B. Dado que λy : C.r[t/x] = (λy:C.r)[t/x], el caso queda
demostrado.

u = rs. Es decir que Γ, x : A ` rs : B. Entonces Γ, x : A ` r : C ⇒ B y Γ, x : A ` s : C,

y por hipótesis de inducción, Γ ` r[t/x] : C ⇒ B y Γ ` s[t/x] : C. Por la regla ⇒e ,
tenemos Γ ` r[t/x]s[t/x] : B. Notar que r[t/x]s[t/x] = (rs)[t/x], por lo que el caso
queda demostrado.

u = n. Es decir que Γ, x : A ` n : B, por lo tanto B = nat y Γ ` n : nat. Notar que

n[t/x] = n, por lo que el caso queda demostrado.
58 4.3. PCF tipado

u = r  s. Es decir que Γ, x : A ` r  s : B, y entonces B = nat y tenemos Γ, x : A `

r : nat y Γ, x : A ` s : nat. Entonces, por hipótesis de inducción Γ ` r[t/x] : nat
y Γ ` s[t/x] : nat. Por lo tanto, por regla , Γ ` r[t/x]  s[t/x] : nat. Dado que
r[t/x]  s[t/x] = (r  s)[t/x], el caso queda demostrado.

u = isZ(r)?s : o. Es decir que Γ, x : A ` isZ(r)?s : o : B, y entonces Γ, x : A ` r : nat,

Γ, x : A ` s : B y Γ, x : A ` o : B. Por hipótesis de inducción, Γ ` r[t/x] : nat, Γ `
s[t/x] : B y Γ ` o[t/x] : B. Entonces, por regla ifz, Γ ` isZ(r[t/x])?s[t/x] : o[t/x] : B.
Dado que isZ(r[t/x])?s[t/x] : o[t/x] = (isZ(r)?s : o)[t/x], el caso queda demostrado.

u = µy : C.r. Es decir que Γ, x : A ` µy : C.r : B, y entonces C = B y Γ, x : A, y :

B ` r : B. Por hipótesis de inducción, Γ, y : B ` r[t/x] : B. Entonces, por regla
µ, Γ ` µy : B.r[t/x] : B. Dado que µy : B.r[t/x] = (µy : C.r)[t/x] el caso queda
demostrado.

u = let y : C = r in s. Es decir que Γ, x : A ` let y : C = r in s : B, y entonces Γ, y :

C, x : A ` s : B y Γ, x : A ` r : C. Por hipótesis de inducción Γ, y : C ` s[t/x] : B
y Γ ` r[t/x] : C, y entonces por la regla let, Γ ` let y : C = r[t/x] in s[t/x] : B.
Dado que let y : C = r[t/x] in s[t/x] = (let y : C = r in s)[t/x], el caso queda
demostrado.

Con el lema anterior podemos demostrar el siguiente teorema.

Teorema 4.20 (Subject reduction). Si Γ ` t : A y t → u entonces Γ ` u : A.

Demostración. Procedemos por inducción sobre la relación →.

(λx : B.u)t → u[t/x]. Entonces Γ ` (λx : B.u)t : A, por lo tanto Γ ` λx : B.u : B ⇒ A

y Γ ` t : B, y entonces Γ, x : B ` u : A. Entonces, por el Lema 4.19, Γ ` u[t/x] : A.

p  q → n si p  q = n. Entonces Γ ` p  q : A, por lo tanto A = nat, y por la regla axc ,

Γ ` n : nat.

isZ(0)?t : u → t. Entonces Γ ` isZ(0)?t : u : A, por lo que Γ ` t : A.

isZ(1)?t : u → u. Entonces Γ ` isZ(1)?t : u : A, por lo que Γ ` u : A.

µx.t → t[µx.t/x]. Entonces Γ ` µx.t : A, por lo tanto Γ, x : A ` t : A. Entonces, por

Lema 4.19, Γ ` t[µx.t/x] : A.

let x : B = t in u → u[t/x]. Entonces Γ ` let x : B = t in u : A, por lo que Γ, x : B ` u :

A y Γ ` t : B. Entonces, por Lema 4.19, Γ ` u[t/x] : A.

4.3.5. Normalización fuerte

En esta sección vamos a demostrar el siguiente teorema.

Teorema 4.21 (Normalización fuerte). Todo término tipado que no contenga µ, termina.
Capítulo 4. Introducción al lambda cálculo y a la teoría de tipos 59

Esta demostración utiliza el concepto de semántica denotacional, que aún no vimos (lo
veremos en la Sección 4.7). Sin embargo, aquí veremos una versión muy reducida de
la semántica denotacional: la idea es interpretar los tipos como conjuntos de términos
fuertemente normalizables, y luego verificamos que si un término tiene un tipo, está
dentro de la interpretación de dicho tipo, y por lo tanto es fuertemente normalizable.
Sea SN el conjunto de todos los términos fuertemente normalizables.

Definición 4.22. La interpretación de los tipos es la siguiente:

JnatK = SN
JA ⇒ BK = {t | ∀r ∈ JAK, tr ∈ JBK}

Es decir, al tipo nat lo interpretamos en el conjunto de todos los términos que normalizan
fuertemente y al tipo A ⇒ B, en el conjunto de términos que aceptan como argumento
un término de JAK y devuelven un término de JBK.

El siguiente lema dice que todos los tipos son conjuntos de términos fuertemente norma-
lizables.

Lema 4.23. ∀A, JAK ⊆ SN .

Demostración. Procedemos por inducción sobre A.

Si A = nat, entonces JnatK = SN ⊆ SN .

Si A = B ⇒ C, entonces para todo t ∈ JAK se tiene que para todo r ∈ JBK, tr ∈ JCK.
Por hipótesis de inducción sobre JCK, tr ∈ SN y por lo tanto t ∈ SN .

El lema que sigue, nos dice que las variables están en todos los tipos.

Lema 4.24. ∀A, ∀x, x ∈ JAK.

Demostración. Procedemos por inducción sobre A.

Si A = nat, entonces claramente x ∈ JnatK = SN .

Si A = B ⇒ C, entonces tenemos que mostrar que ∀r ∈ JBK, xr ∈ JCK. Vamos

a fortalecer la hipótesis y demostrar que si A = B1 ⇒ B2 ⇒ · · · ⇒ Bn ⇒ nat,
entonces para todo ri ∈ JBi K tenemos xr1 r2 . . . rn ∈ JnatK = SN . Procedemos por
inducción sobre n.

• Si n = 1, entonces tenemos que mostrar que ∀r ∈ JB1 K, xr ∈ SN . Por Le-

ma 4.23, r ∈ SN , y por lo tanto xr ∈ SN .
• Por hipótesis de inducción, para ri ∈ JBi K, con i = 1, . . . , n, tenemos xr1 . . . rn ∈
SN . Si rn+1 ∈ JBn+1 K, por Lema 4.23, rn+1 ∈ SN y por lo tanto xr1 . . . rn rn+1 ∈
SN .

Por lo tanto, si A = B1 ⇒ · · · ⇒ Bn ⇒ nat, tenemos x ∈ JAK.

60 4.3. PCF tipado

Definición 4.25 (Términos neutrales). A los términos de la siguiente gramática se les

llama términos neutrales:

N = tt | let x : A = t in t | isZ(t)?t : t

Para cualquier término t, notamos por |t| a la suma de nodos en el árbol formado por
todos los caminos de reducción que comienzan en t.

Lema 4.26. Si todas las reducciones de un término neutral N están en JAK, entonces
N ∈ JAK.

Demostración. Procedemos por inducción en A.

Si A = nat entonces tenemos que mostrar que si todas las reducciones de N están
en JnatK = SN , entonces N está en SN , lo cual es cierto por definición.

Si A = B ⇒ C y todas las reducciones de N están en JB ⇒ CK, entonces si N → t,

tenemos que para todo r ∈ JBK, tr ∈ JCK. Queremos mostrar que N r ∈ JCK. Por
Lema 4.23, r ∈ SN . Por lo tanto procedemos por inducción sobre |r| para mostrar
que todas las reducciones de N r están en JCK, y por lo tanto, por hipótesis de
inducción N r ∈ JCK.
Las reducciones posibles de N r son las siguientes

• tr con N → t, y ya tenemos por suposición que tr ∈ JCK.

• N r0 con r → r0 , entonces dado que |r0 | < |r|, podemos usar la hipótesis de
inducción y concluir que N r0 ∈ JCK.

Dado que N es un término neutral, N no es de la forma λx : D.s y por lo tanto

esas son las únicas reducciones posibles.
Entonces, como N r ∈ JCK, tenemos que N ∈ JB ⇒ CK.

Definición 4.27. Una valuación θ es una función que a cada variable de tipo A le
asigna un elemento del conjunto JAK. Además, usamos la notación θ(t) para un tér-
mino t cualquiera para representar t[θ(x1 )/x1 ][θ(x2 )/x2 ] . . . [θ(xn )/xn ], donde F V (t) =
{x1 , x2 , . . . , xn }.
Decimos que una valuación θ es válida en un contexto Γ (notación θ Γ), si para todo
x : A ∈ Γ se tiene θ(x) ∈ JAK.

El Lema 4.28 nos dice que si un término tiene un tipo en un contexto, entonces cualquier
valuación, válida en ese contexto, del término, será un elemento de la interpretación de
su tipo.

Lema 4.28 (Adecuación). Para todo θ tal que θ Γ, si Γ ` t : A entonces θ(t) ∈ JAK.

Demostración. Procedemos por inducción en la relación de tipado.

Γ, x : A ` x : A.
θ(x) ∈ JAK por definición.
Capítulo 4. Introducción al lambda cálculo y a la teoría de tipos 61

Γ ` n : nat.
θ(n) = n ∈ SN = JnatK.
Γ, x : A ` t : B
Γ ` λx : A.t : A ⇒ B
θ(λx : A.t) = λx : A.θ(t).
Quiero mostrar que θ(λx : A.t) ∈ JA ⇒ BK, es decir que ∀r ∈ JAK, tenemos (λx :
A.θ(t))r ∈ JBK. Procedemos por inducción en |θ(t)| + |r|, donde |s| es la cantidad
de pasos del camino más largo para llegar a la forma normal de s. Como θ(t) y r
son SN , podemos hacer esa inducción.
Las reducciones posibles de (λx : A.θ(t))r son:

• θ(t)[r/x]. Por hipótesis de inducción, si tomamos θ0 = θ, x = r tenemos θ0 (t) ∈

JBK.
• (λx : A.t0 )r con θ(t) → t0 . Como |t0 |+|r| < |θ(t)|+|r|, la hipótesis de inducción
aplica y podemos concluir que (λx : A.t0 )r ∈ JBK.
• (λx : A.θ(t))r0 con r → r0 . Como |θ(t)| + |r0 | < |θ(t)| + |r|, la hipótesis de
inducción aplica y podemos concluir que (λx : A.θ(t))r0 ∈ JBK.

Por lo tanto, todas las reducciones de (λx : A.θ(t))r están en JBK, y entonces, por
Lema 4.26, (λx : A.θ(t))r ∈ JBK.
Γ`t:A⇒B Γ`r:A
Γ ` tr : B
Por hipótesis de inducción, θ(t) ∈ JA ⇒ BK y θ(r) ∈ JAK. Por lo tanto, por definición
de JA ⇒ BK tenemos θ(t)θ(r) ∈ JBK. Nótese que θ(t)θ(r) = θ(tr).
Γ ` t : nat Γ ` r : nat
Γ ` t ⊗ r : nat
Por hipótesis de inducción θ(t) ∈ SN y θ(r) ∈ SN , por lo tanto θ(t) ⊗ θ(r) =
θ(t ⊗ r) ∈ SN = JnatK.
Γ ` t : nat Γ ` r : A Γ ` s : A
Γ ` isZ(t)?r : s : A
Por hipótesis de inducción θ(t) ∈ SN , θ(r) ∈ JAK y θ(s) ∈ JAK. Procedemos por
inducción sobre |θ(t)| para mostrar que todos los reductos de isZ(θ(t))?θ(r) : θ(s)
están en JAK.
Los reductos son:

• isZ(t0 )?θ(r) : θ(s) con θ(t) → t0 . Entonces t0 ∈ SN y |t0 | < |θ(t)|. Por lo tanto,
la hipótesis de inducción aplica y isZ(t0 )?θ(r) : θ(s) ∈ JAK.
• θ(r) si θ(t) = 0, y por hipótesis θ(r) ∈ JAK.
• θ(s) si θ(t) = n 6= 0, y por hipótesis θ(s) ∈ JAK.

Por lo tanto, por Lemma 4.26, θ(isZ(t)?r : s) = isZ(θ(t))?θ(r) : θ(s) ∈ JAK.

62 4.4. Inferencia de tipos simples

Γ, x : A ` t : B Γ ` u : A
Γ ` let x : A = u in t : B
Por hipótesis de inducción, para todo θ válido en Γ, θ(u) ∈ JAK, y para todo θ0 válido
en Γ, x : A, θ0 (t) ∈ JBK. Dado que θ(u) ∈ JAK, tenemos que θ0 = θ, x = θ(u) es una
valuación válida en Γ, x : A, y por lo tanto θ0 (t) ∈ JBK. Procedemos por inducción
sobre |θ(t)| + |θ(u)| para mostrar que todos los reductos de let x : A = θ(u) in θ(t)
están en JBK.
Los reductos son:
• let x : A = u0 in θ(t) con θ(u) → u0 . Entonces la hipótesis de inducción aplica.
• let x : A = θ(u) in t0 con θ(t) → t0 . Entonces la hipótesis de inducción aplica.
• θ(t)[θ(u)/x] = θ0 (t) ∈ JBK.
Por lo tanto, por Lemma 4.26, θ(let x : A = u in t) = let x : A = θ(u) in θ(t) ∈
JAK.
Demostración del Teorema 4.21 (Normalización fuerte). Sea Γ ` t : A donde t no con-
tiene µ. Por el Lema 4.24, θ = id es una valuación válida en Γ. Por lo tanto, por el
Lema 4.28, tenemos t ∈ JAK, y por el Lema 4.23, t ∈ SN .
¿Qué sucede con Ω = (λx.xx)(λx.xx)? No es tipable. Es decir, no existe un tipo A tal
que ` Ω : A.
Ejercicio: Extender PCF con constructores para pares: (t, u), π1 (t, u) y π2 (t, u). Dar la
gramática, semántica operacional, reglas de tipado, y extender la prueba de normalización
fuerte para incluir a los pares.

4.4. Inferencia de tipos simples

4.4.1. Introducción
En muchos lenguajes el programador debe indicar el tipo de las variables. Por ejemplo
λx : nat.x + 1
Sin embargo, en este caso es un poco innecesario, ya que la operación + sólo puede ocurrir
entre naturales, y por lo tanto era posible inferir que x debía ser de tipo nat.
Podemos entonces liberar al programador de escribir los tipos y escribir un algoritmo que
los infiera.

Estilo Curry. Escribimos variables sin tipos, como hicimos con PCF no tipado, y
definimos independientemente el lenguaje de tipos, como ya lo definimos.
Así, en vez de ` λx : nat.x + 1 : nat ⇒ nat escribimos ` λx.x + 1 : nat ⇒ nat.

Gramática
A ::= nat | A ⇒ A
t ::= x | λx.t | tt | n | t  t | isZ(t)?t : t | µx.t | let x = t in t
Capítulo 4. Introducción al lambda cálculo y a la teoría de tipos 63

Reglas de tipado

axv axc
Γ, x : A ` x : A Γ ` n : nat
Γ, x : A ` t : B Γ ` t : A ⇒ B Γ ` u : A ⇒e
⇒i
Γ ` λx.t : A ⇒ B Γ ` tu : B

Γ ` t : nat Γ ` u : nat  Γ ` t : nat Γ ` u : A Γ ` v : A

ifz
Γ ` t  u : nat Γ ` isZ(t)?u : v : A
Γ, x : A ` t : A Γ, x : A ` t : B Γ ` u : A
µ let
Γ ` µx.t : A Γ ` let x = u in t : B

Ahora, para el mismo término, podemos derivar diferentes tipos. Por ejemplo:
axv axv
x : nat ` x : nat ⇒i x : nat ⇒ nat ` x : nat ⇒ nat ⇒i
` λx.x : nat ⇒ nat ` λx.x : (nat ⇒ nat) ⇒ (nat ⇒ nat)

podemos simplemente decir:

axv
x : X ` x : X ⇒i
` λx.x : X ⇒ X
donde X es una variable en el sentido de que “desconocido”, o “cualquier tipo”.

Definición 4.29. Notamos A(X) a un tipo cualquiera que contiene alguna variable X.
Notamos θ a una substitución de meta-variables por tipos.

Ejemplo 4.30. Sea θ = nat/X, nat ⇒ nat/Y . Entonces,

θ(X ⇒ Y ) = nat ⇒ nat ⇒ nat

Teorema 4.31. Si ` t : A(X), entonces ` t : θA(X) para cualquier substitución θ.

Ejemplo 4.32. Como vimos anteriormente, ` λx.x : X ⇒ X. Por lo tanto, tomando

θ = nat/X,
` λx.x : nat ⇒ nat
Tomando θ = (nat ⇒ nat) ⇒ nat/X tenemos

` λx.x : ((nat ⇒ nat) ⇒ nat) ⇒ ((nat ⇒ nat) ⇒ nat)

4.4.2. Algoritmo de Hindley

Supongamos que queremos tipar λf ,2 + f 1, entonces ponemos en el contexto f : X y
tenemos que llegar a f : X ` 2 + f 1 : Y para algún X e Y . Dado que hay una suma,
tenemos que tipar f : X ` 2 : nat y f : X ` f 1 : nat, y como la suma sólo puede ser nat,
sabemos que Y = nat. Por lo tanto tenemos f : X ` 2 : nat y f : X ` f 1 : nat. Entonces,
como es una aplicación, tenemos que f : X ` f : Z ⇒ nat y f : X ` 1 : Z. Entonces
Z = nat y X = nat ⇒ nat. Por lo tanto:
64 4.4. Inferencia de tipos simples

axv axc
f : nat ⇒ nat ` f : nat ⇒ nat f : nat ⇒ nat ` 1 : nat
axc ⇒e
f : nat ⇒ nat ` 2 : nat f : nat ⇒ nat ` f 1 : nat
+
f : nat ⇒ nat ` 2 + f 1 : nat
⇒i
` λf ,2 + f 1 : nat ⇒ nat

Es decir, que en este caso hay una única solución.

Vamos a describir la primera parte del algoritmo inductivamente como una relación

Γ`t A, τ

entre un contexto Γ y un término t, con un tipo A y un conjunto de ecuaciones τ .

Γ, x : A ` x A, ∅ Γ`n nat, ∅

Γ, x : A ` t B, τ Γ`t A, τ Γ ` u B, σ
(X nueva)
Γ ` λx.t A ⇒ B, τ Γ ` tu X, τ ∪ σ ∪ {A = B ⇒ X}
Γ`t A, τ Γ ` u B, σ
Γ`tu nat, τ ∪ σ ∪ {A = nat, B = nat}
Γ`t B, τ Γ ` u A, σ Γ ` v C, ρ
Γ ` isZ(t)?u : v A, τ ∪ σ ∪ ρ ∪ {B = nat, A = C}
Γ, x : A ` t B, τ Γ`u C, τ Γ, x : B ` t A, σ
Γ ` µx.t B, τ ∪ {A = B} Γ ` let x = u in t A, τ ∪ σ ∪ {B = C}
Ejemplo 4.33.

f :A`f A, ∅ f : A ` 1 nat, ∅
f :A`2 nat, ∅ f : A ` f1 X, {A = nat ⇒ X}
f : A ` 2 + f1 nat, {A = nat ⇒ X, nat = nat, X = nat}
` λf ,2 + f 1 A ⇒ nat, {A = nat ⇒ X, nat = nat, X = nat}

4.4.3. Algoritmo de unificación de Robinson

La segunda parte consiste en resolver las ecuaciones sobre los tipos. El lenguaje de tipos no
tiene variables y está formado por la constante nat y el símbolo ⇒ de dos argumentos. Para
resolver las ecuaciones utilizamos el algoritmo de unificación de Robinson, que permite
resolver las ecuaciones de cualquier lenguaje sin variables ligadas.

Definición 4.34. Sea θ una substitución A1 /X1 , . . . , An /Xn . Decimos que θ es una so-
lución del conjunto de ecuaciones τ si para todo B = C en τ , θB y θC son idénticos.

Teorema 4.35. Si ` t A, τ , entonces para toda solución θ de τ , ` t : θA.

Más general: si Γ ` t A, τ , entonces para toda solución θ de τ , θΓ ` t : θA, donde θΓ
es la substitución en cada tipo que aparece en Γ.
Capítulo 4. Introducción al lambda cálculo y a la teoría de tipos 65

Algoritmo de unificación de Robinson

Si una ecuación tiene forma A ⇒ B = C ⇒ D, reemplazarla por las ecuaciones

A = C y B = D.

Si una ecuación tiene la forma nat = nat, borrarla.

Si una ecuación tiene la forma nat = A ⇒ B, o A ⇒ B = nat, responder error.

Si una ecuación tiene forma X = X, borrarla.

Si una ecuación tiene forma A = X, X = A y X aparece en A, pero A 6= X,

responder error.

Si una ecuación tiene forma A = X, X = A y X no aparece en A pero aparece en

otras ecuaciones ecuaciones, substituir X por A en todas las ecuaciones.

Si el algoritmo termina en error: en el sistema no había solución.

Si el algoritmo termina sin error, tendremos una lista de ecuaciones X1 = A1 , . . . , Xn =
An , con Xi distintas y ∀ij, Xi ∈
/ Aj . En ese caso, la substitución θ = A1 /X1 , . . . , An /Xn
es una solución.
En ese caso, θ es “principal”, en el sentido de que para toda otra solución α, existe una
substitución γ tal que α = γ ◦ θ. Decimos que θ = mgu(τ ) (“most general unifier”).
Ejemplo 4.36. Continuando con el ejemplo anterior, teníamos

` λf ,2 + f 1 A ⇒ nat, {A = nat ⇒ X, nat = nat, X = nat}


 A = nat ⇒ X  
A = nat ⇒ X A = nat ⇒ nat
nat = nat ⇒ ⇒
X = nat X = nat
X = nat


Solución: [nat ⇒ nat/A, nat/X]. Por lo tanto,

` λf ,2 + f 1 : (nat ⇒ nat) ⇒ nat

4.5. Polimorfismo
4.5.1. Introducción
En la sección anterior vimos que el tipo principal de λx.x es X ⇒ X. Es decir, λx.x tiene
tipo X ⇒ X para todo X. Podemos entonces atribuirle el tipo

∀X.(X ⇒ X)

y agregar una regla según la cual si t tiene tipo ∀X.A, entonces t tiene tipo A[B/X] para
cualquier B.
A tales lenguajes se los llama polimórficos.
66 4.5. Polimorfismo

Ejemplo 4.37. Usemos los algoritmos de Hindley y Robinson para inferir el tipo del
término let i = λx.x in ii:
i:X`i X, ∅ i : X ` i X, ∅ x:Z`x Z, ∅
i : X ` ii Y, {X = X ⇒ Y } ` λx.x Z ⇒ Z, ∅
` let i = λx.x in ii Y, {X = X ⇒ Y, X = Z ⇒ Z}
El algoritmo de Robinson finalizará con error al leer la ecuación X = X ⇒ Y .
Sin embargo, el término equivalente (λx.x)(λx.x) sí puede ser tipado:

x:X`x X, ∅ x:Y `x Y, ∅
` λx.x X ⇒ X, ∅ ` λx.x Y ⇒ Y, ∅
` (λx.x)(λx.x) Z, {X ⇒ X = (Y ⇒ Y ) ⇒ Z}
 
X = Y ⇒Y
X ⇒ X = (Y ⇒ Y ) ⇒ Z =⇒ =⇒ Y ⇒ Y = Z
X = Z
Es decir, el término tiene tipo Y ⇒ Y para cualquier Y .
La diferencia entre el primer término y el segundo es que en el primero, i debe tener
el mismo tipo en ambas instancias, Z ⇒ Z para cualquier Z, en cambio en el segundo
ejemplo, cada función identidad puede instanciar la Z de manera diferente.
Con un tipo ∀, podemos hacer que el i del let tenga tipo ∀X.(X ⇒ X) y cada ocurrencia
de i se instancie en un tipo diferente, haciendo que el término let i = λx.x in ii pueda ser
tipado como ∀Y.(Y ⇒ Y ).

El ejemplo anterior no es un ejemplo aislado. Podríamos por ejemplo hacer una función
map para árboles, sea cual sea el tipo de los elementos en los árboles, lo que permite
reusabilidad de código y por lo tanto programas más concisos.

4.5.2. Tipos polimórficos

Podemos dar un tipo cuantificado a las variables ligadas por let, pero vamos a dejar tipos
simples para las variables ligadas por λ y µ, de otra manera, está demostrado que no es
posible hacer inferencia de tipos.

Tenemos que distinguir tipos sin cuantificadores (los que llamaremos simplemente “tipos”)
de tipos cuantificados (que llamaremos “esquemas de tipos”).
Definición 4.38. Un esquema de tipo tiene forma ∀X1 . . . ∀Xn .A, donde A es un tipo,
con n ≥ 0.
Definimos entonces una gramática a dos niveles: uno para tipos y otro para esquemas de
tipos:
A ::= X | nat | A ⇒ A
α ::= [A] | ∀X.α
Si A es un tipo, [A] es un esquema de tipo formado por el tipo A donde ninguna variable
está cuantificada.
Capítulo 4. Introducción al lambda cálculo y a la teoría de tipos 67

Definición 4.39. Ahora que tenemos variables y un ligador (∀) en los tipos, extendemos
la definición de variables libres (FV) para tipos:

FV(X) = {X}
FV(nat) = ∅
FV(A ⇒ B) = FV(A) ∪ FV(B)
FV([A]) = FV(A)
FV(∀X.α) = FV(α) \ {X}

Los contextos ahora dan un esquema de tipo a cada variable de término.

Definición 4.40. El sistema de tipos asocia contextos y términos con esquemas de tipos,
Γ ` t : α, y viene dado por
axv axc
Γ, x : α ` x : α Γ ` n : [nat]
Γ, x : [A] ` t : [B] Γ ` t : [A ⇒ B] Γ ` u : [A]
⇒i ⇒e
Γ ` λx.t : [A ⇒ B] Γ ` tu : [B]
Γ ` t : [nat] Γ ` u : [nat] Γ ` t : [nat] Γ ` u : [A] Γ ` v : [A]
 ifz
Γ ` t  u : [nat] Γ ` isZ(t)?u : v : [A]
Γ, x : [A] ` t : [A] Γ ` t : α Γ, x : α ` u : [A]
µ let
Γ ` µx.t : [A] Γ ` let x = t in u : [A]

Γ`t:α ∀ Γ ` t : ∀X.α ∀
Si X ∈
/ FV(Γ),
Γ ` t : ∀X.α i Γ ` t : α[A/X] e

Observaciones.

En la definición anterior se atribuye un esquema de tipo a cada término, en par-

ticular a las variables. Las reglas µ y λ piden x : [A], es decir, un esquema sin
cuantificar. Sólo let permite darle a la variable cualquier esquema.

La condición de la regla ∀i permite tipar, por ejemplo,

axv
x : [X] ` x : [X]
⇒i
` ∀xx : [X ⇒ X]
∀
` λx.x : ∀X.[X ⇒ X] i
∀
` λx.x : [nat ⇒ nat] e

pero impide algo como

ax
 v

x : [X] `x:[X]
` x : ∀X.[X] ∀i

x
 : [X]

Ejercicios: Tipar los siguientes términos con tipos polimórficos

1. λx.x
68 4.6. Interpretación

2. let i = λx.x in ii

3. (λf.f f )(λx.x)

4. (λx.xx)(λx.xx)

Teorema 4.41. Todo término tipado que no contenga a µ, termina.

Observación. Si permitimos ∀ en λ obtenemos “System F” de Girard [1972] y Reynolds

[1974], pero la tipabilidad es indecidible (teorema de Wells [1994]), es decir, no existe
algoritmo de inferencia.
Similarmente, ∀ en µ hace el sistema indecidible (teorema de Kfoury, Tiuryn, y Urzyczyn
[1990]).
Por eso, dar polimorfismo sólo a let es un buen compromiso que permite reusabilidad de
código e inferencia de tipos.

4.6. Interpretación
El programa que calcula el valor de un término se llama intérprete.

4.6.1. Interpretación en CBN

Supongamos que queremos un programa que tome (λx.x × x)4 y nos devuelva 16.
El programa debe reemplazar todas las x por 4 para obtener 4 × 4 puede ser muy costoso
en tiempo. Una alternativa es guardar x = 4 en una estructura anexa llamada contexto
y evaluar x × x en ese contexto.
En un contexto permitimos tener la misma variable varias veces, y se dará la prioridad a
la de más a la derecha.
Ejemplo 4.42. En el contexto x = 3, y − 4, x = 5, z = 8, x vale 5 y no 3.
Evaluamos términos con variables libres y cuando queremos evaluar la variable en sí, la
buscamos en el contexto.
Si el término inicial es cerrado, cada vez que busquemos una variable, esta estará en el
contexto.

Si en el contexto encontramos x = t, donde t no es un valor, deberíamos encontrar también

el contexto en el que t fue evaluado.

Definición 4.43 (Thunk). Un par ht, Γi formado por un término y un contexto de

evaluación, se llama thunk.

Definición 4.44 (Cierre). Cuando queremos en cambio evaluar un término λx.t en un

contexto, el resultado no puede ser simplemente λx.t, tiene que ser t pero con t “cerrado”.
Introducimos para esto otro valor llamado cierre que se compone de un término λx.t y
un contexto Γ, y se nota hx, t, Γi.
Capítulo 4. Introducción al lambda cálculo y a la teoría de tipos 69

Definición 4.45 (Relación ,→ en CBN). Vamos a definir la relación Γ ` t ,→ v que se

lee “t se interpreta a v en Γ”.
Γ0 ` t ,→ v x∈
/ D(∆) Γ ` t ,→ n Γ ` u ,→ m Si n  m = p
Γ, x = ht, Γ0 i, ∆ ` x ,→ v Γ ` n ,→ n Γ ` t  u ,→ p

Γ ` t ,→ hx, t0 , Γ0 i Γ0 , x = hr, Γi ` t0 ,→ v
Γ ` λx.t ,→ hx, t, Γi Γ ` tr ,→ v
Γ ` t ,→ 0 Γ ` r ,→ v Γ ` t ,→ n Γ ` s ,→ v Si n 6= 0
Γ ` isZ(t)?r : s ,→ v Γ ` isZ(t)?r : s ,→ v
Γ, x = hr, Γi ` t ,→ v Γ, x = hµx.t, Γi ` t ,→ v
Γ ` let x = r in t ,→ v Γ ` µx.t ,→ v
Ejemplo 4.46. (Leer de abajo hacia arriba)

` 4 ,→ 4 ` 4 ,→ 4
x = h4, ∅i ` x ,→ 4 x = h4, ∅i ` x ,→ 4
` λx.x × x ,→ hx, x × x, ∅i x = h4, ∅i ` x × x ,→ 16
` (λx.x × x)4 ,→ 16

4.6.2. Interpretación en CBV

En call-by-name es más fácil, ya que siempre se interpretan primero los argumentos, así
que, por ejemplo, en lugar de
Γ0 ` t ,→ v x∈
/ D(∆) x∈
/ D(∆)
tenemos Γ, x = v, ∆ ` x ,→ v
Γ, x = ht, Γ0 i, ∆ ` x ,→ v
Lo mismo sucede con let. Así que los contextos ligan variables con valores, no con thunks.
Sin embargo, la regla µ pide substituir la variable por una expresión, no por un valor, y
si evaluamos esto antes de introducirlo al contexto, el cálculo no termina.
Por lo tanto el contexto contendrá valores extendidos que son o bien valores o bien thunks
formados por un término µx.t y un contexto.
Definición 4.47 (Relación ,→ en CBV).

Γ0 ` µy.t → v
x∈
/ D(∆) x∈
/ D(∆)
Γ, x = v, ∆ ` x ,→ v Γ, x = hµy.t, Γi0 , ∆ ` x ,→ v
Γ ` t ,→ n Γ ` u ,→ m Si n  m = p
Γ ` n ,→ n Γ ` t  u ,→ p
Γ ` r ,→ w Γ ` t ,→ hx, t0 , Γ0 i Γ0 , x = w ` t0 ,→ v
Γ ` λx.t ,→ hx, t, Γi Γ ` tr ,→ v
Γ ` t ,→ 0 Γ ` r ,→ v Γ ` t ,→ n Γ ` s ,→ v Si n 6= 0
Γ ` isZ(t)?r : s ,→ v Γ ` isZ(t)?r : s ,→ v
Γ ` r ,→ w Γ, x = w ` t ,→ v Γ, x = hµx.t, Γi ` t ,→ v
Γ ` let x = r in t ,→ v Γ ` µx.t ,→ v
70 4.7. Semántica denotacional

4.7. Semántica denotacional

4.7.1. Primeras definiciones
Sintaxis (o gramática) : Cómo escribir los términos. Cuáles son válidos y cuáles no.
Semántica: Qué significan.
Ejemplo: “A perro un”. Sintacticamente correcto. Semánticamente incorrecto, ya que la
frase no significa nada.
Definición 4.48 (Semántica). La semántica de un lenguaje es una relación ,→ que a
cada expresión le asocia algo que le da significado.

Semántica denotacional (en programas deterministas). Para cada programa p,

la relación entre las entradas y las salidas de p es una función que escribimos JpK. La
relación se define entonces como
p, e ,→ s ⇐⇒ JpKe = s
La pregunta es, obviamente, cómo definir JpK. (Lo veremos más adelante en esta sección).

Semántica operacional a grandes pasos También llamada semántica operacional a

grandes pasos o semántica natural. Consiste en dar una definición inductiva de ,→ que
nos relacione un término con su valor. Por ejemplo, el intérprete de la Sección 4.6:
(λx.λy.x + y)((λx.x)4)5 ,→ 9
| {z }
Significado de esta expresión: 9

En ese ejemplo damos semántica de acuerdo a lo que calcula.

Así, si considero
(λx.λy.x + y)4 5 y (λx.λy.x + y)5 4
puedo ver que los 3 programas tienen la misma semántica.

Semántica operacional a pequeños pasos También llamada semántica por reescri-

tura. Consiste en definir ,→ a partir de otra relación → que describe las etapas elementales.
Ejemplo:
(λx.(x × x) + x)4 → (4 × 4) + 4 → 16 + 4 → 20

t ,→ r ⇐⇒ t →∗ r y r irreducible
donde →∗ es la clausura reflexiva y transitiva de →.

La no terminación. Un programa puede dar un resultado, producir un error o no

terminar. Los errores se pueden considerar como resultados particulares. Para expresar
programas que no terminan hay varias formas de expresar su semántica:
La primera consiste en considerar que si t no termina, entonces no existe r tal que t ,→ r.
La segunda consiste en agregar un elemento particular ⊥ a los valores de salida y consi-
derar que si t no termina, entonces t ,→ ⊥.
Capítulo 4. Introducción al lambda cálculo y a la teoría de tipos 71

4.7.2. La semántica denotacional de PCF tipado

En general, en los lenguajes funcionales buscamos reducir la distancia que separa la noción
de programa de la de función. Es decir, se busca reducir la distancia entre un programa
y su semántica denotacional.

Interpretación de los tipos. A cada tipo le asociamos un conjunto:

JnatK = N
JA ⇒ BK = JAK → JBK

donde A → B es el conjunto de funciones de A en B.

Interpretación de los términos. A cada término t de tipo A le asociamos un elemento

JtK del conjunto JAK. Si t tiene variables libres, necesitamos dar una función que a cada
x : A en el contexto Γ, le asigne un elemento a ∈ JAK.

JxKθ = θ(x)
Jλx : A.tKθ = λa : JAK.JtKθ,x=a
JtrKθ = JtKθ JrKθ
JnKθ =n
Jt  rKθ = JtKθ  JrKθ

JrKθ si JtKθ = 0
JisZ(t)?r : sKθ =
JsKθ si JtKθ ∈ N∗
Jlet x : A = r in tKθ = JtKθ,x=JrKθ

Hasta ahí es trivial: un programa es una función y su semántica es la misma función.

Esta trivialidad es uno de los objetivos de los lenguajes funcionales.
Observaciones.

1. t/0 tirar error en PCF y no está definida en matemática. Para que esta definición
sea correcta hay que agregar un elemento error a cada conjunto JAK y adaptar la
definición 
error si JrK = 0
Jt/rK =
JtK/JrK si JtK ∈ N, JrK ∈ N∗

2. Aún no dijimos como interpretar µ.

La construcción µ es la única donde la semántica denotacional es interesante, porque es

la única que se aleja de matemática, respecto a la definición de funciones:
En matemática, contrariamente a PCF, sólo podemos tomar un punto fijo si este existe
y si hay varios, ¡tenemos que especificar cual!
Ejemplo 4.49.

1. f (x) = x + 1 no tiene punto fijo. Pero en PCF µx : nat.x + 1 es válido.

72 4.7. Semántica denotacional

2. λf : nat ⇒ nat.λx : nat.(f x) + 1 tampoco tiene punto fijo. . . y basta con cmabiar el
primer λ y tengo el µ.

3. λx : nat.x tiene infinitos puntos fijos.

4. µx : nat.x también.

Teorema 4.50. Si tomamos el punto fijo de una función que no tiene punto fijo o que
tiene varios, el programa que obtenemos no termina.

Observación. También existen programas con un sólo punto fijo y que no terminan en
PCF. Por ejemplo λx : nat.x + x.

Para comprender la semántica denotacional del punto fijo necesitamos comprender la

semántica de los términos que no terminan.

La semántica operacional a pequeños pasos no atribuye ningún resultado a estos

términos.

La semántica operacional a grandes pasos tampoco, pero podemos completar la

relación ,→ agregando ⊥ tal que µx : nat.(x + 1) ,→ ⊥.

En la semántica denotacional la idea es hacer lo mismo: definir una función parcial

J·K tal que Jµx : nat.(x + 1)K no esté definido, y adjuntamos un valor ⊥ a JnatK tal
que
Jµx : nat.(x + 1)K = ⊥

Agregando el valor ⊥, cuando interpretamos, por ejemplo t + r, comenzamos por inter-

pretar t y r y si alguno loopea, también lo hace t + r. Entonces:

JtKθ + JrKθ si JtKθ , JrKθ ∈ N
Jt + rKθ =
⊥ si JtKθ = ⊥ o JrKθ = ⊥

Ahora vemos que la función Jλx : nat.x + 1K que no tenía punto fijo cuando JnatK = N, si
JnatK = N ∪ ⊥ le podemos dar ⊥ como semántica a ese término.
Jλx : nat.xK que tenía muchos puntos fijos, ahora tiene uno más: ⊥.
Jλx : nat.x + xK que tenía sólo un punto fijo en 0, ahora tiene 2: 0 y ⊥, y el segundo es el
que queremos atribuirle como semántica.

Definición 4.51 (Orden de Scott). ⊥ es el elemento más chico de cualquier conjunto

que lo contenga.

Definimos entonces Jµx : nat.tK como el punto fijo más chico de Jλx : nat.tK.
Capítulo 4. Introducción al lambda cálculo y a la teoría de tipos 73

Semántica denotacional completa de PCF (sin error)

JxKθ = θ(x)
Jλx : A.tKθ = λa : JAK.JtKθ,x=a
JtrKθ = JtKθ JrKθ
JnKθ =n

JtKθ  JrKθ si JtKθ , JrKθ ∈ N
Jt  rKθ =
⊥N si no

 JrKθ si JtKθ = 0
JisZ(t)?r : sKθ = JsKθ si JtKθ ∈ N∗
⊥A si JtKθ = ⊥N y A es el tipo del término


Jlet x : A = r in tKθ = JtKθ,x=JrKθ

Jµx : A.tKθ = FIX(λa : JAK.JtKθ,x=a )

donde FIX(f ) es el mínimo punto fijo de f .

Observación. El mínimo de JAK es ⊥A y el mínimo de JA ⇒ BK = ⊥JAK→JBK que es la
función constante ⊥JBK .
Teorema 4.52. Si Γ ` t : A, entonces para toda valuación θ válida en Γ se tiene
JtKθ ∈ JAK.
Demostración. Ejercicio (Ayuda: Inducción sobre la derivación de Γ ` t : A).
Teorema 4.53 (Soundness). Si Γ ` t : A y t → r, entonces para toda valuación θ válida
en Γ se tiene JtKθ = JrKθ .
Demostración. Ejercicio (Ayuda: Inducción sobre la relación →).

4.8. Rapid(ísim)a descripción de la lógica lineal

Esta sección es una adaptación libre de la Sección 3.1 del artículo de Di Cosmo y Miller
[2016]. Para más detalles, se sugiere recurrir a dicha fuente.

4.8.1. Introducción
La lógica lineal fue introducida por Jean-Yves Girard [1987]. Aquí daremos una presen-
tación por medio de cálculo de secuentes, ya que es muy similar a las reglas de tipado
que hemos visto en las secciones anteriores.
La idea principal a retener es que la lógica lineal es una lógica de recursos: la fórmula
A ⇒ B normalmente se entiende como “Si me das A, te devuelvo B”, pero, en la práctica,
significa más bien “Si me das tantas A como necesite, te devuelvo B”. Por ejemplo, el
término
λx.x + Fact x
tiene tipo nat ⇒ nat, pero para calcular x + Fact x, se necesitan dos copias del número
x. Es decir, el recurso (el número x), fue duplicado para poder calcular el resultado. Si,
74 4.8. Rapid(ísim)a descripción de la lógica lineal

por ejemplo, el recurso fuese Fact 1000, y trabajamos en call-by-value (para asegurar que
si hay un resultado, llegaremos al mismo), entonces duplicar el recurso tiene un costo.
En lógica lineal no podemos duplicar recursos, salvo que explícitamente se autorice. Así,
el tipo nat ( nat significa: “Si me das un nat, te devuelvo un nat usándolo exactamente
una vez”, y, en cambio, el tipo !nat ( nat significa nat ⇒ nat.
Ésta lógica nos será de utilidad para definir cálculos cuánticos, ya que el teorema de no
clonado (Teorema 1.27) nos impide clonar recursos cuánticos.
De la misma manera, la función λx,1, que descarta su argumento, no podríamos decir
que tiene tipo nat ( nat. En cambio, se utiliza el tipo ?nat ( nat, donde ? se utiliza,
justamente, para permitir descartar el argumento.

4.8.2. Cálculo de secuentes

Los conectivos de la lógica lineal se dividen en multiplicativos y aditivos, y los conectivos
clásicos tienen su paralelo en ambos:

Clásico Multiplicativo Aditivo

∧ (conjunción) ⊗ (tensor) & (with)
T (verdadero) 1 (uno) > (top)
∨ (disjunción) ` (par) ⊕ (oplus)
F (falso) ⊥ (bottom) 0 (cero)

Implicación lineal: A ( B := ¬A ` B
Implicación intuicionista: A ⇒ B := !A ( B
A ! y a ? se les llama exponenciales, y existen las equivalencias normales de los exponen-
ciales con respecto a la suma y la adición: na+b = na nb .

!(A & B) ≡ (!A ⊗ !B) ?(A ⊕ B) ≡ (?A ` ?B)

!> ≡ 1 ?0 ≡ ⊥
Donde A ≡ B significa que (A ( B) ∧ (B ( A) es derivable.
A continuación se detallan las reglas en el formato ∆ ` Γ, que significa que la conjun-
ción (multiplicativa) de las fórmulas en ∆, implican la disjunción (multiplicativa) de las
fórmulas en Γ.

Gramática

A := p | ¬A | A ⊗ A | A ` A | A & A | A ⊕ A | 1 | ⊥ | > | 0

Donde p representa una fórmula atómica.

Reglas de indentidad y negación

∆ ` B, Γ ∆0 , B ` Γ0 ∆ ` A, Γ ∆, A ` Γ
ax cut ¬l ¬r
A`A ∆, ∆0 ` Γ, Γ0 ∆, ¬A ` Γ ∆ ` ¬A, Γ
Capítulo 4. Introducción al lambda cálculo y a la teoría de tipos 75

Reglas multiplicativas

∆`Γ 1 ∆, A, B ` Γ ∆ ` A, Γ ∆0 ` B, Γ0
1r ⊗ ⊗r
∆, 1 ` Γ l `1 ∆, A ⊗ B ` Γ l ∆, ∆0 ` A ⊗ B, Γ, Γ0

∆`Γ ⊥ ∆, A ` Γ ∆0 , B ` Γ0 ∆ ` A, B, Γ
⊥l ` `
⊥` ∆ ` ⊥, Γ r ∆, ∆0 , A ` B ` Γ, Γ0 l ∆ ` A ` B, Γ r

Reglas aditivas
∆, A ` Γ ∆, B ` Γ ∆ ` A, Γ ∆ ` B, Γ
0l & & &r
∆, 0 ` Γ ∆, A & B ` Γ l1 ∆, A & B ` Γ l2 ∆ ` A & B, Γ
∆, A ` Γ ∆, B ` Γ ∆ ` A, Γ ∆ ` B, Γ
>r ⊕l ⊕ ⊕
∆ ` >, Γ ∆, A ⊕ B ` Γ ∆ ` A ⊕ B, Γ r1 ∆ ` A ⊕ B, Γ r2

Reglas de los exponenciales

!∆, A ` ?Γ !∆ ` A, !Γ
? !
!∆, ?A ` ?Γ l !∆ ` !A, ?Γ r

∆`Γ W ∆, !A, !A ` Γ ∆, A ` Γ
C! D
∆, !A ` Γ ! ∆, !A ` Γ ∆, !A ` Γ !
∆`Γ W ∆ ` ?A, ?A, Γ ∆ ` A, Γ
C? D
∆ ` ?A, Γ ? ∆ ` ?A, Γ ∆ ` ?A, Γ ?

4.8.3. Un ejemplo simple de sistema de tipos lineal

Supongamos que queremos redefinir el fragmento de PCF que no contiene al punto fijo,
de manera que los tipos simples permitan sólo funciones que usan su variable una sola
vez, y si se van a utilizar más de una vez o ninguna, entonces el tipo deberá ser marcado
con !.
En particular, en este sistema podremos duplicar números naturales, pero no funciones.
Definimos el siguiente sistema de tipos para obtener el efecto deseado (ver la diferencia
con la relación de tipado de la Definición 4.17).
axv axc
x:A`x:A ` n : !nat
Γ, x : A ` t : B Γ`t:A(B ∆`u:A (
(i e
Γ ` λx:A.t : A ( B Γ, ∆ ` tu : B
Γ ` t : !nat ∆ ` u : !nat  Γ ` t : !nat ∆ ` u : A ∆ ` u : A
ifz
Γ, ∆ ` t  u : !nat Γ, ∆ ` isZ(t)?u : v : A
Γ, x : A ` t : B ∆ ` u : A
let
Γ, ∆ ` let x : A = u in t : B
Γ`t:A Γ, x : !B, y : !B ` t : A
W C
Γ, x : !B ` t : A Γ, x : !B ` t[x/y] : A
Donde Γ ∪ ∆ = ∅.
76 4.8. Rapid(ísim)a descripción de la lógica lineal

Ejemplo 4.54. El término apply := λx.λy.x(y +y) puede ser tipado como (!nat ( !nat) (
!nat ( !nat:
axv axv
y : !nat ` y : !nat z : !nat ` z : !nat
+
y : !nat, z : !nat ` y + z : !nat
axv C
x : !nat ( !nat ` x : !nat ( !nat y : !nat ` y + y : !nat
(e
x : !nat ( !nat, y : !nat ` x(y + y) : !nat
(i
x : !nat ( !nat ` λy.x(y + y) : !nat ( !nat
(i
` λx.λy.x(y + y) : (!nat ( !nat) ( !nat ( !nat

Notar que el segundo argumento no es lineal, ya que se utiliza dos veces, y eso se ve
reflejado en el tipo (!nat), en cambio, el primer argumento es lineal (!nat ( !nat) y se
utiliza sólo una vez.
En la práctica veremos que todas las reglas de tipado que dimos más arriba, son lógica-
mente derivables.
Capítulo 5

Extensiones cuánticas al lambda cálculo

5.1. Control clásico, datos cuánticos

El paradigma de control clásico y datos cuánticos se atribuye a Peter Selinger [2004], y
la idea es que en cualquier lenguaje de programación cuántico, los datos (qubits), son
cuánticos, pero el flujo de control del programa será clásico. Es decir, no se pueden su-
perponer programas, sólo datos. La primer extensión a lambda cálculo en este paradigma
vino de la mano de Selinger y Valiron [2006], y es el cálculo que vamos a estudiar en la
Sección 5.1.1.

5.1.1. El cálculo de Selinger y Valiron

Gramática
La gramática del cálculo es la siguiente:

t ::=x | λx.t | tt | isZ(t)?t : t | 0 | 1 | new | meas | U | ∗ | (t, t) | let (x, y) = t in t

Donde
new mapea un bit clásico en un qubit.

meas mapea un qubit en un bit clásico, a través de una medición cuántica.

U es un cualquier matriz unitaria.

Las que siguen son notaciones prácticas:

(t1 , t2 , . . . , tn ) = (t1 , (t2 , (. . . , tn )))

let x = r in t = (λx.t)r
λ(x, y).t = λz.(let (x, y) = z in t)

Programas
El estado de un programa se representa con una tripleta [q, `, t] donde
q es un vector normalizado de ni=1 C2 , para algún n > 0.
N

77
78 5.1. Control clásico, datos cuánticos

t es un término lambda.
` es una función de W en N≤n , donde FV(t) ⊆ W . A L se la llama función de
linkeado.
La función de linkeado linkea variables libres específicas de t a qubits específicos de q.
Ejemplo 5.1. La tripleta
1
[ √ (|00i + |11i), {x 7→ 2}, λy.Xx]
2
representa el programa que comienza con el estado de Bell β00 y al pasarle un argumento
cualquiera aplica la compuerta X (not) al segundo qubit, transformando dicho estado en
β01 , pero aún no hemos dicho cómo reduce un programa para poder verificar esta última
afirmación.

Notación. Para simplificar la notación, se usan pi para denotar las variables libres x
tal que `(x) = i. Es decir, pi es la variable que referencia al i-ésimo qubit. De esa manera,
un programa [q, `, t] es abreviado en [q, t0000 ], donde t0 = t[p`(x1 ) /x1 ] . . . [p`(xn ) /xn ].
Ejemplo 5.2. La tripleta del ejemplo 5.1 se escribe abreviadamente como
1
[ √ (|00i + |11i), λy.Xp2 ]
2
Observación. El teorema de no clonado (ver Teorema 1.27) en este lenguaje es traducido
en que cada qubit cuántico no puede ser referenciado más de una vez a través de la función
de linkeado. Sintácticamente esta restricción se traduce en la condición de linealidad: una
lambda abstracción λx.t se dice lineal si la variable x aparece exactamente una vez en t.
El sistema de tipos se encargará de que las variables linkeadas a través de la función ` se
usen linealmente, mientras al resto de las variables se permite una utilización no-lineal.

Semántica operacional: preliminares

Estrategia de reducción. Aún no hemos definido las reglas de reducción, sin embargo,
veremos un ejemplo que ayuda a decidir la estrategia a utilizar.
Sea xor = λx.λy.isZ(x)?(isZ(y)?0 : 1) : y. Luego, definimos el siguiente término:
t = (λx.xor xx)(meas(H(new 0)))

Call-by-value. En call-by-value la reducción es la siguiente

[|i, t] →CBV [|0i, (λx.xorxx)(meas(Hp1 ))]
1
→CBV [ √ (|0i + |1i), (λx.xor xx)(meas p1 )]
2

[|0i, (λx.xor xx)0]
→CBV
[|1i, (λx.xor xx)1]

[|0i, xor 0 0]
→CBV
[|1i, xor 1 1]

[|0i, 0]
→CBV
[|1i, 0]
Capítulo 5. Extensiones cuánticas al lambda cálculo 79

Donde las dos ramas tienen probabilidad 1/2 cada una, por lo tanto, en call-by-value este
programa produce el valor booleano 0 con probabilidad 1.

Call-by-name. En call-by-name, en cambio, la reducción es la siguiente:



 [|01i, 1]
[|10i, 1]

[|i, t] →CBN [|i, xor (meas(H(new 0))) (meas(H(new 0)))] →∗CBN

 [|00i, 0]
[|11i, 0]


(No se detalla paso a paso ya que hay algunas sutilezas con la construcción isZ()? : que
aún no hemos mencionado).
Entonces, en call-by-name este programa produce 0 o 1 con la misma probabilidad.

Sin estrategia. Si no se establece una estrategia, este término podría incluso reducir
a un término mal formado, por ejemplo:

[|i, t] →CBV [|0i, (λx.xorxx)(meas(Hp1 ))]

1
→CBV [ √ (|0i + |1i), (λx.xor xx)(meas p1 )]
2
1
→CBN [ √ (|0i + |1i), xor (meas p1 ) (meas p1 )]
2
Notar que el último término no es válido ya que contiene dos ocurrencias de p1 .

Conclusión: Se utiliza la estrategia call-by-value, ya que es la más natural.

Reescritura probabilista. Como se vio en el ejemplo anterior, es necesario utilizar

un sistema de reescritura probabilista. Esto es, un sistema de reescritura donde algunos
términos pueden reducir en más de una forma, cada una de ellas con una probabilidad
asociada. No nos detendremos más a formalizar ésto, basta decir que todas las reglas de
reducción tendrán probabilidad 1, a excepción de meas que tendrá diferentes formas de
reducirlo con una probabilidad dada por el vector de estado cuántico del programa.
Por ejemplo,

[α|0i + β|1i, meas p1 ] →|α|2 [|0i, 0] y [α|0i + β|1i, meas p1 ] →|β|2 [|1i, 1]

donde t →p r se lee “t reduce a r con probabilidad p”.

Semántica operacional: formalización

Dado que se ha elegido una estrategia call-by-value, definimos los valores de la siguiente
manera:
v ::= x | λx.t | 0 | 1 | meas | new | U | ∗ | (v, v)
El conjunto de estados de valores es V = {[q, `, v]}.
 80 5.1. Control clásico, datos cuánticos

Las reglas de reducción se dan a continuación, donde se ha utilizado la convención para

simplificar la notación sin la función de linkeado.

[q, (λx.t)v] →1 [q, t[v/x]]

[q, isZ(1)?t : r] →1 [q, t]
[q, isZ(0)?t : r] →1 [q, r]
[q, U (pj1 , . . . , pjn )] →1 [q 0 , (pj1 , . . . , pjn )] (∗)
[α|q0 i + β|q1 i, meas pi ] →|α|2 [|q0 i, 0] (∗∗)
[α|q0 i + β|q1 i, meas pi ] →|β|2 [|q1 i, 1] (∗∗)
[q, new 0] →1 [q ⊗ |0i, pn+1 ] (∗ ∗ ∗)
[q, new 1] →1 [q ⊗ |1i, pn+1 ] (∗ ∗ ∗)
[q, let (x1 , x2 ) = (v1 , v2 ) in t] →1 [q, t[v1 /x1 ][v2 /x2 ]]
Para las siguientes reglas, sea [q, t] →p [q 0 , t0 ]. Entonces:
[q, rt] →p [q 0 , rt0 ]
[q, tv] →p [q 0 , t0 v]
[q, (t, r)] →p [q 0 , (t0 , r)]
[q, (v, t)] →p [q 0 , (v, t0 )]
[q, isZ(t)?r : s] →p [q 0 , isZ(t0 )?r : s]
[q, let (x, y) = t in r] → [q 0 , let (x, y) = t0 in r]
[q, let (x, y) = r in t] → [q 0 , let (x, y) = r in t0 ]

(∗) U es una compuerta cuántica de n-qubits y q 0 es q luego de aplicar la compuerta a

los qubits j1 , . . . , jn .

(∗∗) |q0 i y |q1 i son qubits normalizados de la forma

X X
|q0 i = αj |φ0j i ⊗ |0i ⊗ |ψj0 i y |q1 i = αj |φ1j i ⊗ |1i ⊗ |ψj1 i
j j

i−1
donde |φ0j i, |φ1j i ∈ C2 .
n
(∗ ∗ ∗) q ∈ C2

Tipos
El sistema de tipos captura la noción de duplicabilidad, como se discutió anteriormente.
Se utiliza la notación de la lógica lineal de Girard [1987]. Un término de tipo A se asume no
duplicable, y a los términos duplicables se les asignará tipos de la forma !A. La gramática
de los tipos se define como sigue:

A ::= α | X | !A | A ( A | > | A ⊗ A

donde α es alguno de un conjunto de constantes y X es alguno de un conjunto de variables

de tipo.
Capítulo 5. Extensiones cuánticas al lambda cálculo 81

Escribimos !n A en lugar de !! . . .!!A con n repeticiones de !, y An para el producto tensorial

de n As: A ⊗ · · · ⊗ A.
En general, un valor de tipo !A podremos utilizarlo más de una vez. Pero no hay ningún
problema si decimos que ese valor tiene también tipo A, y en ese caso debe usarse sólo
una vez. Por lo tanto, se definen reglas de subtipado, que nos permitirán hacer que si un
término tiene un tipo, también tenga cualquier subtipo de éste.

(X) (>) A <: B (D) !A <: B (!)

α <: α (α) X <: X > <: > !A <: B !A <:!B
A1 <: B1 A2 <: B2 A <: A0 B <: B 0 (()
(⊗)
A1 ⊗ A2 <: B1 ⊗ B2 A0 ( B <: A ( B 0
Que un programa [q, `, t] esté bien tipado, significa simplemente que t esté bien tipado,
por lo tanto, vamos a dar las reglas de tipos sólo para t.
Para cada constante c del lenguaje se asocia un tipo fijo Ac :

A0 = !bit Anew = !(bit ( qbit)

A1 = !bit Ameas = !(qbit ( bit) AU = !(qbitn ( qbitn )

A <: B Ac <: B
(var ) (const)
Γ, x : A ` x : B Γ`c:B
Γ1 , !∆ ` t : bit Γ2 , !∆ ` r : A Γ2 , !∆ ` s : A
(if )
Γ1 , Γ2 , !∆ ` isZ(t)?r : s : A
Γ1 , !∆ ` t : A ( B Γ2 , !∆ ` r : A
(app)
Γ1 , Γ2 , !∆ ` tr : B
x : A, ∆ ` t : B Γ, !∆, x : A ` t : B
(λ1 ) Si FV(t) ∩ |Γ| = ∅, (λ2 )
∆ ` λx.t : A ( B Γ, !∆ ` λx.t :!n+1 (A ( B)
Γ1 , !∆ ` t :!n A1 Γ2 , !∆ ` r :!n A2
(⊗i ) (>)
Γ1 , Γ2 , !∆ ` (t, r) :!n (A1 ⊗ A2 ) ∆ ` ∗ :!n >
Γ1 , !∆ ` t :!n (A1 ⊗ A2 ) Γ2 , !∆, x :!n A1 , y :!n A2 ` r : A
(⊗e )
Γ1 , Γ2 , !∆ ` let (x, y) = t in r : A

Ejemplo: Teleportación
La teleportación fue presentada en la Sección 1.6.2. Reproducimos el circuito aquí por
conveniencia.

|ψi • H

|0i H •

|0i Z b1 X b2 |ψi

Las líneas punteadas delimitan tres partes del circuito: la primera es la creación del
estado de Bell β00 , y le llamaremos Bell. La segunda es las operaciones que realiza Alice,
82 5.2. Control y datos cuánticos

y llamaremos a esta parte del algoritmo Alice. Finalmente, la tercera es la que realiza
Bob, por lo que le llamaremos Bob. Los tipos de cada parte del programa serán:

` Bell :!(> 7→ (qbit ⊗ qbit)

` Alice :!(qbit ( qbit ( bit ⊗ bit)
` Bob :!(qbit ( bit ⊗ bit ( qbit)

Esas funciones se definen por

Bell = λx.CNOT (H (new 0), new 0)

Alice = λq1 .λq2 .(let (p, p0 ) = CNOT (q1 , q2 ) in (meas(H p), meas p0 ))
Bob = λq.λ(x, y).isZ(x)?(isZ(y)?ZX q : Z q) : (isZ(y)?X q : q)

Luego,
Telep = λq.(let (p, p0 ) = Bell ∗ in (Bob p0 (Alice q p)))

Ejercicios:

1. Dar la traza de [ √12 (|0i + |1i), Telep p1 ].

2. Dar términos para Deutsch y la codificación superdensa, y tiparlos.

5.2. Control y datos cuánticos

Antes del cálculo de Selinger y Valiron, y de la idea de control clásico y datos cuánticos,
hubo otras extensiones al lambda cálculo. La más notoria, quizá, es el cálculo de van
Tonder [2004] del cual veremos algunos detalles en la Sección 5.2.1. Sin embargo, luego
de la introducción del paradigma de control clásico y datos cuánticos también hubo
desarrollos en el paradigma de control y datos cuánticos. En particular, dicho paradigma
puede ser más apropiado para estudiar la computación cuántica desde un punto de vista
lógico a través del isomorfismo de Curry-Howard (ver [Sørensen y Urzyczyn, 2006]). El
cálculo lineal-algebraico (Lineal ) de Arrighi y Dowek [2008, 2017] dio origen al estudio de
los lenguajes cuánticos a nivel de su semántica operacional y lo veremos en la Sección 5.2.2,
así como su versión tipada, del trabajo de Arrighi, Díaz-Caro, y Valiron [2017]. Luego
veremos una modificación a dicho cálculo, agregando medición y un sistema de tipos
simples en la Sección 5.2.3, donde se describe el paper de Díaz-Caro y Dowek [2017] y se
da una intuición de su semántica denotacional.

5.2.1. El cálculo de van Tonder

Al igual que con el cálculo de Selinger y Valiron, van Tonder también utiliza un sistema
de tipos lineal para evitar el clonado. Sin embargo, el cálculo de van Tonder estudia
otra propiedad interesante: la reversibilidad. Efectivamente, la computación cuántica,
excluyendo la medición, es reversible, ya que las compuertas cuánticas son unitarias.
Capítulo 5. Extensiones cuánticas al lambda cálculo 83

Inicialmente van Tonder plantea una gramática simple, con constantes para las operacio-
nes cuánticas
t ::= x | λx.t | tt | c
c ::= 0 | 1 | H | CN OT | X | Z | . . .
donde, como puede observarse, no hay medición.
La computación reversible fue estudiada en los 70s, en particular, el trabajo de Bennett
[1973] mostró una manera simple de obtener reversibilidad: llevar un historial de los pasos
de reducción. Por ejemplo, si t0 → t1 → t2 → . . . , la reducción reversible sería
(t0 ) → (t0 , t1 ) → (t0 , t1 , t2 ) → . . .
Sin embargo, en el caso cuántico, no es tan directo. Supongamos que el estado inicial
viene dado por H aplicada al qubit |0i, que van Tonder lo representa dentro de un ket
de la siguiente manera:
|(H 0)i
Las reglas de reducción para este término deberían ser tales que |(H 0)i reduzca a √12 (|0i+
|1i) y |(H 1)i a √12 (|0i−|1i). Sin embargo, estas reglas no son reversibles. Usando el truco
de Bennett podríamos tener
1 1
|(H 0)i → √ (|(H 0); 0i + |(H 0); 1i) = |(H 0)i ⊗ √ (|0i + |1i)
2 2
En este ejemplo, el “historial” se factoriza a la izquierda y el término reducido queda a la
derecha. Sin embargo, consideremos el siguiente ejemplo:
1
|(H (H 0))i → √ (|(H (H 0)); (H 0)i + |(H (H 0)); (H 1)i)
2
1
→ |(H (H 0))i ⊗ (|(H 0); 0i + |(H 0); 1i + |(H 1); 0i − |(H 1); 1i)
2
Aquí el término reducido no puede ser factorizado: el registro quedo enredado con parte
del historial.
Pero en este ejemplo vemos que se está guardando más información de la necesaria. Con
guardar simplemente que subtérmino redujo y con qué operación es suficiente. Retomando
el mismo ejemplo, tendríamos:
1
|(H (H 0))i → √ (|(_ (H _)); (H 0)i + |(_ (H _)); (H 1)i)
2
1
→ |(_ (H _))i ⊗ (|(H _); 0i + |(H _); 1i + |(H _); 0i − |(H _); 1i)
2
= |(_ (H _)); (H _)i ⊗ |0i
Con estas ideas en mente se define el modelo computacional. El estado computacional se
toma como una superposición cuántica de secuencias
h1 ; . . . ; hn ; t
donde h1 ; . . . ; hn es llamado historial, y t registro computacional.
No vamos a discutir el cálculo de van Tonder en este curso, sólo estas observaciones y se
recomienda al interesado el paper [van Tonder, 2004].
84 5.2. Control y datos cuánticos

5.2.2. El lambda cálculo lineal algebraico

El lambda cálculo lineal algebraico (de ahora en más, Lineal) sigue un paradigma di-
ferente a los dos vistos anteriormente: la idea es tener un lambda cálculo puro, donde
no hay distinción entre datos y programas, y, por lo tanto, dado que los datos pueden
superponerse, también pueden hacerlo los programas.
Este cálculo es un primer paso hacia un cálculo cuántico. En este primer paso el cálculo
se centra en la noción computacional de espacios vectoriales.

Gramática
La gramática del lenguaje incluye todos los términos de lambda cálculo, y sus combina-
ciones lineales.

t ::= x | λx.t | tr | 0 | α.t | t + t

donde α ∈ C. Aquí, la constante 0 tiene un significado diferente a la de los cálculos

anteriores: recordemos que Lineal no es un cálculo cuántico, sino un cálculo vectorial, y
por lo tanto 0 representa simplemente al vector nulo.
Los valores de este cálculo son las variables y las abstracciones, y los escribimos utilizando
la letra v.

Semántica operacional
Las reglas de reducción son, además de la beta reducción, una versión orientada de los
axiomas de espacios vectoriales. La orientación de cada regla ha sido elegida de manera
de obtener un cálculo confluente.
La idea principal es que una abstracción, sobre una combinación lineal, se comporte
linealmente como lo hace una matriz sobre un vector. Así,

(λx.t)(α.r + β.s) →∗ α.(λx.t)r + β.(λx.t)s

De esa manera no se impone no clonado con una restricción de lógica lineal (ver el cálculo
de Selinger y Valiron en la Sección 5.1.1), sino que siempre que haya una superposición,
la función actuará linealmente, y por lo tanto sólo actuará en los vectores de base. Re-
cordemos que los vectores de base son clonables: por ejemplo, la compuerta CNOT clona
los qubits |0i y |1i:

CNOT |00i = |00i

CNOT |10i = |11i

En cambio, la misma función aplicada a una superposición, actúa de la siguiente manera:

CNOT (α|0i + β|1i) ⊗ |0i = CNOT (α|00i + β|10i)

= αCNOT |00i + βCNOT |10i
= α|00i + β|11i

Notar que ese qubit difiere de (α|0i + β|1i) ⊗ (α|0i + β|1i).

Capítulo 5. Extensiones cuánticas al lambda cálculo 85

Por lo tanto el cálculo deberá ser call-by-value, ya que si el argumento reduce a una
superposición, es necesario reducirlo antes de pasarlo a una abstracción.

β-reducción Reglas de factorización

(λx.t)v → t[v/x] α.t + β.t → (α + β).t
Reglas elementales α.t + t → (α + 1).t
0.t → 0 t + t → 2.t
1.t → t t+0 →0
α,0 → 0 Reglas de aplicación
α.(β,0) → (α × β),0 (t + r)s → ts + rs
α.(t + r) → α.t + α.r t(r + s) → tr + ts
(α.t)r → α.tr
t(α.r) → α.tr
0t → 0
t0 → 0
Si t → r entonces C[t] → C[r] para cualquier contexto C[·]

Ejemplo 5.3. Consideremos los términos true y false de Church, λx.λy.x y λx.λy.y como
los qubits |0i y |1i. De esa manera podemos codificar el término isZ(t)?r : s simplemente
como trs, ya que si t es |0i, λx.λy.xrs →∗ r y si t es |1i, λx.λy.yrs →∗ s.
La compuerta Hadamard podría ser codificada en Lineal de la siguiente manera:

1 1
Hx = x( √ (|0i + |1i))( √ (|0i − |1i))
2 2

Sin embargo, de esta manera trivial no funciona, ya que los mecanismos utilizados para
no-clonado (las reglas de aplicación), harán que el término reduzca de la siguiente manera:

H|0i = Hλx.λy.x
1 1
= λx.λy.x( √ (|0i + |1i))( √ (|0i − |1i))
2 2
1 1
→ √ λx.λy.x(|0i + |1i)( √ (|0i − |1i))
2 2
1 1
→ √ (λx.λy.x|0i + λx.λy.x|1i)( √ (|0i − |1i))
2 2
1
→∗ (λy.|0i + λy.|1i)(|0i − |1i)
2
1
→∗ (|0i − |0i + |1i − |1i)
2
→∗ 0

El problema está en la linealidad. Lo que debemos hacer es que el encodaje del isZ()? :
detenga la linealidad. Por ejemplo:

isZ(t)?r : s = (t(λx.r)(λx.s))(λx.x)
86 5.2. Control y datos cuánticos

Para hacerlo más legible, usamos la siguiente notación:

[t] = λx.t con x ∈

/ FV(t)
t = t(λx.x)

Y entonces, el encodaje del isZ()? : es el siguiente:

isZ(t)?r : s = {t[r][s]}

Por ejemplo, a la compuerta Hadamard la codificamos correctamente como

1 1
{Hx} = {x[( √ (|0i + |1i))][( √ (|0i − |1i))]}
2 2

Tipos
El sistema de tipos vectorial para Lineal [Arrighi, Díaz-Caro, y Valiron, 2017] propone
que los tipos lleven cuenta de las superposiciones en los términos. Así, si el término t
tiene tipo A y el término r tiene tipo B, el término α.t + β.r tendrá tipo α.A + β.B.
Si consideramos T = X ⇒ Y ⇒ X y F = X ⇒ Y ⇒ Y , el término √12 (|0i + |1i) tendrá
tipo √12 (T + F ). Notar que este tipo tiene norma 1, al igual que el término, y por lo
tanto, un tal tipo nos permite verificar facilmente la norma del vector que produce un
programa.
Dada la estrategia call-by-value, las variables sólo pueden tener tipos no superpuestos,
los que llamamos unit types. Esta necesidad se comprende mejor con el siguiente ejemplo:
Supongamos que permitimos variables con tipos escalados, como α.V . Entonces, el tér-
mino λx.x + t podría tener tipo (α.V ) ⇒ α.V + U , con t de tipo U . Luego, tomemos un
término v de tipo V y tenemos (λx.x + t)(α.v) de tipo α.V + U . Sin embargo

(λx.x + t)(α.v) → α.(λx.x + t)v → α.(v + t) → α.v + α.t

lo cual es problemático, ya que α.V + U no refleja esta superposición.

Por el contrario, las variables de tipo no necesitan ser solo unit. Sin embargo, debemos
distinguir variables unit de las que no lo son, ya que sólo las variables unit pueden
aparecer a la izquierda de una flecha. Por ese motivo definimos dos tipos de variables:
las variables X , que sólo podrán ser reemplazadas por tipos unit, y las variables X,
que pueden ser reemplazadas por cualquier tipo (escribimos simplemente X cuando nos
refiramos a cualquiera de las dos). El tipo X es unit, mientras el tipo X no lo es.
En particular, T = ∀X .∀Y.X ⇒ Y ⇒ X y F = ∀X .∀Y.X ⇒ Y ⇒ Y . El tipo de H es
 
1 1
∀X. [ √ (T + F )] ⇒ [ √ (T + F )] ⇒ X ⇒ X
2 2

Donde [A] = (∀X .X ⇒ X ) ⇒ A.

Capítulo 5. Extensiones cuánticas al lambda cálculo 87

Gramática de los tipos. Formalizando lo anterior, la gramática de los tipos es la

siguiente:

A ::= U | α.A | A + A | X
U ::= X | U ⇒ A | ∀X .U | ∀X.U

Consideramos también las siguientes equivalencias entre tipos, la cual es una congruencia:

1.A ≡ A α.A + β.A ≡ (α + β).A

α.(β.A) ≡ (α × β).A A+B ≡ B+A
α.A + α.B ≡ α.(A + B) A + (B + C) ≡ (A + B) + C

Observación. Por una cuestión técnica, la equivalencia A + 0.B ≡ A no es válida, y por

lo tanto la propiedad de subject reduction es más débil, en el sentido de que si Γ ` t : A
y t →p r, sólo se puede asegurar que Γ ` r : B donde si la regla por la cual se redujo t a
r no es una regla de factorización, entonces B = A, en otro caso, A puede ser B + 0.C.
De todas maneras, obviaremos este detalle técnico en este apunte, y se refiere al lector a
[Arrighi, Díaz-Caro, y Valiron, 2017, §4.2] para más detalles.

Reglas de tipado. Las reglas de tipado se detallan a continuación. Usamos [T /X] para
referir a [U/X ] o [A/X].

Γ`t:A 0 Γ, x : U ` t : A
ax ⇒I
Γ, x : U ` x : U Γ ` 0 : 0.A I Γ ` λx.t : U ⇒ A

Γ ` t : ni=1 αi .∀X.(U ⇒ Ai ) Γ ` r : m
P P
j=1 βj .U [T /X]
Pn Pm ⇒E
Γ ` tr : i=1 j=1 αi × βj .Ai [Tj /X]

Γ ` t : ni=1 αi .Ui X ∈ Γ ` t : ni=1 αi .∀X.Ui

P P
/ FV(Γ)
∀I ∀E
Γ ` t : ni=1 αi .∀X.Ui Γ ` t : ni=1 αi .Ui [T /X]
P P

Γ ` t : A αI Γ`t:A Γ`r:B + Γ`t:A A≡B ≡

I
Γ ` α.t : α.A Γ`t+r :A+B Γ`t:B
Ejemplo 5.4 (Tipando Hadamard). Sean |0i = λx.λy.x y |1i = λx.λy.y. Es fácil verificar
que

` |0i : ∀X Y.X ⇒ Y ⇒ X ,
` |1i : ∀X Y.X ⇒ Y ⇒ Y.

Observación. Usamos la notación ∀XY.A para ∀X.∀Y.A.

También definimos las siguientes superposiciones:

1 1
|+i = √ .(|0i + |1i) y |−i = √ .(|0i − |1i).
2 2
88 5.2. Control y datos cuánticos

De la misma manera,definimos
1

= √ .((∀X Y.X ⇒ Y ⇒ X ) + (∀X Y.X ⇒ Y ⇒ Y)),
2
1
 = √ .((∀X Y.X ⇒ Y ⇒ X ) − (∀X Y.X ⇒ Y ⇒ Y)).
2
Es fácil verificar que ` [|+i] : [
] y ` [|−i] : [].
Para simplificar la notación, tomamos A = [
] ⇒ [] ⇒ [X]. Entonces
ax
x:A`x:A x : A ` [|+i] : [
]
⇒E
x : A ` x[|+i] : [] ⇒ [X] x : A ` [|−i] : []
⇒E
x : A ` x[|+i][|−i] : [X]
⇒E
x : A ` {x[|+i][|−i]} : X
⇒I
` λx.{x[|+i][|−i]} : A ⇒ X
∀
` λx.{x[|+i][|−i]} : ∀X.([
] ⇒ [] ⇒ [X]) ⇒ X I
Ahora podemos aplicar Hadamard a un qubit para obtener el tipo correcto. Sea H =
λx.{x[|+i][|−i]}.
` |0i : ∀X Y.X ⇒ Y ⇒ X
∀
` H : ∀X.([
] ⇒ [] ⇒ [X]) ⇒ X ` |0i : ∀Y.[
] ⇒ Y ⇒ [
] E
∀E ∀
` H : ([
] ⇒ [] ⇒ [
]) ⇒
` |0i : [
] ⇒ [] ⇒ [
] E
⇒E
` H|0i :

Un ejemplo aún más interesante es el siguiente. Sea
1

I = √ .(([
] ⇒ [] ⇒ [
]) + ([
] ⇒ [] ⇒ []))
2
Es decir,
I es
donde los forall han sido instanciados. Es fácil verificar que ` |+i :
I .
Entonces,
` H : ∀X.([
] ⇒ [] ⇒ [X]) ⇒ X ` |+i :
I
⇒E
` H|+i : √12 .
+ √12 .
Y dado que √1 .
+ √12 . ≡ ∀X Y.X → Y → X , podemos concluir
2

` H|+i : ∀X Y.X ⇒ Y ⇒ X .
Notar que H|+i →∗ |0i.

Ejercicio: Escribir el algoritmo de teleportación en Lineal no tipado.

5.2.3. Tipando superposiciones y mediciones proyectivas

En esta sección veremos un trabajo muy reciente [Díaz-Caro y Dowek, 2017; Rinaldi,
2018].
El principal objetivo es agregar medición a Lineal, el cálculo presentado en la Sec-
ción 5.2.2. Como se mencionó anteriormente, para evitar el clonado se conocen dos téc-
nicas:
Capítulo 5. Extensiones cuánticas al lambda cálculo 89

(LL) Usar términos lineales en el sentido de la lógica lineal, y entonces λx.x ⊗ x es un

término mal formado.

(AL) Usar un sistema de reescritura que defina las aplicaciones como aplicaciones lineales,
así λx.x ⊗ x es permitido, pero al aplicarlo a α.|0i + β.|1i producirá α.|00i + β.|11i
y no (α.|0i + β.|1i) ⊗ (α.|0i + β.|1i).

Sin embargo, definir aplicaciones lineales por medio de reescritura no funciona si el cálculo
tiene medición, ya que sólo las compuertas cuánticas se comportan de esa manera. Por
ejemplo, digamos que tenemos un operador de medición notado por π, entonces

(λx.πx)(α.|0i + β.|1i) →∗ α.(λx.πx)|0i + β.(λx.πx)|1i →∗ α.|0i + β.|1i

lo cual claramente es un error.

En este cálculo se propone usar una combinación de las dos técnicas, LL y AL, de esa
manera, una abstracción podrá tomar una superposición, pero sólo en el caso de que la
trate linealmente, en el sentido de LL, en otro caso, la aplicación sólo podrá comportarse
en el sentido de AL.
Claro que para eso, debemos distinguir términos superpuestos de términos que no lo
están.

Gramáticas

La gramática de tipos se separa en dos niveles ya que este cálculo es de primer orden (por
razones que luego discutiremos).

Ψ := Bn | S(Ψ) | Ψ × Ψ Tipos qubit (Q)

A := Ψ | Ψ ⇒ A | S(A) | A × A Tipos generales (T )

La gramática de términos es la siguiente:

b := x | λx:Ψ.t | |0i | |1i | b × b Términos de base (B)

v := b | (v + v) | ~0S(A) | α.v | v × v Valores (V)
t := v | tt | (t + t) | πj t | isZ()?t : t | α.t | t × t | head t | tail t |⇑r t |⇑` t Términos (Λ)

con α ∈ C.
Utilizamos la notación isZ(t)?r : s para (isZ()?r : s)t. El motivo de considerar a isZ()?r : s
como una función es aprovechar la linealidad AL de las funciones, de esa manera,

isZ((α.|0i + β.|1i))?r : s →∗ α.isZ(|0i)?r : s + β.isZ(|1i)?r : s

Dentro de la gramática de términos, distinguimos dos subgramáticas, la de los términos

de base, y la de los valores, que son combinaciones lineales de términos de base.
90 5.2. Control y datos cuánticos

Tipos

Dado que la semántica operacional de una aplicación será diferente si el argumento es

una superposición o no, y esa información la sabremos utilizando los tipos, debemos dar
primero los tipos, y luego la semántica operacional dependiente de ellos.
La lógica de los tipos es que marcamos con una S a las superposiciones, de la misma
manera que en lógica lineal se marca con ! a los términos que pueden ser duplicados.
En realidad, nuestras superposiciones son exactamente los términos que no pueden ser
copiados, y por ese motivo no utilizamos notación de lógica lineal.
Naturalmente existe un subtipado: si un término no es una superposición, es decir, puede
ser copiado, también puede ser tratado como una superposición y por lo tanto no ser
copiado. Es decir, B  S(B).
Formalmente, la relación  es un preorden definido por

A  S(A) S(S(A))  S(A)

AB AB AB AB

Ψ⇒AΨ⇒B S(A)  S(B) A×C B×C C ×AC ×B

Observación. Notar que con esta definición, S(S(A)) ≡ S(A).

El sistema de tipos se define a continuación:

Ax Ax~0 Ax|0i Ax|1i

x:Ψ`x:Ψ ` ~0S(A) : S(A) ` |0i : B ` |1i : B

Γ`t:A Γ`t:A ∆`u:A Γ ` t : S(Bn )

SIα SI+ SE
Γ ` α.t : S(A) Γ, ∆ ` (t + u) : S(A) Γ ` πj t : Bj × S(Bn−j )

Γ ` t : A (AB)  Γ`t:A Γ`r:A If

Γ, x : Ψ ` t : A ⇒I
Γ`t:B Γ ` isZ()?t : r : B ⇒ A Γ ` λx:Ψ.t : Ψ ⇒ A

∆`u:Ψ Γ`t:Ψ⇒A ⇒E
∆ ` u : S(Ψ) Γ ` t : S(Ψ ⇒ A) ⇒ES
∆, Γ ` tu : A ∆, Γ ` tu : S(A)

Γ`t:A W
Γ, x : Bn , y : Bn ` t : A C
Γ, x : Bn ` t : A Γ, x : Bn ` (x/y)t : A

Γ`t:A ∆`u:B ×I Γ ` t : Bn n>1 ×Er

Γ ` t : Bn n>1 ×El
Γ, ∆ ` t × u : A × B Γ ` head t : B Γ ` tail t : Bn−1

Γ ` t : S(S(A) × B) Γ ` t : S(A × S(B))

⇑r ⇑`
Γ `⇑r t : S(A × B) Γ `⇑` t : S(A × B)
Capítulo 5. Extensiones cuánticas al lambda cálculo 91

Semántica operacional

If b has type Bn and b ∈ B, (λx:Bn .t)b −→(1) (b/x)t (βb )

Beta

If u has type S(Ψ), (λx:S(Ψ).t)u −→(1) (u/x)t (βn )

isZ(|1i)?t : r −→(1) t (if1 )
If

isZ(|0i)?t : r −→(1) r (if0 )

n
If t has type B ⇒ A, t(u + v) −→(1) (tu + tv) (lin+r )
If t has type Bn ⇒ A, (α.u) −→(1) α.tu (linαr )
Distribuciones

If t has type Bn ⇒ A, t~0S(Bn ) −→(1) ~0S(A)

lineales

(lin0r )
(t + u)v −→(1) (tv + uv) (lin+l )
(α.t)u −→(1) α.tu (linαl )
~0S(Bn ⇒A) t −→(1) ~0S(A) (lin0l )
(~0S(A) + t) −→(1) t (neutral)
Axiomas de espacios vectoriales

1.t −→(1) t (unit)

If t has type A, 0.t −→(1) ~0S(A) (zeroα )
α.~0S(A) −→(1) ~0S(A) (zero)
α.(β.t) −→(1) (αβ).t (prod)
α.(t + u) −→(1) (α.t + α.u) (αdist)
(α.t + β.t) −→(1) (α + β).t (fact)
(α.t + t) −→(1) (α + 1).t (fact1 )
(t + t) −→(1) 2.t (fact2 )
~0S(S(A)) −→(1) ~0S(A) (zeroS )
If h 6= u × v and h ∈ B, head h × t −→(1) h (head)
Listas

If h 6= u × v and h ∈ B, tail h × t −→(1) t (tail)

⇑r (r + s) × u −→(1) (⇑r r × u + ⇑r s × u) (dist+ r )
⇑` u × (r + s) −→(1) (⇑` u × r + ⇑` u × s) (dist+ l )
⇑r (α.r) × u −→(1) α. ⇑r r × u (distαr )
⇑` u × (α.r) −→(1) α. ⇑r u × r (distαl )
Casteo

If u has type B, ⇑r ~0S(A) × u −→(1) ~0S(A×B) (dist0r )

If u has type A, ⇑` u × ~0S(B) −→(1) ~0S(A×B) (dist0l )
⇑ (t + u) −→(1) (⇑ t + ⇑ u) (dist+ ⇑)
⇑ (α.t) −→(1) α. ⇑ t (distα⇑ )
If u ∈ B, ⇑r u × v −→(1) u × v (neut⇑r )
If v ∈ B, ⇑` u × v −→(1) u × v (neut⇑l )
n m 2jf
−1
Proy.

P Q
πj ( [αi .] |bhi i) −→(1) pk (|ki × |φk i) (proj)
i=1 h=1 k=0
If t −→(1) u, then
contextuales

n n
tv −→(1) uv (λxB .v)t −→(1) (λxB .v)u (t + v) −→(1) (u + v)
Reglas

α.t −→(1) α.u πj t −→(1) πj u t × v −→(1) u × v

v × t −→(1) v × u ⇑r t −→(1) ⇑r u ⇑` t −→(1) ⇑` u
head t −→(1) head u tail t −→(1) tail u isZ(t)?r : s −→(1) isZ(u)?r : s
92 5.2. Control y datos cuánticos

donde, en la regla (proj), se tiene:

j≤m
|ki = |b1 i × · · · × |bj i donde b1 . . . bj es la representación binaria de k
 
m
X αi Y
|φk i =  qP  |bhi i
|α |2
i∈Tk r∈Tk r h=j+1
2
 
X |α |
pk = Pn i 2
i∈Tk
r=1 |αr |

Tk = {i ≤ n | |b1i i × · · · × |bji i = |ki}

Primer orden. El motivo de utilizar primer orden es que en este cálculo hemos mez-
clado los dos enfoques precedentes: LL y AL, y por lo tanto ahora es posible construir
una máquina de clonado si se permite alto orden. El truco es esconder dentro de una
abstracción una superposición, por ejemplo λx:B.α.|0i + β.|1i. Éste es un término dupli-
cable, y no hay problema en ello (no es una superposición, es un programa que produce
una). Sin embargo, dado que ahora tenemos términos LL, podríamos también producir
λy:S(B).λx:B.y, el cual nos permite generar superposiciones duplicables. La solución es
impedir tomar una abstracción como argumento, y por lo tanto este término no podrá
ser duplicado.

Multiple qubits: casteo

Consideremos el siguiente ejemplo:

|0i × (|0i + |1i) → |0i × |0i + |0i × |1i (5.1)

El primer término podría ser tipado con B ⊗ S(B), en cambio el segundo debería ser
tipado con S(B ⊗ B). Naturalmente el subipado va en sentido contrario al necesario:
B ⊗ S(B)  S(B ⊗ B), y por lo tanto este ejemplo rompe la propiedad de preservación de
tipos.
Es normal, en matemática, que al desarrollar un término perdamos información. Por
ejemplo, (x − 1)(x − 2) = x2 − 3x + 2. La información del término izquierdo, que da
sus raíces y una factorización, es perdida al desplegar el término. Por este motivo, no
permitimos la reducción (5.1). En cambio, para poder realizar esa reducción, se debe
castear el término, y entonces el tipo es preservado:

⇑` |0i × (|0i + |1i) → |0i × |0i + |0i × |1i

Teorema 5.5 (Preservación de tipos en términos cerrados, [Díaz-Caro y Dowek, 2017,

Teorema 2]). Si t −→(pi ) ui and ` t : A, entonces ` ui : A.

Teorema 5.6 (Normalización fuerte, [Rinaldi, 2018, Teorema 5.16]). Si ` t : A entonces

t es fuertemente normalizante.
Capítulo 5. Extensiones cuánticas al lambda cálculo 93

Algoritmo de Deutsch
La compuerta Hadamard puede ser implementada de la siguiente manera:
√
H = λx:B.1/ 2.(|0i + (isZ(x)?(−|1i) : |1i))

Notar que la variable es un tipo de base, y por lo tanto, si H se aplica a una superposición,
por ejemplo (α.|0i + β.|1i), reduce de la siguiente manera:
(lin+ ) (linα )2
H(α.|0i + β.|1i) −→r (1) (Hα.|0i + Hβ.|1i) −→r (1) (α.H|0i + β.H|1i)

y por lo tanto, finalmente se aplica a términos de base.

Definimos H1 como la función que toma dos qubits y aplica H al primero:

H1 = λx:B × B ((H (head x)) × (tail x))

Similarmente, Hboth aplica H a ambos qubits:

Hboth = λx:B × B ((H (head x)) × (H (tail x)))

El oráculo Uf está definido por:

Uf |xyi = |x, y ⊕ f (x)i

donde ⊕ es la suma modulo 2. Para implementarlo, necesitamos la compuerta not, la que

puede ser implementada como sigue:

not = λx:B (isZ(x)?|0i : |1i)

Entonces, Uf es:

Uf = λx:B × B ((head x) × (isZ((tail x))?(not (f (head x))) : (f (head x))))

donde f es una función dada de tipo B ⇒ B.

Finalmente, el algoritmo de Deutsch combina todas las definiciones previas:

Deutschf = π1 (⇑r H1 (Uf ⇑` ⇑r Hboth (|0i × |1i)))

Los casteos luego de las compuertas Hadamard se necesitan para desarrollar el término
por completo para luego poder pasarlo a una abstracción que espera términos de base.
El término Deutschf se tipa como sigue:

` Deutschf : B × S(B)

Este término, en la función identidad, reduce así:

√ √ (proj) √ √
Deutschid −→∗(1) π1 (1/ 2.|10i − 1/ 2.|11i) −→(1) |1i × (1/ 2.|0i − 1/ 2.|1i)
94 5.2. Control y datos cuánticos

Algoritmo de teleportación En el ejemplo precedente la aplicación de la medición

tenía sólo un resultado posible: el primer qubit ya estaba en un estado de base antes de
medirlo. Por lo tanto, introducimos un ejemplo un poco más complejo, la teleportación,
donde la medición es usada como un operador que cambia el estado.
La compuerta cnot la implementamos como sigue:

cnot = λx : B × B ((head x) × (isZ((head x))?(not (tail x)) : (tail x)))

Definimos H31 que aplica H al primer qubit en un sistema de tres qubits:

H31 = λx:B × B × B ((H (head x)) × (tail x))

Notar que la única diferencia con H1 es el tipo de la variable. También, necesitamos aplicar
cnot a los dos primeros qubits de un sistema de tres qubits, por lo que definimos cnot312 :

λx:B × B × B ((cnot (head x × (head tail x))) × (tail tail x))

La compuerta Z se implementa de manera similar a not:

Z = λx:B (isZ(x)?(−|1i) : |0i)

A la parte de Alice la definimos así:

Alice = λx:S(B) × S(B × B) (π2 (⇑r H31 (cnot312 (⇑` ⇑r x))))

Notar que antes de pasar a cnot312 el parámetro de tipo S(B) × S(B × B), necesitamos
desarrollar el término por completo usando dos casteos, y de nuevo luego de la compuerta
Hadamard.
El lado de Bob del algoritmo aplicará ciertas compuertas basado en los bits que reciba de
Alice. Por lo tanto, para cualquier ` U : B ⇒ S(B) o ` U : B ⇒ B, definimos U(b) como
la función que aplica U o no dependiendo del bit b:

U(b) = (λx:B λy:B (isZ(x)?Uy : y)) b

Bob se implementa como sigue:

Bob = λx:B × B × B (Z(head x)

(not(head tail x)
(tail tail x)))

El estado de Bell lo definimos directamente:

√ √
β00 = (1/ 2.|00i + 1/ 2.|11i)

Finalmente, la teleportación se define por:

Telep = λq:S(B) (Bob(⇑` Alice (q × β00 )))

Este tipo tiene el tipo esperado S(B) ⇒ S(B), y aplicado a cualquier superposición
(α.|0i + β.|1i) reduce, como es de esperarse, a (α.|0i + β.|1i).
Bibliografía

Pablo Arrighi, Alejandro Díaz-Caro, y Benoît Valiron. The vectorial lambda-calculus.

Information and Computation, 254(1):105–139, 2017.

Pablo Arrighi y Gilles Dowek. Linear-algebraic lambda-calculus: higher-order, encodings,

and confluence. En Proceedings of RTA-2008, (editado por Andrei Voronkov), tomo
5117 de Lecture Notes in Computer Science, págs. 17–31. Springer, 2008.

Pablo Arrighi y Gilles Dowek. Lineal: A linear-algebraic lambda-calculus. Logical Methods

in Computer Science, 13(1:8), 2017. doi:10.23638/LMCS-13(1:8)2017.

Charles Bennett y Gilles Brassard. Quantum cryptography: Public key distribution and
coin tossing. En Proceedings of IEEE International Conference on Computers, Systems
and Signal Processing, págs. 175–179. 1984.

Charles Bennett, Gilles Brassard, Claude Crépeau, Richard Jozsa, Asher Peres, y William
Wootters. Teleporting an unknown quantum state via dual classical and Einstein–
Podolsky–Rosen channels. Physical Review Letters, 70(13):1895–1899, 1993.

Charles Bennett y Stephen Wiesner. Communication via one- and two-particle operators
on Einstein–Podolsky–Rosen states. Physical Review Letters, 69(20):2881–2884, 1992.

Charles H. Bennett. Logical reversibility of computation. IBM Journal of Research and

Development, 17(6):525–532, 1973.

Garret Birkhoff y John von Neumann. The logic of quantum mechanics. Annals of
Mathematics, 37(4):823–843, 1936.

Julian Brown. The Quest for the Quantum Computer. Touchstone, 2001.

David Deutsch. Quantum theory, the church-turing principle and the universal quantum
computer. Proceedings of the Royal Society of London. Series A, Mathematical and
Physical Sciences, 400(1818):97–117, 1985.

David Deutsch y Richard Jozsa. Rapid solution of problems by quantum computation.

Proceedings of the Royal Society of London A: Mathematical, Physical and Engineering
Sciences, 439(1907):553–558, 1992.

Roberto Di Cosmo y Dale Miller. Linear logic. The Stanford Encyclopedia of Philo-
sophy, Winter Edition, 2016. Edward N. Zalta (ed.). https://plato.stanford.edu/
archives/win2016/entries/logic-linear.

95
96 Bibliografía

Alejandro Díaz-Caro y Gilles Dowek. Typing quantum superpositions and measurement.

En Theory and Practice of Natural Computing (TPNC 2017), (editado por Carlos
Martín-Vide, Roman Neruda, y Miguel A. Vega-Rodríguez), tomo 10687 de Lecture
Notes in Computer Science, págs. 281–293. Springer, Cham, 2017.

Paul A. M. Dirac. A new notation for quantum mechanics. Mathematical Proceedings of

the Cambridge Philosophical Society, 35(03):416–418, 1939.

Gilles Dowek y Jean-Jacques Lévy. Introduction to the theory of programming languages.

Undergraduate topics in computer science. Springer, 2011.

Albert Einstein, Boris Podolsky, y Nathan Rosen. Can quantum-mechanical description

of physical reality be considered complete? Physical Review, 44(10):777–780, 1935.

Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures dans

l’arithmétique d’ordre supérieure. Tesis Doctoral, Université Paris Diderot, París, Fran-
cia, 1972.

Jean-Yves Girard. Linear logic. Theoretical Compututer Science, 50:1–102, 1987.

Lov K. Grover. A fast quantum mechanical algorithm for database search. En Proceedings
of the 28th Annual ACM Symposium on Theory of computing, STOC-96, págs. 212–219.
ACM, 1996.

A. Kfoury, J. Tiuryn, y P. Urzyczyn. The undecidability of the semi-unification problem.

En Proceedings of STOC-1990, págs. 468–476. 1990.

Michael Nielsen y Isaac Chuang. Quantum Computation and Quantum Information. 10th
Anniversary Edition. Cambridge University Press., 2010.

Gordon Plotkin. LCF considered as a programming language. Theoretical Computer

Science, 5(3):223–255, 1977.

John Preskill. Quantum computing: pro and con. Proceedings of the Royal Society of
London A, 454:469–486, 1998.

John C. Reynolds. Towards a theory of type structure. En Programming Symposium:

Proceedings of the Colloque sur la Programmation, (editado por Bernard Robinet),
tomo 19 de Lecture Notes in Computer Science, págs. 408–425. Springer, 1974.

Juan Pablo Rinaldi. Demostrando normalización fuerte sobre una extensión cuántica del
lambda cálculo. Proyecto Fin de Carrera, Universidad Nacional de Rosario, Argentina,
2018.

Peter Selinger. Towards a quantum programming language. Mathematical Structures in

Computer Science, 14(4):527–586, 2004.

Peter Selinger y Benoît Valiron. A lambda calculus for quantum computation with clas-
sical control. Mathematical Structures in Computer Science, 16(3):527–552, 2006.
Bibliografía 97

Peter W. Shor. Polynomial-time algorithms for prime factorization and discrete loga-
rithms on a quantum computer. SIAM Journal on Computing, 26(5):1484–1509, 1997.

Morten H. Sørensen y Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism,

tomo 149 de Studies in Logic and the Foundations of Mathematics. Elsevier, 2006.

André van Tonder. A lambda calculus for quantum computation. SIAM Journal on
Computing, 33:1109–1135, 2004.

Gilbert S. Vernam. Cipher printing telegraph systems for secret wire and radio telegrap-
hic communications. Transactions of the American Institute of Electrical Engineers,
XLV:295–301, 1926.

Joe B. Wells. Typability and type checking in the second-order lambda-calculus are equi-
valent and undecidable. En Proceedings of LICS-1994, págs. 176–185. IEEE Computer
Society, 1994.

William K. Wootters y Wojciech .H. Zurek. A single quantum cannot be cloned. Nature,
299:802–803, 1982.