June 2013 - Categories - categories.org.au

Partial functor
by David Leduc 17 Mar '15

17 Mar '15

Hi, A partial functor from C to D is given by a subcategory S of C and a functor from S to D. What is the appropriate notion of natural transformation between partial functors that would allow to turn small categories, partial functors and those "natural transformations" into a bicategory? The difficulty is that two partial functors from C to D might not have the same definition domain. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

7 6

Research positions
by Maria Manuel Clementino 26 Feb '14

26 Feb '14

5-YEAR RESEARCH POSITIONS The Centre for Mathematics of the University of Coimbra (CMUC) invites applications for five 5-year research positions in all areas of Mathematics. Applicants should have a PhD in Mathematics and at least three years of post-doctoral experience, with an international-level publication record and demonstrated ability to perform independent research. Preference will be given to candidates working in one of the areas in which the members of CMUC are currently active. A very good command of English is required. The appointments will be made for three years, renewable for two more. Successful applicants are expected to develop research within the areas of interest of CMUC. They should also contribute to graduate studies, supervising students from the Department of Mathematics. The basic salary is equivalent to the index 195 of the Portuguese research career (in the order of 42 500 euros a year), in accordance with the Ciência 2008 guidelines http://alfa.fct.mctes.pt/apoios/contratacaodoutorados/edital2008 Benefits include private health insurance and social security. Applicants should send • cover sheet (available from www.mat.uc.pt/cmuc/coversheet.pdf) including names and contact information of three persons who can provide a letter of recommendation • curriculum vitae (publication list included) • a 5-year research proposal (2 pages max), emphasizing their own research goals as pdf files to cmuc(a)mat.uc.pt. The subject of the e-mail message must include the job reference C2008 FCTUC CMUC v15-v19. The deadline for applications is *September 10, 2008.* ------------------------------ More information can be found at www.mat.uc.pt

1 1

Re: Quipper: a quantum programming language
by Anthony Bordg 30 Jun '13

30 Jun '13

