Lambda Calculator

Version 1.0

last revision: 2011-11-19

Bruce Ediger

Bruce Ediger's web pages



Table of contents

  1. Introduction
  2. Starting
  3. Using
  4. Downloads
  5. Building and Installing

Introduction

This document describes how to download or build, then use lc v1.0, yet another lambda calculator.

lc interprets a programming language with similarities to various untyped lambda calculus formal systems. It doesn't exactly interpret any "untyped lambda calculus" in that it runs on computers with finite CPU speed and a finite memory. Most or all formal systems fail to take limits into account.

lc performs normal-order (leftmost-outermoust) Beta and Eta reductions. The user can turn off Eta reductions, but Beta reductions always remain in effect.

lc allows the user to create abbreviations, and simple parameterized abbreviations. Abbreviations allow the user to reference possibly very complex terms with a single identifier. Parameterized abbreviations can be used to facilitate use of terms with repetitive structure, like Church Numerals.

Starting

lc is a command line program. You invoke it by typing in its name ("lc") and possibly some flags and options.

Command Line Options

-L filenameRead and intrepret filename before accepting interactive input.
-pDo not print a prompt before accepting input.

lc uses "LC>" as its command prompt. when the user hits return, lc does Beta reduction, and possibly Eta reduction, until it reaches a normal form. It prints the normal form, then waits for more input.

lc reads from stdin and writes output to stdout, so you might use it as part of a pipeline, or with input or output redirection.

The -L option with associated filenames can appear more than once on the command line. lc will read and evaluate the files in the order they appear on the command line.

Using the interpreter

At the LC> prompt, the user can type a lambda calculus term, or an interpreter command.

To quit, the user must cause an end-of-file condition (usually control-D from the keyboard) or send an interrupt signal (usually control-C from the keyboard).

The user can interrupt a long-running reduction with a keyboard interrupt (usually control-C), which will return to the LC> prompt. Such an interrupt probably causes a memory leak. At exit lc notifies the user if it detected any memory leaks.

Examples

Lambda Calculus Terms

A term (to lc) consists of a variable, an abstraction, or an application of one sub-term to another.

Identifiers

Any C- or Java-format identifier can serve as an lc identifier. That means that identifiers take the form of a string beginning with an upper or lowercase letter, followed by zero or more letters, digits or underscores.

Variables

Variables, free or bound, have identifiers as names. lc will rename bound variables to prevent "variable capture". For instance, evaluating (%x.%y.y x) y results in %a.a y, not %y.y y. The bound variable "y" in the original term gets renamed to "a" in the final normal form.

Abstractions

An abstraction follows the traditional lambda calculus pattern: λx.body. The "λx" part denotes the beginning of the abstraction, and the name of the dummy variable that might appear in the body of the abstraction. The body must constitute a term. Any legal-format variable can occur as the bound variable in an abstraction.

Any of the ASCII characters $, %, \ or ^ (dollar sign, percent, backslash, caret) can be used as the "λ" character in an abstraction. You can't use a UTF-8 λ, as this program only understands ASCII.

Either the ASCII character . (period or full stop), or the string -> can denote where the binding site stops, and where the body begins.

lc supports multi-variable abstraction notation. In lambda calculus literature, multi-variable abstractions often get written like this: λxyz.x z y lc interprets the xyz part as a single bound variable named xyz, so the user separates multiple variables with whitespace: \x y z.x z y. The user can also write nested abstractions: \x.\y\.z.x z y.

Example Abstractions
^x.x (x x)
%p q r.p r (q r)
\x.\y->x (x (x (x y)))
$x y z.x (y z)

Applications

Application occurs by creating input with two terms side by side: X Y. Terms associate to the left, so X Y Z gets evaluated as ((X Y) Z). You have to explicitly parenthesize terms to get association-to-the-right: X (Y Z).

The body of an abstraction extends as far as possible. To apply an abstraction to a second term, the user must parenthesize:

(\x y z. x (y z)) A B C

