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:


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.


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.

  • 2
    \$\begingroup\$ Can we assume that there will not be prepended or appended whitespace to the string and that whitespace is otherwise as specified in the sample input? That is, no whitespace between brackets, between the dot and the parameter name and other instances of whitespace is exactly 1 space. \$\endgroup\$
    – JPvdMerwe
    Commented Jan 31, 2011 at 15:42
  • \$\begingroup\$ @JPvdMerwe: Yes, good point, you may assume that. \$\endgroup\$
    – sepp2k
    Commented Jan 31, 2011 at 15:47
  • \$\begingroup\$ Are there any free variables? I mean variables unbound by a lambda like in the expression (\y. a). \$\endgroup\$
    – FUZxxl
    Commented Feb 1, 2011 at 9:46
  • 3
    \$\begingroup\$ Many or all of the solutions here fail to implement capture-avoiding substitution! You should add a test case like ((λ f. (λ x. (f x))) (λ y. (λ x. y))), which should evaluate to (λ x. (λ z. x)), not (λ x. (λ x. x)). \$\endgroup\$ Commented Sep 27, 2015 at 20:35
  • 1
    \$\begingroup\$ @sepp2k Have you considered adding ((λ f. (λ x. (f x))) (λ y. (λ x. y))) as a test case and unaccepting the current answer which incorrectly produces (λ x. (λ x. x))? \$\endgroup\$ Commented Sep 16, 2016 at 0:56

11 Answers 11



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 ...

    return m[x]>>5==3;