Dear Peter, thanks for your detailed answer and this interesting point. 2013/6/21 Peter Selinger <selinger(a)mathstat.dal.ca> > Dear Anthony, > > you asked a detail question, so I'll give a detailed answer. This may > not be of interest to all the readers of this list, so I hope people > will feel free to skip this message. As I mentioned, the application > is a bit minor (but nevertheless fun). > > Suppose in Haskell (or another functional programming language), > you need to define a data type F(X) that is parametric (often > functorial) on another type X. One basic example is that of lists: > > data List x = Nil | Cons x (List x) > > For those not familiar with Haskell syntax, this simply corresponds to > the categorical equation > > List(X) ~= 1 + X x List(X), > > which can be solved by taking an initial algebra of the functor > F(A) = 1 + X x A. > > There are two constructors "Nil" and "Cons". Now suppose that, for > some reason, we need a third constructor "Third", but we want that > constructor to be available *only* when X is equal to some particular > type X_0. In other words, we want: > > data List x = Nil | Cons x (List x) { when x is not x0 } > data List x = Nil | Cons x (List x) | Third x { when x is x0 } > > It is of course not possible in Haskell to define a polymorphic type > by case distinction like this. We could get around it by defining > > data List x = Nil | Cons x (List x) | Third x > > for all x, and making it a *convention* that the third constructor is > only going to be used when x = x0. However, this does not work well, > because many reasonable programs will not type-check. The problem > arises when one needs to define a function from List x to some other > type by case distinction. When it comes to the third case, the type > checker cannot prove that x = x0, and in general, it may not be > possible to define the desired function so that it works for arbitrary > x. > > The solution is to define an identity type > > data Identity a b = Identity (a->b, b->a) > > and four functions > > reflexivity :: Identity a a > symmetry :: Identity a b -> Identity b a > transitivity :: Identity a b -> Identity b c -> Identity a c > identity :: Identity a b -> a -> b. > > (And we make sure that no additional primitive functions of this type > can be defined, for example by making it an abstract type). Then we > can define > > data List x = Nil | Cons x (List x) | Third (Identity x x0) x > > And this does exactly the right thing. When it comes to doing a case > distinction on the type List x, in the third case, we can actually > *prove* that x is equal to x0, because the identity type contains a > witness of this fact. > > The specific thing we needed this for in Quipper is in our library for > arithmetic with fixed-but-arbitrary length quantum integers. We needed > a type Int(X) representing integers in fixed-length binary notation, > but using elements of the type X instead of the usual {0,1} as the > digits. This gives us, for example, a type Int(Bool) of classical > integers, and a type Int(Qubit) of quantum integers. Working with > fixed-length integers is sometimes a bit tedious, because when you > write an arithmetic expression such as 0 + a, you need to first > specify what the length of 0 is, and then it needs to match the length > of a. In order to infer this kind of information automatically, we > added an alternative to the type Int(Bool), where one could store an > ordinary integer (not yet specialized to a particular number of > digits). However, this was only going to work for Int(Bool) and not, > e.g., for Int(Qubit). So we used the above trick to do it. > > (Before starting a long discussion, I should add that we are of course > aware that there are other ways of dealing with fixed-but-arbitrary > length integers in Haskell, for example, by using type-level integers > to parameterize a type Int(n) of n-bit integers. The above is just one > particular example of something we did; I'm not saying that it is the > only or even the best way to do it). > > -- Peter > > Anthony Bordg wrote: > > > > Hi, > > > > can you describe the application of identity types from type theory that > > you found ? > > > > Best wishes > > > > Anthony > > > > > > 2013/6/20 Joyal, André <joyal.andre(a)uqam.ca> > > > > > Dear Peter, > > > > > > I thank you for your answer. > > > > > > Is it possible to "simulate" quantum > > > computing on ordinary computers? > > > Operator algebra is matrix algebra. > > > Surely, there will be a loss of efficiency. > > > But it might help understanding > > > the nature of quantum computations. > > > > > > Best wishes, > > > -André > > > > > > > > > -----Original Message----- > > > From: Peter Selinger [mailto:selinger@mathstat.dal.ca] > > > Sent: Thu 6/20/2013 3:36 PM > > > To: Joyal, André > > > Cc: Categories List > > > Subject: Re: categories: Quipper: a quantum programming language > > > > > > Dear Andre, > > > > > > the answer, unfortunately, is no. At least we don't think so. We > > > developed this programming language for IARPA, an agency of the > > > U.S. government, and effectively nobody knows whether they have a > > > quantum computer or not. > > > > > > In any case, the language is designed so that it *could* run on a > > > quantum computer, if there was one. So now we are just standing by > > > until somebody builds the hardware :) > > > > > > There is actually one kind of quantum computer that is already on the > > > market: the DWave quantum computer. Unfortunately, our language is not > > > compatible with it; the DWave machine uses a technology called > > > "adiabatic quantum computing", and people are still figuring out how > > > to program it. Our language would be compatible with quantum computers > > > based on the quantum circuit model. > > > > > > Maybe the underlying point of your question is: why would anybody care > > > about a quantum programming language, when there is no quantum > > > computer? > > > > > > One possible answer is: to help figure out how much it would actually > > > cost to build one. It is one thing for a quantum algorithm to appear > > > in a research paper. You will find a lot of statements like "it is > > > well-known that such-and-such can be done in O(n^2) operations", "by > > > applying such-and-such trick this problem can be reduced to another > > > problem with polynomial overhead", and so on. It is quite a different > > > thing to actually program the algorithm, and to worry about how to do > > > so efficiently. The difference between using 10^10 operations or 10^50 > > > operations matters a lot in practice, but not in theory. Moreover, one > > > can then account for additional overhead that people don't usually > > > think about much, like the cost of adding many layers of error > > > correction, physical fail-safe mechanisms, and so on. By coding up > > > some algorithms for "realistic" problem sizes, we get a much better > > > idea of what kind of computing resources this would actually require. > > > ("Realistic" can be defined as the problem size where a hypothetical > > > quantum computer would actually outperform a classical computer > > > running the best known classical algorithm for the problem). > > > > > > Finally, there is some interesting theory that we can discover by > > > considering programming languages for quantum computing. To our > > > surprise, we even found a minor, yet satisfying, application of > > > identity types from type theory. > > > > > > Best wishes, -- Peter > > > > > > > > > [For admin and other information see: http://www.mta.ca/~cat-dist/ ] > > > > > >

1 0

Pictures.
by Charles Wells 27 Jun '13

27 Jun '13

I apologize for posting the two pictures I mentioned in a recent message in an inaccessible place. I have reposted them on my own website here: http://www.abstractmath.org/Pix%20for%20Wikipedia/ Explanation: Picasa used to allow you to post pix to the web and make them available to everyone. But now it is merged with Google+, where "Public" means anyone with a Google+ account. Sorry for the trouble. Charles Wells -- professional website: http://www.cwru.edu/artsci/math/wells/home.html Gyre&Gimble (math blog): http://www.abstractmath.org/Word%20Press/ abstract math website: http://www.abstractmath.org/MM//MMIntro.htm astounding math stories: http://www.abstractmath.org/MM//MMAstoundingMath.htm personal website: http://www.abstractmath.org/Personal/index.html sixwingedseraph.facebook.com [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Please help identify photos
by Charles Wells 26 Jun '13

26 Jun '13

The first two photos at this location https://plus.google.com/photos/110533937153449478697/albums/589351695653196… are of me and Michael Barr, and of Mac Lane and Eilenberg. Both were taken at meetings, and E&M were at Isle of Thorns. I would appreciate it if anyone could tell me where Mike and I were, and when the Isle of Thorns meeting was. Perhaps you can also identify the woman behind me in the first picture. I intend to upload these pix to Wikimedia Commons. Thanks Charles -- professional website: http://www.cwru.edu/artsci/math/wells/home.html Gyre&Gimble (math blog): http://www.abstractmath.org/Word%20Press/ abstract math website: http://www.abstractmath.org/MM//MMIntro.htm astounding math stories: http://www.abstractmath.org/MM//MMAstoundingMath.htm personal website: http://www.abstractmath.org/Personal/index.html sixwingedseraph.facebook.com [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Quipper: a quantum programming language
by selinger＠mathstat.dal.ca 21 Jun '13

21 Jun '13

Dear Category Theorists, we are proud to announce the first public release of Quipper, an embedded, scalable functional programming language for quantum computing. The Quipper distribution is available here: http://www.mathstat.dal.ca/~selinger/quipper/ and includes extensive documentation, as well as seven worked examples of non-trivial quantum algorithms from the literature. Here are some highlights: * High-level circuit description language, including both gate-by-gate descriptions and powerful higher-order operators for assembling and manipulating circuits. * A monadic semantics, allowing for a mixture of procedural and declarative programming styles. * Built-in facilities for automatic synthesis of reversible quantum circuits, including from classical Haskell code. * Support for hierarchical circuits. * Extensible quantum data types. * Programmable circuit transformers (that are essentially monoidal functors). * Support for a dynamic lifting operation to allow circuit generation to depend on parameters generated at circuit execution time. * Extensive libraries of quantum functions, including: libraries for quantum integer and fixed-point arithmetic; the Quantum Fourier transform; an efficient quantum random access memory implementation; libraries for simulation of pseudo-classical circuits, Stabilizer circuits, and arbitrary circuits; libraries for exact and approximate decomposition of circuits into specific gate sets. Comments are welcome! Alexander S. Green Peter LeFanu Lumsdaine Neil Julien Ross Peter Selinger Benoit Valiron [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

3 8

More publicity
by Ross Street 21 Jun '13

21 Jun '13

Okay, how about this then? http://blogs.scientificamerican.com/guest-blog/2013/05/16/quantum-mechanica… ==Ross [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

5 4

The Homotopy Type Theory Book
by Michael Shulman 21 Jun '13

21 Jun '13

Dear categories, This is to announce that the following book is now available: Homotopy Type Theory: Univalent Foundations of Mathematics by the Univalent Foundations Program, IAS "The HoTT Book" was written as a massive collaborative effort during the recent special year on Univalent Foundations at the IAS. It is available as a free download, or printed and bound at cost, as described here: http://www.homotopytypetheory.org/book Further description can be found in the following blog posts: http://homotopytypetheory.org/2013/06/20/the-hott-book/ http://golem.ph.utexas.edu/category/2013/06/the_hott_book.html http://math.andrej.com/2013/06/20/the-hott-book/ Regards, Mike Shulman (for The Univalent Foundations Program) [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

a historical question
by Valeria de Paiva 18 Jun '13

18 Jun '13

Hi, I know no one should pay too much attention to what Wikipedia says, but I wonder if anyone can give me a proper reference for: "Cartier was to give a Séminaire Bourbaki<http://en.wikipedia.org/wiki/S%C3%A9minaire_Bourbaki>exposition of intuitionistic logic." This is in the Wikipedia entry for Categorical Logic http://en.wikipedia.org/wiki/Categorical_logic and as anything that is in Wikipedia is repeated lots of times, all over the web. Does anyone know what this sentence is referring to, please? Thanks Valeria -- Valeria de Paiva http://www.cs.bham.ac.uk/~vdp/ http://valeriadepaiva.org/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

5 4

Re: a historical question
by Valeria de Paiva 17 Jun '13

17 Jun '13

Thank you Prof Benabou for the personal evidence and thank you Urs Schreiber and Thomas Streicher for the document!!! Really glad to see that the Seminaire Bourbaki is online and surprised that I couldn't find it yesterday. best, Valeria On Mon, Jun 17, 2013 at 12:32 AM, Urs Schreiber < urs.schreiber(a)googlemail.com> wrote: > I suppose this is referring to > > Pierre Cartier, > "Logique, catégories et faisceaux", > Séminaire Bourbaki, 20 (1977-1978), Exp. No. 513, 24 p. > http://www.numdam.org/item?id=SB_1977-1978__20__123_0 > > [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0