Not quite Basics: The Logician's Idea of Calculus

In yesterdays basics post, I alluded to the second kind of calculus - the thing that computer scientists like me call a calculus. Multiple people have asked me to explain what our kind of calculus is.

In the worlds of computer science and logic, calculus isn't a particular thing:
it's a kind of thing. A calculus is a sort of a logician's automaton: a purely
symbolic system where there is a set of rules about how to perform transformations of
any value string of symbols. The classic example is href="http://scienceblogs.com/goodmath/goodmath/lambda_calculus/">lambda calculus,
which I've written about before, but there are numerous other calculi.

For a few examples: here are two calculi designed by one of my favorite researchers, Robin Milner, for describing distributed computation with communication: the calculus of communicating systems (CCS), and the π calculus. Another great programming language researcher, Luca Cardelli, designed a calculus for describing object-oriented computation. There's another calculus that combines properties of Cardelli's object calculus and π-calculus, called Join calculus. At some point, I'm going to do some writing about π calculus here - I did a lot of π-calculus work for my dissertation, and I think it's remarkably cool.

Just to give you a very brief idea of what I mean by this kind of thing, I'll
give you a quick taste of lambda calculus. To see an explanation of lambda calculus and how it works, you can look here.

Assuming that we handwave a bit to let us use recursion (lambda calculus allows recursion, but it does it by way of a fairly complicated construction called the Y combinator); and also assuming we have Peano arithmetic (so we have numbers, comparison, increment, and decrement) we can write a general addition function as:


Add ≡ λ x y . if (= x 0) y (Add (Dec x) (Inc y))

The way that this would "run" on an example like 2+3 is:

  1. Add 2 3 ≡ if (= 2 0) 3 (Add (Dec 2) (Inc 3)) = (Add 1 4)
  2. Add 1 4 ≡ if (= 1 0) 4 (Add (Dec 1) (Inc 4)) = (Add 0 5)
  3. Add 0 5 ≡ if (= 0 0) 5 (Add (Dec 0) (Inc 5)) = 5

One important thing to understand that sequence is that if is a function with three arguments: a test expression, and expressions for the true and false cases. It's all functions in lambda calculus.

Tags

More like this

I'm on vacation this week, so I'm recycling some posts that I thought were particularly interesting to give you something to read. ------------ In computer science, especially in the field of programming languages, we tend to use one particular calculus a lot: the Lambda calculus. Lambda calculus…
Now that things are settling down a little bit, I wanted to get back to the stuff I was writing about π-calculus. But looking back at what I've already written, I think I did a terrible job of introducing it. So I'm going to start over, and try to be more clear. I'll start with a basic refresher…
Ok. So I'm still tweaking syntax, to try to find a way of writing π-calculus in a way that's easy for me to write in my editor, and for you to read in your browser. Here's the latest version: Sequential Composition: Process1.Process2. Send expressions: !channel(tuple).Process Receive…
Lambda calculus started off with the simple, untyped lambda calculus that we've been talking about so far. But one of the great open questions about lambda calculus was: was it sound? Did it have a valid model? Church found that it was easy to produce some strange and non-sensical expressions using…

I've often wondered what lambda calculus was, so many thanks; on an almost entirely unrelated issue, it once seemed to be the csse that most mathematicians thought of themselves as realists (platonists), even while working formalistically (which would give a special place to the usual calculus, presumably), but I get the impression that most would now class themselves as formalists: is this impression correct?

Another example of Good Math: tuple calculus, one of the alternative foundational descriptions of relational database operations. (Another is relational algebra, which I find more intuitive.)

A calculus and an algebra seem very similar. What's the relation?

I was wondering about that, too.

As far as I can see, they are the very same thing, the only difference being that "algebra" is a precise and universally accepted mathematical notion, around which a particular body of mathematical theory has developed, while "calculus" remains an informal notion, since none of the theory surrounding it has happened to pick it as part of its formal vocabulary. Similar terms were used instead: "algebra" of course, but also "term rewriting system", "grammar", "automaton", and probably more.
So we do have a lot of theory on calculi, it just so happens that none of it has the notion of "a calculus" as a formal element.

So the difference isn't mathematical, but rather, lexicographical in nature.

