Write an interpreter for the untyped lambda calculus



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.


Posted 2011-01-31T14:11:06.710

Reputation: 1 679

3Many 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)). – Anders Kaseorg – 2015-09-27T20:35:03.033

@Kaseorg in ((λ f. (λ x. (f x))) (λ y. (λ x. y))) what is the result? is it (λ x. (λ z. x))? what is z? – RosLuP – 2016-09-05T00:42:36.383

what is the result of "(λ a. ((( w(a) ))) )z" "w(z)" "(w(z))" or "((( w(z) )))" ? – RosLuP – 2016-09-05T01:28:41.523

the lambda program allow the result of (/x.(/y. x^2+y^2)3)7 to be 7^2+3^2? – RosLuP – 2016-09-05T09:06:23.673

@RosLuP The correct result is (λ x. (λ z. x)) because the function should return the outer function's argument, not the inner function's argument. z is a new identifier that was chosen over x, because x would shadow the outer x, leading to a wrong result. Instead of z any other valid identifier could also have chosen. (λ a. ((( w(a) ))) )z is not an input you need to handle as it doesn't adhere to the parenthesization rules I've described (i.e. one pair of parentheses around ever abstraction and application and that's it) and because there won't be free variables in the input. – sepp2k – 2016-09-05T12:22:49.733

@RosLuP So the result can be anything you want, but I'd say the most correct result would still be conforming to the parenthesization rules, so (w z). There's no need to support numbers or infix operators. – sepp2k – 2016-09-05T12:24:38.183

(w z) has parentesis different from (λ x. (λ z. x)) so it would be [λ x. [λ z. x]] – RosLuP – 2016-09-06T22:13:20.283

@RosLuP What do you mean? As I said, the rules are to parenthesize function application and abstraction (with one pair of parentheses each) and nothing else. Both (w z) and (λ x. (λ z. x)) follow these rules exactly. I'm not sure what you mean by "so it would be [λ x. [λ z. x]]". Where did the square brackets come from all of the sudden? – sepp2k – 2016-09-06T22:20:36.083

i'm not one expert and this is the first time i see lambda calculus... now i see (a w) as one function and (λ z. x) as a macro substitution to strings... so they are different and for not confuse parentesis different they for me have to have different type of parentesis so [λ z. x] – RosLuP – 2016-09-06T23:07:19.020

@RosLuP First of all (λ z. x) creates a function (or is a function, really) and (f x) applies a function. So both deal with functions - there are no macros in the lambda calculus. Secondly addition is different from multiplication, but nobody would suggest that something like ((x + y) * z) should instead be written ([x + y] * z). That is, there's no rule that says that different types of expressions need to be parenthesized with different types of parentheses. No programming language in the world has such a rule (inb4 obscure counter example). Thirdly the usual syntax ... – sepp2k – 2016-09-06T23:15:21.750

... for the lambda calculus uses round parentheses everywhere and that's what this challenge asks for. – sepp2k – 2016-09-06T23:16:40.927

1@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))? – Anders Kaseorg – 2016-09-16T00:56:04.767

@RosLup. The presence of a lambda indicates whether an expression is a macro or a literal expression. – codeshot – 2018-03-31T14:04:09.860

1Can 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. – JPvdMerwe – 2011-01-31T15:42:33.003

@JPvdMerwe: Yes, good point, you may assume that. – sepp2k – 2011-01-31T15:47:38.633

Are there any free variables? I mean variables unbound by a lambda like in the expression (\y. a). – FUZxxl – 2011-02-01T09:46:22.130

