lambda
======

This is an untyped Lambda Calculus interpreter. It reduces lambda expressions.


Introduction
============

From Wikipedia:

    Lambda calculus (also written as λ-calculus) is a formal system in
    mathematical logic and computer science for expressing computation based
    on function abstraction and application using variable binding and
    substitution. First formulated by Alonzo Church to formalize the concept
    of effective computability, lambda calculus found early successes in the
    area of computability theory, such as a negative answer to Hilbert's
    Entscheidungsproblem. Lambda calculus is a conceptually simple universal
    model of computation (Turing showed in 1937 that Turing machines equalled
    the lambda calculus in expressiveness). The name derives from the Greek
    letter lambda (λ) used to denote binding a variable in a function.

From "A Tutorial Introduction to the Lambda Calculus" by Raul Rojas

    The set of lambda expressions, Λ, can be defined inductively:
        1.) If x is a variable, then x ∈  Λ
        2.) If x is a variable and M ∈  Λ, then (λx.M) ∈  Λ
        3.) If M, N ∈  Λ, then (M N) ∈  Λ


How to run the interpreter
==========================

The interpreter was written in ML, and compiles on SML/NJ (the Standard ML of
New Jersey compiler). Thus, in order to run the interpreter, you first have
to acquire SML/NJ. Once you have installed SML/NJ, run it. You should see a
prompt like:

    Standard ML of New Jersey v110.74 [built: Sun Feb  2 20:36:53 2014]
    - 

Your version number may be different - that's ok. Once you're running SML/NJ,
enter the following:

    use "lambda.sml";

This tells SML/NJ to use the function definitions within that file. Note that
if you're running SML/NJ from a different directory than the one that contains
the file "lambda.sml", you'll have to use a path to the file, as in
"../lambda.sml".

After compiling and loading the file "lambda.sml", you can run the interpreter
by entering the following:

    main();

You should then see the interpreter prompt, which is the following string:

    {L}-:

And that's it!


Key features
============

Lazy evalutation
----------------
Arguments are not evaluated until they are needed. This ensures that lambda
expressions like "Lx.a (Lx.(x x) Lx.(x x))" are reduced to "a" as opposed
to causing the interpreter to reduce "(Lx.(x x) Lx.(x x))" ad infinitum.

Files
-----
Lambda expressions can be encapsulated within files and subsequently loaded
into the interpreter by prefixing the file name with the "$" character.
This allows complicated functions to be built incrementally.

Tail recursion
--------------
Recursive functions have been deliberatly written to be tail recursive,
allowing ML to perform last-call optimization.

Step-by-step reduction output
-----------------------------
Setting the boolean field "showRedSteps" (show reduction steps) to true enables
the interpreter to print out the steps of the reduction as each reduction takes
place.


Syntax
======

The syntax for the interpreter can be encapsulated by the following three
rules:

    <expression>  := <var> | <function> | <application>
                   | sc_openPar<expression>sc_closePar

    <function>    := sc_lambda<var>sc_separator<expression>

    <application> := <expression> <expression>

Alone, the rules above are gramatically ambiguous. For example, the expression
"a b c" can be interpreted as both "(a b) c" and "a (b c)". However, lambda
calculus is left associative; expressions of the form "a b c" are always
interpreted as "(a b) c".

In general, all lambda expressions must be delimited by either whitespace or
parentheses. This requirement removes a great deal of ambiguity from the
language, without restricting its expressiveness.

Here are some examples of valid lambda expressions:

    a b
    Lx.x
    Lx.a
    (a b)
    (a)(b)
    (((a)))
    Lx.Ly.x
    Lx.(x x)
    a (b Lx.y)
    (Lx.x Ly.y)
    Lx.(x x Ly.x)

And here are some examples of invalid lambda expressions:

    Lx          - every lambda function must have a separator and a body
    Lx.         - every function must have a body
    Lx.()       - every lambda function must have a non-empty body
    Lxy.x       - every lambda function must be a function of exactly one
                  variable
    Lx.xx       - variables must be delimited by whitespace or parentheses
    Lx.(xx)     - variables must be delimited by whitespace or parentheses
    Lx.xLy.y    - all lambda expressions (functions, variables, applications)
                  must be delimited by whitespace or parentheses


Variable characters
===================

A valid variable is any character in the string "abcdefghijklmnopqrstuvwxyz".
Note that neighboring variable characters are not allowed by the syntax of the
language. Thus, an expression of the form "Lx.xa" should be written as
"Lx.(x a)".


Special characters
==================

By default, the interpreter interprets the following characters as special
characters:

    'L' - sc_lambda, the lambda character. It marks the beginning of lambda
          functions.

    '.' - sc_separator, the separator character. It separates function variables
          from function bodies.

    '(' - sc_openPar, the opening parenthesis character. It marks the beginning
          of a parenthetically enclosed lambda expression.

    ')' - sc_closePar, the closeing parenthesis character. It marks the ending
          of a parenthetically enclosed lambda expression.

    '$' - sc_load, the load character. It marks the beginning of the name of
          a file whose contents should be loaded into the interpreter.

You can easily change these default values, should you so desire. Note that if
these are non-unique, things won't work as expected.


Files and loading
=================

The ability to load input from files is a unique meta-construct of the
interpreter. It's not really part of the language, per se, but it allows us to
do some pretty cool things.

Files can be loaded from both the lambda calculus interpreter as well as within
other files. The syntax for loading a file is as follows:

    $file_name

where file_name is the name of the file you wish to load. Note that if you're in
a different directory than the one which contains, you'll have to give a valid
relative path to the file.

Note that files are not loaded until needed. For example, entering the
expression:

    Lx.a ($OR $T $F)

would cause no files to be loaded, since the lambda expression within the
parentheses need not be evaluated. This behavior is a direct result of the lazy
evaluation of the interpreter.

A good naming convention is to use all uppercase letters for file names - this
ensures that there is as little confusion as possible with variables, which
must be lowercase letters.


/files
======

The subdirectory "/files" contains a few useful definitions and structures. They
are as follows:

    0    - The numerical value zero
    10   - The numerical value ten
    S    - The successor function, adds one to its numerical input
    P    - The predecessor function, subtracts one from its numerical input
    E    - The equality function, returns a boolean value indicating whether or
           not its two numerical inputs are equal in value
    Z    - Returns whether or not its numerical input is zero
    ADD  - Calculates the addition of two numerical inputs
    MUL  - Calculates the product of two numerical inputs

    T    - True
    F    - False
    NOT  - Boolean NOT
    AND  - Boolean AND
    OR   - Boolean OR
    NAND - Boolean NAND
    XOR  - Boolean XOR

    Y    - The recursion function

All of these definitions were taken from the paper "A Tutorial Introduction to
the Lambda Calculus" by Raul Rojas. It is included in the root directory of the
project as "intro.pdf". I would highly encourage trying the exercises at the end
of the paper - they're fun :).