Home

Tropical Semirings

Tropical Semirings, Jean-Éric Pin. Idempotency 1994.

It is a well-known fact that the boolean calculus is one of the mathematical foundations of electronic computers. This explains the important role of the boolean semiring in computer science. The aim of this paper is to present other semirings that occur in theoretical computer science. These semirings were baptized tropical semirings by Dominique Perrin in honour of the pioneering work of our brazilian colleague and friend Imre Simon, but are also commonly known as (min, +)-semirings.

In the previous post, Ohad Kammar asked for some more examples of why we should care about adjunctions, which reminded me of one of my favorite examples. You can understand solving many optimization problems as looking for a Galois connection between your problem and the tropical semiring. (Galois connections in general are one of the sources of the program derivation superpowers of the Squiggolists. So if you want to prove programs like Shin Cheng-Mu does, it's worth understanding!)

By neelk at 2010-06-07 09:55 | Theory | other blogs | 12880 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Provenance Semirings

Provenance Semirings (PDF)

Just another application of semirings, not necessarily tropical ones, to computer science.

By Derek Elkins at Mon, 2010-06-07 16:50 | login or register to post comments

Provenance Semirings

...and tropical ones! See slides 22 and 47-48 of this recent talk by Val Tannen.

By jnfoster at Tue, 2010-06-08 12:58 | login or register to post comments

Rig Conservativity

On the borderline of being off topic, I recently bumped into Tom Leinster's and Marcelo Fiore's Objects of Categories as Complex Numbers (2005):

In many everyday categories (sets, spaces, modules, ...) objects can be both added and multiplied. The arithmetic of such objects is a challenge because there is usually no subtraction. We prove a family of cases of the following principle: if an arithmetic statement about the objects can be proved by pretending that they are complex numbers, then there also exists an honest proof.

The relation to computer science is explained in the introduction: because recursive datatypes form a rig (semiring), one can apply the main theorem, and obtain that any identity arrived at using complex arithmetic actually holds for any (non-linear) recursive datatype.

I'm wondering if any real-life datatype can be simplified in this way.

By Ohad Kammar at Mon, 2010-06-07 23:07 | login or register to post comments

In Haskell

I've had a fairly minimal implementation of them in the monoids library on Hackage for a while:

http://hackage.haskell.org/packages/archive/monoids/0.1.36/doc/html/Data-Ring-Semi-Tropical.html

By Edward Kmett at Wed, 2010-06-23 20:49 | login or register to post comments

New paper on Programming

New paper on Programming from Galois Connections from Shin-Cheng Mu and Oliveira. Really exciting looking stuff: http://www.iis.sinica.edu.tw/~scm/2010/programming-from-galois-connections/

By S. Clover at Fri, 2010-12-10 15:56 | login or register to post comments