12 −12 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

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.

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.

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.

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.