July 2015 - Categories - categories.org.au

Current Issues in the Philosophy of Practice of Mathematics & Informatics
by Ralph Matthes 09 Aug '15

09 Aug '15

[why on the categories mailing list? some of the courses are strongly based on category theory, and it seems that quite some subscribers to this list are interested in connections between mathematics and philosophy] Dear colleagues, The thematic trimester CIPPMI "Current Issues in the Philosophy of Practice of Mathematics & Informatics" will be held from 4th April to 1st July 2016 at the Centre International de Math??matiques et d'Informatique de Toulouse (CIMI). This thematic trimester is organised by an interdisciplinary team of researchers in Mathematics, Philosophy, and Computer Science from the Institut de Math??matiques de Toulouse (IMT) & the Institut de Recherche en Informatique de Toulouse (IRIT). It will feature course sessions, workshops, and a thematic school on themes at the interface of Philosophy, Mathematics and Computer Science. You will find all relevant information on the website of the thematic trimester that will be regularly updated: http://www.cimi.univ-toulouse.fr/cippmi/en A mailing list allows you to receive the different announcements from CIPPMI: https://sympa.math.ups-tlse.fr/wws/info/cippmi You can register at http://www.cimi.univ-toulouse.fr/cippmi/fr/inscriptionregistration A funding for accommodation is available in priority for junior researchers and for some senior researchers without funding from their laboratory. For further information, please consult the page: http://www.cimi.univ-toulouse.fr/cippmi/fr/boursesgrants With apologies for cross-posting, best regards, the CIPPMI scientific organisation committee. --- Ralph Matthes IRIT (CNRS & Univ. Toulouse) http://www.irit.fr/~Ralph.Matthes/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

7 7

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics
by Patrik Eklund 31 Jul '15

31 Jul '15

Hi Martin, Thanks for your response. My catlist posting was using rather general formulations but there are underlying detail that can be found in our papers. Let me add just a few historical remarks. One main idea of our work is that their is a "lativity" in logic that is not respected. It's not comparable to the "lativity" in set theory where you can create classes out of sets, but you cannot throw classes back into the basket of sets, whatever that would be. The same thing happens in logic. We must start with the signature, based on which we construct terms, and terms are used inside sentences. Once we have the "bag of sentences" we may proceed "latively" to construct other things. When we eventually come to proof rules, the bag of sentences was closed a long time ago. Yet, G??del uses "provability" to create new sentences, and simply opens up that bag of sentences, and throws in these new ones. It has always been accepted, but this in fact breaches the lativity principle, which indeed is not respected in logic. The lativity principle cannot be formulated in set theory alone, and set theory is also very much untyped, we have to say. It basically also boils down to separating object languages from their metalanguages. First-order logic as developed from a fons-et-origo becomes acceptable over decades while being developed hand-in-hand, so as to say, with set theory. Type constructors in type theory are good examples that basically appear in no language whatsoever. They are simply brought in from the outside, almost like a holy spirit. But then we have category theory, and in our approach we use it as an object language where that hand-in-hand appears as a metalanguage. And then I turn category theory into a new metalanguage in order to deal with lativity of logic. There is a bit of lativity in Goguen-Burstall's and Meseguer's general models, but unfortunately types do not explicitly occur since the Sign category is considered as abstract until it is made precise for particular logics. And when it's made "precise" e.g. for first-order, it simply adopts e.g. the traditional explanation of terms, so they are not formally constructed within that categorical metalanguage. This is of course then the also reason why the Cat theory enters when dealing with semantics. It's also too general. Yes, we cannot create the set of all sets, similarly as we shouldn't even try out creating the type of all types. Nevertheless, Martin-L??f took the liberty of doing that, and was opportunistic enough to publish it. Things went wrong but it was not called a paradox. Constructions were "improved" over decades, but the HoTT community still uses universality, so that paradox just appears as the emperors new clothes. Sch??nfinkel, Curry and Church saw all these problems, and Hilbert saw it, too, of course, since all of these three were discussing these quite frequently over many years in G??ttingen. Hilbert never wrote anything about it, but probably because he couldn't solve it (or wasn't interested in medals), and he was becoming too old at that time anyway. Sch??nfinkel and Church write more explicitly that something remains to be understood, but Curry less so. Curry just went on even if the foundations were shaky. Kleene never did that, and he was in any case cleaning up other things. von Neumann probably saw what was going on, but he kept himself always out of that mess. So when that mess now has rooted itself like the Mentha Piperita, opportunists travel around, and the bank voles follow them. > I am not sure why these questions are being asked in this list: In our work now it's indeed about understanding that lativity, and these questions turn up when we use categories as a metalanguage for logic. We thereby also say that types are not fundamental, but rather given because of an object in a category. We also see how we need to debate category theory itself. Take monoidal categories. They are not really categories, are they? They do contain a category, but they are not categories. They are not algebraic structures either, are they? Freeness issues become tricky, and it becomes doubtful if universal algebra can overcoat lativity of logic. Universal algebra kind of strangles logic to become what it is generally accepted to be. Cheers, Patrik -- Prof. Patrik Eklund Ume?? University Department of Computing Science SE-90187 Ume?? Sweden ------------------------- mobile +46 70 586 4414 website www8.cs.umu.se/~peklund [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

