Write an interpreter for the untyped lambda calculus

Question

The challenge is to write an interpreter for the untyped lambda calculus in as few characters as possible. We define the untyped lambda calculus as follows:

Syntax

There are the following three kinds of expressions:

• A lambda expression has the form (λ x. e) where x could be any legal variable name and e any legal expression. Here x is called the parameter and e is called the function body.

  For simplicity's sake we add the further restriction that there must not be a variable with the same name as x currently in scope. A variable starts to be in scope when its name appears between (λ and . and stops to be in scope at the corresponding ).

• Function application has the form (f a) where f and a are legal expressions. Here f is called the function and a is called the argument.
• A variable has the form x where x is a legal variable name.

Semantics

A function is applied by replacing each occurrence of the parameter in the functions body with its argument. More formally an expression of the form ((λ x. e) a), where x is a variable name and e and a are expressions, evaluates (or reduces) to the expression e' where e' is the result of replacing each occurrence of x in e with a.

A normal form is an expression which can not be evaluated further.

The Challenge

Your mission, should you choose to accept it, is to write an interpreter which takes as its input an expression of the untyped lambda calculus containing no free variables and produces as its output the expression's normal form (or an expression alpha-congruent to it). If the expression has no normal form or it is not a valid expression, the behaviour is undefined.

The solution with the smallest number of characters wins.

A couple of notes:

• Input may either be read from stdin or from a filename given as a command line argument (you only need to implement one or the other - not both). Output goes to stdout.
• Alternatively you may define a function which takes the input as a string and returns the output as a string.
• If non-ASCII characters are problematic for you, you may use the backslash (\) character instead of λ.
• We count the number of characters, not bytes, so even if your source file is encoded as unicode λ counts as one character.
• Legal variable names consist of one or more lower case letters, i.e. characters between a and z (no need to support alphanumeric names, upper case letters or non-latin letters - though doing so will not invalidate your solution, of course).
• As far as this challenge is concerned, no parentheses are optional. Each lambda expression and each function application will be surrounded by exactly one pair of parentheses. No variable name will be surrounded by parentheses.
• Syntactic sugar like writing (λ x y. e) for (λ x. (λ y. e)) does not need to be supported.
• If a recursion depth of more than 100 is required to evaluate a function, the behaviour is undefined. That should be more than low enough to be implemented without optimization in all languages and still large enough to be able to execute most expressions.
• You may also assume that spacing will be as in the examples, i.e. no spaces at the beginning and end of the input or before a λ or . and exactly one space after a . and between a function and its argument and after a λ.

Sample Input and Output

• Input: ((λ x. x) (λ y. (λ z. z)))

  Output: (λ y. (λ z. z))

• Input: (λ x. ((λ y. y) x))

  Output: (λ x. x)

• Input: ((λ x. (λ y. x)) (λ a. a))

  Output: (λ y. (λ a. a))

• Input: (((λ x. (λ y. x)) (λ a. a)) (λ b. b))

  Output: (λ a. a)

• Input: ((λ x. (λ y. y)) (λ a. a))

  Output: (λ y. y)

• Input: (((λ x. (λ y. y)) (λ a. a)) (λ b. b))

  Output: (λ b. b)

• Input: ((λx. (x x)) (λx. (x x)))

  Output: anything (This is an example of an expression that has no normal form)

• Input: (((λ x. (λ y. x)) (λ a. a)) ((λx. (x x)) (λx. (x x))))

  Output: (λ a. a) (This is an example of an expression which does not normalize if you evaluate the arguments before the function call, and sadly an example for which my attempted solution fails)

• Input: ((λ a. (λ b. (a (a (a b))))) (λ c. (λ d. (c (c d)))))

  Output: `(λ a. (λ b. (a (a (a (a (a (a (a (a b)))))))))) This computes 2^3 in Church numerals.

Answer 1

Python - 321 320

Here's my (fixed) attempt:

l="("
def S(s):
 if s[0]!=l:return s
 if s[1]=="\\":g=s.find('.');return"(\\ %s. %s)"%(s[3:g],S(s[g+2:-1]))
 i=2;c=s[1]==l
 while c:c+=(s[i]==l)-(s[i]==')');i+=1
 t=S(s[1:i])
 z=s[i+1:-1]
 if l!=t[0]:return"(%s %s)"%(t,S(z))
 g=t.find('.')
 t=S(t[g+2:-1]).replace(t[3:g],z)
 if t!=s:t=S(t)
 return t
print S(raw_input())

Answer 2

Newest:

I've squeezed it down to 644 chars, I factored parts of cEll into cOpy and Par; cached calls to cell and cdr into temporary local variables, and moved those local variables to globals in "terminal" (ie. non-recursive) functions. Also, decimal constants are shorter than character literals and this nasty business ...

atom(x){
    return m[x]>>5==3;
}

... correctly identifies lowercase letters (assuming ASCII), but also accepts any of `{|}~.

