SBMF 2008

arXiv:0707.1527v2 [quant-ph] 29 Jul 2009

Programming Telepathy: Implementing

Quantum Non-locality Games

Anya Tafliovich1 ,2
Computer Science
University of Toronto
Toronto, Canada

Eric C. R. Hehner3
Computer Science
University of Toronto
Toronto, Canada

Abstract
Quantum pseudo-telepathy is an intriguing phenomenon which results from the application of quantum
information theory to communication complexity. To demonstrate this phenomenon researchers in the field
of quantum communication complexity devised a number of quantum non-locality games. The setting of
these games is as follows: the players are separated so that no communication between them is possible
and are given a certain computational task. When the players have access to a quantum resource called
entanglement, they can accomplish the task: something that is impossible in a classical setting. To an
observer who is unfamiliar with the laws of quantum mechanics it seems that the players employ some sort
of telepathy; that is, they somehow exchange information without sharing a communication channel.
This paper provides a formal framework for specifying, implementing, and analysing quantum non-locality
games.

Keywords: Quantum computing, quantum non-locality, pseudo-telepathy games, formal verification,

formal methods of software design, logic of programming

1 This work is in part supported by NSERC

2 Email: anya@[Link]
3 Email: hehner@[Link]
This paper is electronically published in
Electronic Notes in Theoretical Computer Science
URL: [Link]/locate/entcs
 Tafliovich

1 Introduction

The work develops a formal framework for specifying, implementing, and analysing
quantum pseudo-telepathy: an intriguing phenomenon which manifests itself when
quantum information theory is applied to communication complexity. To demon-
strate this phenomenon researchers in the field of quantum communication complex-
ity devised a number of quantum non-locality games. The setting of these games
is as follows: the players are separated so that no communication between them is
possible and are given a certain computational task. When the players have access
to a quantum resource called entanglement, they can accomplish the task: some-
thing that is impossible in a classical setting. To an observer who is unfamiliar with
the laws of quantum mechanics it seems that the players employ some sort of telepa-
thy; that is, they somehow exchange information without sharing a communication
channel.
Quantum pseudo-telepathy, and quantum non-locality in general, are perhaps
the most non-classical and the least understood aspects of quantum information
processing. Every effort is made to gain information about the power of these phe-
nomena. Quantum non-locality games in particular have been extensively used to
prove separations between quantum and classical communication complexity. The
need for a good framework for formal analysis of quantum non-locality is evident.
We look at quantum non-locality in the context of formal methods of program
development, or programming methodology. This is the field of computer science
concerned with applications of mathematics and logic to software engineering tasks.
In particular, the formal methods provide tools to formally express specifications,
prove correctness of implementations, and reason about various properties of spec-
ifications (e.g. implementability) and implementations (e.g. time and space com-
plexity).
In this work the analysis of quantum non-locality is based on quantum pred-
icative programming ([33,32]), a recent generalisation of the well-established pred-
icative programming ([23,24,25]). It supports the style of program development in
which each programming step is proved correct as it is made. We inherit the advan-
tages of the theory, such as its generality, simple treatment of recursive programs,
and time and space complexity. The theory of quantum programming provides tools
to write both classical and quantum specifications, develop quantum programs that
implement these specifications, and reason about their comparative time and space
complexity all in the same framework.
Presenting new non-locality paradigms or new pseudo-telepathy games is not
the subject of this work. Our goal is developing a formal framework that encom-
passes all aspects of quantum computation and information. Formal analysis of
quantum algorithms, including their time complexity, is presented in [33]. Analysis
of quantum communication appears in [34]. This paper focuses on formal analysis
of non-locality paradigms; we choose known pseudo-telepathy games as illustrative
examples of our formalism.
The rest of this work is organised as follows. Section 2 is a brief introduction to
quantum predicative programming. The contribution of this work is Section 3 which
introduces a formal framework for specifying, implementing, and analysing quan-
2
 Tafliovich

tum pseudo-telepathy and presents several examples of implementing and analysing

non-locality games. Section 5 states conclusions and outlines directions for future
research. A brief introduction to quantum computing is included in the Appendix.

1.1 Our contribution and related work

This work attempts to bring together two areas of active research: the study of
quantum non-locality and applications of formal methods to quantum information
and computation. Currently, the two worlds rarely meet.
Quantum non-locality has been studied extensively first by physicists and lately
by researchers in the fields of quantum information and quantum communication
complexity. Since the work of Bell in 1964 ([8]), researchers have been trying to
provide an intuitive explanation of the genuinely non-classical behaviour produced
by quantum mechanics. Today, quantum pseudo-telepathy games are considered one
of the best and easiest to understand examples of these non-classical phenomena
(e.g. [21,14,11,12]).
Formal approaches to quantum programming include the language
qGCL [30,38,39], process algebraic approaches developed in [4,27,26], tools
developed in the field of category theory by [1,2,3,16,31], functional languages
of [6,7,5,35,36], as well as work of [20,19], [17], and [22]. A detailed discussion
of the work related to quantum predicative programming is presented in [33].
Some researchers address the subject of formalising quantum non-locality more
directly than others (e.g. [38]). To the best of our knowledge, formal approaches to
reasoning about quantum pseudo-telepathy games have not been considered.

2 Quantum Predicative Programming

This section introduces the programming theory of our choice — quantum predica-
tive programming. We briefly introduce parts of the theory necessary for under-
standing Section 3 of this work. For a course in predicative programming the reader
is referred to [23]. An introduction to probabilistic predicative programming can
be found in [24,25]. Quantum predicative programming is developed in [33,32] and
is extended with reasoning about quantum communication in [34].

2.0.1 Predicative programming

In predicative programming a specification is a boolean expression. The variables
in a specification represent the quantities of interest, such as prestate (inputs),
poststate (outputs), and computation time and space. We use primed variables to
describe outputs and unprimed variables to describe inputs. For example, speci-
fication x′ = x + 1 in one integer variable x states that the final value of x is its
initial value plus 1. A computation satisfies a specification if, given a prestate, it
produces a poststate, such that the pair makes the specification true. A specifica-
tion is implementable if for each input state there is at least one output state that
satisfies the specification.
We use standard logical notation for writing specifications: ∧ (conjunction), ∨
(disjunction), ⇒ (logical implication), = (equality, boolean equivalence), 6= (non-
3
 Tafliovich

equality, non-equivalence), and if then else. The larger operators == , =⇒, ≤ ,

