Lambda Calculator

Lambda Calculator is a JavaScript-based engine for the lambda calculus invented by Alonzo Church. It allows the user to enter a lambda expression and see the sequence of reductions taken by the engine as it reduces the expression to normal form. The program allows a variety of customization options, including choices between the pure calculus and a simple applied calculus and between eager and lazy evaluation. It is a useful tool for learning and experimenting with the lambda calculus.

Lambda Calculator (© 2012) is by Carl Burch, a computer science professor at Hendrix College. [personal page] The “official” page for the Web application is www.cburch.com/lambda/. The source code is available at www.cburch.com/lambda/source/ and is released under the terms of Mozilla Public License 2.0.

Icons are from the Oxygen icon theme (oxygen-icons.org) and are available under the Creative Commons Attribution-ShareAlike 3.0 License or the GNU Library General Public License.

Despite its name, “the lambda calculus” has nothing to do with the calculus you may have studies involving differentials and integrals. In fact, it is a very basic system of mathematics.

It starts with some new notation to talk about a function. For example, consider the function that takes a number as a parameter and produces the number's square as its result. Traditionally, we would notate this as the function “f(x) = x²”; but in the lambda calculus we instead describe it as “λx.x²”.

Notice that the lambda calculus doesn't involve giving the function a name. You can see the λ symbol in it (the Greek letter lambda), but that isn't a name: It's simply notation to indicate that we're beginning to describe a function. The choice of x is arbitrary; “λq.q²” describes the exact same function.

We can build a larger expression using function application. In traditional mathematics, we'd write “f(5)” to indicate that we are evaluating f for when its parameter is 5. In lambda calculus's notation, parentheses for parameters are optional, but we'll use parentheses to indicate the extent of a function's description. We would instead write:

Given this basic expression, we can reduce it. by simply passing the parameter into the function. This operation of substituting a value for a parameter name (x in this example) is technically called a beta reduction.

Of course, from here we can apply basic mathematics to conclude that “(λx.x²) 5” reduces to 25.

Let's look at a more complex example. In this example, we're working with two different functions, where the parameter to the first function is computed by passing parameter into the second function. Since there are two functions involved here, we'll end up performing two different beta reductions (in the first step and the third step).

(λy.4 × y) ((λz.z² + 2 × z) 5)
⇒	(λy.4 × y) (5² + 2 × 5)
⇒	(λy.4 × y) 35
⇒	4 × 35
⇒	140

Function application is left-associative. Suppose we write the following instead (just omitting one set of parentheses).

Here we have three pieces separated by spaces: The y-parameter function, then a z-parameter function, then the number 5. This actually indicates that we should apply the z-parameter function into the y-parameter function first, and we should pass 5 into the result. We can go ahead with the first beta reduction to arrive at the following.

In the lambda calculus, this is nonsensical: We wouldn't talk about multiplying a number (4) by a function. But the lambda calculus is meant to be as simple as possible. It simply dictates the rules of reducing an expression, even if in this case the rule says to reduce to irreducible nonsense.

Of course, sometimes we actually want this behavior. Consider the following sequence of reductions.

(λf.[λa.f (f a)]) (λb.b²) 5
⇒	[λa.(λb.b²) ((λb.b²) a)] 5
⇒	(λb.b²) ((λb.b²) 5)
⇒	(λb.b²) (5²)
⇒	(λb.b²) 25
⇒	25²
⇒	625

Here our first step was to substitute a lambda expression for the letter f. That produced another function taking a parameter named a, which we could accommodate by substituting in 5. There are two more beta reductions before we arrive at the final result of 625.

This Web app's job is simply to reduce an expression you type until it reaches a form that can be reduced no further. To enter an expression, type it into the text field near the page's top and then either press the Enter key or click the checkmark . The Web app will show the outcome of the computation below.

So what can you type into the text field? In the simplest case, you can simply enter an arithmetic expression. But the Web app always expects you to express expressions in prefix notation: Rather than write an arithmetic operator between its two parameters, you will write the arithmetic operator first followed by its two parameters. For example, to compute 6 × 9, you'd type “* 6 9”. And to compute 6 × 9 −12, you'd type “- (* 6 9) 12”.

Of course, the Web app can also handle functions written using lambda notation. Suppose we want to compute the value of the following.

Since most keyboards aren't outfitted with a lambda key, we'll instead use backslashes.

Sometimes expressions become difficult to read due to the many parentheses. Feel free to use matched set of brackets ([ and ]) or braces ({ and }).

You always need spaces or parentheses to indicate function application; when symbols are mashed together (as in *4y), the Web app reads them together as a single symbol.

With the applied lambda calculus (the default), several symbols have a special meaning: For instance, any sequence of only digits is understood to represent the corresponding integer, even if it has a negative sign in front. We also have the following operators:

+, -, *, /	given two integers, apply the arithmetic operation to them
=, /=, <, >, <=, >=	given two integers, apply the comparison to arrive at the identifier true or false
if	given three values of which the first is either true or false, return the second value if the first is true and the third if the first is false