Et viola:|

#include<stdio.h>
#include<string.h>
#define X m[x]
#define R return
char*n,*m;int u,w,d;C(x,y){w=n-m;n+=sprintf(n,y?"(%s %s)":"(%s)",&X,m+y)+1;R w;}T(x){R X>>5==3;}
L(x){R X==92;}O(x,j){w=n-m;memcpy(n,&X,j);n+=j;*n++=0;R w;}E(x){X==' '?++x:0;R
X==41?0:L(x)?O(x,4):P(x);}P(x){d=0,w=x;do{X==40?d++:X==41?d--:0;++x;}while(d>0);R
O(w,x-w);}D(x){u=E(x+1);R u?E(x+1+strlen(m+u)):0;}V(x){int a=E(x+1),b=D(x);R
T(x)|T(a)?x:L(a)?C(a,V(b)):L(E(a+1))?V(S(V(b),E(a+3),D(a))):V(C(V(a),b?V(b):0));}S(w,y,x){R
T(x)?(X==m[y]?w:x):C(L(w+1)?E(x+1):S(w,y,E(x+1)),D(x)?S(w,y,D(x)):0);}
Y(char*s){n+=strlen(s=strcpy(n,s))+1;printf("%s\n%s\n\n",s,m+V(s-m));n=m+1;}

char*s[]={
"((\\ a. a) (b))",
"((\\ x. x) (\\ y. (\\ z. z)))",
"(\\ x. ((\\ y. y) x))",
"(((\\ x. (\\ y. x)) (\\ a. a)) (\\ b. b))",
"((\\ x. (\\ y. y)) (\\ a. a))",
"(((\\ x. (\\ y. y)) (\\ a. a)) (\\ b. b))",
"((\\x. (x x)) (\\x. (x x)))",0};
#include<unistd.h>
main(){char**k;n=m=sbrk(4096);*n++=0;for(k=s;*k;k++)Y(*k);R 0;}

Earlier:

Can I get a few votes for effort? I've been working on this day and night for a week. I dug out the original McCarthy paper and was plagued by a bug in the paper itself until I read the appendix to Paul Graham's The Roots of Lisp. I was so distracted that I locked myself out of my house, then completely forgot until arriving home again that night at 12:30 (a little late to be calling the building manager who lives way out in the county), and had to spend the night at my grandmother's (hacking away until my laptop battery was dry).

And after all that, it's not even close to the winning entry!

I'm not sure how to make this any shorter; and I've used all the dirty tricks I can think of! Maybe it can't be done in C.

With some generosity in the counting (the first chunk takes a string and prints out the result), it's 778 770 709 694 chars. But to make it stand-alone, it has to have that sbrk call. And to handle more complicated expressions, it needs the signal handler, too. And of course it cannot be made into a module with any code that tries to use malloc.

So, alas, here it is:

#include<stdio.h>
#include<string.h>
#define K(j) strncpy(n,m+x,j);n+=j;goto N;
#define R return
#define X m[x]
#define L =='\\'
char*m,*n;T(x){R islower(X);}V(x){int a=E(x+1);R
T(x)?x:T(a)?x:m[a]L?C(a,V(D(x))):m[E(a+1)]L?V(S(V(D(x)),E(a+3),D(a))):V(C(V(a),D(x)?V(D(x)):0));}
C(x,y){char*t=n;sprintf(n,y?"(%s %s)":"(%s)",m+x,m+y);n+=strlen(n)+1;R
t-m;}Y(char*s){char*t=strcpy(n,s);n+=strlen(n)+1;printf("%s=>%s\n",s,m+V(t-m));n=m+1;}S(x,y,z){R
T(z)?(m[z]==m[y]?x:z):C(m[z+1]L?E(z+1):S(x,y,E(z+1)),D(z)?S(x,y,D(z)):0);}D(x){R
E(x+1)?E(x+strlen(m+E(x+1))+1):0;}E(x){char*t=n,d=0;if(X==' ')++x;if(T(x)){K(1)}if(X
L){K(4)}do{d=X?(X=='('?d+1:(X==')'?d-1:d)):0;*n++=m[x++];}while(d);N:*n++=0;R t-m;}

char*samp[]={
    "a","a","b","b",
    "((\\ a. a) (b))", "(b)",
    "((\\ x. x) (\\ y. (\\ z. z)))", "(\\ y. (\\ z. z))",
    "(\\ x. ((\\ y. y) x))", "(\\ x. x)",
    "(((\\ x. (\\ y. x)) (\\ a. a)) (\\ b. b))", "(\\ a. a)",
    "((\\ x. (\\ y. y)) (\\ a. a))", "(\\ y. y)",
    "(((\\ x. (\\ y. y)) (\\ a. a)) (\\ b. b))", "(\\ b. b)",
    "((\\x. (x x)) (\\x. (x x)))", "undef",
    NULL};