and ≥ are the same as =, ⇒, ≤, and ≥, but with lower precedence. We use
standard mathematical notation, such as + − × / mod. We use lowercase letters
for variables of interest and uppercase letters for specifications.
In addition to the above, we use the following notations: σ (prestate), σ ′ (post-
state), ok (σ ′ = σ), and x := e defined by x′ = e ∧ y ′ = y ∧ . . .. The notation ok
specifies that the values of all variables are unchanged. In the assignment x := e, x
is a state variable (unprimed) and e is an expression (in unprimed variables) in the
domain of x.
If R and S are specifications in variables x, y, . . . , then the sequential composition
of R and S is defined by

R; S == ∃x′′ , y ′′ , . . . · R′′ ∧ S ′′

where R′′ is obtained from R by substituting all occurrences of primed variables

x′ , y ′ , . . . with double-primed variables x′′ , y ′′ , . . . , and S ′′ is obtained from S by
substituting all occurrences of unprimed variables x, y, . . . with double-primed vari-
ables x′′ , y ′′ , . . . .
Various laws can be proved about sequential composition. One of the most
important ones is the substitution law, which states that for any expression e of the
prestate, state variable x, and specification P ,

x := e; P == (for x substitute e in P )
Specification S is refined by specification P if and only if S is satisfied whenever
P is satisfied, that is ∀σ, σ ′ · S ⇐ P . Given a specification, we are allowed to
implement an equivalent specification or a stronger one.
A program is an implemented specification. A good basis for classical (non-
quantum) programming is provided by: ok, assignment, if then else, sequential
composition, booleans, numbers, bunches, and functions.
Given a specification S, we proceed as follows. If S is a program, there is no
work to be done. If it is not, we build a program P , such that P refines S, i.e.
S ⇐ P . The refinement can proceed in steps: S ⇐ . . . ⇐ R ⇐ Q ⇐ P .
In S ⇐ P it is possible for S to appear in P . No additional rules are required
to prove the refinement. For example, it is trivial to prove that

x ≥ 0 ⇒ x′ = 0 ⇐= if x = 0 then ok else (x := x − 1 ; x ≥ 0 ⇒ x′ = 0)

The specification says that if the initial value of x is non-negative, its final value
must be 0. The solution is: if the value of x is zero, do nothing, otherwise decrement
x and repeat.

2.0.2 Probabilistic predicative programming

A probability is a real number between 0 and 1, inclusive. A distribution is an
expression whose value is a probability and whose sum over all values of variables
is 1. Given a distribution of several variables, we can sum out some of the variables
to obtain a distribution of the rest of the variables.
4
 Tafliovich

To generalise boolean specifications to probabilistic specifications, we use 1 and

0 both as numbers and as boolean true and false, respectively. 4 If S is an im-
plementable deterministic specification and p is a distribution of the initial state
x, y, ..., then the distribution of the final state is
X
x, y, ... · S × p

If R and S are specifications in variables x, y, . . . , then the sequential composition

of R and S is defined by
X
R; S == x′′ , y ′′ , . . . · R′′ × S ′′

where R′′ is obtained from R by substituting all occurrences of primed variables

x′ , y ′ , . . . with double-primed variables x′′ , y ′′ , . . . , and S ′′ is obtained from S by
substituting all occurrences of unprimed variables x, y, . . . with double-primed vari-
ables x′′ , y ′′ , . . . .
If p is a probability and R and S are distributions, then

if p then R else S == p × R + (1 − p) × S

Various laws can be proved about sequential composition. One of the most
important ones, the substitution law, introduced earlier, applies to probabilistic
specifications as well.
We use assignment, sequential composition, and if-then-else to reason about
probability distributions that result from (probabilistically) changing the state vari-
ables. To reason about probability distributions that result from learning some new
information, with no change to the state variables, we use the learn operator, in-
troduced in [25]. If P is the original probability distribution and b is a boolean
expression that describes the information we learn, then the resulting probability
distribution is defined by

P ! b == (P × b′ )/(P ; b)

If P is a non-negative expression (not necessarily a probability distribution),

then P ! 1 is the normalisation of P .
If P and Q are distributions, then P ≤ Q is the generalisation of refinement
P ⇒ Q to the probabilistic case.

2.0.3 Quantum Predicative Programming

Let C be the set of all complex numbers with the absolute value operator | · | and
the complex conjugate operator ∗ . Then a state of an n-qubit system is a function
ψ : 0, ..2n → C, such that x : 0, ..2n · |ψx|2 == 1.
P

If ψ and φ are two states of an n-qubit system, then their inner product, denoted

4 Readers familiar with ⊤ and ⊥ notation can notice that we take the liberty to equate ⊤ = 1 and ⊥ = 0.

5
 Tafliovich

by hψ|φi, is defined by 5 :
X
hψ|φi = x : 0, ..2n · (ψx)∗ × (φx)

A basis of an n-qubit system is a collection of 2n quantum states b0,..2n , such

that ∀i, j : 0, ..2n · hbi |bj i = (i = j). We adopt the following Dirac-like notation
for the computational basis: if x is from the domain 0, ..2n , then x denotes the
corresponding n-bit binary encoding of x and |xi : 0, ..2n → C is the following
quantum state:
|xi = λi : 0, ..2n · (i = x)
If ψ is a state of an m-qubit system and φ is a state of an n-qubit system,
then ψ ⊗ φ, the tensor product of ψ and φ, is the following state of a composite
m + n-qubit system:

ψ ⊗ φ = λi : 0, ..2m+n · ψ(i div 2n ) × φ(i mod 2n )

We write ψ ⊗n to mean ψ tensored with itself n times.

An operation defined on an n-qubit quantum system is a higher-order function,
whose domain and range are maps from 0, ..2n to the complex numbers. An identity
operation on a state of an n-qubit system is defined by

I n = λψ : 0, ..2n → C · ψ

For a linear operation A, the adjoint of A, written A† , is the (unique) operation,

