Lambda the Ultimate

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? :-)

...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.

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.

Or whatever they call that stuff Prolog is based on.

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.

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.

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.

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.

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.)

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 former¹

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.

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

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".

(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:

Arithmetic

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.

Algebra

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)

or

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.

Calculus

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.