A distilled overview of the Lambda Calculus

Prerequisite Concepts

What is a Calculus?

In this context, forget the branch of mathematics.

A "calculus" refers to:

  a particular method or system of calculation or reasoning.

What is a Lambda?

What is a Lambda?!

Hold that thought.

Formal Systems

Basic arithmetic is a formal system.

Lambda Calculus is a formal system too.

A "formal system" is composed of:

  - An alphabet of valid Symbols
  - Rules for constructing valid statements from the alphabet
  - Rules for how a statement can be modified to make a new one

Arithmetic as a Formal System

Arithmetic is all about Simplification.

The formal system of Arithmetic:

  - Alphabet composed of numbers, operators, parenthesis
  - Statements are any combination of numbers, operators, or balanced parenthesis
  - Statements are "simplified" into new statements

      5 * (2 + 2) / 8
            5 * 4 / 8
               20 / 8
                  2.5

Algebra as a Formal System

Algebra is all about Balance.

The formal system of Algebra:

  - Adds = and variable names to the alphabet
  - Statements take the form:

               EXPR = EXPR

  - Expressions are any valid arithmetical statement
  - Expressions can also contain variable names
  - Statements are "balanced" into new statements to determine the value of a
    particular variable of interest

      2 * x + y * 2 = x + 3 * y
      鈹鈹鈹鈹鈹           鈹
          x + y * 2 = 3 * y
              鈹鈹鈹鈹鈹   鈹鈹鈹鈹鈹
                  x = 1 * y
                      鈹鈹鈹鈹鈹
                  x = y

Lambda Calculus as a Formal System

Lambda Calculus is all about Reduction.

  - Adds 位 and . to the alphabet
  - Statements take the form:

            [位 HEAD . BODY] EXPR

  - HEAD is a list of algebraic variable names
  - BODY and EXPR are algebraic expressions
  - A HEAD . BODY term listing N variables, followed by N EXPR terms can be
  reduced to just the BODY term:

      [位 a b c . a + b * c] (1 + 1) (2 * 10) (100 / 2)
         鈹       鈹           鈹鈹鈹鈹鈹
        [位 b c . (1 + 1) + b * c] (2 * 10) (100 / 2)
           鈹               鈹       鈹鈹鈹鈹鈹鈹
          [位 c . (1 + 1) + (2 * 10) * c] (100 / 2)
             鈹                        鈹   鈹鈹鈹鈹鈹鈹鈹
          [位 (1 + 1) + (2 * 10) * (100 / 2)]
          鈹鈹                               鈹
             (1 + 1) + (2 * 10) * (100 / 2)
                   2 + (2 * 10) * (100 / 2)
                         2 + 20 * (100 / 2)
                         2 + 20 * 50
                             22 * 50
                                1100