Paul Blain Levy | 22 Aug 16:06 2015
Picon
Picon

coherence for symmetric monoidal and (co)affine categories

Dear all,

Given a category C, define symm(C) to be the following category:

- an object is a finite family [or finite sequence, if preferred] of
C-objects

- a morphism from (C_i | i in I) to (D_j | j in J) consists of an
bijection f : I --> J and, for each i in I, a C-morphism C_i --> D_fi.

Define coaff(C) likewise but with "injection" instead of "bijection".

It seems to be folklore that

(1) symm(C) is the free symmetric monoidal category on C

(2) coaff(C) is the free coaffine category (symmetric monoidal category
with initial unit) on C.

In the special case where C is discrete, these statements follow from
the coherence arguments in Mac Lane's "Natural associativity and
commutativity" and Petric's "Coherence in substructural categories".

But for general C, where are these statements proved?

Paul

--

-- 
Paul Blain Levy
School of Computer Science, University of Birmingham
(Continue reading)

Tarmo Uustalu | 17 Aug 15:39 2015
Picon
Picon

ETAPS 2016 call for papers

******************************************************************

                   CALL FOR PAPERS: ETAPS 2016

19th European Joint Conferences on Theory And Practice of Software

            Eindhoven, The Netherlands, 2-8 April 2016

                    http://www.etaps.org/2016

******************************************************************

-- ABOUT ETAPS --

ETAPS is the primary European forum for academic and industrial
researchers working on topics relating to software science. ETAPS,
established in 1998, is a confederation of five main annual
conferences, accompanied by satellite workshops. ETAPS 2016 is the
nineteenth event in the series.

-- MAIN CONFERENCES (4-7 April) --

    * ESOP: European Symposium on Programming
        (PC chair Peter Thiemann, Universität Freiburg, Germany)
    * FASE: Fundamental Approaches to Software Engineering
        (PC chairs Perdita Stevens, University of Edinburgh, UK,
         and Andrzej Wasowski, IT University of Copenhagen, Denmark)
    * FOSSACS: Foundations of Software Science
        and Computation Structures
        (PC chairs Bart Jacobs, Radboud Universiteit Nijmegen, 
(Continue reading)

John Baez | 17 Aug 10:14 2015

categories of models of cartesian PROPs

Hi -

Here are two questions:

Suppose you have a category with finite products, say T, and a symmetric
monoidal category, say C.   Let [T,C] be the category where

    objects are symmetric monoidal functors from T to C,
    morphisms are monoidal natural transformations.

*1.  What structure beyond a mere category does [T,C] automatically get in
this sort of situation?*

*2.  What further structure do we get if C has some particular class of
limits or colimits?*

I haven't thought about this much.  Even if T were just symmetric monoidal,
I think [T,C] should get a symmetric monoidal structure due to "pointwise
multiplication", just as the set of homomorphisms from one commutative
monoid to another becomes a commutative monoid where

fg(x) := f(x) g(x)

Should [T,C] also have some sort of "comultiplication"?  What extra
benefits do we get from T being cartesian?

Here's why I care:

My student Brendan Fong wrote a masters' thesis about Bayesian networks,
which he's trying to polish up and publish.
(Continue reading)

Ichiro Hasuo | 13 Aug 08:54 2015
Picon

HSCC 2016: Call for Papers

Dear colleagues,

Please find below a CfP for HSCC 2016, a conference devoted to
the study of hybrid systems (with both discrete and continuous
dynamics).

The topic might seem out of the scope of the categories list,
but there have been exciting examples of "transfer" of results
and ideas from the discrete world to the hybrid one,
exploiting the abstraction power of the categorical language.
They include [Haghverdi, Tabuada and Pappas,
Theoretical Computer Science, 2005] and [Jacobs, Theoretical
Computer Science, 2000]. I believe there's a chance that
category theory will help making self-driving cars way safer :-)

All the best,
Ichiro Hasuo
http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/

==================================================
19th International Conference on Hybrid Systems: Computation and Control (HSCC)
April 12-14, 2016,
Vienna, Austria

URL: http://www.cs.ox.ac.uk/conferences/hscc2016/

Important dates

Abstract Submission deadline (required): October 8, 2015. (no
extensions possible)
(Continue reading)

