Stupid Question.

I realize this may be a dumb question... having had some Abstract/Modern Algebra classes, I understand what an Algebra is, but I have never really understood what defines a "Calculus". What's the common thread between Lambda Calculus, Pi-Calculus, and traditional "Calculus"(and all the other calculi...) that merits them being called a calculus?

I realize this may be an obvious thing, but my tendency is to assume that there is some formal definition of Calculus out there which is being used which I am just unaware of. Again, if I'm just being dumb, someone email me and put me out of my misery :)

Comment viewing options

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

A strawman for others to beat upon

I didn't have any relevant classes as well (so the following is a pure speculation), but I think that every calculus defines:
  1. A formal language (a subset of powerset of finite strings over some finite alphabet) - is there any calculus without a syntax?
  2. Inference or rewriting rules, which induce a reduction relationship between terms from the language.

After you have the reduction, you can start proving properties of your calculus, such as confluence or strong normalization, etc.

Now when I've written this, it looks almost as a definition of a "theory". Hmm, someone more educated, what's the difference? Is it that theories are more declarative while calculi more operational?

Another question, how is a calculus different from an abstract machine? Is some calculus an exokernel of every abstract machine? :-)

No authoritative definition I know of...

...but it was an issue I and an MSc student of mine spent a long time wrestling with, which involved some heavy argumentation about what certain calculi can and cannot express. The definition we finally worked out was something like: a calculus is a design pattern for the construction of formal systems. It's a bit different from Andris' definition, but it hadles awkward cases such as using the sequent calculus to handle such different theories as intuitionistic logic and relevance logic.

A framework?

a calculus is a design pattern for the construction of formal systems
I remembered reading some comments about their calculus being a framework for building such and such formal systems. Now, what's the formal difference between a design pattern and a framework? :-)

Can a bit of history help us? Did calculi as we know them appear first in the context of Hilbert's Program?

Though only marginally related, I think this (pseudo)history paper is fun to read (though the calculus it mentions is unrelated at all :-) ).


Yes, I think it gets across the right idea, but there is risk of confusion with the research on logical frameworks, which may be particular formal systems (eg. LF is, modulo a bit of hand-waving, the lambda-Pi calculus). Also frmework suggests everything is properly nailed down, actually there is a bit of fuzz factor involved, since when people present a new calculus, it is generally given by means of a few examples, without sharp criteria delineating what are or are not inference rules.

In brief, pattern is better than framework becuase framework is too informal and too formal.

BTW, good link, and I think the history should cast light on this. I don't have the facts at my fingertips, though.

Mumble, mumble, mumble

I'm pretty sure there is no formal definition for "calculus", nor would I normally attempt one. But, if I were forced to give one, my definition would be close to Andris'. The only addition I would make is that "calculus" connotes a theory (system) that one expects people can work in, or with, over a long period. So, for example, lambda-calculus, pi-calculus and differential calculus are all deep and worthwhile systems, which can serve as a mathematical workspace or an object of serious study.

Frankly, I think cas's definition is too broad.

Mouth full of pebbles?

Why not take them out and try calculating with them?

I was never too clear about what distinguished Codd's relational algebra from his relational calculus. It seems to be a layers of abstraction type of issue: expressions in one can be reduced to expressions in the other, so the upper layer gets to be called a calculus and the lower layer gets to be called an algebra.

Codd's relational algebra from his relational calculus

One primary difference between Codd's relational algebra from his relational calculus is:

* relational algebra is procedural

* relational calculus is declarative

Break down

* relational algebra is procedural
* relational calculus is declarative

I think the procedural/declarative distinction breaks down here.

The relational algebra is more focused on properties that the relational system must have as a whole, whereas the calculus is focused on how to retrieve particular info from the system, i.e. the whole / "answer" distinction of my rule of thumb.

Too broad? Maybe