Another question: May I choose other names for the variables in the output? I mean (\a. a) instead of (\b. b)`? – FUZxxl – 2011-02-01T09:48:12.800

And a third one: Can you make the varnames to one char each? This would make my solution shorter. – FUZxxl – 2011-02-01T10:03:45.597

@FUZxxl: 1. There won't be any free variables in the input. 2. Yes, you may print any expression which is alpha-congruent to the expected output. 3. I think making the conditions easier after there already is a solution which works for the current specification would be unfair. Feel free to post both solutions, but as far as "winning" goes the one which can handle long variable names is the one that counts. – sepp2k – 2011-02-01T13:21:25.660

Does the last example mean the interpreter has to support non-strict (a.k.a. lazy) evaluation? – Joey Adams – 2011-02-01T17:41:16.287

@Joey: Yes, it should find a normal form for every expression which has one, so it can't use strict evaluation. – sepp2k – 2011-02-01T18:05:24.730




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));

luser droog

Posted 2011-01-31T14:11:06.710

Reputation: 4 535

The code commented // um ... is looping through the string and counting parentheses until it finds the matching close-paren at the correct nesting level. – luser droog – 2015-02-19T19:24:09.647

1This incorrectly evaluates ((\ f. (\ x. (f x))) (\ y. (\ x. y))) to (\ x. (f x)). – Anders Kaseorg – 2015-09-27T20:43:52.893

There appear to be some similarities with this and jar.2 xlisp 4.0 from IOCCC 1989.

– luser droog – 2013-02-13T03:18:19.637

Also this segfaults on multi-letter variable names such as (\ xx. xx), which according to the specification must be supported. – Anders Kaseorg – 2016-09-16T01:05:46.637

@AndersKaseorg You're right. I missed that. Reworking it to handle longer symbols... – luser droog – 2016-09-16T07:18:35.877

I tried to expand this into a fuller Lisp interpreter.

– luser droog – 2013-10-29T06:59:50.483

Have an upvote for your effort and your grandma's story from 8 years later :) – ComFreek – 2019-07-08T15:55:06.850

542 – ceilingcat – 2019-11-19T09:51:36.593

islower can be shortened to & 32. '\\' can be shortened to 92. – S.S. Anne – 2019-12-17T15:53:12.427

1I 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. – luser droog – 2011-08-07T09:10:26.313


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|

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

John Tromp

Posted 2011-01-31T14:11:06.710

Reputation: 957

-1 Unreadable. Golfing isn't really a compiled language's activity. – J B – 2012-09-10T16:09:36.407

7BLC 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. – John Tromp – 2012-09-10T17:24:23.577

Well, yes, but now you're just claiming a ×3 codegolf score improvement over the honest-to-goodness readable BF-or-better type of languages. I'm not pissed off anymore, but my downvote remains. – J B – 2012-09-10T18:29:05.503

3Where 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. – John Tromp – 2012-09-10T21:22:06.487

@JohnTromp Yes, some kind of bit-density-weighting seems like a very good candidate for a golf rule. Some of the ones I've seen with unicode chars seem to be getting away with something. (grumble, grumble). – luser droog – 2012-09-19T04:42:24.877

1BTW +1 This is damn cool! – luser droog – 2012-09-19T04:45:17.197

1If 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! – luser droog – 2012-09-19T04:48:27.350

1What would it take to make it read the actual input format? I think that's where you're losing potential upvotes. – luser droog – 2013-02-13T03:23:05.043

Oh here you are again. I don't stop being amused by this guy's work. – MaiaVictor – 2014-01-09T04:05:59.050

@JohnTromp Can you please update the link to blc? It returns a 404. – Björn Lindqvist – 2019-04-21T21:01:18.683

Fixed. Also added link to 2012 IOCCC winner of "Most Functional". – John Tromp – 2019-04-23T07:25:56.630


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.

Anders Kaseorg

Posted 2011-01-31T14:11:06.710

Reputation: 29 242

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? – RosLuP – 2016-09-16T05:36:02.383

2@RosLuP My program accepts λ, not . – Anders Kaseorg – 2016-09-16T09:37:01.683

type this imput ((λ x. x) (λ y. (λ z. z))) in ideone.com return: Runtime error time: 0 memory: 4876 signal:-1 – RosLuP – 2016-09-17T21:34:25.517


@RosLuP Ideone seems to have broken Unicode support. Try the command line or another online interpreter (it works on Rextester, for example).

– Anders Kaseorg – 2016-09-18T02:57:07.457

From Rextester ((λ a. (λ b. (a (a (a b))))) (λ x. (λ d. (c (c d))))) to this input your prog returns a.out: source_file.hs:5:26-28: Missing field in record construction a.

Some program from input =((\ a. (\ b. (a (a (a b))))) (\ x. (\ d. (c (c d))))) returns =(\ b. (\ A. (c (c A)))) – RosLuP – 2016-09-18T06:39:23.383

@RosLuP That input is invalid because c is a free variable; the OP commented “there won't be any free variables in the input”.

– Anders Kaseorg – 2016-09-18T07:03:12.167

Let us continue this discussion in chat.

– Anders Kaseorg – 2016-09-18T07:31:46.717

As far as I can see (λ x. (λ x. x)) is the correct result according to the specification. The specification says each variable is replaced by the argument, not by a modified form of the argument. So this answer doesn't fulfil the specification - which is unfortunate because it's a brilliant program. – codeshot – 2018-04-01T22:37:38.860


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

– Anders Kaseorg – 2018-04-02T14:16:04.220


Python - 321 320

Here's my (fixed) attempt:

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]))
 while c:c+=(s[i]==l)-(s[i]==')');i+=1
 if l!=t[0]:return"(%s %s)"%(t,S(z))
 if t!=s:t=S(t)
 return t
print S(raw_input())


Posted 2011-01-31T14:11:06.710

Reputation: 2 565

1This fails to do capture-avoiding substitution. For example, ((\ f. (\ x. (f x))) (\ y. (\ x. y))) evaluates incorrectly to (\ x. (\ x. x)). – Anders Kaseorg – 2015-09-27T20:35:43.837

1Why is this marked as an answer when it's barely working? Have you tried the given inputs and outputs by the author? – rbaleksandar – 2015-11-22T17:54:01.810

1The author’s provided test cases are insufficient to demonstrate the bugs in this answer. – Anders Kaseorg – 2016-02-25T19:50:13.017

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. – Anders Kaseorg – 2016-09-16T01:02:46.743

1This answer is neither correct nor the shortest. It fails to avoid capture and has string substitution bugs. – Richard Padley – 2017-12-31T18:03:23.273

@AndersKaseorg, The specification doesn't permit capture avoidance as far as I can see. A solution that avoids captures will not meet the specification. None of the examples in the challenge are affected by this as far as I can see. – codeshot – 2018-04-01T22:34:53.380

@codeshot A comment from the question author indicated that capture avoidance is required for this problem. Also, as I’ve said, this answer has additional unrelated bugs.

– Anders Kaseorg – 2018-04-02T14:19:36.913

This looks nice, but doesn't seem to work. I've added some example inputs and outputs, for which your code produces the wrong results. – sepp2k – 2011-01-31T16:31:23.450

Nice, good job. – sepp2k – 2011-01-31T18:42:19.683


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.


Posted 2011-01-31T14:11:06.710

Reputation: 23 109

This fails to do capture-avoiding substitution. For example, ((\ f. (\ x. (f x))) (\ y. (\ x. y))) evaluates incorrectly to (\ x. (\ x. x)). – Anders Kaseorg – 2015-09-27T20:45:33.540

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. – Anders Kaseorg – 2016-09-16T01:07:53.847

hello envy, my old friend :) – luser droog – 2011-08-08T10:07:50.603


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]


Posted 2011-01-31T14:11:06.710

Reputation: 349

This doesn’t conform to the input and output specifications from the problem. – Anders Kaseorg – 2015-09-27T20:00:10.113


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 #\._])


Posted 2011-01-31T14:11:06.710

Reputation: 39

Where can I get Waterhouse Arc? – Anders Kaseorg – 2015-09-27T20:08:32.890

1Invalid as an interpreter is nowhere to be found – cat – 2016-02-27T00:50:09.423

@AndersKaseorg here

– ASCII-only – 2018-06-04T02:51:53.063

@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? – Anders Kaseorg – 2018-06-04T04:48:32.323

@AndersKaseorg Never mind. Found it

– ASCII-only – 2018-06-04T05:22:54.327


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;



Posted 2011-01-31T14:11:06.710

Reputation: 3 036

The specification requires \ or λ, not /. It also requires support for multi-letter variable names. – Anders Kaseorg – 2016-09-16T01:18:07.993

'\n' etc symbol '' has other uses it is better use '/' instead – RosLuP – 2016-09-16T05:18:58.660

1Still, the challenge is to satisfy the specification, not to make it better. – Anders Kaseorg – 2016-09-16T09:41:49.547

i wrote something for be it a little more conforming... but size explode... – RosLuP – 2016-09-17T21:28:30.887

1932 bytes – ceilingcat – 2019-04-25T06:51:01.790


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


Posted 2011-01-31T14:11:06.710

Reputation: 1 946

3This fails to do capture-avoiding substitution. For example, ((λ f. (λ x. (f x))) (λ y. (λ x. y))) evaluates incorrectly to (λ x. (λ x. x)). – Anders Kaseorg – 2015-09-27T20:46:16.563


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


Posted 2011-01-31T14:11:06.710

Reputation: 349

This doesn’t conform to the input and output specifications from the problem. – Anders Kaseorg – 2015-09-27T19:55:50.810


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.

Björn Lindqvist

Posted 2011-01-31T14:11:06.710

Reputation: 590

You can shorten some of those function names, and turn some of them into lambdas. You also have some excess whitespace here and there – Jo King – 2019-04-22T02:19:29.450

(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]. – Esolanging Fruit – 2019-04-22T02:21:37.033

1045 bytes through mostly formatting changes like indentation and lambdas – Jo King – 2019-04-22T03:34:03.507


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

Daniel Schepler

Posted 2011-01-31T14:11:06.710

Reputation: 1 001


C 637 bytes

#define R return
#define E if(i>=M||j>=M)R-1;
#define H d[j++]
enum{O=40,C,M=3999};signed char Q[M],D[M],t[M],Z,*o=Q,*d=D,*T;int m,n,s,c,w;K(i,j,k){!Z&&(Z=t[O]=1)+(t[C]=-1);E;if(!o[i]){H=0;R 0;}if((c=t[o[i]]+t[o[i+1]])!=2||o[i+2]!=92){H=o[i++];R K(i,j,i);}for(i+=2,w=0;i<M&&o[i]&&c;++i)c+=t[o[i]],!w&&c==1?w=i:0;E;if(c){for(;H=o[i++];)E;R 0;}for(c=k+7,n=j;c<w&&j<M;++c)if(o[c]==o[k+4]){if(o[c+1]==46){d[n++]=o[k++];R K(k,n,k);}for(m=w+2;m<i-1&&j<M;)H=o[m++];}else H=o[c];E;Z=2;R K(i,j,i);}char*L(char*a){for(s=n=0;n<M&&(o[n]=a[n]);++n);if(n==M)R 0;for(;++s<M;){Z=0;if((n=K(0,0,0))!=-1&&Z==2)T=d,d=o,o=T;else break;}R n==-1||s>=M?0:d;}

This version not use auxiliary variables (so this not follow 100% what lambda calculus says... as many other here...). Each variable has to be 1 chararcter long (as some other here ). Test code:

#define P printf

{char  *r[]={ "((\\ 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))))",
              "((\\ a. (\\ b. (a (a (a b))))) (\\ c. (\\ d. (c (c d)))))",
              "((\\ f. (\\ x. (f x))) (\\ y. (\\ x. y)))",
             0}, *y;
 int    w;

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


o=((\ x. x) z) d=z
o=((\ x. x) (\ y. (\ z. z))) d=(\ y. (\ z. z))
o=(\ x. ((\ y. y) x)) d=(\ x. x)
o=((\ x. (\ y. x)) (\ a. a)) d=(\ y. (\ a. a))
o=(((\ x. (\ y. x)) (\ a. a)) (\ b. b)) d=(\ a. a)
o=((\ x. (\ y. y)) (\ a. a)) d=(\ y. y)
o=(((\ x. (\ y. y)) (\ a. a)) (\ b. b)) d=(\ b. b)
o=((\ x. (x x)) (\ x. (x x))) d=Error
o=(((\ x. (\ y. x)) (\ a. a)) ((\ x. (x x)) (\ x. (x x)))) d=(\ a. a)
o=((\ a. (\ b. (a (a (a b))))) (\ c. (\ d. (c (c d))))) d=(\ b. (\ d. (b (b (b (b (b (b (b (b d))))))))))
o=((\ f. (\ x. (f x))) (\ y. (\ x. y))) d=(\ x. (\ x. x))

this is the semi ungolf one:

#define R return
#define E if(i>=M||j>=M)R-1;
#define H d[j++]
enum{O=40,C,M=3999}; // assume ascii
signed char Q[M],D[M],t[M],Z,*o=Q,*d=D,*T;
int m,n,s,c,w;

{!Z&&(Z=t[O]=1)+(t[C]=-1); //inizializza tabelle

 E;if(!o[i]){H=0;R 0;}
      {H=o[i++]; R K(i,j,i);}
 if(c){for(;H=o[i++];)E;R 0;} 
//  01234567w12 i
//  ((/ x. x) z)
//   x                 w              z
// o[k+4]..o[k+5];  o[k+7]..o[w];  o[w+2]..o[i-1]

// sostituzione
// sostituisce a x z in w e lo scrive in d
         {if(o[c+1]==46) // non puo' sostituire una variabile dove c'e' lambda
             {d[n++]=o[k++]; R K(k,n,k);}
      else H=o[c];
 R K(i,j,i);

 if(n==M)R 0;
//    if(Z==2)printf("n=%d>%s\n", n, d);
    else break;
 R n==-1||s>=M?0:d; 


Posted 2011-01-31T14:11:06.710

Reputation: 3 036

The specification requires \ or λ, not /. It also requires support for multi-letter variable names. Additionally (I know you’re aware of this, but yes, it’s still wrong), this incorrectly evaluates ((/ f. (/ x. (f x))) (/ y. (/ x. y))) to (/ x. (/ x. x)). – Anders Kaseorg – 2016-09-16T01:27:43.643

I change / to \ there is the problem not allow multi characters variable. if test some other this is for other solution too – RosLuP – 2017-10-19T07:17:49.973