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

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.

Answer 2

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 3

Using a few tricks, this is possible to do in almost any functional languages. At least I have seen something like this in Haskell and OCaml. However some times you have to get around restrictions of the type systems. Usually you get the "untyped" feature by implementing it as a unityped system. So each lambda function would have the type

type lambda = lambda -> lambda

In the default setting for example OCaml will not allow such a recursive type, but this can be circumvented for example by defining:

type lambda = L of lambda -> lambda

Answer 4

I'm a teaching assistant for functional programming course. For the pedagogical purpose, we have seen this online lambda calculus reducer as a fun and useful tool to explore the calculus. They also have available source code in SML if you want to play with it.

Answer 5

I wrote one, earlier this year. Here it is.

Answer 6

I created a web hosted interpreter for a lambda calculus based language I call pureƒn in an effort to learn the workings of the Lambda Calculus. It may be useful for people wanting to learn and experience some of the fundamental principles of computer science in an interactive manner with minimal notation complexity.

pureƒn is a programming environment based on the functionality of the Lambda Calculus, but with a simplified notation. pureƒn allows for the definition, application and reduction of functional abstractions. The notation and syntax are minimal yet sufficient to allow the underlying concepts to be easily understood.

The underlying compiler was written in Python and compiles the abstractions into functions that reduce to normal form (if possible) automatically when applied to each other. This means that if you define the S, K and I combinator functions, and then apply them as S K K, the function that gets returned will be the I function, not just a function that behaves like I, meaning that the following would hold true:

>>>S(K)(K) is I
True

Answer 7

Here is one written in Python. It appears to be very immature, but it is an interesting start of implementing one Python. It depends on the module ply.

Here is another one (sort of) for C++—very interesting.

If your main intention is to get some basic automation involved in learning lambda calculus (for example, trying to derive arithmetic operations for yourself) and particular Church numerals and booleans, a primitive but easy-to-implement solution is to limit yourself to a small subset of Python, in which you can define your own Church numerals and operators, and check them by functions which convert them into the regular Python types. A function to do this for Church numerals:

lambda churchnum: churchnum(lambda x: x+1)(0)

And one for Church booleans:

lambda churchbool: churchbool(True)(False)