If this debate goes on, I should dig up the definition we settled on. I should say it's about proof calculus, and here a pretty obvious adequacy definition is: does the definition of proof calculus give a notion of identity on such paradigmatic examples as "sequent calculus" and "calculus of natural deduction" that accords with how experts actually use the terms? I think the Andris definition doesn't.

It's worth pointing out that proof calculus behaves a bit differently in this respect from lambda calculus. But then again, Matt's original (and very far from stupid) question mentioned the differential calculus, which is another kettle of fish entirely.

Definitions, eh? Can't live with them, can't live without them.

Definition sidestepped

I've just checked, and...

The MSc thesis is by Phiniki Stouppa, and is titled The Design of Modal Proof Theories: The Case of S5 [pdf]. It's a really nice introduction to design issues in structural proof theory and the problems that calculi moulded on the sequent calculus have with modal logic, but she was uncomfortable with introducing talk of design patterns into a work on proof theory, so the definition of calculus was left implicit. Which means that this article thread is the first 'publication' of this idea...

Don't forget the Predicate Calculus

Or whatever they call that stuff Prolog is based on.

and propositional...

There's the propositional calculus too, sometimes called sentential calculus.

All these seem to be really framworks, or design patterns, for defining formal systems. A propositional calculus can be defined as a formal systems in various ways; variations in the syntax, proof theory and model theory are common. But all of them are concerned only with atomic sentences (propositions), without predicates or qualifiers.

You have various definitions/variations of "predicate calculus" as well.

Rule of Thumb

In my own "rule of thumb" understanding, the distinction between an algebra and a calculus is the same as the distinction between denotational and operational semantics.

My notion is that algebras (and denotational semantics) are declarative descriptions of a mathematical structure that exists "all at the same time", whereas a calculus (or operational semantics) is a set of rules to be applied in some sequence to find particular "answers".

This is also similar to the distinction between pure FP and procedural programming.

I've found this rule of thumb to work most of the time.

another example...

In this paper, the authors present both an algebra and a calculus for a particular system, demonstrate a translation between them, and then intermix notations freely. It helps to clarify the distinction between a calculus and an algebra, and the usage seems to match Marc's rule of thumb...

