@typeswitch And last week, I was in one of the joints in Scotland that can totally do an ice cream float properly. But dairy does me in just now.

@plragde @krismicinski Beware of low-flying responsibilities! Some of us have to go to business meetings in order to repel business. The beer helps.

I'm upset and scared tonight, about mortality (not mine). Don't let me get crotchety for quavers.

@ohad @JacquesC2 It more or less is what I meant, but my point is that the symmetry can perhaps be characterised by what happens when you stabilise a point in an orbit (doesn’t matter which point, does matter which orbit). The rest of that orbit (and the other orbits, which I forgot about in my haste) get partitioned into suborbits. My hope is that I can obtain a presentation of group(oid) actions with a more coalgebraic flavour, in terms of hereditary refinement of partitions. I haven’t cooked it right, yet.

I have a suspicion that the category of partitions and refinements is going to be important, particularly for its pullbacks. And binomial coefficients will show up again.

@dimpase I even own a few. I'm aware of the standard setup, which I was indeed taught as a lad. Orbits arise as the quotient of the set acted on by the equivalence induced by the group.

But as a computer scientist, I prefer to avoid quotients, much as I prefer to avoid things which demand respect. So I'm trying to turn the construction upside-down, starting by characterising the orbits (and their iterated stabilisers), then seeking to recover the group structure. It looks like I sometimes extract things which may not be group actions, but are groupoid actions on systems with nontrivial state.

I've got lots of things to be doing, but one of them is sitting in a sunbeam.

@ionchy Note the singular indefinite article. Which one of us is it?

*part of the problem may be that these systems have, mostly on purpose, stopped being associated with “AI” (because they don’t fit in with the hype and anthropomorphization narratives anymore). i’m talking about things like:
- symbolic program synthesis
- proof search
- constraint solvers
- evolutionary algorithms
- planning
- any of the above combined with learning methods, like POMDPs or reinforcement learning or inductive logic programming

Show thread

Think of a regular pentagonal container, storing data at its points (labelled A..E). The pentagon can be rotated about its centre to align with indices 0..4, cyclically, with A in any of those positions. But two of the edges are also articulated! You (the devil) can switch around B and C; you can also switch around D and E. This container can be aligned with the place numbers in 20 ways: 5 ways to place A, then two ways each to order BC and DE.

But these symmetries do not form a subgroup of S5.

Which positions you can swap depend on where A is. There is nontrivial state in this system. It's a group*oid*.

Thinking of wiggly (or, more demonically, squirming) containers as having positions acted on by a symmetry group is missing some perfectly sensible containers.

Show thread

One of the things I'm enjoying in tangling with containers that have wiggly positions with @pigworker is how differently we're approaching the same problem.

I'm currently really puzzled by why groups have anything to do with the matter at all! One approach is to start with containers with wiggly positions - groups are then in on the ground floor.

Another approach is to look at various free constructions (left adjoints to forgetful functors from theories back down to set) that can be seen as giving rise to those containers. From that perspective, that groups are involved at all is very mysterious.

Uk politics, policing 

No snowflake ever snowflaked so hard as the Met Police Commissioner objecting to the word “institutional”. I’m sorry, in light of the most damning report of policing in decades we suddenly are expected to spend time listening to coppers talking about their hurt feelings over such words?

@wilbowma Sorry. My native language is 1970s television. And given today's nonsense in UK politics, I couldn't help responding to laudable ambitions to honesty by being camp as tits.

So we obtain an inductive definition of orbits of a given size. An orbit of size n+1 is a partition of n into parts k, all of which have an orbit of size k.

It is clear that every one-orbit subgroup of Sn gives us such an orbit of size n.

But is the reverse the case?

No!

5-1 splits as 2,2. S5 has no subgroup whose action on 5 has a stabiliser which behaves like Z22.

What's going on?

Show thread

That's to say, what it is to be an orbit it to know how to stabilise a point (wlog any point, so who needs a type of such points?) in that orbit.

Show thread
Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.