Robert Dawson | 11 Aug 14:20 2015
Picon

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

Patrik Eklund wrote:'

... at least some members of this catlist will see me just as a devoted
soldier "seeking the bubble reputation, even in the _canon's_ mouth".

I'm trying to figure out if this is a misspelling or a pun so clever
that I can't quite figure it out.

Robert Dawson

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Thomas Streicher | 11 Aug 11:12 2015
Picon

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

> In logic we typically have signatures, terms, sentences, structured sets
> of sentences, entailment, models, satisfactions, axioms, theories and
> proof calculi. We cannot e.g. define entailment before we have a notion
> of sentences, and we should not define sentences before we have a notion
> of terms. The latter is a bit more controversial. In first-order logic I
> would see P(x), where P is a "predicate symbol", as a term, and not as a
> sentence, whereas putting a quantifier in front of it, Ex.P(x), makes it
> no longer a term. This is why I have difficulties e.g. to accept that
> the two 'not's in expressions like "not Ex.P(x)" and "Ex.not P(x)" would
> be the same. I am starting to think they are only informal as symbols, a
> bit similar as Church said lambda is and informal symbol, so actually
> not part of the formal syntax. Am I wrong or am I wrong?

I don't understand why atomic formulas are terms but not formulas.
Always thought the Lawvere's hyperdoctrines made all this very clear:
terms are in the base and formulas are in the fibres.
In case there is a generic family of propositions  A:Prop |- True(A)
we can turn predicates into terms of type Prop. That's the shift to HOL.

The 2 different negations are just negations in two different fibres.

Thomas

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Patrik Eklund | 9 Aug 11:52 2015
Picon
Picon

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

On 2015-08-09 05:10, Fred E.J. Linton wrote:
> Not wishing to broadcast my illiteracy in the matter ...
> So I ask you now, in public, where my shame can be greatest: what do
> you mean by "lativity"?

Thank you, Fred, for your questions. We were actually nervously waiting
for somebody to ask that question, so we will remember you always for
having done that.

In logic we typically have signatures, terms, sentences, structured sets
of sentences, entailment, models, satisfactions, axioms, theories and
proof calculi. We cannot e.g. define entailment before we have a notion
of sentences, and we should not define sentences before we have a notion
of terms. The latter is a bit more controversial. In first-order logic I
would see P(x), where P is a "predicate symbol", as a term, and not as a
sentence, whereas putting a quantifier in front of it, Ex.P(x), makes it
no longer a term. This is why I have difficulties e.g. to accept that
the two 'not's in expressions like "not Ex.P(x)" and "Ex.not P(x)" would
be the same. I am starting to think they are only informal as symbols, a
bit similar as Church said lambda is and informal symbol, so actually
not part of the formal syntax. Am I wrong or am I wrong?

In logic we indeed need a signature (sorts and operators) in order to
construct the categorical object of terms. Construction is important. We
need terms to categorically construct sentences, which appear because of
a sentence functor not being extendable to a monad. Otherwise sentences
are terms, aren't they, because then we could substitute sentences
within sentences, and that does not comply with our traditional view of
sentences.

(Continue reading)

Nicola Gambino | 4 Aug 15:46 2015
Picon

Jobs at the University of Leeds

Dear friends and colleagues,

the University of Leeds is currently advertising two positions in Pure Mathematics: 

(1) University Academic Fellow in Pure Mathematics

  http://jobs.leeds.ac.uk/MAPMA1022

(2) Holders of External Fellowships in Pure Mathematics

    http://jobs.leeds.ac.uk/MAPMA1026

Please feel free to contact me if you wish to have more information.

With best wishes,
Nicola

===
Dr Nicola Gambino
School of Mathematics
University of Leeds
E-mail: n.gambino <at> leeds.ac.uk

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Andreas Blass | 30 Jul 17:28 2015
Picon

Current Issues in the Philosophy and Practice of Mathematics & Informatics

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/ ]

Patrik Eklund | 29 Jul 07:54 2015
Picon
Picon

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics

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,
(Continue reading)

Dirk Hofmann | 28 Jul 18:07 2015
Picon

CT2015 slides and pictures


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/ ]


Gmane