#include<unistd.h>

unsigned sz;
#include<signal.h>
void fix(x){signal(SIGSEGV,fix);brk(m+(sz*=2));}
main(){
    char**t;
    signal(SIGSEGV,fix);
    m=n=sbrk(sz=10*getpagesize());
    *n++=0;
    for(t=samp;*t;t+=2){
        Y(*t);
        printf("s.b. => %s\n\n", t[1]);
    }
    return 0;
}

Here's the block just before the final reductions. The tricks here are integer cursors instead of pointers (taking advantage of the 'implicit int' behavior), and the use of 'scratch memory': the char*n is the 'new' or 'next' pointer into the free space. But sometimes I write a string into the memory, then call strlen and increment n; effectively using memory and then allocating it, after the size is easier to calculate. Add some whitespace and you can see it's pretty much straight from the McCarthy paper.

#include<stdio.h>
#include<string.h>
char*m,*n;atom(x){return x?(islower(m[x])?m[x]:0):0;}
eq(x,y){return x&&y&&atom(x)==atom(y);}
cell(x){char*t=n,d=0;if(!x||!m[x])return 0;if(m[x]==' ')++x;
if(atom(x)){*n++=m[x];*n++=0;return(n-m)-2;}
if(m[x]=='\\'){memcpy(n,m+x,4);n+=4;*n++=0;return(n-m)-5;}
do{d=m[x]?(m[x]=='('?d+1:(m[x]==')'?d-1:d)):0;*n++=m[x++];}while(d);*n++=0;return t-m;}
car(x){return x?cell(x+1):0;}
cdr(x){return car(x)?cell(x+strlen(m+car(x))+1):0;}
cons(x,y){char*t=n;return x?(sprintf(n,y?"(%s %s)":"(%s)",m+x,m+y),n+=strlen(n)+1,t-m):0;}
subst(x,y,z){if(!x||!y||!z)return 0;return atom(z)?(eq(z,y)?x:z):
cons(m[z+1]=='\\'?car(z):subst(x,y,car(z)),cdr(z)?subst(x,y,cdr(z)):0);}
eval(x){int a;return atom(x)?x:atom(a=car(x))?x:m[a]=='\\'?cons(a,eval(cdr(x))):
m[car(a)]=='\\'?eval(subst(eval(cdr(x)),cell(a+3),cdr(a))):
eval( cons(eval(a),cdr(x)?eval(cdr(x)):0));}
try(char*s){char*t=strcpy(n,s);n+=strlen(n)+1;
printf("input: %s\n", s);printf("eval => %s\n", m+eval(t-m));n=m+1;}

Answer 3

Ruby 254 characters

