12 −12 characters

## Haskell, 342323317317 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 v="(λ "++v++". "++f(i(\_->v))%('x':v)++")"
(f#g)x=f x$g x q("(",'λ':s)k|[(w,_:t)]<-lex s=t? \b->k(\e->T#l$b.(:e).(,)w).tail
q("(",s)k=s? \f->(? \x->k((a.f)#x).tail)
q(v,s)k=k(maybe T{}id.lookup v)s
main=interact(? \f->(f[]%"x"++))

data T=T{a::T->T,(%)::ShowS}
i d=T(i. \x v->'(':d v++' ':x%v++")")d
l f=fT\v->"(λ "++v++". "++f(i(\_->v))%('x':v)++")"
(?)=q.lex
q("(",'λ':s)k|[(w,_:t)]<-lex s=t? \b->k(\e->T#l$b.(:e).(,)w).tail q("(",s)k=s? \f->(? \x->k((a.f)#x).tail) q(v,s)k=k(maybe T{}id.lookup v)s main=interact(? \f->(f[]%"x"++))  Notes: • This runs in GHC 7.0, as required because this challenge was set in January 2011. It would be 16 characters shorter if I were allowed to assume GHC 7.10. Ungolfed version with documentation. ## Haskell, 342323317 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=fT\v->"(λ "++v++". "++f(i(\_->v))%('x':v)++")" (?)=q.lex 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 zax z)
main=interact(? \f->(f[]%"x"++))


Notes:

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

11 −6 characters

## Haskell, 342323323 317 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 v="(λ "++v++". "++f(i(\_->v))%('x':v)++")"
(f#g)x=f x$g x q("(",'λ':s)|[k|[(w,_:t)]<-lex s,(e,_:u)<-ps=t? t=\b->k(\g\e->T#l$e>T#l$b.(:ge).(,)w,u).tail q("(",s)|(f,t)<-pk=s? s,(x,_:u)<\f-p>(? t=\x->k((a.f)#x,u).tail) q(v,s)=k=k(maybe T{}id.lookup v,s)s main=interact$main=interact(\? \f->(f,nf[]%"x"++)->f[]%"x"++n).p


Notes:

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

Ungolfed version with documentation.

## Haskell, 342323 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 v="(λ "++v++". "++f(i(\_->v))%('x':v)++")"
(f#g)x=f x$g x q("(",'λ':s)|[(w,_:t)]<-lex s,(e,_:u)<-p t=(\g->T#l$e.(:g).(,)w,u)
q("(",s)|(f,t)<-p s,(x,_:u)<-p t=((a.f)#x,u)
q(v,s)=(maybe T{}id.lookup v,s)
q("(",'λ':s)k|[(w,_:t)]<-lex s=t? \b->k(\e->T#l$b.(:e).(,)w).tail q("(",s)k=s? \f->(? \x->k((a.f)#x).tail) q(v,s)k=k(maybe T{}id.lookup v)s main=interact(? \f->(f[]%"x"++))  Notes: • This runs in GHC 7.0, as required because this challenge was set in January 2011. It would be 16 characters shorter if I were allowed to assume GHC 7.10. Ungolfed version with documentation. 10 −19 characters ## Haskell, 342342 323 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 f=Td=T(i. \x nv->'(':fd n++'v++' ':x%n++"x%v++")")fd l f v="(λ "++v++". "++f(i(\_->v))%('x':v)++")" p s=readParen(0<1)q s++[(maybe T{}idp=q.lookup v,t)|(v,t)<-head.lex s] (f#g)x=f x$g x
q("(",'λ':s)=[|[(w,_:t)]<-lex s,(e,_:u)<-p t=(\g->T#l$e.(:g).(,)w,u) q("(",s)|(wf,'.':t)<-lexp s,(ex,_:u)<-p t] q s=[t=((a.f)#x,u)| q(fv,t)<-p s,)=(xmaybe T{}id.lookup v,us)<-p t] main=interactmain=interact$(\s->do\(f,[n]n)<-p s;f[]%"x"++[n]>f[]%"x"++n).p


Notes:

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

• This assumes input and output are terminated with exactly one newline. It would be 6 characters shorter with no newline handling, but I wasn’t sure if that’s allowed.

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

Ungolfed version with documentation.

## Haskell, 342 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 f=T(i. \x n->'(':f n++' ':x%n++")")f
l f v="(λ "++v++". "++f(i(\_->v))%('x':v)++")"
p s=readParen(0<1)q s++[(maybe T{}id.lookup v,t)|(v,t)<-lex s]
(f#g)x=f x$g x q('λ':s)=[(\g->T#l$e.(:g).(,)w,u)|(w,'.':t)<-lex s,(e,u)<-p t]
q s=[((a.f)#x,u)|(f,t)<-p s,(x,u)<-p t]
main=interact(\s->do(f,[n])<-p s;f[]%"x"++[n])


Notes:

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

• This assumes input and output are terminated with exactly one newline. It would be 6 characters shorter with no newline handling, but I wasn’t sure if that’s allowed.

Ungolfed version with documentation.

## Haskell, 342 323 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 v="(λ "++v++". "++f(i(\_->v))%('x':v)++")"
(f#g)x=f x$g x q("(",'λ':s)|[(w,_:t)]<-lex s,(e,_:u)<-p t=(\g->T#l$e.(:g).(,)w,u)
q("(",s)|(f,t)<-p s,(x,_:u)<-p t=((a.f)#x,u)
q(v,s)=(maybe T{}id.lookup v,s)
main=interact\$(\(f,n)->f[]%"x"++n).p


Notes:

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

Ungolfed version with documentation.

9 Grammar.
8 Fix to work with GHC 7.0, current as of January 2011.
7 Link to ungolfed version
6 −4 characters
5 −3 characters
4 −8 characters
3 Note about newline handling.
2 Note that my program works without the simplifying guarantee.
1