ULC

Untyped Lambda Calculus

Haskell implementation on Alonzo Church's untyped lambda calculus. It's a Turing Complete model of computation.

This calculus is considered the canonical hello world of functional programming languages.

Prerequisites

You need Haskell, this compiles with GHC 8.2.2 at least (Stack resolver: lts-11.0).

Optional: If you want to run the tests for this module, you'll need QuickCheck.

To Build & Run

You can use cabal to build and run this, see this README, alternatively you can use vanilla ghc to build:

To compile and run do: ghc -O2 -o ulc Main then run ./ulc

Alternatively to use the GHCi Interpreter do: ghci Main then type main

In either case you get something like the following:

Welcome to the Untyped λ-calculus REPL
Type some terms or press Enter to leave.
>

Note: When run in GHCi, you don't have the luxury of escaped characters, backspace, delete etc... Compile it using GHC if you need this.

Examples

Where you can then have some fun, try these examples:

• x
• \x.x

The parser is also smart enough to recognise λ, so you can copy and paste from the output:

Welcome to the Untyped λ-calculus REPL
Type some terms or press Enter to leave.
>   x
=   x
>   \x.x
=   λx.x
>   λx.x
=   λx.x

> denotes the REPL waiting for input, = means no reductions occurred (it's the same term), ~> denotes one reduction, and ~>* denotes 0 or more reductions (although in practice this is 1 or more due to =).

There is also a reduction tracer, which should print each reduction step. prefix any term with :reductions in order to see the reductions:

>   :reductions (\x.x) (\y.y) z
~>  (λy.y) z
~>  z

Note: if you provide a non-normalizing term, reductions will not terminate. Use STLC for termination guarantees.

You can save variables for the life of the program with a :let expression. Any time a saved variable appears in a term, it will be substituted for the saved term:

>   :let x = y
saved x = y
>   x
=   y
>   \y.x
=   λz.y

You can read and run a file of commands by prefixing the filepath with :load. This will behave as if each non-empty line of the file were entered into the REPL manually. Terms previously added to the environment via :let commands will be in scope for later commands, so this can be used for building a library of term definitions. For example, if the file bool.ulc contains the following:

:let true  = \t.\f.t
:let false = \t.\f.f

:let not = \b.b false true
:let and = \a.\b.a b false
:let or  = \a.\b.a true b

We can import these definitions in the REPL:

>   :load bool.ulc
saved true = λt.λf.t
saved false = λt.λf.f
saved not = λb.b (λt.λf.f) (λt.λf.t)
saved and = λa.λb.a b (λt.λf.f)
saved or = λa.λb.a (λt.λf.t) b
>   not true
~>* λt.λf.f

Note: We do capture avoiding substitution if a bound variable is the same as one we are substituting in. We rename the bound term to a new variable.

Syntax

We base the language on the BNF for the untyped calculus:

However we adopt the standard bracketing conventions to eliminate ambiguity in the parser. Concretely, the parser implements the non-ambiguous grammar as follows:

Some notes about the syntax:

• The above syntax only covers the core calculus, and not the repl extensions (such as :let bindings above). The extensions are simply added on in the repl.
• Variables are strings (excluding numbers), as this is isomorphic to a whiteboard treatment and hence the most familiar.
• Nested terms may not require brackets: \x.x x and follows the convention of abstractions being left associative, application being right associative, and application having higher precedence than abstraction.
• Whitespace does not matter \x.(x x), except in between application where a minimum of one space is needed.
• Non-terminating terms may be interrupted with Ctrl+C or whatever your machine uses to interrupt computations.
• This grammar left-recursive and non-ambiguous.

Semantics

The semantics implements beta-reduction on terms and alpha-equivalence as the Eq instance of Term:

• This implementation follows a small-step operational semantics and Berendregt's variable convention (see substitution in ULC.hs).
• Reductions include the one-step reduction (see reduce1 in ULC.hs), the many-step reduction (see reduce in ULC.hs).

Other Implementation Details

• ULC.hs contains the Haskell implementation of the calculus, including substitution, reduction, and other useful things.
• Parser.hs contains the monadic parser combinators needed to parse input strings into term ASTs for the calculus. It follows the grammar above.
• Repl.hs contains a simple read-eval-print loop which hooks into main, and into the parser. It uses Haskeline to provide a line-editing interface, input history, and tab-completion of named terms saved in the environment.
• Main.hs is needed for GHC to compile without any flags, it also invokes the repl.
• Tests.hs is the test suite. We run have unit tests for terms in the language. QuickCheck is used to generate arbitrary trees and test they are parsed and printed correctly. Load the module and run the tests with runTests.
• examples.ulc, bool.ulc contain common examples in the untyped calculus, you can load and use them following the :load example above.

For contributions, see the project to-do list, Contributions, and submit a PR with something you think it needs.

Work initially documented here.