such that for any two states ψ and φ, hψ|Aφi = hA† ψ|φi.
The unitary transformations that describe the evolution of an n-qubit quantum
system are operations U defined on the system, such that U † U = I n .
In this setting, the tensor product of operators is defined in the usual way. If ψ
is a state of an m-qubit system, φ is a state of an n-qubit system, and U and V are
operations defined on m and n-qubit systems, respectively, then the tensor product
of U and V is defined on an m + n qubit system by (U ⊗ V )(ψ ⊗ φ) = (U ψ) ⊗ (V φ).
Just as with tensor products of states, we write U ⊗n to mean operation U ten-
sored with itself n times.
Suppose we have a system of n qubits in state ψ and we measure it. Suppose
also that we have a variable r from the domain 0, ..2n , which we use to record the
result of the measurement, and variables x, y, . . ., which are not affected by the
measurement. Then the measurement corresponds to a probabilistic specification
that gives the probability distribution of ψ ′ and r ′ (these depend on ψ and on the
type of measurement) and states that the variables x, y, . . . are unchanged.
For a general quantum measurement described by a collection M = M0,..2n of
measurement operators, which satisfy the completeness equation (see Appendix A),
the specification is measureM ψ r, where
 
Mr ψ
′
measureM ψ r == hψ|Mr†′ Mr′ ψi × ψ ′ = q  × (σ ′ = σ)
†
hψ|Mr′ Mr′ ψi

5 We should point out that this kind of function operations is referred to as lifting.

6
 Tafliovich

where σ ′ = σ is an abbreviation of (x′ = x) × (y ′ = y) × . . . and means “all other

variables are unchanged”.
The simplest and the most commonly used measurement in the computational
basis is:
measure ψ r == |ψr ′ |2 × (ψ ′ = |r′ i) × (σ ′ = σ)
In this case the distribution of r ′ is |ψr ′ |2 and the distribution of the quantum
state is:
X
r ′ · |ψr ′ |2 × (ψ ′ = |r′ i)
which is precisely the mixed quantum state that results from the measurement.
In order to develop quantum programs we need to add to our list of implemented
things. We add variables of type quantum state as above and we allow the following
three kinds of operations on these variables. If ψ is a state of an n-qubit quantum
system, r is a natural variable, and M is a collection of measurement operators that
satisfy the completeness equation, then:
(i) ψ := |0i⊗n is a program
(ii) ψ := U ψ, where U is a unitary transformation on an n-qubit system, is a
program
(iii) measureM ψ r is a program
The special cases of measurements are therefore also allowed.
The Hadamard transform, widely used in quantum algorithms, is defined on a
1-qubit system and in our setting is a higher-order function on 0, 1 → C:
√
H = λψ : 0, 1 → C · λi : 0, 1 · (ψ0 + (−1)i × ψ1)/ 2

The operation H ⊗n on an n-qubit system applies H to every qubit of the system.

Its action on the zero state of an n-qubit system is:
X √
H ⊗n |0i⊗n = x : 0, ..2n · |xi/ 2n

On a basis state |xi, the action of H ⊗n is:

X √
H ⊗n |xi = y : 0, ..2n · (−1)x·y × |yi/ 2n

where x · y is the inner product of x and y modulo 2.

3 Quantum Non-locality
In predicative programming, to reason about distributed computation we (dis-
jointly) partition the variables between the processes involved in a computation.
Parallel composition is then simply boolean conjunction. For example, consider
two processes P and Q. P owns integer variables x and y and Q owns an integer
variable z. Suppose P == x := x + 1; y := x and Q == z := −z. Parallel
7
 Tafliovich

composition of P with Q is then simply

P ||Q == P ∧ Q
== (x := x + 1 ; y := x) ∧ (z := −z)
== x′ = x + 1 ∧ y ′ = x + 1 ∧ z ′ = −z

In quantum predicative programming, one needs to reason about distributed

quantum systems. Recall that if ψ is a state of an m-qubit system and φ is a
state of an n-qubit system, then ψ ⊗ φ, the tensor product of ψ and φ, is the
state of a composite m + n-qubit system. On the other hand, given a composite
m + n-qubit system, it is not always possible to describe it in terms of the tensor
product of the component m- and n-qubit systems. Such a composed system is
entangled. Entanglement is one of the most non-classical, most poorly understood,
and most interesting quantum phenomena. An entangled system is in some sense
both distributed and shared. It is distributed in the sense that each party can apply
operations and measurements to only its qubits. It is shared in the sense that the
actions of one party affect the outcome of the actions of another party. Simple
partitioning of qubits is therefore insufficient to reason about distributed quantum
computation.
The formalism we introduce fully reflects the physical properties of a distributed
quantum system. We start by partitioning the qubits between the parties involved.
For example, consider two parties P and √ Q. P owns √ the first qubit of the composite
entangled quantum system ψ = |00i/ 2 + |11i/ 2 and Q owns the second qubit.
A specification is a program only if each party computes with its own qubits. In
our example,

P == ψ0 := Hφ0 ; measure ψ0 p and Q == measure ψ1 q

are programs, if p and q are integer variables owned by P and Q, respectively. The
parties P and Q can access only their own qubits: they could in theory be light
years apart.
We define parallel composition of P and Q which share an n+m quantum system
in state ψ with the first n qubits belonging to P and the other m qubits belonging
to Q as follows. If

P == ψ0..n := UP ψ0..n and Q == ψn..n+m := UQ ψn..n+m

where UP is a unitary operation on an n-qubit system and UQ is a unitary operation

on an m-qubit system, then

P ||ψ Q == ψ := (UP ⊗ UQ )ψ

Performing ok is equivalent to performing the identity unitary operation, and

therefore if
P == ψ0,..n := UP ψ0,..n and Q == ok
then
P ||ψ Q == ψ := (UP ⊗ I ⊗m )ψ
8
 Tafliovich

Similarly, if

P == measureMP ψ0..n p and Q == measureMQ ψn..n+m q

where MP and MQ are a collection of proper measurement operators for n- and

m-qubit systems, respectively, then

P ||ψ Q == measureMP ⊗MQ ψ pq

where pq is the number that corresponds to the binary string pq.

In our example,
√ √
ψ := |00i/ 2 + |11i/ 2; P ||ψ Q expand, substitute
√ √
== ψ := |00i/ 2 + |11i/ 2;
measure (Hψ0 ) p ||ψ measure ψ1 q compose on ψ
√ √
== ψ := |00i/ 2 + |11i/ 2; measure (H ⊗ I)ψ pq substitute
√ √
== measure (H ⊗ I)(|00i/ 2 + |11i/ 2) pq apply H ⊗ I
== measure (|00i + |01i + |10i − |11i)/2 pq measure
== |(|00i + |01i + |10i − |11i)/2 pq|2 × (ψ ′ = |p′ q′ i) application
== (ψ ′ = |p′ q′ i)/4