You can define symbols to correspond to expressions. For example, suppose we want to define the symbol sq to stand for the function λz.z². To do this, we'd first enter the expression “\z.* z z” into the main text field and press Enter. Below its reduction, you will see a text field with an “add to dictionary” icon . Type the symbol name “sq” into the field and either press enter or click the icon.

Now you can freely use this symbol in other expressions, and it will always translate into the expression from the dictionary. For example, you could enter “sq 6”, and it would be reduced to 36.

Ways to edit and view the dictionary:

• To redefine a symbol to stand for another expression: Simply re-add the same symbol into the dictionary; the previous definition will be overwritten.

• To view all definitions in the current dictionary: Select the dictionary icon .

• To delete a definition: While viewing the dictionary, select the definition to bring up a delete icon , and then select the delete icon.

• To export the dictionary: While viewing the dictionary, select the “Show Text” button. A text area appears summarizing all definitions in ASCII form.

Options are available through selecting the wrench icon . They are divided into two categories, “Engine” and “Display”

Engine

Maximum Reductions

This is the maximum number of reductions that will be performed. Some expressions, such as “(λx.x x) (λx.x x)”, will never attain normal form, so we need some sort of limit to avoid an infinite loop. Moreover, some expressions expand so large after several reductions that they need to be terminated to avoid taking an inordinate amount of time.

Evaluation Order

Configures the rule used to choose which reductions to perform. The most intuitive is “eager evaluation”, in which parameters are always evaluated before using them to evaluate a function's result. In the following example (which uses infix operators for clarity), we begin by computing the parameter of 9 before we give the value into the y-parameter function.

(λy.y × y) ((λz.z + 5) 4)
⇒	(λy.y × y) (4 + 5)
⇒	(λy.y × y) 9
⇒	9 × 9
⇒	81

In “normal evaluation”, we always pass expressions as parameters without any attempt to reduce them; we only reduce them later, as needed. Starting from the same point as above, the first step is to substitute for y, and only later do we find that the expression passed for y reduces to 9.

(λy.y × y) ((λz.z + 5) 4)
⇒	((λz.z + 5) 4) × ((λz.z + 5) 4)
⇒	(4 + 5) × ((λz.z + 5) 4)
⇒	9 × ((λz.z + 5) 4)
⇒	9 × (4 + 5)
⇒	9 × 9
⇒	81

The advantage of normal evaluation is that a parameter is never computed if it happens that the function never uses it. However, it has the disadvantage that parameters are re-computed each time that the function needs it; in the above example, we perform the same addition twice in the course of the computation, and so the computation takes longer.

In “lazy evaluation”, we track repetitions of a parameter; when we reduce one, we track all others. This allows each parameter to be computed just once — or not at all if the function happens never to use the parameter.

(λy.y × y) ((λz.+ z 5) 4)
⇒	((λz.z + 5) 4) × ((λz.z + 5) 4)
⇒	(4 + 5) × (4 + 5)
⇒	9 × 9
⇒	81

The default is “lazy evaluation”, since it arrives at its conclusion with the fewest reductions.

Calculus Type

If “applied calculus” is selected, the calculator will perform basic arithmetic and comparisons, including the following:

+, -, *, /	given two integers, applies the arithmetic operation to them
=, /=, <, >, <=, >=	given two integers, applies the comparison to arrive at the identifier true or false
if	given three values of which the first is either true or false, return the second value if the first is true and the third if the first is false

However, the lambda calculus can be used with no such primitives. This is called “the pure lambda calculus”. If this is selected, there are no symbols; the only thing the calculator will do is to apply beta and eta reductions.

You can also select “pure calculus with numerals”. This defines the nonnegative integers to correspond to particular lambda expressions as suggested by Alonzo Church:

0:	λs.λz.z
1:	λs.λz.s z
2:	λs.λz.s (s z)
3:	λs.λz.s (s (s z))
(and so on)

Use Eta Reductions

An eta reduction allows expressions of the form “λx.??? x” to be reduced simply to ??? when the expression ??? has no occurrences of x. Some do not like this type of reduction, so you can disable it by unchecking this option.

Display

Substitute Symbols

If checked, when displaying lambda expressions it does an exhaustive search for opportunities to replace equivalent subexpressions in the dictionary with corresponding symbols; of course, it cannot determine the suitability of these replacements. If unchecked, the full lambda expression is always displayed with no such substitutions. Of course, it is faster not to search for dictionary subexpressions, but the lambda expressions are usually harder to interpret.

Show Intermediate Steps

If checked, the result of each individual reduction is stored and you have the option of viewing intermediate steps.

Vary Parentheses

If checked, displayed expressions will occasionally include matched sets of square brackets or curly braces in place of parentheses to help with identifying pairs. If unchecked, only parentheses are used.

Maximum Display Width

For expressions that expand to be longer than indicated in this setting, an ellipsis (…) is included.