f=->u,r{r.chars.take_while{|c|u+=c==?(?1:c==?)?-1:0;u>0}*''}
l=->x{x=~/^(\(*)\(\\ (\w+)\. (.*)/&&(b,v,r=$1,$2,$3;e=f[1,r];(e==s=l[e])?b==''?x:(s=f[2,r];(x==y=b.chop+e.gsub(v,s[2+e.size..-1])+r[1+s.size..-1])?x:l[y]):(b+'(\\ '+v+'. '+s+r[e.size..-1]))||x}

It can be used like

puts l["((\\ x. (\\ y. x)) (\\ a. a))"]    # <= (\ y. (\ a. a))

The solution is not yet fully golfed but already almost unreadable.

Answer 4

Binary Lambda Calculus 186

The program shown in the hex dump below

00000000  18 18 18 18 18 18 44 45  1a 10 18 18 45 7f fb cf  |......DE....E...|
00000010  f0 b9 fe 00 78 7f 0b 6f  cf f8 7f c0 0b 9f de 7e  |....x..o.......~|
00000020  f2 cf e1 b0 bf e1 ff 0e  6f 79 ff d3 40 f3 a4 46  |........oy..@..F|
00000030  87 34 0a a8 d0 80 2b 0b  ff 78 16 ff fe 16 fc 2d  |.4....+..x.....-|
00000040  ff ff fc ab ff 06 55 1a  00 58 57 ef 81 15 bf bf  |......U..XW.....|
00000050  0b 6f 02 fd 60 7e 16 f7  3d 11 7f 3f 00 df fb c0  |.o..`~..=..?....|
00000060  bf f9 7e f8 85 5f e0 60  df 70 b7 ff ff e5 5f f0  |..~.._.`.p...._.|
00000070  30 30 6f dd 80 5b b3 41  be 85 bf ff ca a3 42 0a  |00o..[.A......B.|
00000080  c2 bc c0 37 83 00 c0 3c  2b ff 9f f5 10 22 bc 03  |...7...<+...."..|
00000090  3d f0 71 95 f6 57 d0 60  18 05 df ef c0 30 0b bf  |=.q..W.`.....0..|
000000a0  7f 01 9a c1 70 2e 80 5b  ff e7 c2 df fe e1 15 55  |....p..[.......U|
000000b0  75 55 41 82 0a 20 28 29  5c 61                    |uUA.. ()\a|
000000ba

doesn't accept quite the format you propose. Rather, it expects a lambda term in binary lambda calculus (blc) format. However, it does show every single step in the normal form reduction, using minimal parentheses.

Example: computing 2^3 in Church numerals

Save the above hex dump with xxd -r > symbolic.Blc

Grab a blc interpreter from http://www.cwi.nl/~tromp/cl/uni.c

cc -O2 -DM=0x100000 -m32 -std=c99 uni.c -o uni
echo -n "010000011100111001110100000011100111010" > threetwo.blc
cat symbolic.Blc threetwo.blc | ./uni
(\a \b a (a (a b))) (\a \b a (a b))
\a (\b \c b (b c)) ((\b \c b (b c)) ((\b \c b (b c)) a))
\a \b (\c \d c (c d)) ((\c \d c (c d)) a) ((\c \d c (c d)) ((\c \d c (c d)) a) b)
\a \b (\c (\d \e d (d e)) a ((\d \e d (d e)) a c)) ((\c \d c (c d)) ((\c \d c (c d)) a) b)
\a \b (\c \d c (c d)) a ((\c \d c (c d)) a ((\c \d c (c d)) ((\c \d c (c d)) a) b))
\a \b (\c a (a c)) ((\c \d c (c d)) a ((\c \d c (c d)) ((\c \d c (c d)) a) b))
\a \b a (a ((\c \d c (c d)) a ((\c \d c (c d)) ((\c \d c (c d)) a) b)))
\a \b a (a ((\c a (a c)) ((\c \d c (c d)) ((\c \d c (c d)) a) b)))
\a \b a (a (a (a ((\c \d c (c d)) ((\c \d c (c d)) a) b))))
\a \b a (a (a (a ((\c (\d \e d (d e)) a ((\d \e d (d e)) a c)) b))))
\a \b a (a (a (a ((\c \d c (c d)) a ((\c \d c (c d)) a b)))))
\a \b a (a (a (a ((\c a (a c)) ((\c \d c (c d)) a b)))))
\a \b a (a (a (a (a (a ((\c \d c (c d)) a b))))))
\a \b a (a (a (a (a (a ((\c a (a c)) b))))))
\a \b a (a (a (a (a (a (a (a b)))))))

Since the hexdump is rather unreadable, here is a "disassembled" version

@10\\@10\\@10\\@10\\@10\\@10\@\@\@\@@\@1010\@\\\@10\\@10\@\@@@1111111111101
1110@11111110\@@110@11111110\\\\@1110\@1111110\@@101101111110@111111110\@111
111110\\\\@@110@111111011110@11111011110@@10@1111110\@10110\@@111111110\@111
111110\@110@101111011110@1111111111010@1010\\@1110@11010@\@\@1010\@110@1010\
\@@@@@\@1010\@\\\\@@@10\@@111111111011110\\@@101111111111111110\@@101111110\
@@10111111111111111111111110@@@@1111111110\\110@@@@\@1010\\\\@@10\@@@1111101
11110\\@\@@@10111111101111110\@@1011011110\\@@11111010110\\@111110\@@1011110
1110@111010\10\1011111110@111110\\\@101111111111011110\\@@11111111110@@11111
0111110\10\@@@@11111110\\@10\\1101111101110\@@1011111111111111111111110@@@@1
11111110\\@10\\@10\\11011111101110110\\\@@101110110@1010\\11011111010\@@1011
111111111111110@@@@\@1010\@\\@@@10\@@@1110@10\\\@1011110\\110\\\@10\\\@1110\
@@@11111111110@1111111101010\10\\@\@@@1110\\\@10@1110111110\\1110\110@@@1111
0110@@@1111010\\110\\\@10\\\@@1101111111101111110\\\@10\\\@@1101111110111111
10\\\110@1010110\\101110\\@@11010\\\@@1011111111111110@11110\@@1011111111111
101110\@\@@@@@@@@11010101010101010\\110\\10\\1010\10\\\1010\\1010@@@110\110\
@

replacing 00 (lambda) with \ and 01 (application) with @ Now it's almost as readable as brainfuck:-)