... correctly identifies lowercase letters (assuming ASCII), but also accepts any of `{|}~. (This same observation about ASCII is made in this excellent video about UTF-8.)

Et viola:|

#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
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

"((\\ 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};
main(){char**k;n=m=sbrk(4096);*n++=0;for(k=s;*k;k++)Y(*k);R 0;}


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:

#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
C(x,y){char*t=n;sprintf(n,y?"(%s %s)":"(%s)",m+x,m+y);n+=strlen(n)+1;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;}

    "((\\ 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",

unsigned sz;
void fix(x){signal(SIGSEGV,fix);brk(m+(sz*=2));}
        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. You can see it's pretty much straight from the McCarthy paper, with the exception of cell() which interfaces between the functions and the string representation of data.

char*m,*n;  //memory_base, memory_next
atom(x){  // x is an atom if it is a cursor to a lowercase alpha char.
    return x?(islower(m[x])?m[x]:0):0;
eq(x,y){  // x and y are equal if they are both atoms, the same atom.
    return x&&y&&atom(x)==atom(y);
cell(x){  // return a copy of the list-string by cursor, by parsing
        return 0;
    if(m[x]==' ')
    if(m[x]=='\\'){  // our lambda symbol
    do{  // um ...
    return t-m;
car(x){  // return (copy of) first element
    return x?cell(x+1):0;
cdr(x){  // return (copy of) rest of list
    return car(x)?cell(x+strlen(m+car(x))+1):0;
cons(x,y){  // return new list containing first x and rest y
    return x?(sprintf(n,y?"(%s %s)":"(%s)",m+x,m+y),n+=strlen(n)+1,t-m):0;
subst(x,y,z){  // substitute x for z in y
        return 0;
    return atom(z)? (eq(z,y)?x:z):
eval(x){  // evaluate a lambda expression
    int a;
    return atom(x)?x:
        eval( cons(eval(a),cdr(x)?eval(cdr(x)):0));
try(char*s){  // handler
    printf("input: %s\n", s);
    printf("eval => %s\n", m+eval(t-m));
  • 3
    \$\begingroup\$ I found a few more tricks to save a character or two, but nothing radical. sprintf(n,...);n+=strlen(n)+1; is better as n+=sprintf(n,...)+1; Inverting the array syntax x[m] instead of m[x] allow me to replace all indirections with a 'postfix' macro #define M [m]...x M which saves 1 char and gives a "free" line break since whitespace is necessary to separate the tokens. \$\endgroup\$ Commented Aug 7, 2011 at 9:10
  • \$\begingroup\$ There appear to be some similarities with this and jar.2 xlisp 4.0 from IOCCC 1989. \$\endgroup\$ Commented Feb 13, 2013 at 3:18
  • \$\begingroup\$ I tried to expand this into a fuller Lisp interpreter. \$\endgroup\$ Commented Oct 29, 2013 at 6:59
  • 1
    \$\begingroup\$ Have an upvote for your effort and your grandma's story from 8 years later :) \$\endgroup\$
    – ComFreek
    Commented Jul 8, 2019 at 15:55
  • 4
    \$\begingroup\$ islower can be shortened to & 32. '\\' can be shortened to 92. \$\endgroup\$
    – S.S. Anne
    Commented Dec 17, 2019 at 15:53

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  |[email protected]|
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|

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://tromp.github.io/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


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

Also see http://www.ioccc.org/2012/tromp/hint.html

  • 9
    \$\begingroup\$ BLC just happens to use a binary alphabet. 00 is lambda, 01 is application, and 1^{n}0 is a variable in unary. There's no compilation involved. \$\endgroup\$
    – John Tromp
    Commented Sep 10, 2012 at 17:24
  • 4
    \$\begingroup\$ Where do you get a factor x3? You actually raise a good point in that languages with smaller source alphabets like BF are penalised. For fair comparison, all sizes should be expressed in bits, and BF characters only take 3 bits each. Most other languages need 7 bits for ASCII, some use all 8. \$\endgroup\$
    – John Tromp
    Commented Sep 10, 2012 at 21:22
  • 2
    \$\begingroup\$ BTW +1 This is damn cool! \$\endgroup\$ Commented Sep 19, 2012 at 4:45
  • 2
    \$\begingroup\$ If fractran in fractran is acceptable, I don't see why this should be a problem at all. You can't read it? You want to? Learn! \$\endgroup\$ Commented Sep 19, 2012 at 4:48
  • 1
    \$\begingroup\$ What would it take to make it read the actual input format? I think that's where you're losing potential upvotes. \$\endgroup\$ Commented Feb 13, 2013 at 3:23

Haskell, 342 323 317 305 characters

As of this writing, this is the only solution that evaluates ((λ f. (λ x. (f x))) (λ y. (λ x. y))) to the correct result (λ x. (λ z. x)) rather than (λ x. (λ x. x)). Correct implementation of the lambda calculus requires capture-avoiding substitution, even under this problem’s simplifying guarantee that no variable shadows another variable in its scope. (My program happens to work even without this guarantee.)

data T=T{a::T->T,(%)::ShowS}
i d=T(i. \x v->'(':d v++' ':x%v++")")d
l f=f`T`\v->"(λ "++v++". "++f(i(\_->v))%('x':v)++")"
q[(v,s)]k|v/="("=k(maybe T{}id.lookup v)s|'λ':u<-s,[(w,_:t)]<-lex u=t? \b->k(\e->l$b.(:e).(,)w).tail|0<1=s? \f->(?(.tail).k. \x z->f z`a`x z)
main=interact(? \f->(f[]%"x"++))


  • This runs in GHC 7.0, as required because this challenge was set in January 2011. It would be 13 characters shorter if I were allowed to assume GHC 7.10.

Ungolfed version with documentation.

  • \$\begingroup\$ your prog in ideone haskell compiler to the input ((\ x. x) (\ y. (\ z. z))) return "run time error" even in ((\\ x. x) (\\ y. (\\ z. z)))... what does it mean "lex" in Haskell? \$\endgroup\$
    – user58988
    Commented Sep 16, 2016 at 5:36
  • 2
    \$\begingroup\$ @RosLuP My program accepts λ, not \. \$\endgroup\$ Commented Sep 16, 2016 at 9:37
  • \$\begingroup\$ type this imput ((λ x. x) (λ y. (λ z. z))) in ideone.com return: Runtime error time: 0 memory: 4876 signal:-1 \$\endgroup\$
    – user58988
    Commented Sep 17, 2016 at 21:34
  • 1
    \$\begingroup\$ @RosLuP Ideone seems to have broken Unicode support. Try the command line or another online interpreter (it works on Rextester, for example). \$\endgroup\$ Commented Sep 18, 2016 at 2:57
  • 2
    \$\begingroup\$ @codeshot The question author has already commented that ((λ f. (λ x. (f x))) (λ y. (λ x. y))) ↦ (λ x. (λ z. x)) is correct for this problem (just like the real lambda calculus). \$\endgroup\$ Commented Apr 2, 2018 at 14:16

Ruby 254 characters

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.

  • \$\begingroup\$ hello envy, my old friend :) \$\endgroup\$ Commented Aug 8, 2011 at 10:07
  • \$\begingroup\$ This fails to do capture-avoiding substitution. For example, ((\ f. (\ x. (f x))) (\ y. (\ x. y))) evaluates incorrectly to (\ x. (\ x. x)). \$\endgroup\$ Commented Sep 27, 2015 at 20:45
  • \$\begingroup\$ In addition to the above capture bug, this also incorrectly evaluates (\ y. (\ xx. ((\ x. xx) y))) to (\ y. (\ xx. yy)), where overzealous string substitution has manufactured the nonexistent variable yy. \$\endgroup\$ Commented Sep 16, 2016 at 1:07

Edit: check my answer below for 250 under pure JavaScript.

2852 243 characters using LiveScript (No Regex! Not fully golfed - could be improved)

S=(a,b,t=-1,l=0)->|L a=>[\\,S(a.1,b,t,l+1)];|A a=>(map (->S(a[it],b,t,l)),[0 1]);|a==l+-1=>S(b,0,l+-1,0)||a|l-1<a=>a+t;|_=>a
R=(a)->|L a=>[\\,R a.1]|(A a)&&(L a.0)=>R(S(R(a.0),R(a.1)).1)|_=>a


a = [\\,[\\,[1 [1 0]]]]
b = [\\,[\\,[1 [1 [1 0]]]]]
console.log R [a, b]
# outputs ["\\",["\\",[1,[1,[1,[1,[1,[1,[1,[1,[1,0]]]]]]]]]]]

Which is 3^2=9, as stated on OP.

If anyone is curious, here is an extended version with some comments:

# Just type checking
λ = 100
isλ = (.0==λ)
isA = -> it.forEach? && it.0!=λ
isV = (.toFixed?)

# Performs substitutions in trees
# a: trees to perform substitution in
# b: substitute bound variables by this, if != void
# f: add this value to all unbound variables
# l: internal (depth)
S = (a,b,t=-1,l=0) ->
    | isλ a             => [λ, (S a.1, b, t, l+1)]
    | isA a             => [(S a.0, b, t, l), (S a.1, b, t, l)]
    | a == l - 1        => (S b, 0, (l - 1), 0) || a
    | l - 1 < a < 100   => a + t
    | _                 => a

# Performs the beta-reduction
R = (a) ->
    | (isλ a)               => [λ,R a.1]
    | (isA a) && (isλ a.0)  => R(S(R(a.0),R(a.1)).1)
    | _                     => a

# Test
a = [λ,[λ,[1 [1 0]]]]
b = [λ,[λ,[1 [1 [1 0]]]]]
console.log show R [a, b]
  • \$\begingroup\$ This doesn’t conform to the input and output specifications from the problem. \$\endgroup\$ Commented Sep 27, 2015 at 20:00

Waterhouse Arc - 140 characters

f[is cons?&car._'λ]n[if
atom._ _
f._ `(λ,_.1,n:_.2)(=
c n:_.0
e _)(if
c.1 _)e.1
_]c.2)(map n
_))]λ[n:read:rem #\._])
  • \$\begingroup\$ Where can I get Waterhouse Arc? \$\endgroup\$ Commented Sep 27, 2015 at 20:08
  • 1
    \$\begingroup\$ Invalid as an interpreter is nowhere to be found \$\endgroup\$
    – cat
    Commented Feb 27, 2016 at 0:50
  • \$\begingroup\$ @AndersKaseorg here \$\endgroup\$
    – ASCII-only
    Commented Jun 4, 2018 at 2:51
  • \$\begingroup\$ @ASCII-only I know what Arc is, but the “Waterhouse” part suggested to me that some particular dialect was necessary. Have you gotten it to run? \$\endgroup\$ Commented Jun 4, 2018 at 4:48
  • \$\begingroup\$ @AndersKaseorg Never mind. Found it \$\endgroup\$
    – ASCII-only
    Commented Jun 4, 2018 at 5:22

C 1039 bytes

#define F for
#define R return
#define E if(i>=M||j>=M)R-1;
enum{O='(',C,M=3999};signed char Q[M],D[M],t[M],Z,v,*o=Q,*d=D,*T;int m,n,s,c,w,x,y;K(i,j,k){!Z&&(Z=t[O]=1)+(t[C]=-1);E;if(!o[i]){d[j]=0;R 0;}if((c=t[o[i]]+t[o[i+1]])!=2||o[i+2]!='\\'){d[j++]=o[i++];R K(i,j,i);}F(i+=2,y=w=0;i<M&&o[i]&&c;++i)c+=t[o[i]],!w&&c==1?w=i:0,!y&&o[i]=='.'?y=i+2:0;E;if(c){F(;d[j++]=o[i++];)E;R 0;}F(c=y;c<w;++c)if(o[c]=='\\')F(n=0,m=w+2;m<i;++m){if(o[m]==o[c+2]){F(x=0;o[m+x]&&isalpha(o[m+x])&&o[m+x]==o[c+2+x];++x);if(o[c+2+x]!='.'||isalpha(o[m+x]))continue;if(v>'Z')R-1;F(n=c+2;n<w;++n)if(o[n]==o[m]){F(x=0; o[m+x]&&isalpha(o[m+x])&&o[m+x]==o[n+x];++x);if(o[m+x]=='.'&&!isalpha(o[n+x]))F(;--x>=0;) o[n+x]=v;}++v;}}F(c=y;c<w&&j<M;++c){F(x=0;o[c+x]&&o[c+x]==o[k+4+x]&&isalpha(o[c+x]); ++x);if(o[k+4+x]=='.'&&!isalpha(o[c+x])){F(m=w+2;m<i-1&&j<M;++m)d[j++]=o[m];c+=x-1;}else d[j++]=o[c];}E;Z=2;R K(i,j,i);}char*L(char*a){F(s=n=0;n<M&&(o[n]=a[n]);++n);if(n==M)R 0;v='A';F(;++s<M;){Z=0;n=K(0,0,0);if(Z==2&&n!=-1)T=d,d=o,o=T;else break;}R n==-1||s>=M?0:d;}

Variables allow as input using lowercase letters [from a..z] the sys can generate variables using uppercase letters [from A..Z] if need in the output... Assume ascii character configuration.

#define P printf
{char  *r[]={ "((\\ abc. (\\ b. (abc (abc (abc b))))) (\\ cc. (\\ dd. (cc (cc dd)))))",
              "((\\ fa. (\\ abc. (fa abc))) (\\ yy. (\\ abc. yy)))",
              "((\\ x. x) z)", 
              "((\\ x. x) (\\ y. (\\ z. z)))", 
              "(\\ x. ((\\ y. y) x))", 
              "((\\ x. (\\ y. x)) (\\ a. a))", 
              "(((\\ 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)))",
              "(((\\ x. (\\ y. x)) (\\ a. a)) ((\\ x. (x x)) (\\ x. (x x))))",
             0}, *p;
 int    w;

 for(w=0; r[w] ;++w)
    P("o=%s d=%s\n", r[w], p==0?"Error ":p);
 R  0;

  • \$\begingroup\$ The specification requires \ or λ, not /. It also requires support for multi-letter variable names. \$\endgroup\$ Commented Sep 16, 2016 at 1:18
  • \$\begingroup\$ '\n' etc symbol '\' has other uses it is better use '/' instead \$\endgroup\$
    – user58988
    Commented Sep 16, 2016 at 5:18
  • 1
    \$\begingroup\$ Still, the challenge is to satisfy the specification, not to make it better. \$\endgroup\$ Commented Sep 16, 2016 at 9:41
  • \$\begingroup\$ i wrote something for be it a little more conforming... but size explode... \$\endgroup\$
    – user58988
    Commented Sep 17, 2016 at 21:28
  • 1
    \$\begingroup\$ 932 bytes \$\endgroup\$
    – ceilingcat
    Commented Apr 25, 2019 at 6:51

Python: 1266 characters (measured using wc)

from collections import *;import re
def ab(t):c(t,0);p=c(t,0);c(t,0);return B(p,tm(t))
def tm(t):return ab(t)if t[0]=='\\'else ap(t)
def at(t):
    if t[0]=='(':c(t,0);r=tm(t);c(t,0);return r
    if 96<ord(t[0][0])<123:return c(t,0)
    if t[0]=='\\':return ab(t)
def ap(t):
    l = at(t)
    while 1:
        r = at(t)
        if not r:return l
        l = A(l,r)
def P(s):return tm(re.findall(r'(\(|\)|\\|[a-z]\w*|\.)',s)+['='])
def V(e):o=y(e);return V(e.b)-{e.i} if o==B else V(e.l)|V(e.r)if o==A else{e}
def R(e,f,t):return B(e.i,R(e.b,f,t)) if y(e)==B else A(R(e.l,f,t),R(e.r,f,t))if y(e)==A else t if e==f else e
def N(i,e):return N(chr(97+(ord(i[0])-96)%26),e) if i in V(e)else i
def S(i,e,a): return A(S(i,e.l,a),S(i,e.r,a)) if y(e)==A else(e if e.i==i else B(N(e.i,a),S(i,R(e.b,e.i,N(e.i,a)),a)))if y(e)==B else a if e==i else e
def T(e):
    if y(e)==A:l,r=e;return S(l.i,l.b,r)if y(l)==B else A(T(l),r)if y(l)==A else A(l,T(r))
    if y(e)==B:return B(e.i,T(e.b))
def F(e):o=y(e);return r'(\%s. %s)'%(e.i,F(e.b))if o==B else'(%s %s)'%(F(e.l),F(e.r)) if o==A else e
def E(a):
    try: return E(T(a))
    except NameError:print(F(a))

Not the shortest by a long shot, but it correctly handles alpha-renaming and all the examples listed in OPs post.

  • \$\begingroup\$ You can shorten some of those function names, and turn some of them into lambdas. You also have some excess whitespace here and there \$\endgroup\$
    – Jo King
    Commented Apr 22, 2019 at 2:19
  • \$\begingroup\$ (1) Replacing 4-space indentation with a single space will save quite a few bytes. (2) Can you replace except NameError with just except? (3) Two-character function names can be renamed to one-character names. (4) There are a few places where you have assignments that have spaces around the =. (5) if t[0]=='c' can be replaced with if'c'==t[0]. \$\endgroup\$ Commented Apr 22, 2019 at 2:21
  • \$\begingroup\$ 1045 bytes through mostly formatting changes like indentation and lambdas \$\endgroup\$
    – Jo King
    Commented Apr 22, 2019 at 3:34

C++ (gcc), 782 766 758 731 bytes

#include <string>
#include <map>
#define A return
#define N new E
using S=std::string;using C=char;using I=int;S V(I i){A(i>8?V(i/9):"")+C(97+i%9);}S W(C*&s){C*b=s;while(*++s>96);A{b,s};}struct E{I t,i;E*l,*r;E(E&o,I d,I e){t=o.t;i=o.i+(o.i>=d)*e;t?l=N{*o.l,d,e},t-1?r=N{*o.r,d,e}:0:0;}E(I d,std::map<S,I>m,C*&s){t=*s-40?i=m[W(s)],0:*++s-92?l=N{d,m,s},r=N{d,m,++s},++s,2:(m[W(s+=2)]=d,l=N{d+1,m,s+=2},++s,1);}I R(I d){A t?t-1?l->t==1?l->l->s(d,0,*r),*this=*l->l,1:l->R(d)||r->R(d):l->R(d+1):0;}I s(I d,I e,E&v){t?t-1?l->s(d,e,v),r->s(d,e,v):l->s(d,e+1,v):i==d?*this={v,d,e},0:i-=i>d;}S u(I d){A t?t-1?S{"("}+l->u(d)+' '+r->u(d)+')':S{"(\\ "}+V(d)+". "+l->u(d+1)+')':V(i);}};S f(C*s){E a{0,{},s};for(I c=999;a.R(0)&&c--;);A a.u(0);}

Try it online!

The basic idea here is that the code uses an internal representation based on the idea of de Bruijn indices -- except that I reverse the indices to indicate the lambda-depth of the binding of the referred variable. In the code:

  • E::t represents the type of a node - 0 for a variable leaf node, 1 for a lambda node, and 2 for a function application node. (Chosen so that it coincides with the arity of the node, which just happens to be possible.) Then E::l and E::r are the children as appropriate (just E::l for a lambda node), and E::i is the lambda-depth index for a variable leaf node.
  • The constructor E::E(E&o,int d,int e) clones a subexpression which was initially at lambda-depth d for pasting into a new location at lambda-depth d+e. This involves preserving variables at lambda-depth less than d while incrementing variables at lambda-depth at least d by e.
  • E::s does a substitution of the subexpression v into variable number d in *this while decrementing variable numbers greater than d (and e is an internal detail tracking the lambda-depth increment for when it needs to call E::c).
  • E::R searches for a single beta-reduction to perform, preferring top-most or left-most instances according to a pre-order search through the AST. It returns nonzero if it found a reduction to perform or zero if it found none.
  • E::u is a to_string type operation which reconstitutes a "human readable" string using synthetic names for the variables. (Note that because of a little golfing of the V helper function it will only generate names containing a through i.)
  • The constructor E::E(int d, std::map<std::string, int> m, char*&s) does parsing of an input string s into an expression AST based on a mapping m of currently bound variable names into lambda-depth indices.
  • f is the main function answering the question.

(As you can see at the TIO link, the code does handle variable names with multiple characters, and it also gets a correct answer of (\ a. (\ b. a)) for ((\ f. (\ x. (f x))) (\ y. (\ x. y))). It also just so happens that the parsing code can handle variable shadowing at no extra cost.)

-16 bytes partially due to idea by ceilingcat (which I had also come up with independently), and partially due to changing E*a=new E; to E&a=*new E; and then changing a-> to a.

-8 more bytes due to another comment by ceilingcat (factor out assignment of a.t from ternary)

-27 bytes from converting parser and clone into constructors of E


Haskell 456 C

It can be much shorter if the lazy evaluation feature of Haskell is fully utilized. Sadly, I don't know how to do it.

Also, many characters are wasted in the parsing step.

data T=A[Char]|B[Char]T|C T T
s(A a)=a
s(B a b)="(λ "!a!". "!s b!")"
s(C a b)='(':s a!" "!s b!")"
e d(A a)=maybe(A a)id(lookup a d)
e d(B a b)=B a.e d$b
e d(C a b)=f d(e d a)(e d b)
f d(B x s)q=e((x,q):d)s
f d p q=C p q
p('(':'λ':s)=let(A c,t)=p(d s);(b,u)=p(d.d$t);in(B c b,d u)
p('(':s)=let(a,t)=p s;(b,u)=p(d t)in(C a b,d u)
p(c:s)|elem c" .)"=(A "",c:s)|1<2=let((A w),t)=p s in(A(c:w),t)
main=do l<-getLine;putStrLn$r l

Ungolfed version

data Expression = Literal String 
                | Lambda String Expression
                | Apply Expression Expression
                deriving Show

type Context = [(String, Expression)]

show' :: Expression -> String
show' (Literal a) = a
show' (Lambda x e) = "(λ " ++ x ++ ". " ++ show' e ++ ")"
show' (Apply e1 e2) = "(" ++ show' e1 ++ " " ++ show' e2 ++ ")"

eval :: Context -> Expression -> Expression
eval context e@(Literal a) = maybe e id (lookup a context)
eval context (Lambda x e) = Lambda x (eval context e)
eval context (Apply e1 e2) = apply context (eval context e1) (eval context e2)

apply :: Context -> Expression -> Expression -> Expression
apply context (Lambda x e) e2 = eval ((x, e2):context) e
apply context e1 e2 = Apply e1 e2

parse :: String -> (Expression, String)
parse ('(':'λ':s) = let
    (Literal a, s') = parse (tail s)
    (e, s'') = parse (drop 2 s')
    in (Lambda a e, tail s'')

parse ('(':s) = let
    (e1, s') = parse s
    (e2, s'') = parse (tail s')
    in (Apply e1 e2, tail s'')

parse (c:s) | elem c " .)" = (Literal "", c:s)
            | otherwise    = let ((Literal a), s') = parse s 
                             in (Literal (c:a), s')

run :: String -> String
run = show' . eval [] . fst . parse
main = do
  line <- getLine
  putStrLn$ run line
  • 3
    \$\begingroup\$ This fails to do capture-avoiding substitution. For example, ((λ f. (λ x. (f x))) (λ y. (λ x. y))) evaluates incorrectly to (λ x. (λ x. x)). \$\endgroup\$ Commented Sep 27, 2015 at 20:46

Got 231 with JavaScript / no Regex

(function f(a){return a[0]?(a=a.map(f),1===a[0][0]?f(function d(b,a,e,c){return b[0]?1===b[0]?[1,d(b[1],a,e,c+1)]:2===b[0]?b[1]===c-1?d(a,0,c-1,0)||b:c-1<b[1]?[2,b[1]+e]:b:[d(b[0],a,e,c),d(b[1],a,e,c)]:b}(a[0],a[1],-1,0)[1]):a):a})

Receives 2-elements arrays. 1 stands for λ and 2 stands for a bruijn index variable.


zero = [1,[1,[2,0]]]; // λλ0
succ = [1,[1,[1,[[2,1],[[[2,2],[2,1]],[2,0]]]]]]; // λλλ(1 ((2 1) 0))
console.log(JSON.stringify(reduce([succ,[succ,[succ,zero]]]))); // 0+1+1+1
// Output: [1,[1,[[2,1],[[2,1],[[2,1],[2,0]]]]]] = λλ(1(1(1 0))) = number 3
  • \$\begingroup\$ This doesn’t conform to the input and output specifications from the problem. \$\endgroup\$ Commented Sep 27, 2015 at 19:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.