Introduction to Coalgebra Outline What are coalgebras, intuitively (Co ...

Basics Induction and coinduction Bisimilarity and finality Coalgebras and quantum computing


Radboud University Nijmegen


Outline Basics

Introduction to Coalgebra

Induction and coinduction Algebras and coalgebras

Bart Jacobs

Bisimilarity and finality Language example

Institute for Computing and Information Sciences – Digital Security Radboud University Nijmegen

Coalgebras and quantum computing Introducing QBits Combining qubits Monads for computations Walks illustrating computation types Quantum walks, coalgebraically Reversibility of computation

EWSCS 2011: 16th Estonian Winter School in Computer Science 28 feb. – 4 march, Estonia

4th March 2011

Bart Jacobs

4th March 2011 Basics Induction and coinduction Bisimilarity and finality Coalgebras and quantum computing

Coalgebra Intro

1 / 98


What are coalgebras, intuitively

X

X

X

construct

/X

modify/observe

/

X

···

X

• . . . but at this stage you may think of them as types σ(X )

equations)

containing a single type variable X


Coalgebra Intro

4 / 98

1+N

• infinite version usually written as

Q

Xi

• coproducts X + Y = {hx, 0i | x ∈ X } ∪ {hy , 1i | y ∈ Y }, with

coprojections

[f ,g ]

/ X + Y o κ2

• infinite version written as 4th March 2011

X + Y −−−→ Z =============== X − →Z Y − →Z

Y `

i∈I


i.e.

zero : 1 −→ N succ : N −→ N

[0,+,−]

Note: this captures algebraic operations, not equations

Xi Coalgebra Intro

/N

g

f

[zero,succ]

  0 : 1 −→ G /G + : G × G −→ G 1 + (G × G ) + G i.e.  − : G −→ G • Clearly this works for many algebraic structures: for each signature Σ there is a functor: ` X 7−→ f ∈Σ X arity(f ) (disjoint union over all operations) whose algebras are precisely the Σ-algebras. • Groups

g

f

i∈I

5 / 98

The functor/type here is F (X ) = 1 + X .

hf ,g i

Z −−−→ X × Y =============== Z− →X Z− →Y

/Y

Coalgebra Intro

• Natural numbers

• products X × Y = {hx, y i | x ∈ X , y ∈ Y }, with projections:

X ×Y


Algebra examples F (X ) → X

• Identity X , and constants A • including empty set ∅, often written as 0 • singleton set 1 = {∗} π2

Bart Jacobs


Intermezzo: type constructors for “boxes”

Bart Jacobs

···

• Formally, the boxes are functors, usually Sets → Sets, . . .

• related to dynamical systems (and evolution via differential

X


Think of a fields & methods in an object-oriented class

requires a new kind of mathematics.

κ1

2 / 98

Coalgebras with “state space” X are maps out of X , of the form:

side-effect”)

X o

Coalgebra Intro

Algebras with “carrier” X are maps into X , of the form:

• Describing such state-based systems and their dynamics

π1


(Co)algebras, pictorially