4 Pseudo-telepathy games
We formalise pseudo-telepathy games with n players as follows. For each player i,
0 ≤ i < n, we have a domain Di from which the inputs to player i are provided
and a range Ri of player i’s possible output results. In addition we may have a
promise P : a condition on the inputs to the players. If no promise is given, we
set P to 1. The winning condition W can involve inputs as well as outputs for
each player. The strategy S is a program, i.e. an implemented specification. The
strategy S is winning if, assuming the promise, the strategy yields a distribution
that corresponds to the winning condition:

S !P ≤ W !1

4.1 Deutsch-Jozsa game

The Deutsch-Jozsa pseudo telepathy game [13,11] is based on a well-known Deutsch-

Jozsa algorithm [18]. The setting of the game is as follows. Alice and Bob are
separated several light years apart and are each presented with a 2k -bit string.
They are promised that either the strings are identical or they differ by exactly half
of the bits. To win the game the players must each output a k-bit string, and these
strings should be identical if and only if their input strings were identical.
We formalise the game as follows. We partition the space into the world of Alice
(variables subscripted A) and the world of Bob (variables subscripted B). Then we
9
 Tafliovich

have the following formalisation of the game:

k
DA = DB = {0, 1}2 the domain of inputs
k
RA = RB = {0, 1} the range of outputs
P = P0 ∨ P1 the promise on the inputs, where:
P0 == xA = xB
X
== ( i : 0, ..2k · (xA )i = (xB )i ) = 2k the inputs are identical
X
P1 == ( i : 0, ..2k · (xA )i = (xB )i ) = 2k−1 the inputs differ by half of the bits
′ ′ ′ ′
W == P0 ∧ (yA = yB ) ∨ P1 ∧ (yA 6= yB ) the winning condition

We demonstrate the quantum solution by implementing the following specifica-

tion S:
X √
S == ψ := z : 0, ..2k · |zzi/ 2k ; (SA ||ψ SB ) where
Si == ψi := Ui⊗k ψi ; ψi := H ⊗k ψi ; measure ψi yi for unitary
(xi )z
Ui |zi = (−1) ×|zi where i : A, B

Implementing the initial assignment:

X √
ψ := z : 0, ..2k · |zzi/ 2k
== ψ := |0i⊗2k ; ψ0,..k := H ⊗k ψ0,..k ; ψ := CN OTd⊗k ψ

We begin by analysing the distribution that results from executing the solution
program (we omit domains of u, v, z for clarity and sum out the final quantum state,
since it does not appear in the winning condition)
X
ψ′ · S
X X √
== ψ ′ · ψ := z · |zzi/ 2k ; (SA ||ψ SB ) expand SA , SB
X X √
== ψ ′ · ψ := z · |zzi/ 2k ;
((ψA := UA⊗k ψA ; ψA := H ⊗k ψA ; measure ψA yA ) ||ψ
(ψB := UB⊗k ψB ; ψB := H ⊗k ψB ; measure ψB yB )) substitute
X X √
== ψ ′ · ψ := z · |zzi/ 2k ;
(measure H ⊗k (UA⊗k ψA ) yA ||ψ composition
measure H ⊗k (UB⊗k ψB ) yB ) on ψ
X X √
== ψ ′ · ψ := z · |zzi/ 2k ; substitute and
measure H ⊗2k
⊗ ((UA⊗k
yA yB UB⊗k )ψ) measure
 X √  2
== H ⊗2k (UA⊗k ⊗ UB⊗k ) z · |zzi/ 2k (yA yB )′ ×
(x′A = xA ) × (x′B = xB ) linearity
X  √ 2
== H ⊗2k z · (UA⊗k |zi ⊗ UB⊗k |zi) / 2k (yA yB )′ ×
(x′A = xA ) × (x′B = xB ) apply Ui
10
 Tafliovich

X  √ 2
== H ⊗2k z · (−1)(xA )z ×|zi ⊗ (−1)(xB )z ×|zi) / 2k (yA yB )′ ×
(x′A = xA ) × (x′B = xB ) linearity
X  √ 2
== z · (−1)(xA )z +(xB )z ×H ⊗k |zi ⊗ H ⊗k |zi / 2k (yA yB )′ ×
(x′A = xA ) × (x′B = xB ) apply H
X
== z· (−1)(xA )z +(xB )z×
X √
( u · (−1)z·u × |ui/ 2n ) ⊗
X √ √ 2
( v · (−1)z·v × |vi/ 2n ) ) / 2k (yA yB )′ ×
(x′A = xA ) × (x′B = xB ) collect terms
X √ 3 2
== u, v, z · (−1)(xA )z +(xB )z +u·z+v·z ×|uvi/ 2k (yA yB )′ ×
(x′A = xA ) × (x′B = xB )
X √ 3 2
== u, v, z · (−1)(xA )z ⊕(xB )z ⊕(u⊕v)·z ×|uvi/ 2k (yA yB )′ ×
(x′A = xA ) × (x′B = xB )

To demonstrate that S is winning, we need to show S ! P ≤ W ! 1. Let us perform

some preliminary calculations first:

S × P0′ expand
X √ 3 2
== u, v, z · (−1)(xA )z ⊕(xB )z ⊕(u⊕v)·z ×|uvi/ 2k (yA yB )′ ×
(x′A
= xA ) × (x′B
= xB ) × (x′A
= x′B ) math
X √ 3 2
== u, v, z · (−1)(u⊕v)·z ×|uvi/ 2k (y A yB )
′
×
(x′A = x′B = xA = xB ) sum
X √ 2
== z · |zzi/ 2k (yA yB )′ × (x′A = x′B = xA = xB ) application
== (x′A = x′B = xA = xB ) × (yA
′ ′
= yB )/2k
′ ′
== P0 × (yA = yB )/2k × (x′A = xA ) × (x′B = xB )

Similarly, analysing the amplitudes in the second case, we get:

S × P1′ expand
X √ 3 2
== u, v, z · (−1)(xA )z ⊕(xB )z ⊕(u⊕v)·z × |uvi/ 2k (yA yB )′ ×
X
(x′A = xA ) × (x′B = xB ) × ( i · ((x′A )i = (x′B )i ) == 2k−1 ) split sum
X √ 3
== u 6= v, z · (−1)(xA )z ⊕(xB )z ⊕(u⊕v)·z × |uvi/ 2k +
X √ 3 2
u, z · (−1)(xA )z ⊕(xB )z × |uui/ 2k (yA yB )′ ×
X
(x′A = xA ) × (x′B = xB ) × ( i · ((x′A )i = (x′B )i ) == 2k−1 ) second sum

11
 Tafliovich

X √ 3
== u 6= v, z · (−1)(xA )z ⊕(xB )z ⊕(u⊕v)·z × |uvi/ 2k +
X √ 3 2
u · ((−1) × 2k−1 + 1 × 2k−1 ) × |uui/ 2k (yA yB )′ ×
X
(x′A = xA ) × (x′B = xB ) × ( i · ((x′A )i = (x′B )i ) == 2k−1 ) math
X √ 3 2
== u 6= v, z · (−1)(xA )z ⊕(xB )z ⊕(u⊕v)·z × |uvi/ 2k (yA yB )′ ×
X
(x′A = xA ) × (x′B = xB ) × ( i · ((xA )i = (xB )i ) == 2k−1 ) application
′ ′
== P1 × (yA 6= yB ) × /(2k × (2k − 1)) × (x′A = xA ) × (x′B = xB )

Normalising the winning condition:

W !1 def of !
X
== W/ σ′ · W expand
′ ′ ′ ′
== (P0 × (yA = yB ) + P1 × (yA 6= yB ))/
X
′ ′ ′ ′ ′
yA , yB · P0 × (yA = yB ) + P1 × (yA 6= yB ) sum
′ ′ ′ ′
== (P0 × (yA = yB ) + P1 × (yA 6= yB ))/
(P0 × 2k + P1 × 2k × (2k − 1)) math
′ ′
== P0 × (yA = yB )/2k + P1 × (yA
′ ′
6= yB )/(2k × (2k − 1))

Finally, the strategy is winning since:

S !P def of !
== S × (P0 + P1 )/(S ; (P0 + P1 )) expand
X
== S × P0 + S × P1 / σ ′′ · (S ′′ × (P0′′ + P1′′ )) above proofs
′ ′
== P0 × (yA = yB )/2k × (x′A = xA ) × (x′B = xB )+
′ ′
P1 × (yA 6= yB ) × /(2k × (2k − 1)) × (x′A = xA ) × (x′B = xB )
== (W ! 1) × (x′A = xA ) × (x′B = xB )
≤ W !1

The Deutch-Jozsa game is an example of two-player games. We now turn our

attention to multi-player pseudo-telepathy games.

4.2 Mermin’s game

In Mermin’s game [28] there are three players. Each player i receives a bit xi as
input and outputs a bit yi . The promise is that the sum of the inputs is even. The
players win the game if the parity of the sum of the outputs is equal to the parity
of half the sum of the inputs.
We formalise the game as follows: Di = Ri = {0, 1}, for i : 0, 1, 2. The promise
is P == (x0 ⊕ x1 ⊕ x2 ) = 0. The winning condition is W == (y0′ ⊕ y1′ ⊕ y2′ ) =
(x0 + x1 + x2 )/2.
We implement √ the following
√ quantum strategy. The players share an entangled
state ψ = |000i/ 1 + |111i/ 2. After receiving the input, each player applies the
12
 Tafliovich

√
operation U defined by U |0i = |0i and U |1i = −1 × |1i to her qubit if the input
is 1. The player then applies a Hadamard transform. The qubit is measured in the
computational basis and the result of the measurement is the output.
The program is:
√ √
S == ψ := |000i/ 2 + |111i/ 2 ; S0 ||ψ S1 ||ψ S2
Si == if xi = 1 then ψi := U ψi else ok ; ψi := Hψi ; measure ψi yi

where i : 0, 1, 2.
To prove the solution is correct, we begin by analysing the resulting distributions
of the state variables. As before, we sum out the final quantum state, since it does
not appear in the winning condition.
X
ψ′ · S
X √ √
== ψ ′ · ψ := |000i/ 2 + |111i/ 2 ;
||ψ i : 0, 1, 2 · if xi = 1 then ψi := U ψi else ok ;
ψi := Hψi ; measure ψi yi conditional
X
′
√ √
== ψ · ψ := |000i/ 2 + |111i/ 2 ;
||ψ i : 0, 1, 2 · ψi := U xi ψi ; ψi := Hψi ; measure ψi yi substitute
X √ √
== ψ ′ · ψ := |000i/ 2 + |111i/ 2 ;
||ψ i : 0, 1, 2 · measure H(U xi ψi ) yi compose
X √ √
== ψ ′ · ψ := |000i/ 2 + |111i/ 2 ; substitute
measure H ⊗3 (U x0 ⊗ U x1 ⊗ U x2 ψ) y0 y1 y2 and measure
√ √ 2
== H ⊗3 (U x0 ⊗ U x0 ⊗ U x0 (|000i/ 2 + |111i/ 2)) (y0 y1 y3 )′ ×
((x0 x1 x2 )′ = x0 x1 x2 ) apply U
√ √ √ 2
== H ⊗3 (|000i/ 2 + ( −1)x0 +x1 +x2 × |111i/ 2) (y0 y1 y3 )′ ×
((x0 x1 x2 )′ = x0 x1 x2 )

To demonstrate that the strategy S is winning, we need to show S ! P ≤ W ! 1.

We begin with some preliminary calculations:

S × P′ expand
√ √ √ 2
== H ⊗3 (|000i/ 2 + ( −1)x0 +x1 +x2 × |111i/ 2) (y0 y1 y3 )′ ×
((x0 x1 x2 )′ = x0 x1 x2 ) × (x′0 ⊕ x′1 ⊕ x′2 = 0) split into cases
√ √ 2
== H ⊗3 (|000i/ 2 + |111i/ 2) (y0 y1 y3 )′ ×
((x0 x1 x2 )′ = x0 x1 x2 ) × (x′0 + x′1 + x′2 = 0) +
√ √ 2
H ⊗3 (|000i/ 2 − |111i/ 2) (y0 y1 y3 )′ ×
((x0 x1 x2 )′ = x0 x1 x2 ) × (x′0 + x′1 + x′2 = 2) apply H
13
 Tafliovich