3 2

Current Issues in the Philosophy and Practice of Mathematics & Informatics
by Andreas Blass 30 Jul '15

30 Jul '15

I just received Patrik Eklund's message containing the statement "Yet, Gödel uses "provability" to create new sentences, and simply opens up that bag of sentences, and throws in these new ones." Presumably others have already responded to this in messages that haven't yet reached me, but, just in case they haven't: Much of the work in Gödel's paper on the incompleteness theorems is devoted to making sure that what Eklund wrote here is not the case. Gödel shows how statements about provability can be encoded as arithmetical statements, which are not at all new but were available (in what Eklund calls "that bag") all along. Andreas Blass [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

CT2015 slides and pictures
by Dirk Hofmann 28 Jul '15

28 Jul '15

Dear Colleagues, this is just to announce that we have updated our website http://ct2015.web.ua.pt/ with slides of the talks and links to some pictures. Have nice summer holidays!! Best regards Dirk (for the organising committee) [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

'Dérivateurs à Barcelone' final announcement
by Fernando Muro 23 Jul '15

23 Jul '15

Dear colleagues, This is the final announcement for the conference 'Dérivateurs à Barcelone’, to be held in the University of Barcelona from Tuesday 1 to Friday 4 September 2015. Titles, abstracts, and a schedule can be already found in: http://www.ub.edu/Derivateurs2015/ The registration deadline is August 25, but if you wish some help with lodging it would be better to register sooner. Best regards, — The organizing committee Leo Alonso (Santiago de Compostela) Carles Casacuberta (Barcelona) Ana Jeremías (Santiago de Compostela) Georges Maltsiniotis (Jussieu) Fernando Muro (Sevilla) [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

CALL FOR PARTICIPATION (RAMiCS 2015)
by Michael Winter 23 Jul '15

23 Jul '15

? ? ? ? CALL FOR PARTICIPATION 15th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2015) 28 September to 1 October 2015, Braga, Portugal URL: http://ramics2015.di.uminho.pt The RAMiCS Conference is the main forum for Relational and Algebraic Methods in Computer Science. Special focus lies on formal methods for software engineering, logics of programs and links with neighbouring disciplines. ============================================================ Registration, venue, travel information and accommodation --------------------------------------------------------- Please visit http://ramics2015.di.uminho.pt Registration deadline --------------------- 4 September 2015 ============================================================ Invited Talks ------------- Towards a Probabilistic Interpretation of Game Logic Ernst-Erich Doberkat Connections Between Relation Algebras and Cylindric Algebras Ian Hodkinson A quest for Kleene algebra in 2 dimensions Gheorghe Stefanescu ============================================================ List of Accepted Papers ----------------------- L-Fuzzy Databases in Arrow Categories Evans Adjei, Wazed Chowdhury, Michael Winter Mechanised Relation-Algebraic Order Theory in Ordered Categories without Meets Musa Al-Hassy, Wolfram Kahl Closure, Properties and Closure Properties of Multirelations Rudolf Berghammer, Walter Guttmann Tool-Based Verification of a Relational Vertex Coloring Program Rudolf Berghammer, Peter H?fner, Insa Stucke Investigating and Computing Bipartitions with Algebraic Means Rudolf Berghammer, Insa Stucke, Michael Winter Completeness via canonicity for distributive substructural logics: a coalgebraic perspective Fredrik Dahlqvist, David Pym Relational Mathematics for Relative Correctness Jules Desharnais, Nafi Diallo, Wided Ghardallou, Ali Jaoua, Marcelo Frias, Ali Mili Roughness by Residuals: Algebraic desription of rough sets and an algorithm for finding core relations Martin Eric M?ller Relational Formalisations of Compositions and Liftings of Multirelations Hitoshi Furusawa, Yasuo Kawahara, Georg Struth, Norihiro Tsumagari Towards Interactive Verification of PLC Programs using MKA and KIV Roland Gl?ck, Florian Benedikt Krebs Text categorization using hyper rectangular keyword extraction: Application to news articles classification Abdelaali Hassaine, Souad Mecheter, Ali Jaoua Type Checking by Domain Analysis in Ampersand Stef Joosten, Sebastiaan Joosten Relations among Matrices over a Semiring Dylan Killingbeck, Milene Santos Teixeira, Michael Winter Completeness and Incompleteness in Nominal Kleene Algebra Dexter Kozen, Konstantinos Mamouras, Alexandra Silva Solving a tropical optimization problem via matrix sparsification Nikolai Krivulin Antichain Algebra Bernhard M?ller Metaphorisms in Programming Jose Oliveira Decomposition of Database Preferences on the Power Set of the Domain Patrick Roocks Encoding and Decoding in Refinement Algebra Kim Solin Generalized N-ary relations Bartosz Zielinski ============================================================ List of Student Track Papers ---------------------------- Loop Analysis and Repair Nafi Diallo A Generic Matrix Manipulator Dylan Killingbeck RLE-based Algorithm for Testing Biorders Oliver Lanzerath Relational Equality in the Intensional Theory of Types Victor Miraldo Decision Methods for Concurrent Kleene Algebra with Tests: Based on Derivative Yoshiki Nakamura On a monadic encoding of continuous behaviour Renato Neves Relational Approximation of Maximum Independent Sets Insa Stucke Monoid Modules and Structured Documents Algebra Andreas Zelend ============================================================ Programme Committee ------------------- Rudolf Berghammer (Kiel, Germany) Jules Desharnais (Laval U., Canada) Marcelo Frias (Buenos Aires, Argentina) Steven Givant (Mills College, USA) Hitoshi Furusawa (Kagoshima, Japan) Timothy G. Griffin (Cambridge, UK) Walter Guttmann (Canterbury, New Zealand) Robin Hirsch (London, UK) Peter H?fner (NICTA, Australia) Ali Jaoua (Doha, Qatar) Peter Jipsen (Chapman U., USA) Wolfram Kahl (McMaster U., Canada) Rodger Maddux (Iowa State U., USA) Ali Mili (NJIT, U. Heights, USA) Bernhard M?ller (U. Augsburg, Germany) Martin E. M?ller (U. Augsburg, Germany) Jos? N. Oliveira (U. Minho, Portugal; General chair) Ewa Orlowska (Warsaw, Poland) Agnieszka Rusinowska (Univ. Paris 1, France) Gunther Schmidt (Munich, Germany) Renate Schmidt (Manchester, UK) Isar Stubbe (U. Littoral-C?te-d'Opale, France) Michael Winter (Brock U., Canada; PC chair) Steering Committee ------------------ Rudolf Berghammer (Kiel, Germany) Jules Desharnais (Laval U., Canada) Ali Jaoua (Doha, Qatar) Peter Jipsen (Chapman U., USA) Bernhard M?ller (U. Augsburg, Germany) Jos? N. Oliveira (U. Minho, Portugal) Ewa Orlowska (Warsaw, Poland) Gunther Schmidt (Munich, Germany) Michael Winter (Brock U., Canada) Organising Committee -------------------- Jos? N. Oliveira (U. Minho, Portugal; General chair) Michael Winter (Brock U., Canada; PC chair) Lu?s S. Barbosa (U. Minho, Portugal) Manuel A. Cunha (U. Minho, Portugal) Ant?nio N. Ribeiro (U. Minho, Portugal) [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Correction: Steve's legacy
by wlawvere 22 Jul '15