(Actually, it's just a really good paper all around, and while the Kleisli Query System has been mentioned here before, I'm not sure whether we've linked this particular paper.)

Suggested variation

I like both the Birkmanis and the Hamann definitions, but here are some quibbles.

One, it is extremely common for the grammars of calculi as presented in papers and such to be ambiguous, requiring that things like precedence and associativity conventions be specified on the side. The fact that we care about this implicit structure suggests that the true objects of interest in the calculus are not strings but some kind of trees. Of course we can say that the set of strings we are really thinking of is an unambiguous encoding of those trees, but I think that unnecessarily complicates the definitions of individual calculi just to slightly simplify the definition of "calculus".

Two, it is also extremely common to consider as primitive not the individual terms of the calculus' syntax but equivalence classes of those terms induced by some very basic but nontrivial notion of syntactic equivalence (e.g., alpha-conversion in lambda-calculus or structural congruence in pi-calculus). Perhaps it's not so common that it must be part of the definition of calculus, but maybe.

Three, I would deemphasize the importance of reduction, confluence and their friends. Some calculi, like the lambda-Pi calculus of LF, can be more difficult to reason about when their equational theories are expressed in terms of reductions than when they are specified in other ways. I don't think it's an essential part of being a calculus that its equational theory, which is symmetric, has to be derived from a notion of reduction, which is directed.

Marc Hamann's definition is nice because it can be glossed as "a calculus is a system for calculating". This applies even to the differential and integral calculi.


If I expected such an interest to the topic, I would be more accurate in my comments.

I agree with the first two of your quibbles. Both the abstract syntax against concrete syntax and the quotient of terms by some equivalence did occur to me after the initial post, so now I would probably say that each calculus has a front-end, and a back-end. The front-end deals with textual legacy (concrete syntax, equivalence classes) and the back-end deals with reduction of purified terms. A tempting analogy at the first sight... The problem being that many calculi require equivalence (heating/cooling) to act interactively with reduction (reaction).

An unrelated question: how many calculi out there do not use induction in their definition?

Equational calculi vs. algebras

Aha, judging by existence of the term "equational calculus", some calculi do not have notion of reduction. Looks remarkably like algebras. Any comments appreciated.

[on edit: also, how are calculi related to equational rewriting?]

Dangerous bend ahead...

There's a trivial rewrite relation you can obtain from any equational theory: A ---> B just in case A=B. So equational theories and rewrite theories would at first glance appear to have the same theory...

...but note that rewrite theories tend to assume a whole range of relations being given for each rewrite relation: single step rewrite, reflexive-transitive closure, reduces in m...n steps, etc., and in first-order logic, in general, not each of these can be used to define the others. So rewrite calculi are a sort of finer-grained tool.

As for how are calculi related to equational rewriting?, I'm working on my grand unified set of definitions of calculi, algebras and theories that will give everyone a peg to hang their favourite definition on...


I'm wondering if Andris' definition can, after all, be reconciled with mine.

Suppose we say that a proof calculus is a calculus whose pebbles are other calculi, namely logical systems that allow us to manipulate logical consequence relations. A proof calculus can be a sort of pattern, then it is like the differential calculus before Cauchy introduced his underpinnings; or it can be fully rigorous, in which case it is like the integral calculus after Lebesgue.

Mathworld definition

Although it's unlikely to resolve anything, Mathworld's definition of calculus is:

In general, "a" calculus is an abstract theory developed in a purely formal way.

Lots of variation in usage

I think different people use these and a few related terms in a fairly loose, context-dependent way.

For example, I've heard people use the term "algebraic" to stress the fact that a system lacks an internal notion of variable binding (e.g., "combinatory algebra" versus "lambda calculus"). On the other hand most people would speak of propositional and (first-order) predicate calculi in the same breath, in a logical context, even though the former has no quantifiers and the latter does.

Other times I've seen people use "algebraic" in relation to equational proof (versus other, more general types of proof structures).

Dana Scott once appealed to the notion of limits in the semantics of lambda calculus as being crucial for justifying the term "calculus", but clearly limits are not necessary for semantics of most logical calculi.

So, I'm not sure if there is really a standard usage to be unearthed here, though I'd be quick to admit this might just be my own limited understanding.

The paper of Scott's in question, by the way, is a great survey of issues/features/properties in lambda and related calculi, albeit somewhat out of date. I think it is either "Lambda calculus - some models, some philosophy" from The Kleene Symposium (North-Holland, 1980) or "Some philosophical issues concerning theories of combinators" from Lambda Calculus and Computer Science Theory (Springer LNCS #37, 1975). I think it's more likely the former, but I suspect both would be enjoyed by anyone interested in either :) .

(If I can find the copy I have buried somewhere in my office, I'll re-post with greater conviction. Unfortunately, it's not the sort of thing one is likely to find on the web, as it was type-written, the old-fashioned way, and is probably tied up by copyright laws in any case.)


Are these papers available online by any chance?

Re: papers

No, I couldn't find them on-line: I think the technology used in their production and their original method of publication make it unlikely they'd be available that way. Good university libraries should have the original omnibus volumes; lesser ones could probably get them via inter-library loan. Ironically, I doubt either volume is still available from the publisher.

If I find my own copies, I could try to get a next-gen copy to you by p-mail or e-mail, but I'm loathe to promise anything to a whole community in a public forum.


Sometimes some good soul manages to scan interesting papers and put them online (as course readings, for example).

Anyway, if youmanage to find your copies, let me know...

Available online

An awful lot of Springer's content is now online, if not publically available. The Scott paper is at

What Scott actually said

OK, here is the comment of Scott's I recalled from the paper (it was the paper entitled "Some philosophical issues concerning theories of combinators", in fact):

