Category Archives: Good Math

Erlang: a Language for Functional Concurrency (Updated!)

Leave a reply

Several commenters pointed out that I made several mistakes in my description of Erlang. It turns out that the main reference source I used for this post, an excerpt from a textbook on Erlang available on the Erlang website, is quite out of date. I didn’t realize this; I assumed that if they pointed towards that as a tutorial, that it would represent the current state of the language. My bad. As a result, several things that I said about Erlang – including some negative comments, were inaccurate. I’ve updated the article, and the changes are marked with comments.

As long-time readers will recall, one of my greatest interests in programming languages. A while back, I wrote a tutorial on Haskell, which is one of the most influential languages currently in the programming language research community. Haskell is a pure, lazy, functional language which gained a lot of attention in recent times for being incredibly expressive, while maintaining a solid theoretical basis with well-defined semantics. What made Haskell unusual was that it’s a completely pure functional language – meaning no true state at all – not for I/O, not for assignment, not for mutable data – but through the
use of a clever construct called a monad, you can create the effect of state without disturbing the functional semantics of the language. It’s quite a nice idea, although I must admit that I remain somewhat skeptical about how scaleable it might be.

One of the competitors of Haskell for mindshare in the community of people who are interested in functional programming languages is a language called Erlang. In many ways, Erlang is a polar opposite to Haskell. Erlang is, basically, a functional language, but it’s designers didn’t object to tossing in a bit of state when it made things easier. It’s dynamically typed,
and even for a dynamically typed language, it’s support for typing is weak. It’s gotten its attention for a couple of big reasons:

  1. Erlang was designed by Ericsson for implementing the software in their switches and routers. It’s the first functional language designed by a company for building production applications for extremely complex performance-critical low-level applications like switching and routing.
  2. Erlang is specifically designed for building distributed systems. As I’ve mentioned before, programming for distributed systems is incredibly difficult, and most programming languages are terrible at it.

Concurrency and distributed systems are a big deal. I’d argue that programming for concurrency and distribution are the biggest problems facing software developers today. Pretty much every computer that you can buy has multiple processors, and to take full advantage of their power, code needs to use concurrency. And the network is an unavoidable part of our environment: many of the applications that we’re writing today need to be aware of the internet, and need to interact with other systems. These are just simple facts of the modern computing world – and software developers need tools to deal with them.

Continue reading →

From Sets to Arithmetic

Leave a reply

Even though this post seems to be shifting back to axiomatic set theory, don’t go thinking that we’re
done with type theory yet. Type theory will make its triumphant return before too long. But before
that, I want to take a bit of time to go through some basic constructions using set theory.

We’ve seen, roughly, how to create natural numbers using nothing but sets – that’s basically what
the ordinal and cardinal number stuff is about. Even doing that much is tricky – witness my gaffe about
ordinals and cardinals and countability. (What I was thinking of is the difference between the ε series in the ordinals, and the ω series in the cardinals, not the ordinals and cardinals themselves.) But if we restrict ourselves to sets of finite numbers (note: sets of finite numbers, not finite sets of numbers!), we’re pretty safe.

Of course, we haven’t defined arithmetic – we’ve just defined numbers. You might think it would be
pretty important to define arithmetic on the numbers. If you thought that, you’d be absolutely
Correct. So, that’s what I’m going to do next. First, I’m going to define addition and subtraction – multiplication can be defined in terms of addition. Division can be defined in terms of multiplication
and subtraction – but I’m going to hold off on defining division until we get to rational numbers.

Continue reading →

Tiptoeing into Type Theory

18 Replies

When Cantor’s set theory – what we now call naive set theory – was shown to have problems in the form of Russell’s paradox, there were many different attempts to salvage the theory. In addition to the axiomatic approaches that we’ve looked at (ZFC and NBG), there were attempts by changing the basis of set theory – discarding sets in favor of something similar, but with restrictions that avoid the problems of naive set theory. Today, I’m going to talk about an example of the latter approach, called type theory. Type theory is a very different approach from what we’ve seen before, and one which is particularly useful and interesting to people in my neck of the woods.

Continue reading →

Basics: Proof by Contradiction

Leave a reply

I haven’t written a basics post in a while, because for the most part, that well has run dry, but once
in a while, one still pops up. I got an email recently asking about proofs by contradiction and
counterexamples, and I thought that would be a great subject for a post. The email was really
someone trying to get me to do their homework for them, which I’m not going to do – but I can
explain the ideas, and the relationships and differences between them.

Proof by contradiction, also known as “reductio ad absurdum”, is one of the most beautiful proof
techniques in math. In my experience, among proofs of difficult theorems, proofs by contradiction are the
most easy to understand. The basic idea of them is very simple. Want to prove that something is true? Look
at what would happen if it were false. If you get a nonsensical, contradictory result from assuming its
false, then it must be true.

Continue reading →