Without parenthesizing the abstraction, \x y z. x (y z) A B C constitutes a single abstraction with a six-term sized body.

Interpreter Commands

Reduction Control and Display

You must double-quote file names containing any characters that an lc identifier can't contain. That means full or partially qualifed path names (they contain slash characters) or any file names with whitespace in them.

You can check the state of any of these commands by typing them in without "on" or "off" at the LC> prompt.

Abbreviations

define or def stores a copy of the term without performing any reductions. Each time an identifier used in a previous abbreviation appears, lc inserts a copy of the term so abbreviated.

The special token $$ represents the results of the last successful reduction. $$ changes whenever lc calculates a normal form. $$ takes on the value of that new normal form. The user can insert the last normal form calculated by inserting $$ one or more times in the next expression typed in.

The identifier of an abbreviation gets its term substituted in its place, as if surrounded by parentheses. For example:

LC> def abbrev1 (\x.\y.\z.x (y z))
LC> A abbrev1 C
A ((\x.\y.\z.x (y z)) C

Abstractions can "capture" identifiers in the abbreviation that lexically match the bound variable:

LC> def X3 x x x
LC> (\x.X3) A
A A A
LC>

Parameterized Abbreviations

Marked parts of term abbreviated by identifier get expanded. When the interpreter sees a use of an abbreviation like identifier{N}, it expands the marked terms N times. The number N has to be greater than zero. This feature can be used to make Church numerals more convenient.

LC> def C0 \f n.n
LC> def C  \f n.*f n
LC> print C{2}
%f.%n.f (f n)
LC>

Note that the Church Numeral for zero is special: you can't define it using parameterized abbreviations. This seems consistent with the inductive definition of numbers in systems like Peano Arithmetic.

You can create simple or complex parameterized abbreviations:

LC> def X \x.*x
LC> X{4}
%x.x x x x
LC> def XY \x y.*x (x *y)
LC> XY{3}
%x.%y.x (x (x (x (y y y))))

Examining Terms

None of these commands produce terms, just output on stdout.

Operations on Terms

godelize makes a godelization of a term by Torben Mogensen's "higher order syntax" method. The godelization is in Beta normal form, even if the original term is not.

This form of godelization comes from:
Efficient Self-Interpretation in Lambda Calculus, by Torben Mogensen.

normalize causes an out-of-normal-order reductions on the term it applies to. Judicious use of normalize can be used to compare normal forms, or it can be used to store an abbreviation of a normal form.

Both of these operations produce terms. They can appear in the definition of an abbreviation, or in the midst of a more complicated term.

Comparing Terms

Lexical equivalence ("==") requires exact string-matching between all variables, bound or free. Alpha equivalence ("=") requires string-matches for all free variables, and identical appearances of bound variables and their binding sites.

lc does not perform any reductions on either side of "=" or "==". The user can use normalize on either or both sides of a comparison to compare beta normal forms.

Neither comparison produces a term, just output on stdout indicating equivalence or non-equivalence.

Downloads

Building and Installing

lc compiles and runs under Linux, and probably Solaris and most BSD operating systems. I wrote it in the strictest ANSI-C I could, with the exception of some signals it handles.

I did not use GNU "autoconf" tools for this project, as I wanted to use alternative C compilers, and lexer and compiler-compiler (lex, flex, yacc, bison, byacc) alternatives, and with Diet libc. All tests pass under every combination that I tried.

Use one of these commands:

make gnu GNU-named tools. Works for most or all linux distros.
make cc Traditional unix names for tools. Use for Solaris and *BSD
make pcc Compile with the re-invigorated PCC C compiler
make lcc Compile using the lcc C compiler.
make tcc Compile using the tcc C compiler.
make clang Compile with the LLVM C-language front end, Clang

This should result in an executable file named "lc". You can use mv or cp to put the file named "lc" in your PATH, or you can execute it in place. lc does not automatically read startup or "rc" files, nor does it assume it runs while residing in a specific directory.