• Mathematical models for state-based computation • your computer has a complicated internal state • you as user can only modify it to some extend • also, you can observe only so much • Basically only two kinds of operations: • move to a next state, somehow (deterministically, non-deterministically, probabilistically, . . . ) • make an observation (“measurement”) about the current state • These operations can be combined (“observation has

Bart Jacobs

Bart Jacobs

6 / 98

Bart Jacobs

4th March 2011

Coalgebra Intro

7 / 98




Coalgebra examples X → F (X )

Automata-theoretic coalgebra examples

• Streams (infinite lists) AN of elements of a set A: hhead,taili

AN

• A deterministic automaton with input actions A is a

coalgebra:

/ A × AN

• Both finite and infinite lists A∞ = A? + AN possible head

/ 1 + A × A∞

for the functor F (X ) = 1 + A × X . Note: observation with side-effect Bart Jacobs


• A non-deterministic automaton, or transition system, with

input actions A is a coalgebra:

succs

X

Coalgebra Intro

/ XA × 2

where 2 = {0, 1}.

/ P(X )A

• Other functors (actually “monads”) than powerset P may be

used: eg. partial automata via lift, or probabilistic automata via distribution.

8 / 98

Bart Jacobs


Markov chains


Coalgebra Intro


• Generic framework for describing state-based systems • Bisimilarity, as indistinguishability of states

• Modal logic, also generically

• Coherence between operational & denotational semantics

• General trace semantics • Current own interest: coagebra & quantum computing Lect. • Quantum language has strong coalgebraic flavour: states, transitions, observations, indistinguishability, . . . • Can this be made mathematically precise?

Coalgebras X → D(X ) are Markov chains, giving probabilistic transitions: P ri x −→ xi with i ri = 1. They can also be used in labeled form, as X −→ D(X )A

or as


X

Lect. II, III Lect. III, IV

• Coinductive definition and reasoning principles

Such ϕ ∈ D(X ) is a formal convex combination:   support(ϕ) = {x1 , . . . , xn } r = ϕ(xi ) > 0 r1 x1 + · · · + rn xn where  i r1 + · · · + rn = 1

V

X −→ D(A × X ) Coalgebra Intro

10 / 98

Bart Jacobs


Functors, part I


Coalgebra Intro

11 / 98


Functor example I

• Before we can proceed we need to know a little bit more

• For a set X write P(X ) for the powerset: the set of all

• In functional programming “functoriality” is often described

• This P(−) forms a functor • For a function g : X → Y there is a suitable function

about functors, for the time being only on sets

subsets of X

by “map” properties, such as list map

• A functor F maps sets X to sets F (X ), and also functions to

P(X ) → P(Y )

functions, in an orderly manner:

• this is new function is written P(g ) : P(X ) → P(Y ) • it is given by image:

• if g : X → Y , then F (g ) : F (X ) → F (Y) id id • F preserves identity maps: F X −→ X = F (X ) −→ F (X )

P(g ) U ⊆ X = {g (x) | x ∈ U} ⊆ Y

• F preserves composition: F (h ◦ g ) = F (h) ◦ F (g ), in:

= = = =

F (g ) F (h) g h F X −→ Y −→ Z = F (X ) −→ F (Y ) −→ F (Z )

• Often, when the action on functions is “obvious”, it is

omitted from the description of a functor

Bart Jacobs

9 / 98

Coalgebra essentials & Plan

For a set X , define the set of discrete distributions on X P D(X ) = {ϕ : X → [0, 1] support(ϕ) is finite, and x ϕ(x) = 1}

Bart Jacobs

hstep,final?i

X

for the functor F (X ) = A × X , where: head(α) = α(0) tail(α) = α0 = λn ∈ N. α(n + 1)

A∞


4th March 2011

Coalgebra Intro

13 / 98

Bart Jacobs

4th March 2011

{y ∈ Y | ∃x ∈ U. y = g (x)} g (U) as it is sometimes written g [U] also possible ` g (U) for categorical logicians Coalgebra Intro

14 / 98




Functor example I

Functor example II

We check explicitly:

• For a set X write X ? for the associated set of finite lists:

P(id)(U) = {id(x) | x ∈ U} =U

X ? = {hx1 , x2 , . . . , xn i | xi ∈ X }

• The mapping X 7−→ X ? is a functor

Hence P(id) = id. Similarly, P preserves composition: P(h) ◦ P(g ) (U) = P(h) P(g )(U) = P(h) {y ∈ Y | ∃x ∈ U. y = g (x)}

• For g : X → Y we have g ? : X ? → Y ? given by:

g ? hx1 , x2 , . . . , xn i = hg (x1 ), g (x2 ), . . . , g (xn )i

• It is not hard to check the functoriality properties:

= {z ∈ Z | ∃y ∈ Y . ∃x ∈ U. y = g (x) and z = h(y )} = {z ∈ Z | ∃x ∈ U. z = h(g (x))} = P(h ◦ g )(U)

Bart Jacobs


Coalgebra Intro

id? = id

15 / 98

g


Definition a

(g +A) : X +A −→ Y +A given by


a map f : X → Y for which the rectangle on the left commutes. F (X ) X

(g + A)(κ1 x) = κ1 g (x) (g + A)(κ2 a) = κ2 a

17 / 98

Bart Jacobs

[0,+]

[hi,;]

1 + A? × A? ) • There is an algebra homomorphism:

/N

n times

/Y d

Coalgebra Intro

18 / 98


Definition there is a unique algebra map:

F (!b ) F (A) _ _ _ _ _ _/ F (X ) α

b

!b A _ _ _ _ _ _ _ _/ X

/ 1 + A? × A? [hi,;]

/ A?

b

α

• An algebra F (A) → A is initial if for each algebra F (X ) → X

/ A?

where f (n) = ha, a, . . . , ai, for some a ∈ A. | {z } 4th March 2011

d

g

X


concatenation ; in:

f

/ F (Y ) O

a map g : X → Y for which the diagram on the right commutes.

• Also lists A? for an algebra via empty list hi and list

c

b

Initiality and finality

• Consider the signature functor F (X ) = 1 + (X × X ) for monoids • The natural numbers N form an algebra, via:

id+(f ×f )

/Y

f

F (g )

F (X ) O c

Algebra homomorphism example

1 + N × N)

/ F (Y )

• A coalgebra homomorphism from X → F (X ) to Y → F (Y ) is


1 + N × N)

F (f )

a

Coalgebra Intro

b

• An algebra homomorphism from F (X ) → X to F (Y ) → Y is

• Coproduct with a constant X 7→ X + A, with

Bart Jacobs


• A coalgebra for F is a map X → F (X )

g × A : X × A −→ Y × A given by (g × A)(x, a) = (g (x), a)

N

16 / 98

• An algebra for F is a map F (X ) → X

hx0 , x1 , x2 , . . . , i = hg (x0 ), g (x1 ), g (x2 ), . . .i

[0,+]

Coalgebra Intro

Let F be a functor

• Product with a constant X 7→ X × A, with:

Bart Jacobs

(h ◦ g )? = h? ◦ g ?

and

Definition

• Infinite lists: X 7→ X N with: g N : X N → Y N , given by:

Bart Jacobs


Functor examples II

N


ζ

• A coalgebra Z → F (Z ) is final if for each coalgebra c

For A = 1 = {∗} ∼ = we get N − → 1?

Coalgebra Intro

19 / 98

X → F (X ) there is a unique coalgebra map: F (!c ) F (X ) _ _ _ _ _ _/ F (Z ) c

O

X ___ Bart Jacobs

4th March 2011

O

_!c_

ζ

_ _ _/ Z Coalgebra Intro

20 / 98




Fixed point results

Induction example, I Lemma

Fact

Fix a set A and consider the functor F (X ) = 1 + (A × X ).

∼ =

The initial algebra of F is given by finite lists A? with algebra structure given by empty list (nil) hi and prefix · in:

• An initial algebra is an isomorphism F (A) − →A ∼ =

• a final coalgebra is an isomorphism Z − → F (Z )

1 + A × A?

Consequence: By Cantor’s theorem, the powerset functor P has neither an initial algebra nor a final coalgebra.

[hi,·]

• existence is used for definition by (co)induction

[ hi,· ] ∼ =

/ A?

f

[p,q]

A? _ _ _ _ _ _ _ _ _ _ _/ X is given by: f (hi) = p and f (a · σ) = q(a, f (σ)). It is a homomorphism by construction.

• uniqueness is used for reasoning by (co)induction 4th March 2011 Basics Induction and coinduction Bisimilarity and finality Coalgebras and quantum computing

Proof: The dashed map f in: id+(id×f ) 1 + A × A? _ _ _ _ _ _/ 1 + A × X

Unique existence

Bart Jacobs


Coalgebra Intro

21 / 98

Bart Jacobs


Induction example, II


Coalgebra Intro

22 / 98


Induction example, III

We wish to define the length function len : → N formally, by initiality. This requires an algebra map ?? on N in: id+(id×len) 1 + A × A? _ _ _ _ _ _/ 1 + A × N A?

[hi,·]

• Consider the functor F (X ) = 1 + (X × A × X ), for a fixed set

A

• its operations give binary, A-labeled trees • what if we had taken F (X ) = A + (X × A × X ) • or: F (X ) = B + (X × A × X ) • or: F (X ) = B + (X × X × X )

??

len A? _ _ _ _ _ _ _ _ _ _ _/ N

This ?? must be of the form [p, q], with p : 1 → N and q : A × N → N satisfy:

• We write its initial algebra as:

Hence it is clear how to choose p, q, namely as:

• We do not really need to know what is inside the set

len(hi) = p

p=0 Bart Jacobs

and

1 + BinTree(A) × A × BinTree(A)

len(a · σ) = q(a, n)

and

q(a, n) = n + 1


• a form of mathematical behaviourism 23 / 98

1 + BinTree(A) × A × BinTree(A) _ _ _ _ _ _/ 1 + A? × A × A?

[hi,??]

BinTree(A) _ _ _ _ _ _ _ _ _ _ _ _ _ _ _/ A? A?

4th March 2011

Coalgebra Intro

24 / 98


Coalgebra Intro

• Definitions by induction illustrated via initiality

• Initiality formulation is “generic”: it works for every functor /

signature

• This genericity is convenient when formalising induction in

(functional) programming languages and theorem provers

A?

• Examples of reasoning by induction (via uniqueness) are

This map ?? : ×A× −→ is: for inorder traversal (σ, a, τ ) 7−→ σ; a · τ for preorder traversal (σ, a, τ ) 7−→ a · σ; τ

Bart Jacobs


Summary, so far

We sketch how to do tree traversal BinTree(A) → A? , in two ways (“inorder” and “preorder”)

A?

Bart Jacobs


Induction example, III (cntd)

∼ =

/ BinTree(A)

BinTree(A); its universal properties suffice to be able to use it

ie. as: q = λ(a, n). n + 1 Coalgebra Intro

[nil,node] ∼ =

missing so far, but will be given next, for coinduction

25 / 98

Bart Jacobs

4th March 2011

Coalgebra Intro

26 / 98




Coinduction example I

Coinduction example II • We wish to define even : AN → AN • This involves a coalgebra ?? in:

Lemma The final coalgebra of the functor F (X ) = A × X is the set AN of infinite sequences ha0 , a1 , . . .i of elements ai ∈ A, with coalgebra structure: h hd,tli hd(σ) = σ(0) / A × AN AN ∼ = tl(σ) = hσ(1), σ(2), . . .i

id×even A ×O AN _ _ _ _ _ _/ A ×O AN

AN

Definition by coinduction: from single-step to “and-so-forth”

is given by f (x) = hp(x), p(q(x)), p(q 2 (x)), p(q 3 (x)), . . .i. Coalgebra Intro

27 / 98

Bart Jacobs


Coinduction example III


28 / 98


• The next aim is merge : AN × AN → AN

• We thus have to provide a coalgebra c in a diagram:

• Which coalgebra do we need now on the left?

A ×O AN _

_id×odd _ _ _

id×merge A × (AN × AN ) _ _ _ _ _ _/ A ×O AN O

_/ A × AN O

∼ = hhd,tli

c

_ _ _ _odd_ _ _ _/ AN

AN

tl(f (σ)) = tl(even(tl(σ))) = even(tl(tl(tl(σ)))) = f (tl(tl(σ)))


Coalgebra Intro

∼ = hhd,tli

_ _ _ merge _ _ _ _ _/ AN

c(σ, τ ) = hhd(σ), (τ, tl(σ))i

coalgebra homomorphism in the above diagram! hd(f (σ)) = hd(even(tl(σ))) = hd(tl(σ))

×

AN

• This coalgebra c : AN × AN −→ A × AN × AN is:

• How to prove odd(σ) = even(tl(σ)) ? • Use uniqueness, and show that f (σ) = even(tl(σ)) is also a

Bart Jacobs

Coalgebra Intro

Coinduction example IV

• We also wish odd : AN → AN

AN

?? = hhd, tl ◦ tli

hhd,tli

hhd◦tl,tl◦tli

p(σ) = hd(even(σ)) = σ(0) = hd(σ) even q(σ) = tl(even(σ)) = hσ(2), σ(4), . . .i

• Thus we use:

f X _ _ _ _ _ _ _ _/ AN


_ _ _ even _ _ _ _ _/ AN

• If we write ?? = hp, qi, then commutation says:

id×f A ×O X _ _ _ _ _ _/ A ×O AN

hp,qi

∼ = hhd,tli

??

Proof: The required unique dashed map f in:

Bart Jacobs


• Then, for instance: • hd(merge(σ, τ )) = hd(σ) • hd(tl(merge(σ, τ ))) = hd(merge(π2 c(σ, τ ))) = hd(merge(τ, tl(σ))) = hd(τ ) • hd(tl2 (merge(σ, τ ))) = · · · = hd(tl(σ)) etc. 29 / 98

Bart Jacobs


Coinduction example V


Coalgebra Intro

30 / 98


Coinduction example VI Thus we calculate:

• Now we wish to prove merge(even(σ), odd(σ)) = σ

hd(f (σ)) = hd(merge(even(σ), odd(σ)))

• Obviously, the identity id : AN → AN is the unique coalgebra

= hd(even(σ))

homomorphism g in:

A ×O

hhd,tli

AN

AN

= hd(σ)

_ _ id×g _ _ _ _/ A × AN O

tl(f (σ)) = tl(merge(even(σ), odd(σ)))

∼ = hhd,tli

_ _ _ _g _ _ _ _/ AN

= merge(odd(σ), tl(even(σ)))

• Hence it suffices to prove that the map

= merge(even(tl(σ)), even(tl(tl(σ))))

f (σ) = merge(even(σ), odd(σ))

= merge(even(tl(σ)), odd(tl(σ))) = f (tl(σ))

is also such a coalgebra homomorphism.

Conclusion: id = f = λσ. merge(even(σ), odd(σ)) Bart Jacobs

4th March 2011

Coalgebra Intro

31 / 98

Bart Jacobs

4th March 2011

Coalgebra Intro

32 / 98




Summary on induction and coinduction


Bisimilarity

• Formalisation of the intuitive idea: indistinguishability of

• Induction and coinduction, formulated via initiality and finality

states, via the available operations

are each other’s duals • Initiality & finality mechanism is:

• Several definitions possible, but they all coincide for

“reasonable” functors

• generic / uniform • powerful • abstract (can be formulated in other categories than sets)

• Important relation with final coalgebras, and coinductive proof

• Initiality & finality can also be used in binary form; this is the

• Also relevant for Hennessey-Milner result in coalgebraic modal

techniques

logic: states are bisimilar if and only if they satisfy the same formulas.

next topic

Bart Jacobs


Coalgebra Intro

33 / 98


Bisimilarity (as behavioural equivalence)

c

ζ

c


Coalgebra Intro

x ↔ y ⇐⇒ !c (x) = !d (y ) in Z ⇐⇒ x, y are mapped to the same element of the final coalgebra e

Proof: (⇐) obvious; (⇒) Assume f (x) = g (y ) in W → F (W ) in: By finality: g f / X W o Y !e ◦ f = !c !e ◦ g = !d Hence: !e !c 36 / 98

!d

!c (x) = !e (f (x)) = !e (g (y )) = !d (y )


Coalgebra Intro

37 / 98


• but under suitable size conditions they do exist (boundedness,

States x ∈ X and y ∈ Y are bisimilar iff the are contained in a bisimulation R ⊆ X × Y

accessibility)

• Given such restrictions, there are several constructions: • as limits of chains • via modal formulas • as quotients of known final coalgebras

• such a relation R is closed under the coalgebras

• formally, hr1 , r2 i : R ,→ X × Y carries a coalgebra itself in:

F (R)

F (r2 )

O

4th March 2011

Z

• Not all functors have final coalgebras (recall powerset P)

Assume the functor F is “reasonable” (preserves weak pullbacks)

r1

* t

Final coalgebras

Lemma (Bisimilarity as greatest bisimulation)

F (r1 )

Bart Jacobs


Bisimilarity alternative II

O

d

Assume X → F (X ), Y → F (Y ), and x ∈ X and y ∈ Y as before.

The definition is often used where coalgebras c and d are the same. This gives bisimilarity for two states of the same coalgebra.

Bart Jacobs


=

satisfying f (x) = g (y ) in W .

X o

35 / 98

Assume F as a final coalgebra Z − → F (Z ). ∼

d

Two states x ∈ X and y ∈ Y will be called bisimilar, written as e x ↔ y , if there is a third coalgebra W → F (W ) with two homomorphisms: g c e d f / X → F (X ) W → F (W ) o Y → F (Y )

c

Coalgebra Intro

Lemma

Assume two coalgebras X → F (X ) and Y → F (Y ) of the same functor F .

F (X ) o


Bisimilarity alternative I

Definition (cospan style)

Bart Jacobs

Bart Jacobs

R

r2

/ F (Y ) O

• Here we do not care very much about how they are built, but

focus on its finality and how to use it

d

/Y

Coalgebra Intro

38 / 98

Bart Jacobs

4th March 2011

Coalgebra Intro

39 / 98




Final automaton example I


Final automaton example II

• Fix two sets: A for inputs, B for outputs

• We consider coalgebras, or deterministic automata: hδ,i

X

Theorem (Arbib & Manes, Reichel) The final coalgebra of the automaton functor F (X ) = X A × B is ? the set of functions B A (from input sequences to observations) with: A ζ=hζ1 ,ζ2 i ? / B A? ×B BA ∼ =

/ XA × B

• For each state x ∈ X , it gives:

a successor state δ(x)(a) ∈ X , for each input a ∈ A an observation (x) ∈ B

?

where for a function/state ϕ ∈ B A ζ1 (ϕ)(a) = λσ ∈ A? . ϕ(a · σ) ζ2 (ϕ) = ϕ(hi)

• For a finite sequence σ = ha1 , . . . , an i ∈ A? we put:

δ ? (x)(σ) = δ · · · δ(x)(a1 ) · · · (an )

This gives multiple-step transitions. Bart Jacobs


Coalgebra Intro

40 / 98

Bart Jacobs


Final automaton example III


Coalgebra Intro

41 / 98


Final automaton example IV

hδ,i

For an arbitrary coalgebra X −−→ X A × B we have: A _ _beh_ _×id_ _/ B A? A × B XA × O B O

∼ = ζ=hζ1 ,ζ2 i

hδ,i

Automaton bisimulations

beh ? X _ _ _ _ _ _ _ _ _/ B A where: beh(x)(σ) = δ ∗ (x)(σ) . This make the diagram commute: ζ2 (beh(x)) = beh(x)(hi)

= δ ? (x)(hi)

hδ,i

For a (single) automaton X −−→ X A × B a bisimulation is a relation R ⊆ X × X which is closed under the operations: • R(x, x 0 ) =⇒ (x) = (x 0 )

ζ2 (beh(x))(a)(σ) = beh(x)(a · σ) ? = δ (x)(a · σ) = δ ? δ(x)(a) (σ) = beh δ(x)(a) (σ) = behA δ(x) (a)(σ).

Bart Jacobs


Coalgebra Intro

Thus, states within R cannot be distinguished.

42 / 98

X1

P(A? )

Write L(A) = over alphabet A

×B ∼ = X ×B

?

• final coalgebra is 2A = P(A? ) • this is the set of languages over alphabet A • behaviour map beh : X → P(A? ) maps a state to the accepted


(special case II)

for the final coalgebra of languages hδ,i ∼ =

/ L(A)A × 2

Two languages L, K ∈ L(A) are bisimilar if there is a bisimulation R ⊆ L(A) × L(A); this R satisfies hi ∈ L iff hi ∈ K R(L, K ) =⇒ R(La , Ka ), for each a ∈ A

language in that state

• bisimilar states thus accept the same language

Coalgebra Intro

43 / 98

δ(L)(a) = La , the Brzozowski derivative of L ? = {σ ∈ A | a · σ ∈ L} (L) = 1 ⇐⇒ hi ∈ L

Special case I: B = 2 = {0, 1}, so functor is F (X ) = X A × 2

4th March 2011

Coalgebra Intro

where, for L ∈ L(A),

∼ =

• structure map is tail and head B N − → BN × B

Bart Jacobs

=

? 2A

L(A)

• A? = 1? ∼ =N • final coalgebra consists of infinite sequences / streams

2


Final language coalgebra

Special case I: A = 1, so functor is F (X ) =

? BA ∼ = BN

Bart Jacobs


Final automaton example V 1

• R(x, x 0 ) =⇒ R δ(x)(a), δ(x 0 )(a) , for all inputs a ∈ A.

= (x)

44 / 98

Bart Jacobs

4th March 2011

Coalgebra Intro

45 / 98




Regular languages example I


Regular languages form a coalgebra Regular languages are closed under the Brzozowski derivative, via:

Recall that the subset R(A) ⊆ L(A) of regular languages is the smallest one with: • 0 = ∅ ∈ R(A)

• 1 = {hi} ∈ R(A)

• L + K = L ∪ K ∈ R(A), for L, K ∈ R(A)

• LK = {σ; τ | σ ∈ L, τ ∈ K } ∈ R(A), for L, K ∈ R(A)

S

n n∈N L

∈ R(A), for L ∈ R(A)


Coalgebra Intro

46 / 98

• Thus, for regular languages L, K ∈ R(A),

iff L = K • a new proof method for equality of regular languages • the traditional one is cumbersome: it involves either algebraic reasoning, or turning expressions into machines, and then minimalising them ↔R

a∗ (1 + a)∗ 48 / 98

Bart Jacobs


Equality of regular languages, example II

(a∗ b)∗ a

b

a

= aa a∗ = 1a∗ = a∗

b

= 0 = a∗


X

b Coalgebra Intro

49 / 98


a∗ + a∗ b(a + ba∗ b)∗ ba∗ = {σ ∈ A? | σ contains an even number of b’s}

= (a + b)b (a + b)∗ = (ab + bb )(a + b)∗ = (0 + 1)(a + b)∗ = (a + b)∗ ∗

• Non-trivial example:

• R is also closed under derivatives. Eg. for (−)b :

∗


Equality of regular languages, example III

• Aim: (a + b)∗ = (a∗ b)∗ a∗ , over alphabet A = {a, b} • Take as relation R = {( (a + b)∗ , (a∗ b)∗ a∗ )} • Clearly, for (L, K ) ∈ R, hi ∈ L ⇔ true ⇔ hi ∈ K

b

47 / 98

• Assume (L, K ) ∈ R; • clearly, hi ∈ L iff hi ∈ K • R is also closed under derivatives Obviously, for L = 0 = K , so take L = (1 + a)∗ , K = a∗ , (1 + a)∗ a = (1 + a)a (1 + a)∗ = (1a + aa )(1 + a)∗ = (0 + 1)(1 + a)∗ = (1 + a)∗

∼ =

Coalgebra Intro

R = {((1 + a)∗ , a∗ )} ∪ {(0, 0)}

R(A) _ _ _ _ _ _ _ _/ L(A) = P(A? )

(a + b)∗


• Assume we wish to prove (1 + a)∗ = a∗ , over alphabet A = {a, b} • We need ((1 + a)∗ , a∗ ) ∈ R for a bisimulation R ⊆ R(A) × R(A) • Take the subset relation consisting of 2 pairs only:

what it means that languages L, K ∈ R(A) are bisimular

Coalgebra Intro

/ R(A)A × 2

Equality of regular languages, example I

• namely: they are equal, when mapped to the final coalgebra • But the finality map R(A) −→ L(A) is inclusion, in: R(A)A × 2 _ _ _ _ _ _/ L(A)A × 2 O O


Bart Jacobs


• Now that regular language R(A) carry a coalgebra, we know

Bart Jacobs

hδ,i

R(A)

Equality of regular languages via coinduction

L

hi ∈ K + L iff hi ∈ K or hi ∈ L hi ∈ KL iff hi ∈ K and hi ∈ L hi ∈ K ∗ .

This yields a coalgebra / automaton

Examples: a∗ , a∗ b ∗ , (ab)∗ , (1 + a)∗ etc.

Bart Jacobs

hi 6∈ b

(K + L)a = Ka + La Ka L + La if hi ∈ K (KL)a = Ka L otherwise K ∗ a = Ka K ∗

• {a} ∈ R(A), for each a ∈ A — often simply: a ∈ R(A)

• L∗ =

hi 6∈ 0 hi ∈ 1

0a = 0 1a = 0 1 if b = a ba = 0 otherwise

• The proof is non-trivial, but essentially straightforward via

bisimulations

∗

• This technique is now incorporated in a tool (CIRC, based on

= (a∗ b) b a∗ + a b = (a∗ b)b (a∗ b)∗ a∗ + ab a∗ = ((a∗ )b b + bb )(a∗ b)∗ a∗ + 0a∗ = (0 + 1)(a∗ b)∗ a∗ + 0 = (a∗ b)∗ a∗ .

Maude)

• Many more examples of such equality proof via bisimulations

in the work of Jan Rutten

• Similarly for the derivative (−)a . Hence R is a bisimulation,

and the goal is proven.

Bart Jacobs

4th March 2011

Coalgebra Intro

50 / 98

Bart Jacobs

4th March 2011

Coalgebra Intro

51 / 98




Prerequisites for quantum computation

What is needed?

• Do you need to be a quantum physicist to understand

quantum computation?

• NO!

Main prerequisites for quantum computation • Linear algebra (over complex numbers C)

• Hilbert spaces (esp. finite dimensional ones)

One can be a masterful practioner of computer science without having the foggiest notion of what a transistor is, not to mention how it works

• Tensors and spectral decomposition

Prerequisites for this talk

(David Mermin, Quantum Computer Science. An Introduction.)

• Basic linear algebra

• Here, as usual, we only deal with the abstract, mathematical

• Basic category theory

model for quantum computation, not with its possible future realisation — which is work for physicists.

Bart Jacobs


Coalgebra Intro

53 / 98


Coalgebra Intro

54 / 98


Quantum mechanics/computation is strange

• Letting nature do matrix multiplications for us

The four strangest phenomena

• Computations are divided over multiple parallel worlds

• Superposition: linear combinations of basic states

(“quantum parallellism”)

• Entanglement of states: explained via tensors ⊗

• A new physical basis for computation

• Computation is reversible: explained via unitary maps (via daggers (−)† ie. adjoints) • Measurement • side-effect: the state changes to the result of the measurement • entangled objects are both changed when only one is measured

• Much focus so far on algorithms and complexity

• More recently also on semantics and quantum languages (Abramsky, Coeke, Panangaden, Selinger, . . . ) • Actual, physical realisation of quantum computer still embryonic (in the order of 10 qubits)

Mathematical explanation via diagonalisation of operators

• Quantum key distribution more developed (but also under attack, see quantum hackers)


Bart Jacobs


What is quantum computing about?

Bart Jacobs


Coalgebra Intro

(using eigenvectors & eigenvalues)

55 / 98

Bart Jacobs


Quantum computation is powerful


Coalgebra Intro

56 / 98


Attractions

• New area inbetween computer science, physics and logic • John Baez: category theory forms Rosetta Stone

• More efficient in certain tasks, via a new form of parallellism • Notably factorisation of numbers (Shor); threatening for RSA;

• Great potential for both theory and applications • Chance to get theory in place before (programming) languages emerge • Early in CS: languages came before theory

• New levels of security, e.g. with key exchange via

entanglement

• Issues are both familiar and new • See later discussion of ‘walks’

Bart Jacobs

4th March 2011

Coalgebra Intro

57 / 98

Bart Jacobs

4th March 2011

Coalgebra Intro

58 / 98




Dirac notation for vectors

Quantum bits and classical bits

• Following Dirac, physicists use the notation | x i to denote an

Quantum bit (or qubit)

arbitrary vector. This is convenient with inner/outer products. • Binary numbers inside | − i are often used for base vectors. • For example, • In C2 one may read:

• And in C4 ,

 1 0 | 00 i = 0 0

• Etc. Bart Jacobs

1 |0i = 0

0 |1i = 1

 0 1 | 01 i = 0 0

 0 0 | 10 i = 1 0


A Qubit is a unit vector in C2 , written as: α| 0 i + β| 1 i with α, β ∈ C satisfying |α|2 + |β|2 = 1. Thus, a qubit is a superposition of | 0 i and | 1 i. The α, β are called probability amplitudes.

Classical bit (or cbit)

 0 0 | 11 i = 0 1

Coalgebra Intro

A cbit is either 0 or 1. More formally, it is a unit vector over Booleans: α| 0 i + β| 1 i with α, β ∈ B satisfying α XOR β = 1. 59 / 98

Bart Jacobs


Measurement, informally

Coalgebra Intro

60 / 98


Given vector spaces V , W we need:

• obtain either | 0 i or | 1 i as successor state (side effect)

• The biproduct V × W , with elements (v , w )

• the probability of getting | 0 i is |α|2 ∈ [0, 1]

• The tensor product V ⊗ W , with elements v ⊗ w

• the probability of getting | 1 i is |β|2 ∈ [0, 1]

Tensor distributes over biproducts: W ⊗ (V × U) ∼ = (W ⊗ V ) × (W ⊗ U).

(Recall: |α|2 + |β|2 = 1.)

Note The state (α, β) itself remains hidden

In the finite dimensional case: dim(V ×W ) = dim(V )+dim(W )

Measurement can be done with respect to any basis.


Coalgebra Intro

61 / 98

Bart Jacobs


Biproducts


dim(V ⊗W ) = dim(V )·dim(W )

Coalgebra Intro

62 / 98


Tensor products

The biproduct V × W of vector/Hilbert spaces is both a categorical product and coproduct (sum), with projections: V o vo

π1

V ×W (v , w )

π2

The tensor product V ⊗ W contains linear combinations of pairs v ⊗ w . The mapping ⊗ : V × W → V ⊗ W is “bilinear” (and universal).

/W /w

If and coprojections (injections): V v

κ2

/V ×W o / (v , 0)

(0, w ) o

κ2

4th March 2011

V has basis | a1 i, . . . , | an i W has basis | b1 i, . . . , | bm i, | ai bj i = | ai i ⊗ | bj i

w

Coalgebra Intro

then V ⊗ W has a basis given by:

W

for i ≤ n, j ≤ m.

The scalars C are unit element for ⊗, ie. C ⊗ V ∼ = V. ⊗ is used for parallel composition, possibly with entanglement.

The singleton space {0} is unit element for ×, ie. {0} × V ∼ = V. Bart Jacobs


Two products

Given a qubit in state α| 0 i + β| 1 i one can measure it, and:

Bart Jacobs


63 / 98

Bart Jacobs

4th March 2011

Coalgebra Intro

64 / 98




Tensor example

Putting qubits together

• A single qubit lives in C2 = C × C, with basis | 0 i, | 1 i

Two qubits α0 | 0 i + α1 | 1 i and β0 | 0 i + β1 | 1 i can be put in parallel, in C2 ⊗ C2 , as: α0 | 0 i + α1 | 1 i ⊗ β0 | 0 i + β1 | 1 i = α0 β0 | 00 i + α0 β1 | 01 i + α1 β0 | 10 i + α1 β1 | 11 i.

• Two qubits in parallel live in C2 ⊗ C2 , for which:

C2 ⊗ C2 = ∼ = ∼ = =

C × C ⊗ C × C C⊗C × C⊗C × C⊗C × C⊗C C×C×C×C C4

However, an arbitrary element in C2 ⊗ C2 is of the form:

with basis | 00 i, | 01 i, | 10 i, | 11 i, where | 00 i = | 0 i ⊗ | 0 i etc. n • n qubits live in C2 ⊗ · · · ⊗ C2 ∼ = C2 , with base vectors | bn−1 . . . b0 i

Bart Jacobs


for bi ∈ {0, 1}.

Coalgebra Intro

65 / 98

γ00 | 00 i + γ01 | 01 i + γ10 | 10 i + γ11 | 11 i It captures two entangled qubits, since in general such separate α’s and β’s cannot be recovered from γ’s.

Bart Jacobs


Two basic results


66 / 98


• Mathematical models for state-based computation: • state space, say X • transition map X → F (X ) • F is a functor that fixes the type of computation • A deterministic automaton involves a pair of maps:

An arbitrary element γ00 | 00 i + γ01 | 01 i + γ10 | 10 i + γ11 | 11 i ∈ C2 ⊗ C2 with |γ00 |2 + |γ01 |2 + |γ10 |2 + |γ11 |2 = 1 is of non-entangled form: α0 | 0 i + α1 | 1 i ⊗ β0 | 0 i + β1 | 1 i

hstep,final?i

X where 2 = {0, 1}.

γ00 γ11 = γ01 γ10 .

input actions A is a coalgebra:

LEMMA Classical bits can always be separated:

Coalgebra Intro

succs

/ P(X )A

• By replacing powerset P by distribution functor D one obtains

(Since classically, only one of the γij is 1; the others are 0) 4th March 2011 Basics Induction and coinduction Bisimilarity and finality Coalgebras and quantum computing

/ XA × 2

• A non-deterministic automaton, or transition system, with

X

Bart Jacobs

Coalgebra Intro

Recap on coalgebras

LEMMA (separability/disentanglement condition)

if and only if


probabilistic automata (aka. Markov chain)

67 / 98

Bart Jacobs



Coalgebra Intro

68 / 98


Distribution monad D

Coalgebras of monads

For a set X , define P D(X ) = {ϕ : X → [0, 1] support(ϕ) is finite, and x ϕ(x) = 1}

• In this context we use coalgebras X → T (X ) where T is a

monad: a special functor with unit and mulitplication

• As a result, coalgebras can be composed

Such ϕ ∈ D(X ) is a formal convex combination:   support(ϕ) = {x1 , . . . , xn } r = ϕ(xi ) > 0 r1 x1 + · · · + rn xn where  i r1 + · · · + rn = 1

X

• More formally: the set of coalgebras TX forms a monoid • Even more formally: a monoid in the category of T -algebras

• Main monad examples: • Powerset P • Distribution D • Multiset M

Bart Jacobs

4th March 2011

Coalgebras X → D(X ) are Markov chains, giving probabilistic transitions: P ri x −→ xi with i ri = 1. Coalgebra Intro

69 / 98

Bart Jacobs

4th March 2011

Coalgebra Intro

70 / 98




Multiset monad M

Starting to walk


(for the classically educated)

The mulitset monad M over complex numbers is similar to, but simpler than, the distribution monad D. For a set X , now define M(X ) = {ϕ : X → C support(ϕ) is finite } Such ϕ ∈ M(X ) is a formal linear combination: support(ϕ) = {x1 , . . . , xn } z1 x1 + · · · + zn xn where zi = ϕ(xi ) ∈ C

Such formal linear combinations form the free vector space on X .

Coalgebras X → M(X ) are like weighted automata, adding weights/resources in C as labels to transitions. Bart Jacobs


Coalgebra Intro

Tales from the Ministry of Coalgebraic Walks 71 / 98

Bart Jacobs


Walk the walk


Coalgebra Intro

72 / 98


Non-deterministic walks: definition Coalgebraic represenation, of possible left-or-right stepping: s

Z

Consider a line of integer points . . . , −2, −1, 0, 1, 2, . . . ∈ Z. Different styles of walks, say of a drunkard, on this line will be described next:

k

/ P(Z)

/ {k − 1, k + 1}

Iteration, starting in 0 ∈ Z, yields:

• non-deterministic

···

• probabilistic

0 → 7 7→ 7→ ···

• quantum

All three computational styles can & will be represented coalgebraically.

-3 -2 -1

0

1

2

···

3

•@ {−1, 1} ~~ @ •@ •@ {−2, 0, 2} ~~ @ ~~ @ {−3, −1, 1, 3} •@ •@ •@ ~~ @ ~~ @ ~~ @ {−n, −n + 2, · · · n − 2, n} •@ •@ •@ •@ ~~ @ ~~ @ ~~ @ ~~ @ • • • • •

etc

Bart Jacobs


Coalgebra Intro

73 / 98


Non-deterministic walks: iteration

U

s#

/

S

k

− 1, k + 1}

Coalgebra Intro

1 2

is expressed

/ D(Z)

/ 1 (k − 1) + 1 (k + 1) 2 2

Iteration, starting in 0 ∈ Z, now yields: 0 7→ 7→

Aside: categorically, this can be described directly as iteration in the Kleisli category of the powerset monad P. 4th March 2011

74 / 98


d

Z

/ P(Z)

k∈U {k

Coalgebra Intro

Probabilistic left-or-right stepping, each with chance via a formal convex sum / distribution, as:

The subset of successors of 0 ∈ Z, after n steps, is obtained as the n-th iterate: n s # ({0}) = {−n, −n + 2, · · · n − 2, n}.

Bart Jacobs


Probabilistic walks: definition

Formally, iteration is done via the Kleisli extension endomap: P(Z)

Bart Jacobs

7→

1 2 (-1) 1 4 (-2) 1 8 (-3)

+ + +

1 2 (1) 1 1 2 (0) + 4 (2) 3 3 8 (-1) + 8 (1)

···

-3 -2 -1 1

+

1 8 (3)

1 16

xx

1 8

{{ DD

1 4 1 4

{{ 2 DD {{

3 8

0 1 1 vv HH 1 DD { 2 { 1 D {{ 2 D 3 DD { 8 { 3 8

2 DD

1

{{ 4 DD 1 4

3

DD

···

1

F {{ 8 F

1 16

etc 75 / 98

Bart Jacobs

4th March 2011

Coalgebra Intro

76 / 98




Probabilistic walks: the general formula

Probabilistic walks: iteration

This tree of probabilities involves Pascal’s triangle. Starting in k ∈ Z, after n iterations one obtains the formal convex sum: n n n n n 0

2n

(k−n)+

1

2n

(k−n+2)+

2

2n

(k−n+4)+. . .+

n−1 2n

(k+n−2)+

n

2n

(k+n)


Coalgebra Intro

Again there is a Kleisli extension endomap d # : D(Z) → D(Z) r1 k1 + · · · + rn kn 7−→ 12 r1 (k1 − 1) + 12 r1 (k1 + 1) + · · · + 12 rn (kn − 1) + 21 rn (kn + 1) The subset of successors of 0 ∈ Z, after n steps, is obtained as the n-th iterate: n n n n

Using the sum formula for binomial coefficients: n n n n n n 0 + 1 + 2 + · · · + n−1 + n = 2 .

Bart Jacobs


d#

n

(1 0) =

0

2n

(−n)+

1

2n

(−n+2)+. . .+

n−1 2n

(n−2)+

n

2n

(n)

It is iteration in the Kleisli category of the distribution monad D. 77 / 98

Bart Jacobs


Quantum walks


Coalgebra Intro

78 / 98


Quantum walks: endomap definition I

Two vector spaces • M(Z), the free vector space on Z (over C), with base vectors

Situation / plan

written as: | k i ∈ M(Z), for k ∈ Z

• Quantum walks are standardly described as endomap S → S (see eg. work of Julia Kempe)

• C2 , the one qubit space, with base vectors | ↑ i and | ↓ i (think of the direction of the walk)

• Here it will be shown that there is also an (equivalent)

coalgebraic / monadic description.

The state space is C2 ⊗ M(Z), with basis

Bart Jacobs


Coalgebra Intro

79 / 98

Bart Jacobs


Quantum walks: endomap definition II


| ↑i ⊗ |k i | ↓i ⊗ |k i

Coalgebra Intro

80 / 98


Quantum walks: iteration and probabilities I

The relevant endomap is: C2 ⊗ M(Z) | ↑i ⊗ |k i | ↓i ⊗ |k i

q

Obtaining probabilities in quantum walks

/ C2 ⊗ M(Z)

• We are interested in the probability of reaching | k i after n

/ √1 | ↑ i ⊗ | k − 1 i + √1 | ↓ i ⊗ | k + 1 i 2

steps. Starting from 0 — more precisely, from | ↑ i ⊗ | 0 i.

2

/ √1 | ↑ i ⊗ | k − 1 i – √1 | ↓ i ⊗ | k + 1 i 2

• We do so by n-times iterating the endomap q, and then

2

measuring in the basis | k i.

• The sum of norms |αi |2 of amplitudes αi for | k i then gives

Implicitly, the Hadamard operator H : C2 → C2 is used: 1 1 H = √12 1 −1 Bart Jacobs

4th March 2011

Coalgebra Intro

the probability.

81 / 98

Bart Jacobs

4th March 2011

Coalgebra Intro

82 / 98




Quantum walks: iteration and probabilities II √1 | 2

| ↑ i ⊗ | 0 i 7→

√1 | 2

↑ i ⊗ | -1 i +

(

probabilities 1 2|

7→

1 2|

| -1 i |1i

= =

1 2 1 2

↑ i ⊗ | -2 i + ↓ i ⊗ | 0 i + 12 | ↑ i ⊗ | 0 i − 12 | ↓ i ⊗ | 2 i  1 1 2   | -2 i | 2 | = 4 1 2 probabilities | 0 i | 2 | + | 12 |2 =   | 2 i | − 12 |2 = 14 7 → · · · (next page)

Bart Jacobs


Quantum walks: iteration and probabilities II

↓i ⊗ |1i | √12 |2 | √12 |2

1 16

yy

1 8

|| BB

1 4 5 8

|| BB ||

1 2 5 8

Coalgebra Intro

1 √ | 2 2

83 / 98

Bart Jacobs


0

1

1 ww GG 1 BB | 2 | 1 2 BB | | 1 BB | 8 |


=

1 8

2 BB

3

1 8

| ↓i ⊗ 2 2 1 √ | ↑i ⊗ 2 2 ↑ i ⊗ | -3 i −

1 √ | 2 2

1 √ | 2 2

|1i + |1i +

↑i

1 √ | ↑i ⊗ 2 2 1 √ | ↓i ⊗ 2 2 ↑ i ⊗ | -1 i

√1 | 2 ⊗ |1i

+

↓ i ⊗ | -1 i +

1 √ | 2 2

 |1i     |3i

1 √ | 2 2

| -1 i + |3i

1 √ | 2 2 ⊗ |3i

+

+ ↓i  1 2  | =  | -3 i | 2√  2    | -1 i | √1 |2 + |

1 8 1 2 √ | 2 2 2 1 1 2 √ | − 2 2| = 8 1 2 | 2√ | = 18 2


↑ i ⊗ | -1 i

1 √ | 2 2

↓i ⊗ |1i

↓ i ⊗ | -1 i

=

5 8

Coalgebra Intro

84 / 98


LEMMA C2 ⊗ M(X ) ∼ = M(X + X )

···

where + is disjoint union

Proof By the following chain of isomorphisms: C2 ⊗ M(X ) = (C ⊕ C) ⊗ M(X ) ∼ = C ⊗ M(X ) ⊕ C ⊗ M(X ) by distributivity ∼ = M(X ) ⊕ M(X ) since C is tensor unit ∼ = M(X + X ) ⊕ is also coproduct of spaces, and M is a free functor.

1 16

Coalgebra Intro

−

1 √

Basic isomorphism

1

B || 4 B 1 BB | 8 EE |

−

↑ i ⊗ | -3 i +

There is “drift to the left” due to interference.

The matrix involved — Hadamard’s H in this case — determines the drifting, and thus how the tree is traversed. This may yield optimisations in data processing.

Bart Jacobs

1 √ | 2 2

probabilities

The resulting tree of quantum walk probabilities starts as: -3 -2 -1

· · · 7→

1 2

Quantum walks: iteration and probabilities III

···


85 / 98

Bart Jacobs


Quantum endomorphism as coalgebra


Coalgebra Intro

86 / 98


Qubit action is monadic!

THEOREM Linear maps (in VectC ) C2 ⊗ M(Z) −→ C2 ⊗ M(Z) correspond bijectively to functions (in Sets) Z −→ M(Z + Z)2

In the background, there is a new monad transformer result.

.that is, to coalgebras with state space Z of the functor M(2 · −)2 .

LEMMA If T is a monad, then so is X 7→ T (n · X )n , for each n ∈ N

Proof C2 ⊗ M(Z) −→ C2 ⊗ M(Z) ====================== M(Z + Z) −→ M(Z + Z) ==================== Z + Z −→ M(Z + Z) ================= Z −→ M(Z + Z)2 Bart Jacobs

4th March 2011

For quantum walks we use T = M and n = 2.

linear linear

Coalgebra Intro

87 / 98

Bart Jacobs

4th March 2011

Coalgebra Intro

88 / 98




Three categories for reversible computation

Bifinite relations • The category BifRel is defined as follows • object are sets X , and • maps X → Y are relations r : X × Y → 2 = {0, 1} such that:

• Reversible computation will be described in three categories:

BifRel dBisRel BifMRel

sets with bifinite relations, for non-deteministic computation sets with discrete bistochastic relations, for probabilistic computation sets with bifinite multirelations, for quantum computation

• for each x ∈ X the set {y ∈ Y | r (x, y ) 6= 0} is finite; • also, for each y ∈ Y the set {x ∈ X | r (x, y ) 6= 0} is finite.

• Thus: such r factors both as:

• This makes BifRel a dagger category.

Coalgebra Intro

89 / 98

Bart Jacobs


/Z

⇐⇒ m = n − 1 or m = n + 1 ⇐⇒ n = m − 1 or n = m + 1 ⇐⇒ s(n, m) = 1

0

0

X

Coalgebra Intro

91 / 98

/Z

0

(d ◦ d )(n, n ) =



1 2

0

92 / 98


• for each x ∈ X the set {y ∈ Y | r (x, y ) 6= 0} is finite; • also, for each y ∈ Y the set {x ∈ X | r (x, y ) 6= 0} is finite.

• Thus: such r factors both as:

• Also d is not unitary: ie. s † 6= s −1

†

Coalgebra Intro

• The category BifMRel is defined as follows • object are sets X , and • maps X → Y are relations r : X × Y → C such that:

in dBisRel

if m = n − 1 or m = n + 1 otherwise.

1 4


Bifinite multirelations

• Its reverse is: d † (m, n) = d(n, m) • For instance:

Bart Jacobs


• The probabilistic walks Z → D(Z) form an endomap: d

/ D(X )

Y

• This makes also dBisRel a dagger category.

Probabilistic walks in dBisRel

Z 1 • Namely, d(n, m) = 2 0

and as

via argument swapping: r † (y , x) = r (x, y ).

(The identity Z → Z in BifRel is id(n, n0 ) = 1 iff n = n0 ) 4th March 2011 Basics Induction and coinduction Bisimilarity and finality Coalgebras and quantum computing

/ D(Y )

• For a map r : X → Y in dBisRel there is again r † : Y → X

0

(s ◦ s )(n, n ) = 1 ⇐⇒ n = n − 2 or n = n or n = n + 2

Bart Jacobs


• we get discrete probability distributions in two directions:

• But s is not unitary: ie. s † 6= s −1 0

90 / 98

• for each x there are finitely many y with r (x, y ) 6= 0 and P y r (x, y ) = 1 • also, for each y ∈ Y the set {x ∈ X | r (x, y ) 6= 0} is finite and P x r (x, y ) = 1

• Its reverse is: s † (m, n) = 1 ⇐⇒ s(n, m) = 1

†

Coalgebra Intro

• The category dBisRel is defined as follows • object are sets X , and • maps X → Y are functions r : X × Y → [0, 1] such that:

in BifRel

• Namely, s(n, m) = 1 iff m = n − 1 or m = n + 1

• For instance:


Discrete bistochastic relations

• The non-deterministic walks Z → Pfin (Z) form an endomap: s

/ Pfin (X )

Y

direction, via argument swapping: r † (y , x) = r (x, y ).

Non-deterministic walks in BifRel

Z

and as

• For a map r : X → Y there is r † : Y → X in the reverse

• Only the quantum walks turn out to be reversible


/ Pfin (Y )

X

• Each of the three walks will be described there

Bart Jacobs


X

/ M(Y )

and as

Y

/ M(X )

• For a map r : X → Y there is r † : Y → X again via:

if n0 = n − 2 or n0 = n + 2 if n0 = n otherwise.

r † (y , x) = r (x, y ).

• This makes BifMRel a dagger category.

(The identity Z → Z in dBisRel is id(n, n0 ) = 1 iff n = n0 ) Bart Jacobs

4th March 2011

Coalgebra Intro

93 / 98

Bart Jacobs

4th March 2011

Coalgebra Intro

94 / 98




Probabilistic walks in dBisRel

One of the four verifications

• The quantum walks Z → M(Z + Z)2 form an endomap:

Z+Z

q

• Namely,

 q(κ1 n, κ1 (n − 1))     q(κ1 n, κ2 (n + 1)) q(κ2 n, κ1 (n − 1))     q(κ2 n, κ2 (n + 1))

/Z+Z

P q ◦ q † (κ1 m, κ1 n) = x q † (κ1 m, x) · q(x, κ1 n)

in BifMRel

= √12 = √12 = √12 = − √12

= q † (κ1 m, κ1 (m + 1)) · q(κ1 (m + 1), κ1 n)

+ q † (κ1 m, κ2 (m + 1)) · q(κ2 (m + 1), κ1 n)   √1 · √1 + √1 · √1 if n = m 2 2 2 2 = 0 otherwise   1 if κ n = κ m 1 1 =  0 otherwise

Recall Hadamard 1 1 √1 2 1 −1

• Its reverse is: q † (u, v ) = q(v , u)

= id(κ1 m, κ1 n).

• This time: q is is unitary: ie. q † 6= q −1 Bart Jacobs



Coalgebra Intro

95 / 98

Bart Jacobs


Future work


Coalgebra Intro

96 / 98


Thanks for your attention; hopefully you feel inspired

Better understand the three categories: BifRel

/ dBisRel

/ BifMRel

and see what structure (categorical and logical) is typical for which kind of computing.

Bart Jacobs

4th March 2011

Coalgebra Intro

97 / 98

Bart Jacobs

4th March 2011

Coalgebra Intro

98 / 98