22 Jul '15

The quadratic equation satisfied by the arrow graph is X^2 = X+2D, not X+2. [The generic dot D is not the terminal object 1 in this category. See p. 267 Conceptual Mathematics, 2nd edition.] Bill [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

The Legacy of Steve Schanuel!
by wlawvere 21 Jul '15

21 Jul '15

The Legacy of Steve Schanuel! My friend and collaborator Steve Schanuel died a year ago on July 21, 2014. Steve was a mathematicians' Mathematician. He loved the many facets of mathematics and loved to solve problems that colleagues and students presented to him. He was generous and patient with young students and happiest when he could solve interesting problems that made him sparkle with joy. The students loved him, and so did we, his colleagues. A free man with no wish for fame or fortune, unencumbered by politics, history, society, gossip, he did not get distracted by philosophy. He gave his time and energy to the problems that presented themselves, he loved to discuss them and spin further solutions. He did not like to write, and seemed to be happy when scribbling and thinking. But when a real mathematical problem presented itself, he was the most serious and hardworking scientist. That applied in particular to the real problem of passing knowledge on to young people. We both shared the passion of teaching and the belief that large numbers of students could benefit from some explicit knowledge of conceptual methods. It had originally been proposed to us to write a text book on 'Discrete mathematics', to which Steve immediately replied 'no, we will emphasize methods that are applicable to both the continuous and the discrete'. In the mathematical world he is best known for Schanuel's Lemma, and for Schanuel's Conjecture. Steve discovered the Lemma when he was still a graduate student at Chicago; it became a key instrument for those who participated in the development of Grothendieck's linear 'Klassentheorie' (K-Theory). The brilliant Schanuel's Conjecture, concerning transcendental number theory, has given rise to several advances due to the efforts of Steve himself and of dedicated logicians and number theorists, but it has still not been proved. But there are further contributions, of relevance to all branches of mathematics, that bear the stamp of elementary clarity so characteristic of Steve's work. For example, his 'What is the Length of a Potato?' presents original contributions in the process of a supremely elementary exposition of the classical subject of geometric measure theory. When I first met Steve in 1974, he explained to me a way of presenting the theory of affine-linear spaces in terms of the category of vector spaces. We developed that idea for 20 years, during which Steve proved several new mathematical results that I explain in my 1994 contribution to the historical analysis of the work of the great geometer Hermann Grassmann. Partly in response to some remarks in Federico Gaeta's notes on Grothendieck's 1973 Buffalo course, and partly as a necessary basis for his 1990 theory of Negative Sets, Steve devised the notion of extensive category as a natural relativization of the notion of distributive category. His insight was that the spaces in such categories have both Euler characteristic and dimension, that both of these quantities can be derived from a single 'rig', and that moreover the two quantities alone sometimes determine the space up to isomorphism. This remarkable non-linear Klassentheorie became a key thread in what we came to call 'Objective Number Theory'. Some of the results, which Steve derived from his theory of rigs, later turned out to be important in the study of O-minimality, in particular in the work of his student Adam Strzebonski on semi-algebraic groups. In retrospect, it may seem astonishing that the term 'rig' had not been proposed decades earlier: we constantly come across examples of commutative algebraic systems with two constants 0, 1, and two binary operations, +, x, which do not necessarily have negatives and hence become rings only upon tensoring with Z. Thus omitting the 'n' for negatives, such algebras seem to deserve the name 'rigs'. The previously available name 'Commutative semi-rings with 1' is unwieldy and even carries a faint suggestion that these objects are only half-legitimate. We were amused when we finally revealed to each other that we had each independently come up with the term 'rig'. Thorough algebraist that he was, Steve went on to determine the simple objects in the category of rigs and to develop part of the needed theory of finite presentation; naturally, he also investigated modules over rigs, projective and otherwise. Steve's basic construction, passing from a distributive category to its rig of isomorphism classes, and then tensoring with standard rigs, gave crucial additional information in some basic examples. Tensoring with Z to obtain a ring provided Euler characteristics for the spaces in the category. But tensoring instead with the rig '2' (in which 1 + 1 = 1) measures the dimension of the spaces. In some crucial cases, such as his 'negative sets' (where X = 1+2X) those two invariants are sufficient to determine the space up to isomorphism. The 'number theory of objects' turns out to be more subtle than either the theory of small infinite cardinals or of recursive sets (both of the latter have the same resulting rig, consisting of natural numbers, together with one infinite element satisfying too many equations, of course the theory of recursive SUB-sets is by contrast very rich). While teaching Conceptual Mathematics, we had noted that in the category of directed graphs, the arrow satisfies the quadratic equation X^2 = X + 2, and hence reasoned that algebraic equations have further uses in combinatorics. Noting that Steve's equation for a negative set is a special case of the equation describing the data type 'lists in the alphabet A', namely X = 1+AX, we tried simple substitution in order to get a description of 'lists of lists', namely X = 1 + X^2, which is also known as the binary tree equation for data types. This led easily to the conclusion that the tree data type has the primitive 6th root of unity as its Euler characteristic, and that in fact the more precise form X^7=X of this conclusion gives an interesting object of dimensions. This led to the conjecture that in some combinatorial categories there are no isomorphisms other than those which are rig-theoretic consequences of the defining equations, in other words, that they objectify the rig presented; that simply means that the proof of entailments is just high school algebra, except that negatives and cancellation are not used; in such calculations the expressions may become longer and longer under repeated substitutions, but then suddenly collapse due to the use of the defining equations. Our friend Andreas Blass dubbed this case of the conjecture 'Seven Trees in One', and proved it in a brilliant paper motivated by the idea of the classifying topos for the equation in question. Subsequently, several other cases were proved by Robbie Gates. It became clear that equations of the fixed-point kind were appropriate candidates for objectification, at least from the data type point of view, with the right-hand side of the polynomial equation involving a signature in the sense of universal algebra; a fixed-point bijection holds for free algebras over free theories (also known as 'Peano algebras'). Matias Menni's recent work has succeeded to remove restrictive conditions on the signature. Extensions to fixed-point equations in several variables (corresponding to signatures for multi-sorted universal algebra), had also been proposed by Steve. For many winter vacations Steve accompanied Fatima and me to Oaxaca, Mexico, where we worked on extending and recording the results of Objective Number Theory. Steve and I studied deep into the nights; sometimes Fatima heard us giggle, because we had discovered how simply some results could be proved. In the morning she typed the notes that I had left on her table. Whenever unfinished trains of thought occurred in the manuscript, we wrote SHOULD in large letters... We felt that our work received an additional inspiration from the ancient Zapotec city that could be glimpsed from our roof top. Although Steve is gone, his work and his guiding spirit live on. F. William Lawvere July 21, 2015 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

PhD Position in Verified Voting at ANU
by Dirk Pattinson 20 Jul '15

20 Jul '15

[ not on categories per se but possibly of interest to maths/ logic graduates ] Applications are invited for a fully funded PhD position in the Logic and Computation Group at the Australian National University. Project: Trustworthy Electronic Voting Supervisors: Dirk Pattinson and Rajeev Gore Starting: December 2015 Contact: Dirk Pattinson (dirk.pattinson(a)anu.edu.au) Deadline: August 15, 2015 -------------------------------------------------------------------- Project Summary Verifiable vote counting is one of the cornerstones of a trustworthy electronic voting system. Correctness and trust can be achieved by understanding voting protocols, specified textually in legislation, as formal rules. Vote counting can then be cast as successive rule application, where the sequence of rule application serves as an independently verifiable certificate attesting to the correctness of the count. The project offers a wide range of activities, ranging from foundations, rule design, efficiency considerations to concrete case studies. The project seeks to further investigate this idea and apply it to real-world voting systems and mainly deals with the following aspects: - generation of provably correct vote counting functions from rules - efficiency of rule-based vote counting and certificate checking - formal proofs of meta-properties of voting protocols - case studies with real-world voting protocol - minimising the gap between formal rules and legal specification -------------------------------------------------------------------- Small Print - the studentship is open to individuals of any nationality. - the Logic and Computation Group (http://logic.cecs.anu.edu.au/) is part of the Research School of Computer Science (http://cs.anu.edu.au/) at the Australian National University (http://www.anu.edu.au/) - We are based in Canberra, Australia, the top-ranking region of the 2014 OECD quality of life survey (http://www.canberratimes.com.au/act-news/canberra-named-the-best-place-in-t…) - We actively seek to promote diversity in our workplace. -------------------------------------------------------------------- [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Octoberfest
by Richard Blute 19 Jul '15

19 Jul '15

2015 Category Theory "Octoberfest" Workshop University of Ottawa, Ottawa, Canada October 31-November 1, 2015 FIRST ANNOUNCEMENT * * * The Category Theory "Octoberfest" is an (almost) annual workshop, traditionally held in October, bringing together researchers in category theory and its applications. This year's meeting will be hosted in the Department of Mathematics and Statistics at the University of Ottawa The scientific program starts on October 31, and consists of one and a half days of research talks. Research talks If you wish to give a talk please send a title and abstract to rblute(a)uottawa.ca by October 1. Time slots are limited, so please register early if you would like to be considered for a talk. Accommodations We are currently making arrangements for special rates at area hotels. Details in Second Announcement. Registration If you would like to attend the meeting, please register by emailing rblute(a)uottawa.ca. There will be a reasonable on-site registration fee to cover workshop costs. We would appreciate it if you would let us know soon if you are probably going to attend. Rick Blute: rblute(a)uottawa.ca Pieter Hofstra: phofstra(a)uottawa.ca [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0