Functional Language for Untyped Lambda Calculus

Question

Is there an interpreter (or compiler) for untyped lambda calculus? (According to this thread it's possible.) I recognize that it would be of little use as a programming language, particularly if much of the language (such as numerals and boolean operators) were implemented (either by the user or by a library) in the language itself. However, I still think it would be a fun tool useful for learning and exploring the calculus. For this an interpreter would be preferable to a compiler, tho either would work. Does anyone know of such a program?

Answer 1

You can use any untyped language that has lambda abstractions. For example Python or JavaScript. There are two main downsides:

1. These languages don't have lazy evaluation. This means that not all lambda terms will converge, even though they have a normal form. You have to take this into account and modify the task accordingly.
2. You won't see the result as a lambda-term in normal form. You have to know what to expect from the result and use the language to evaluate it to something that can be displayed.

Knowing this, let's make an example in Python: First we create helper functions to convert between numbers and Church numerals:

# Construct Church numeral from an integer
def int2church(n):
    def repeat(f, m, x):
        if (m == 0): return x
        else: return f(repeat(f, m-1, x))
    return lambda f: (lambda x: repeat(f, n, x))

def church2int(l):
    return l(lambda x: x + 1)(0)

now we can define standard operations on numerals:

zero = int2church(0)
one = int2church(1)

pred = lambda n: lambda f: lambda x: n(lambda g: lambda h: h(g(f)))(lambda u: x)(lambda u: u)

mul = lambda m: lambda n: (lambda f: m(n(f)))

expn = lambda n: lambda m: m(n)

tetra = lambda n: lambda m: m(expn(n))(one)

and compute for example 4³:

expn = lambda n: (lambda m: m(n))

a = int2church(4)
b = int2church(3)
print church2int(expn(a)(b))

or tetration:

a = int2church(5)
b = int2church(2)
print church2int(tetra(a)(b))

To be able to express even more interesting stuff, we can define the Y combinator:

y = lambda f: (lambda x: f(lambda v: x(x)(v))) (lambda x: f(lambda v: x(x)(v)))

and compute for example factorials:

true = lambda x: (lambda y: x)
false = lambda x: (lambda y: y)

iszero = lambda n: n(lambda x: false)(true)

fact = y(lambda r: lambda n: iszero(n)(one)(mul(n)(lambda x: r(pred(n))(x))))
print church2int(fact(int2church(6)))

Note that the Y combinator had to be adapted for strict evaluation using η-expansion, as well as the factorial function to avoid infinite recursion due to strict evaluation.

Answer 2

Benjamin Pierce provides implementations of the untyped and simply-typed λ-calculus that accompany his textbook Types and Programming Languages. They are written in OCaml and include example definitions. It shouldn't be difficult to write an interpreter or compiler for simple λ-calculi, however.