Why did Set Theory start with transfinite numbers?

Leave a reply

I was visiting my mom, and discovered that I didn’t leave my set theory book on the train; I left it at her house. So I’ve been happily reunited with my old text, and I’m going to get back to a few more posts about the beautiful world of set theory.

When you talk about set theory, you’re talking about an extremely abstract notion, one which is capable of representing all sorts of structures: topological spaces, categories, geometries, graphs, functions, relations, and more. And yet, almost every description of set theory plunges straight into the cardinal and ordinal numbers. Why? That’s a question that mystified me for quite a long time. Why do we take this beautiful structure, which can do so many things, and immediately jump in to these odd things about infinities?

Continue reading →

Mathematical Constructions and the Abstraction Barrier

79 Replies

There was an interesting discussion about mathematical constructions in the comment thread on my post about the professor who doesn’t like infinity, and I thought it was worth turning it into a post of its own.

In the history of this blog, I’ve often talked about the idea of “building mathematics”. I’ve shown several constructions – most often using something based on Peano arithmetic – but I’ve never really gone into great detail about what it means, and how it works.

I’ve also often said that the underlying theory of most modern math is built using set theory. But what does that really mean? That’s the important question, and the subject of this post.

Continue reading →

Computing Strongly Connected Components

23 Replies

As promised, today I’m going to talk about how to compute the strongly connected components
of a directed graph. I’m going to go through one method, called Kosaraju’s algorithm, which is
the easiest to understand. It’s possible to do better that Kosaraju’s by a factor of 2, using
an algorithm called Tarjan’s algorithm, but Tarjan’s is really just a variation on the theme
of Kosaraju’s.

Continue reading →

Making Graph Algorithms Fast, using Strongly Connected Components

Leave a reply

One of the problems with many of the interesting graph algorithms is that they’re complex. As graphs get large, computations over them can become extremely slow. For example, graph coloring is NP-complete – so the time to run a true optimal graph coloring algorithm on an arbitrary graph grows exponentially in the size of the graph!

So, quite naturally, we look for ways to make it faster. We’ve already talked about using
heuristics to get fast approximations. But what if we really need the true optimum? The other approach to making it faster, when you really want the true optimum, is parallelism: finding some way to subdivide
the problem into smaller pieces which can be executed at the same time. This is obviously a limited
technique – you can’t stop the exponential growth in execution time by adding a specific finite
number of processors. But for particular problems, parallelism can make the difference between
being able to do something fast enough to be useful, and not being able to. For a non-graph
theoretic but compelling example, there’s been work in something called microforecasting, which is precise weather forecasting for extreme small areas. It’s useful for predicting things like severe lightning storms in local areas during events where there are large numbers of people. (For example, it was used at the Atlanta olympics.) Microforecasting inputs a huge amount of information about local conditions – temperature, air pressure, wind direction, wind velocity, humidity, and such, and computes a short-term forecast for that area. Microforecasting is completely useless if it takes longer to compute the forecast than it takes for the actual weather to develop. If you can find a way to split the computation among a hundred processors, and get a forecast in 5 minutes, you’ve got something really useful. If you have to run it on a single processor, and it takes 2 hours – well, by then, any storm
that the forecast predicts is already over.

For graphs, there’s a very natural way of decomposing problems for parallelization. Many complex graphs for real problems can be divided into a set of subgraphs, which can be handled in parallel. In
fact, this can happen on multiple levels: graphs can be divided into subgraphs, which can be divided
into further subgraphs. But for now, we’ll mainly focus on doing it once – one decomposition of
the graph into subgraphs for parallelization.

Continue reading →

Colored Petri Nets

8 Replies

Colored Petri Nets
The big step in Petri nets – the one that really takes them from a theoretical toy to a
serious tool used by protocol developers – is the extension to colored Petri nets (CPNs). Calling them “colored” is a bit of a misnomer; the original idea was to assign colors to tokens, and allow color-based expressions on the elements of the net. But study of analysis models quickly showed
that you could go much further than that without losing the basic analyzability properties
that are so valuable. In the full development of CPNs, you can associate essentially arbitrary
collections of data with Petri net tokens, so long as you use a strong type system, and keep
appropriate restrictions on the expressions used in the net. The colors thus become
data types, describing the types of data that can be carried by tokens, and the kinds of tokens that
can located in a place in the net.

So that’s the fundamental idea of CPNs: tokens have types, and each token type has some data value associated with it. Below the fold, we’ll look at how we do that,
and what it means.

Continue reading →

Counted Petri Nets, and Useless Protocol Specification Tools

Leave a reply

There’s one variant of Petri nets, called counted Petri nets, which I’m fond of for personal reasons. As Petri net variants go, it’s a sort of sloppy but simple one, but as I said, I’m fond of it.

As a warning, there’s a bit of a diatribe beneath the fold, as I explain why I know about this obscure, strange Petri net variant.

Continue reading →