Just to be sure I fed "logic" and "calculus" to Google and out came an interesting reference: `The Calculus of Logic' by George Boole.

I never read this paper before, but it appears to be the very origin of the "logician's" meaning of calculus, since the main purpose of the paper, as I understand it, is to convince the reader that logical reasoning can be described and studied as calculation, using mathematics very similar to ("traditional") calculus. Its closing paragraph makes this very explicit:

The view which these enquiries present of the nature of language is a very interesting one. They exhibit it not as a mere collection of signs, but as a system of expression, the elements of which are subject to the laws of the thought which they represent. That those laws are as rigorously mathematical as are the laws which govern the purely quantitative conceptions of space and time, of number and magnitude, is a conclusion which I do not hesitate to submit to the exactest scrutiny.

I think Boole's view has been universally accepted among mathematicians, and computer science was built on it. This explains the use of the word calculus to describe lambda calculus, pi calculus, etc. But when I encountered the work of Boole itself, in my first few weeks of computer science, the word "calculus" was never used: his theory is known as Boolean algebra!

Can any calculus be regarded as an algebra?

I think so. To me, as a programmer, an algebra is a set of construction rules for labelled, oriented trees, plus a set of equivalence rules that allow us to rewrite a tree fragment into some other tree fragment. For instance, when I look at the algebra of rational numbers, my trees are all possible expressions that can be built with 0, 1, +, -, *, and /, and the rational numbers themselves are the equivalence classes of those terms under rewriting. For instance, the equivalence class of 1 + (1 + 1) is known as "3".

In fact, I regard this way of viewing algebras as fundamentally superior: it makes metaphysical sense to me, unlike the traditional mathematical view, which regards algebras as describing the structure of "existing" sets that are somehow "out there".

Now all calculi can be described in this way. Lambda calculus expressions, for instance, are also labelled trees; a \lambda is a node with two children, just like +. Unlike +, \lambda isn't completely total, since its first argument must be a variable; so we're dealing with a many-sorted algebra.

The key difference between an algebra and a calculus is that algebras are intertwined with their semantics. An algebra says "there's a set of values, and some set of operations on those variables with some particular set of properties". The algebra, and the ability to perform symbolic operations in it, are inevitably intertwined with the semantics of the operations over the set of values. Without knowing something about the semantics, there's nothing you can do with an algebra. The semantics of the values and operations dictates what you can do in an algebra.

A calculus is more like a logic: it's a symbol system with a set of rules that define what you can do with it. But with a calculus, the operations are defined syntactically - without knowing what you're manipulating, you can do things with a calculus. For a calculus (just like for a logic), there is a model which defines the semantics for the calculus - but the calculus dictates the model.

Personally, I find a calculus to be more like a logicians version of an automaton than an algebra.

I think I see what mean, but I do not see the distinction you make.

There is an ambiguity in the term "semantics" here. On one hand, it refers to how things behave: what we can do with them. Taken that way, I think your statement is incorrect: everything we can do with rational numbers, for instance, is entirely defined by the algebra of rational numbers. Everything we can do with the objects of a particular algebra is defined entirely by the construction rules and equivalence rules defined by that algebra. Calculation with rational numbers is just as syntactical as, say, calculation in lambda calculus.

Logicians have a different view of what semantics is: they think it is about reference. They build formal systems, with formal manipulation rules, but do not study them in isolation; instead, they study their correspondence with some other system. When they get really serious they provide a mathematical description of this second system and its own rules, and then they can formally reason about questions such as whether the first system accurately and completely describes the second (soundness and completeness).

What I don't like about this is the metaphysics, the way logicians talk about it. The terms and the rules of the formal system are called "just syntax" and "meaningless". The correspondence is called an "interpretation" of the formal system. The second system is supposed to be "the real thing out there". The correspondence is said to give the formal system its meaning (semantics).

This often makes perfect sense, e.g. when the second system has many other known or unknown properties and rules and the first is only an abstraction of a tiny aspect of it. But I think it's wrong to be categorical about it, and say that a formal system always acquires its meaning through an interpretation of this kind. In particular, I think it's misleading to apply this to the algebra of rational numbers, or number theory in general. There is no such thing as "the actual rational numbers out there" that supposedly provides the semantics for the algebra of rational numbers. What we do have is real-world situations in which rational numbers can be applied, so whenever we want to apply rational numbers we do establish a correspondence between their algebra and some system in which rational quantities play a role. But that correspondence doesn't define the semantics of rational numbers.

(Sorry to use up so much space. I'm not even sure if discussion of this kind is appropriate here - it's more about terminology than about mathematics itself.)

[Reinier]
The same structure [Algebra] that has the rational numbers as a model, also as, for instance, the rational functions [polynomial dividing polynomial] as a model.

By Anonymous (not verified) on 22 Nov 2007 #permalink