OT: Literature on translation of lambda calculus to combinators

Dušan Kolář

28 Jan 2010 28 Jan '10

4:54 a.m.

Dear cafe, Could anyone provide a link to some paper/book (electronic version of both preferred, even if not free) that describes an algorithm of translation of untyped lambda calculus expression to a set of combinators? Preferably SKI or BCKW. I'm either feeding google with wrong question or there is no link available now... Thanks, Dušan

Show replies by date

Max Bolingbroke

28 Jan 28 Jan

5:02 a.m.

New subject: OT: Literature on translation of lambda calculus to combinators

See, for example, slide 119 and onwards in the slides at http://www.cl.cam.ac.uk/teaching/0809/FFuncProg/FoFP_2009_slides.pdf The slides covers SKI and BCSKI. Cheers, Max 2010/1/28 Dušan Kolář :

...

Dear cafe,

Could anyone provide a link to some paper/book (electronic version of both preferred, even if not free) that describes an algorithm of translation of untyped lambda calculus expression to a set of combinators? Preferably SKI or BCKW. I'm either feeding google with wrong question or there is no link available now...

Thanks,

Dušan

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Serguey Zefirov

5:28 a.m.

New subject: OT: Literature on translation of lambda calculus to combinators

Also see http://www.haskell.org/haskellwiki/Super_combinator Wiki page. Fixed set of combinators gives you complexity of translation that is more than linear of the length of lambda expression. The length of output string is O(3^length(lambdaExpression)) for SK combinator pair. 2010/1/28 Dušan Kolář :

...

Dear cafe,

Could anyone provide a link to some paper/book (electronic version of both preferred, even if not free) that describes an algorithm of translation of untyped lambda calculus expression to a set of combinators? Preferably SKI or BCKW. I'm either feeding google with wrong question or there is no link available now...

Thanks,

Dušan

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Stephen Tetley

5:53 a.m.

New subject: OT: Literature on translation of lambda calculus to combinators

Hi Dušan The Ester shell written in Clean compiles via the SKI combinators. It is describe in the paper - 'A Functional Shell that Operates on Typed and Compiled Applications' by Arjen van Weelden and Rinus Plasmeijer which is available here: http://www.st.cs.ru.nl/papers/2004/plar2004-Esther_AFP.pdf Ester is part of the Clean 2.2 distribution, but I've had a quick look at it now and I suspect it has diverged a bit from the version described in the paper. The paper references Antoni Diller's 'Compiling Functional Languages' (Wiley - ISBN 0 471 92027 4) as the source of the algorithms they use. This book is long out of print but it is good and comprehensive. I got my copy second-hand from an affiliate on Amazon UK a few years ago after reading the Ester paper. Amazon UK currently has quite a few copies available - the £8+postage price is pretty cheap, the sellers will post internationally (caveat - I've no experience with any of the affiliates listed). There is a full implementation (in Pascal) in the appendix. Diller references David Turner's paper "A New Implementation Technique for Applicative Languages" (1979 "Software - Practice and Experience", vol 9, pp 31-49). If you have a university affiliation you should be able to source this, I haven't seen it myself. Best wishes Stephen

Job Vranish

9:23 a.m.

New subject: OT: Literature on translation of lambda calculus to combinators

There is a nice simple algorithm on wikipedia: http://en.wikipedia.org/wiki/Combinatory_logic (for both SKI and BCKW) translated to haskell: -- The anoying thing about the algorithm is that it is difficult to separate the SKI and LC expression types -- it's easiest to just combine them. data Expr = Apply Expr Expr | Lambda String Expr | Id String | S | K | I deriving (Show) convert (Apply a b) = Apply (convert a) (convert b) convert (Lambda x e) | not $ occursFree x e = Apply K (convert e) convert (Lambda x (Id s)) | x == s = I convert (Lambda x (Lambda y e)) | occursFree x e = convert (Lambda x (convert (Lambda y e))) convert (Lambda x (Apply e1 e2)) = Apply (Apply S (convert $ Lambda x e1)) (convert $ Lambda x e2) convert x = x occursFree var (Apply a b) = (occursFree var a) || (occursFree var b) occursFree var (Lambda a b) = if a == var then False else (occursFree var b) occursFree var (Id a) = if a == var then True else False occursFree var _ = False testExpr = Lambda "x" $ Lambda "y" $ Apply (Id "y") (Id "x") test = convert testExpr Hope that helps, - Job 2010/1/28 Dušan Kolář

...

Dear cafe,

Could anyone provide a link to some paper/book (electronic version of both preferred, even if not free) that describes an algorithm of translation of untyped lambda calculus expression to a set of combinators? Preferably SKI or BCKW. I'm either feeding google with wrong question or there is no link available now...

Thanks,

Dušan

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Felipe Lessa

10:21 a.m.

New subject: OT: Literature on translation of lambda calculus to combinators

On Thu, Jan 28, 2010 at 09:23:23AM -0500, Job Vranish wrote:

...

-- The anoying thing about the algorithm is that it is difficult to separate the SKI and LC expression types -- it's easiest to just combine them.

Why is it difficult? -- Felipe.

Job Vranish

11:48 a.m.

New subject: OT: Literature on translation of lambda calculus to combinators

...

Why is it difficult?

Ideally we'd like the type of convert to be something like: convert :: LambdaExpr -> SKIExpr but this breaks in several places, such as the nested converts in the RHS of the rule: convert (Lambda x (Lambda y e)) | occursFree x e = convert (Lambda x (convert (Lambda y e))) A while ago I tried modifying the algorithm to be pure top-down so that it wouldn't have this problem, but I didn't have much luck. Anybody know of a way to fix this? - Job On Thu, Jan 28, 2010 at 10:21 AM, Felipe Lessa wrote:

...

On Thu, Jan 28, 2010 at 09:23:23AM -0500, Job Vranish wrote:

...
-- The anoying thing about the algorithm is that it is difficult to separate the SKI and LC expression types -- it's easiest to just combine them.

Why is it difficult?

-- Felipe. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Nick Smallbone

29 Jan 29 Jan

4:33 a.m.

New subject: OT: Literature on translation of lambda calculus to combinators

Job Vranish writes:

...

Ideally we'd like the type of convert to be something like: convert :: LambdaExpr -> SKIExpr but this breaks in several places, such as the nested converts in the RHS of the rule: convert (Lambda x (Lambda y e)) | occursFree x e = convert (Lambda x (convert (Lambda y e)))

A while ago I tried modifying the algorithm to be pure top-down so that it wouldn't have this problem, but I didn't have much luck.

Anybody know of a way to fix this?

The way to do it is, when you see an expression Lambda x e, first convert e to a combinatory expression (which will have x as a free variable, and will obviously have no lambdas). Then you don't need nested converts at all. Not-really-tested code follows. Nick data Lambda = Var String | Apply Lambda Lambda | Lambda String Lambda deriving Show data Combinatory = VarC String | ApplyC Combinatory Combinatory | S | K | I deriving Show compile :: Lambda -> Combinatory compile (Var x) = VarC x compile (Apply t u) = ApplyC (compile t) (compile u) compile (Lambda x t) = lambda x (compile t) lambda :: String -> Combinatory -> Combinatory lambda x t | x `notElem` vars t = ApplyC K t lambda x (VarC y) | x == y = I lambda x (ApplyC t u) = ApplyC (ApplyC S (lambda x t)) (lambda x u) vars :: Combinatory -> [String] vars (VarC x) = [x] vars (ApplyC t u) = vars t ++ vars u vars _ = []

Job Vranish

10:35 a.m.

New subject: OT: Literature on translation of lambda calculus to combinators

Cool, Thanks :D also quickcheck says the two algorithms are equivalent :) On Fri, Jan 29, 2010 at 4:33 AM, Nick Smallbone wrote:

...

Job Vranish writes:

...
Ideally we'd like the type of convert to be something like: convert :: LambdaExpr -> SKIExpr but this breaks in several places, such as the nested converts in the RHS of the rule: convert (Lambda x (Lambda y e)) | occursFree x e = convert (Lambda x (convert (Lambda y e)))

A while ago I tried modifying the algorithm to be pure top-down so that it wouldn't have this problem, but I didn't have much luck.

Anybody know of a way to fix this?

The way to do it is, when you see an expression Lambda x e, first convert e to a combinatory expression (which will have x as a free variable, and will obviously have no lambdas). Then you don't need nested converts at all.

Not-really-tested code follows.

Nick

data Lambda = Var String | Apply Lambda Lambda | Lambda String Lambda deriving Show

data Combinatory = VarC String | ApplyC Combinatory Combinatory | S | K | I deriving Show

compile :: Lambda -> Combinatory compile (Var x) = VarC x compile (Apply t u) = ApplyC (compile t) (compile u) compile (Lambda x t) = lambda x (compile t)

lambda :: String -> Combinatory -> Combinatory lambda x t | x `notElem` vars t = ApplyC K t lambda x (VarC y) | x == y = I lambda x (ApplyC t u) = ApplyC (ApplyC S (lambda x t)) (lambda x u)

vars :: Combinatory -> [String] vars (VarC x) = [x] vars (ApplyC t u) = vars t ++ vars u vars _ = []

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Torsten Grust

1 Feb 1 Feb

3:14 a.m.

New subject: OT: Literature on translation of lambda calculus to combinators

Dear all, Dušan Kolář writes:

...

[...] Could anyone provide a link to some paper/book (electronic version of both preferred, even if not free) that describes an algorithm of translation of untyped lambda calculus expression to a set of combinators? Preferably SKI or BCKW. I'm either feeding google with wrong question or there is no link available now...

13 years ago (ugh...) I've posted a tutorial-style treatment of the compilation of Dave Turner's SASL to SKI. Also addresses reduction and simple optimizations of the resulting SKI programs. http://www-db.informatik.uni-tuebingen.de/files/publications/sasl.ps.gz Cheers, —Torsten

Matthias Görgens

8:48 a.m.

New subject: OT: Literature on translation of lambda calculus to combinators

Dear Dušan, You can also find an algorithm in everyone's favourite book in combinatorial logic "To Mock a Mockingbird" (http://en.wikipedia.org/wiki/To_Mock_a_Mockingbird). Cheers, Matthias.

Hans Aberg

10:04 a.m.

New subject: OT: Literature on translation of lambda calculus to combinators

On 28 Jan 2010, at 10:54, Dušan Kolář wrote:

...

Could anyone provide a link to some paper/book (electronic version of both preferred, even if not free) that describes an algorithm of translation of untyped lambda calculus expression to a set of combinators? Preferably SKI or BCKW. I'm either feeding google with wrong question or there is no link available now...

Here is a paper that uses that standard arithmetic operators that Church defined: http://www.dcs.ed.ac.uk/home/pgh/amen.ps Hans

5587

Age (days ago)

5591

Last active (days ago)

List overview

Download

11 comments

10 participants

participants (10)

Dušan Kolář
Felipe Lessa
Hans Aberg
Job Vranish
Matthias Görgens
Max Bolingbroke
Nick Smallbone
Serguey Zefirov
Stephen Tetley
Torsten Grust