Recursive definitions must always be joined with inductive proofs. It is just these natural proof methods that are usually missing from ordinary combinatory algebra. (The same could be said about the theory of URS.) It does not really seem right to call lambda-calculus really a calculus if the induction rule (and some theory of limits) is missing. As far as it goes, lambda-algebra is fine, but it does not go far enough.

There are other relevant comments in the paper: I'll mail a scanned version to Ehud and Matt, but I'd like to get permission from Dana Scott before I make it publicly available.

Cocalculi wanted

Recursive definitions must always be joined with inductive proofs.
Ah, so my seemingly unrelated question about induction managed to guess two words from this phrase :-)

On a serious side - if a calculus uses (only) coinduction as its main principle, is it a cocalculus then? And if both - is it a bicalculus? Any examples of such calculi?

According to Curry...

This is from "Foundations of Mathematical Logic" by Haskell B. Curry (sec. 4A1):

The term 'algebra' is used in this book as a name for a system with free variables but no bound variables. Thus the system of Example 5 (Sec. 2C3) is an algebra and is aptly called propositional algebra. In contradistinction the term 'calculus' will, as a rule, be used to describe a system with bound variables, so that it is suitable to speak of a calculus of lambda conversion, a predicate calculus, etc. These terms agree with ordinary mathematical usage, where the distinguishing characteristic of the infinitesimal calculus, as opposed to elementary algebra, is the presence of bound variables in the former1

And in the footnote:

1. Systems like combinatory logic which contain no variables do not come under either term.

Note that the Example 5 he cites is really what is now commonly called "propositional calculus" or "sentential calculus", but he uses the term "propositional algebra", in line with his definition for algebra vs. calculus.

What is Calculi

The term calculus is used mainly for systems where the notation involved is essentially equivalent to a programming language, and the sentences demonstrated are typically equations asserting the claim that two expressions evaluate to the same value.
Roger Bishop Jones

Side note: "Pre-calculus"

Not sure about the EU, but here in the US high school students take a calculus prerequisite called "Pre-calculus". While calculus is not so hard to define, pre-calculus is the mother of all ambiguities. In truth, pre-calculus means nothing other than "stuff we can't fit in the Algebra curriculum before Calculus, but you need to know before you can seriously understand Newton's differential calculus".

Level of concern?

(Trivial aside: The term calculus comes from the diminuitive form of Latin calx (stone). I've usually seen the connection made via the pebbles used in abacus-style calculation on a table.)

This is probably too simplistic, but I'd like to suggest a useful progression in the style of calculation from arithmetic to algebra to calculus, as both practiced and taught:

In an arithmetic, the focus is on the concrete values. One learns, e.g. the addition and multiplication tables for integers and the "truth tables" for standard operations on boolean values of true and false. One's calculations are in terms of completely specified, concrete cases.
Attention shifts from values to operations, and variables appear. The variables may have implicit universal quantification in expressions such as
a × (b + c) = (a × b) + (a × c)
p ∩ (q ∪ r) = (p ∪ q) ∩ (a ∪ r)
or implicite existential quantification in expressions such as
x = 6 - 3x
but the focus is on the properties and interactions of the operators. "Abstract algebra" is introduced a purely focused on defining systems by properties of operators (either without, or prior to, the introduction of concrete cases that satisfy those properties). One's calculations consist of manipulating expressions, reducing more complex tasks to simpler (directly solvable) tasks by using these properties.
Focus shifts again, this time from learning and applying "laws" (associativity, symmetry, etc.) to the process of building successive abstractions. One perceives a pattern, formally states and proves it, and proceeds to construct successive abstractions on prior ones, now working at the level of entire classes of calculations with some common feature. One's calculations often consist of producing new laws or relating classes of problems in previously-unrecognized ways.
There aren't the kinds of hard boundaries that this (over-)simplified view seems to imply, but there are progressive shifts of concern from concrete to conceptual levels.