# What is the point of calling $\lambda$-calculus an algebra?

What is the difference of calling $\lambda$-calculus an algebra instead of a calculus? I raise this question because I read somewhere the line "$\lambda$-calculus is not a calculus but an algebra" (iirc, attributed to Dana Scott). What is the point? Thanks.

-
Coming from an apprentice of the subject with likely no insight whatsoever: isn't determining whether two lambda-calculus expressions are equivalent undecidable? Does that have any influence on why it wouldn't be considered a "calculus"? Because that's a fundamental question that can't be algorithmically calculated... –  Jeremy Kun Feb 27 '12 at 17:29

A calculus is a system of computation based on the manipulation of symbolic expressions. An algebra is a system of symbolic expressions and relations between them[*]. That is, a calculus is a system for figuring out answers, and an algebra is a way of expressing the relations between terms.

The $\lambda$-calculus is either a calculus or an algebra, depending on whether you want to think of the $\beta$ and $\eta$ rules as oriented reduction rules or unoriented equations. If you think of the rules as being oriented, then you have fixed an evaluation order, and the rules tell you how to take a term and produce a normal form. If you think of the rules as being unoriented, then they give you the equality relation on $\lambda$-terms.

[*] There is also a categorical definition of algebra, which is a formal definition somewhat more restrictive than the informal idea. Loosely speaking, the difference is that the formal definition of algebra encompasses just those systems without variable binding. So SKI combinators form an algebra, but the $\lambda$-calculus doesn't.

-
As mentioned in my comment, the categorical definition of algebras can be shown to encompass structures with binding operations. The main idea is that whereas structures without binders can be represented as algebras on sets, structures with binders can be represented by algebras on -presheafs-. –  cody Jan 31 '12 at 10:19
AFAIK, it's the definition of algebra in universal algebras doesn't allow operations with higher-order signatures (according to John Mitchell's Foundations of Programming Languages). –  Blaisorblade Jun 27 '13 at 23:32

Traditionally, an algebra is a carrier set with operations that satisfy some equations (think "group"). There are many ways in which the notion can be generalized:

• multi-sorted algebras have several carrier sets. An example would be a module $M$ over a ring $R$, where we want to consider the whole thing as a single algebra. Another, rather silly example, is a directed graph, which has two carrier sets, $E$ of edges and $V$ of vertices, and two operations, source $s : E \to V$ and target $E \to V$, satisfying no equations.

• more general axioms which are not just equations may be allowed. For example, the axioms for a field are all equations except for $x \neq 0 \implies x \cdot x^{-1} = 1$. Another example is something like an integral domain.

• more general operations may be allowed, in particular ones of infinite arity, or higher-order operations which take functions as arguments. An example of an infinitary operation is the $M$ in midpoint algebras of Martin Escardo and Alex Simpson. If you go far in this direction you arrive at monads.

In this sense the untyped $\lambda$-calculus is an algebra because it is specified in terms of a carrier set with some (higher-order) operations satisfying some equations ($\beta$ and $\eta$).

-

There is a quite precise definition of what an algebra is in category theory: see this article for instance. It took a few years to understand how a structure with bound variables could be understood in the same context as the term algebra structure commonly used in mathematics and computer science, and it turns out that the categorical concept of F-algebras is capable of unifying the two. I am not sure bout the historical aspects of the solution but one possible approach is the presheaf algebras introduced by Fiore, Plotkin and Turi (available here) settled the question and spurred different but similar approaches, see e.g. Hirshowitz et al. and his phd student Julianna Zsido.

Some exiting research remains to be done on how to use the categorical concepts to refactor and deepen our understanding of structures with bound variables, in the hopes of eliminating syntactic "cruft" which usually comprises the most boring chapters of theses on $\lambda$-calculi and related structures.

-
F-algebras usually are free algebras, i.e. don't allow equations; Pierce's category theory intro (from 1992) claims there is no development of equations for F-algebras. I've only read of solutions in the abstract of Chung-Kil (Gil) Hur's PhD thesis, from 2010: "Categorical equational systems: algebraic models and equational reasoning". Is that what I guess, and is it the first treatment o the topic? –  Blaisorblade Jun 27 '13 at 23:37
I don't think there's any reason the F-algebra approach does not apply to theories with equations. The idea is that you can form initial algebras with equations from the free ones (without equations) by "quotienting" by the appropriate theory. I don't know much about Gil's work or what Pierce meant by his remark. –  cody Jun 28 '13 at 0:22
Addendum: after a cursory glance, Gil's work with Marcello Fiore does seem to treat a general notion of equational theories for F-algebras. –  cody Jun 28 '13 at 0:25

While it is true that the notion of "calculus" is less well-defined than the notion of an "algebra", broadly "calculus" generally implies a process of calculation, while algebras have patterns of construction with equational theories.
You could say there is more of a feeling that algebras "already exist" as structures and we are merely uncovering truths about them, rather than using some method to produce new answers that didn't exist before.

If you think about what Scott was trying to accomplish with Scott domains, his statement makes sense: he was trying to find predefined mathematical and algebraic structures that would serve as a fixed semantics for LC. He wanted to do away the feeling that the meaning of a term was whatever happened to come out of a particular process.

You might be interested in a previous answer about a related question: What constitutes denotational semantics?

-

I would be very reluctant to call lambda-calculus an "algebra" for a very simple reason. It is a formal system defined purely using syntax, without any reference to meaning. The equivalences $\beta$ and $\eta$ are at a meta-level, using variables like $M$ and $N$ that range over terms. That is not what algebraists would call an "algebra". On the other hand, logicians have long used the term "calculus" to mean formal systems where rules are expressed at the meta-level.

If Scott ever did call lambda calculus an "algebra" (which I rather doubt), then he would have been making a rather subtle point, viz., that you can think of lambda calculus as having an a priori meaning.

Still he would have a hard time convincing any algebraists of his claim, because he doesn't have equations in lambda calculus, he has equivalences (i.e., at the meta-level). "Combinatory algebra", on the other hand, is perfectly normal.

-

There is no such thing as a calculus, but there is a well-defined mathematical object called algebra, though the word has many uses. However, my guess is that the name was given in the sense of

(...) the abstract study of number systems and operations within them.

since, in $\lambda$-calculus, you define objects (terms, which you may call numbers) and operations within those objects.

-
Look at Neel's answer. –  Dave Clarke Jan 30 '12 at 19:24
Yep. That certainly looks like a definition, but it is not a standard one. I agree with Neel that it can be whatever you want depending on your interpretation of the rules, but that also depends on your definition of "a calculus" and "an algebra", neither of which is standard (apart from the formal object coming from a vector space, which is not the case with $\lambda$-calculus). –  Janoma Jan 30 '12 at 19:41