2
== (|000i + |011i + |101i + |110i)/2 (y0 y1 y3 )′ ×
((x0 x1 x2 )′ = x0 x1 x2 ) × (x′0 + x′1 + x′2 = 0) +
2
(|001i + |010i + |100i + |111i)/2 (y0 y1 y3 )′ ×
((x0 x1 x2 )′ = x0 x1 x2 ) × (x′0 + x′1 + x′2 = 2) application
== (y0′ ⊕ y1′ ⊕ y2′ = (x′0 + x′1 + x′2 )/2) × ((x0 x1 x2 )′ = x0 x1 x2 ) × P/4

Normalising the winning condition:

W !1 def of !
X
== W/ σ′ · W expand
== ((y0′ ⊕ y1′ ⊕ y2′ = (x0 + x1 + x2 )/2)/
X
y0′ , y1′ , y2′ · y0′ ⊕ y1′ ⊕ y2′ = (x0 + x1 + x2 )/2 sum
== ((y0′ ⊕ y1′ ⊕ y2′ = (x0 + x1 + x2 )/2)/4 × P

Finally, the strategy S is winning, since:

S !P def of !
′
== S × P /(S ; P ) above proofs
′ ′ ′ ′ ′ ′ ′
== (y0 ⊕ y1 ⊕ y2 = (x0 + x1 + x2 )/2) × ((x0 x1 x2 ) = x0 x1 x2 ) × P/4/
X √ √ √
σ ′′ · |H ⊗3 (|000i/ 2 + ( −1)x0 +x1 +x2 × |111i/ 2(y0 y1 y2 )′′ |2 × math
′′ ′′ ′′ ′′
((x0 x1 x2 ) = x0 x1 x2 ) × (x0 ⊕ x1 ⊕ x2 = 0)
== (y0′ ⊕ y1′ ⊕ y2′ = (x′0 + x′1 + x′2 )/2) × ((x0 x1 x2 )′ = x0 x1 x2 )/4 × P def of W
== (W !1) × ((x0 x1 x2 )′ = x0 x1 x2 )
≤ (W !1)

4.3 Parity Games

In parity games [10,11,15] there are at least three players. Each player i is given
a number αi : 0, ..2l , or, equivalently, an l-bit binary string. The promise is that
i : 0, ..n · αi is divisible by 2l . Each player outputs a single bit βi . The winning
P

condition is that the sum of the outputs is half the sum of the inputs mod 2:
X
P == ( i : 0, ..n · αi ) mod 2l = 0
X X
W == ( i : 0, ..n · βi′ ) mod 2 = ( αi /2l ) mod 2

Consider the√following strategy. The players share an entangled state ψ =

(|0i⊗n + |1i⊗n )/ 2. Each player i executes the following program:

ψi := Ui ψi ; ψi := Hψi ; measure ψi βi

where the operator Ui is defined by

√
−1×αi /2l
Ui |0i = |0i and Ui |1i = eπ× × |1i

and H is the Hadamard transform.

14
 Tafliovich

Again, we can prove that S ! P ≤ W ! 1, where S refers to the parallel execution

of the above program after the initialisation of the shared entangled state. As
before, we sum out the final quantum state, since it does not appear in the winning
condition:
X
ψ′ · S
X √
== ψ ′ · ψ := (|0i⊗n + |1i⊗n )/ 2 ;
||i ψi := Ui ψi ; ψi := Hψi ; measure ψi βi substitute
X
′ ⊗n ⊗n
√
== ψ · ψ := (|0i + |1i )/ 2 ;
||i measure H(Ui ψi ) βi compose
X
′ ⊗n ⊗n
√
== ψ · ψ := (|0i + |1i )/ 2 ; substitute
⊗n
measure H (U0 ⊗ . . . ⊗ Un ψ) β0,..n and measure
√ 2
== H ⊗n (U0 ⊗ . . . ⊗ Un (|0i⊗n + |1i⊗n )/ 2) β0,..n
′
×
(α′0,..n = α0,..n ) apply U
√ P
i·αi /2l
√ ′ 2
== H ⊗n (|0i⊗n + eπ× −1×
× |1i⊗n )/ 2 β0,..n ×
(α′0,..n = α0,..n )

Beginning with some preliminary calculations:

S × P′ expand
√ P
i·αi /2l
√ ′ 2
== H ⊗n (|0i⊗n + eπ× −1×
× |1i⊗n )/ 2 β0,..n ×
X
(α′0,..n = α0,..n ) × (( i : 0, ..n · α′i ) mod 2l = 0) split cases
X
== (( i : 0, ..n · α′i /2l ) mod 2 = 0) × (α′0,..n = α0,..n )×
√ ′ 2
H ⊗n (|0i⊗n + |1i⊗n )/ 2 β0,..n +
X
(( i : 0, ..n · α′i /2l ) mod 2 = 1) × (α′0,..n = α0,..n )×
√ ′ 2
H ⊗n (|0i⊗n − |1i⊗n )/ 2 β0,..n apply H
X
== (( i : 0, ..n · α′i /2l ) mod 2 = 0) × (α′0,..n = α0,..n )×
X √  2
′
x · (px = 0) × |xi/ 2n−1 β0,..n +
X
(( i : 0, ..n · α′i /2l ) mod 2 = 1) × (α′0,..n = α0,..n )×
X √  2
′
x · (px = 1) × |xi/ 2n−1 β0,..n application
X X 
== ( i : 0, ..n · βi′ ) mod 2 = ( i : 0, ..n · αi /2l ) mod 2 × P ×
(α′0,..n = α0,..n )/2n−1

where px is defined by
X
if x = x0 x1 . . . xn−1 then px = ( i : 0, ..n · xi ) mod 2

15
 Tafliovich

Finally, the strategy S is winning, since:

S !P def !
′
== S × P /(S ; P ) above proof
X X 
== ( i : 0, ..n · βi′ ) mod 2 = ( i : 0, ..n · αi /2l ) mod 2 × P ×
(α′0,..n = α0,..n )/2n−1 /
X X 
σ ′′ · ( i : 0, ..n · α′′i /2l ) mod 2 = 0 × (α′′0,..n = α0,..n )×
X √  2
′′
x · (px = 0) × |xi/ 2n−1 β0,..n +
X 
( i : 0, ..n · α′′i /2l ) mod 2 = 1 × (α′′0,..n = α0,..n )×
X √  2 sum
′′
x · (px = 1) × |xi/ 2n−1 β0,..n
X X 
== ( i : 0, ..n · βi′ ) mod 2 = ( i : 0, ..n · αi /2l ) mod 2 ×
(α′0,..n = α0,..n )/2n−1 × P def of W
== (W ! 1) × (α′0,..n = α0,..n )
≤ W !1

Note that if n = 3 and l = 1, the parity game is a Mermin game.

5 Conclusion and Future Work

We have presented a formal framework for specifying, implementing, and analysing
quantum pseudo-telepathy games.
Current research focuses on formalising quantum cryptographic protocols, such
as BB84 [9], in our framework. While the communication involved in these protocols
is amenable to analysis using tools developed in [34], the analysis of security aspects
requires additional machinery. Integration of the techniques developed in this work
is one of the more promising directions.

References
[1] Abramsky, S., High-level methods for quantum computation and information, in: Proceedings of the
19th Annual IEEE Symposium on Logic in Computer Science (2004), pp. 410–414.

[2] Abramsky, S. and B. Coecke, A categorical semantics of quantum protocols, in: Proceedings of the 19th
Annual IEEE Symposium on Logic in Computer Science (2004), pp. 415–425.

[3] Abramsky, S. and R. Duncan, A categorical quantum logic, Mathematical Structures in Computer
Science 16 (2006), pp. 469–489.

[4] Adão, P. and P. Mateus, A process algebra for reasoning about quantum security, in: Proceedings of
the 3rd International Workshop on Quantum Programming Languages (QPL 2005), Electronic Notes
in Theoretical Computer Science 170 (2007), pp. 3–21.

[5] Altenkirch, T. and J. Grattage, A functional quantum programming language, in: Proceedings of the
20th Annual IEEE Symposium on Logic in Computer Science (2005), pp. 249–258.

[6] Arrighi, P. and G. Dowek, Operational semantics for formal tensorial calculus, in: Proceedings of
the 2nd International Workshop on Quantum Programming Languages, number 33 in TUCS General
Publications (2004), pp. 21–38.

16
 Tafliovich

[7] Arrighi, P. and G. Dowek, Linear-algebraic λ-calculus, arXiv:quant-ph/0501150 (2005).

[8] Bell, J. S., On the Einstein-Podolsky-Rosen paradox, Physics 1 (1964), pp. 195–200.

[9] Bennett, C. H. and G. Brassard, Quantum cryptography: Public-key distribution and coin tossing, in:
Proceedings of IEEE International Conference on Computers, Systems and Signal Processing (1984),
pp. 175–179.
[10] Brassard, G., A. Broadbent and A. Tapp, Multi-party pseudo-telepathy, in: Proceedings of the 8th
International Workshop on Algorithms and Data Structures, Lecture Notes in Computer Science 2748
(2003), pp. 1–11.

[11] Brassard, G., A. Broadbent and A. Tapp, Quantum pseudo-telepathy, Foundations of Physics 35 (2005),
pp. 1877–1907.
[12] Brassard, G., H. Buhrman, N. Linden, A. A. Méthot, A. Tapp and F. Unger, Limit on nonlocality
in any world in which communication complexity is not trivial, Physical Review Letters 96 (2006),
p. 250401.
[13] Brassard, G., R. Cleve and A. Tapp, Cost of exactly simulating quantum entanglement with classical
communication, Physical Review Letters 83 (1999), pp. 1874–1878.

[14] Brassard, G., A. A. Méthot and A. Tapp, Minimum entangled state dimension required for pseudo-
telepathy, arXiv:quant-ph/0412136 (2004).

[15] Buhrman, H., P. Hoyer, S. Massar and H. Roehrig, Combinatorics and quantum nonlocality, Physical
Review Letters 91 (2003), p. 047903.

[16] Coecke, B., The logic of entanglement, arXiv:quant-ph/0402014 (2004).

[17] Danos, V. and E. Kashefi, Pauli measurements are universal, in: Proceedings of the 3rd International
Workshop on Quantum Programming Languages (QPL 2005), Electronic Notes in Theoretical
Computer Science 170 (2007), pp. 95–100.

[18] Deutsch, D. and R. Jozsa, Rapid solution of problems by quantum computation, Proceedings of the
Royal Society of London 439 (1992), pp. 553–558.

[19] D’Hondt, E. and P. Panangaden, Reasoning about quantum knowledge, in: Proceedings of the 25th
IARCS Annual International Conference on Foundations of Software Technology and Theoretical
Computer Science, Lecture Notes in Computer Science 3821 (2005), pp. 553–564.

[20] D’Hondt, E. and P. Panangaden, Quantum weakest preconditions, Mathematical Structures in

Computer Science 16 (2006), pp. 429–451.

[21] Galliard, V., S. Wolf and A. Tapp, The impossibility of pseudo-telepathy without quantum entanglement,
arXiv:quant-ph/0211011 (2002).

[22] Gay, S. J. and R. Nagarajan, Communicating quantum processes, in: Proceedings of the 32nd ACM
SIGACT-SIGPLAN Symposium on Principles of Programming Languages (2005), pp. 145–157.

[23] Hehner, E. C., “a Practical Theory of Programming,” Springer, New York, 1993, first edition, current
edn. (2009) Available free at [Link]/∼ hehner/aPToP.

[24] Hehner, E. C., Probabilistic predicative programming, in: Proceedings of the 7th International
Conference on Mathematics of Program Construction, Lecture Notes in Computer Science 3125 (2004),
pp. 169–185.
[25] Hehner, E. C., A probability perspective, Formal Aspects of Computing (2009), to appear.

[26] Jorrand, P. and M. Lalire, Toward a quantum process algebra, in: Proceedings of the 1st ACM
Conference on Computing Frontiers (2004), pp. 111–119.

[27] Lalire, M. and P. Jorrand, A process algebraic approach to concurrent and distributed computation:
operational semantics, in: Proceedings of the 2nd International Workshop on Quantum Programming
Languages, number 33 in TUCS General Publications (2004), pp. 109–126.

[28] Mermin, N. D., Quantum mysteries revisited, Americal Journal of Physics 58 (1990), pp. 731–734.

[29] Nielsen, M. A. and I. L. Chuang, “Quantum Computation and Quantum Information,” Cambridge
University Press, 2000.
[30] Sanders, J. W. and P. Zuliani, Quantum programming, in: Mathematics of Program Construction,
Lecture Notes in Computer Science 1837 (2000), pp. 80–99.

[31] Selinger, P., Towards a quantum programming language, Mathematical Structures in Computer Science
14 (2004), pp. 527–586.

17
 Tafliovich

[32] Tafliovich, A., “Quantum Programming,” Master’s thesis, University of Toronto (2004).

[33] Tafliovich, A. and E. C. Hehner, Quantum predicative programming, in: Proceedings of the 8th
International Conference on Mathematics of Program Construction, Lecture Notes in Computer Science
4014 (2006), pp. 433–454.

[34] Tafliovich, A. and E. C. Hehner, Programming with quantum communication, in: Seventh Workshop on
Quantitative Aspects of Programming Languages, Electronic Notes in Theoretical Computer Science
(2009).

[35] Valiron, B., Quantum typing, in: Proceedings of the 2nd International Workshop on Quantum
Programming Languages, number 33 in TUCS General Publications (2004), pp. 163–178.

[36] van Tonder, A., A lambda calculus for quantum computation, SIAM Journal on Computing 33 (2004),
pp. 1109–1135.

[37] Yimsiriwattana, A. and S. J. L. Jr, Distributed quantum computing: A distributed Shor algorithm,
arXiv:quant-ph/0403146 (2004).

[38] Zuliani, P., Non-deterministic quantum programming, in: Proceedings of the 2nd International
Workshop on Quantum Programming Languages, number 33 in TUCS General Publications (2004),
pp. 179–195.

[39] Zuliani, P., Compiling quantum programs, Acta Informatica 41 (2005), pp. 435–474.

A Quantum Computation
In this section we introduce the basic concepts of quantum mechanics, as they
pertain to the quantum systems that we will consider for quantum computation.
The discussion of the underlying physical processes, spin- 21 -particles, etc. is not
our interest. We are concerned with the model for quantum computation only. A
reader not familiar with quantum computing can consult [29] for a comprehensive
introduction to the field.
The Dirac notation, invented by Paul Dirac, is often used in quantum mechanics.
In this notation a vector v (a column vector by convention) is written inside a ket:
|vi. The dual vector of |vi is hv|, written inside a bra. The inner products are
bra-kets hv|wi. For n-dimensional vectors |ui and |vi and m-dimensional vector
|wi, the value of the inner product hu|vi is a scalar and the outer product operator
|vihw| corresponds to an m by n matrix. The Dirac notation clearly distinguishes
vectors from operators and scalars, and makes it possible to write operators directly
as combinations of bras and kets.
In quantum mechanics, the vector spaces of interest are the Hilbert spaces of
dimension 2n for some n ∈ N. A convenient orthonormal basis is what is called a
computational basis, in which we label 2n basis vectors using binary strings of length
n as follows: if s is an n-bit string which corresponds to the number xs , then |si is
a 2n -bit (column) vector with 1 in position xs and 0 everywhere else. The tensor
product |ii ⊗ |ji can be written simply as |iji. An arbitrary vector in a Hilbert
space can be written as a weighted sum of the computational basis vectors.
Postulate 1 (state space) Associated to any isolated physical system is a Hilbert
space, known as the state space of the system. The system is completely described
by its state vector, which is a unit vector in the system’s state space.
Postulate 2 (evolution) The evolution of a closed quantum system is described
by a unitary transformation.

18
 Tafliovich

Postulate 3 (measurement) Quantum measurements are described by a collec-

tion {Mm } of measurement operators, which act on the state space of the system
being measured. The index m refers to the possible measurement outcomes. If
the state of the system immediately prior to the measurement is described by a
†
vector |ψi, then the probability of obtaining result m is hψ|Mm Mm |ψi, in which
case the state of the system immediately after the measurement is described by
the vector √ Mm†|ψi . The measurement operators satisfy the completeness
hψ|Mm Mm |ψi
P †
equation m · Mm Mm == I.
An important special class of measurements is projective measurements, which
are equivalent to general measurements provided that we also have the ability to
perform unitary transformations.
A projective measurement is described by an observable M , which is a Hermitian
operator on the state space of the system being measured. This observable has
P
a spectral decomposition M = m · λm × Pm , where Pm is the projector onto
the eigenspace of M with eigenvalue λm , which corresponds to the outcome of
the measurement. The probability of measuring m is hψ|Pm |ψi, in which case
immediately after the measurement the system is found in the state √ Pm |ψi .
hψ|Pm |ψi
Given an orthonormal basis |vm i, 0 ≤ m < 2n , measurement with respect to
this basis is the corresponding projective measurement given by the observable
P
M = m · λm × Pm , where the projectors are Pm = |vm ihvm |.
Measurement with respect to the computational basis is the simplest and the
most commonly used class of measurements. In terms of the basis |mi, 0 ≤ m < 2n ,
the projectors are Pm = |mihm| and hψ|Pm |ψi = |ψm |2 . The state of the system
immediately after measuring m is |mi.
For example, measuring a single qubit in the state α × |0i + β × |1i results in
the outcome 0 with probability |α|2 and outcome 1 with probability |β|2 . The state
of the system immediately after the measurement is |0i or |1i, respectively.
Suppose the result of the measurement is ignored and we continue the com-
putation. In this case the system is said to be in a mixed state. A mixed state
is not the actual physical state of the system. Rather it describes our knowl-
edge of the state the system is in. In the above example, the mixed state is
expressed by the equation |ψi = |α|2 × {|0i} + |β|2 × {|1i}. The equation is
meant to say that |ψi is |0i with probability |α|2 and it is |1i with probability
|β|2 . An application of operation U to the mixed state results in another mixed
state, U (|α|2 × {|0i} + |β|2 × {|1i}) = |α|2 × {U |0i} + |β|2 × {U |1i}.
Postulate 4 (composite systems) The state space of a composite physical sys-
tem is the tensor product of the state spaces of the component systems. If we
have systems numbered 0 up to and excluding n, and each system i, 0 ≤ i < n,
is prepared in the state |ψi i, then the joint state of the composite system is
|ψ0 i ⊗ |ψ1 i ⊗ . . . ⊗ |ψn−1 i.
While we can always describe a composite system given descriptions of the com-
ponent systems, the reverse is not true. Indeed, given a state vector that describes
a composite system, it may not be possible to factor it to obtain the state
√ vectors
√of
the component systems. A well-known example is the state |ψi = |00i/ 2+|11i/ 2.

19
 Tafliovich

Such a state is called an entangled state.

20