Return to Answer

Haskell, 342 323 317317 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)++")"
(?)=q.head.lex
(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=f`T`\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 z`a`x 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 1613 characters shorter if I were allowed to assume GHC 7.10.

Ungolfed version with documentation.

Haskell, 342 323323 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)++")"
p=q(?)=q.head.lex
(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, 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.