CODEWITHSUNDEEP
haskelllambda-calculuscombinators
user17732759
user17732759

Reputation:

Implementing SKI transformation

I need to implement the following algorithm in order to convert Lambda Calculus into Combinatory Logic.

The rules are from https://en.wikipedia.org/wiki/Combinatory_logic#Completeness_of_the_S-K_basis

T[x] => x

T[(E₁ E₂)] => (T[E₁] T[E₂])

T[λx.E] => (K T[E]) (if x does not occur free in E)

T[λx.x] => I

T[λx.λy.E] => T[λx.T[λy.E]] (if x occurs free in E)

T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂]) (if x occurs free in E₁ or E₂)

This is what I have so far:

data CLExpr  =  S | K | I | CLVar Int | CLApp CLExpr CLExpr 

data LamExpr  =  LamApp LamExpr LamExpr  |  LamAbs Int LamExpr  |  LamVar Int 

skiTransform :: LamExpr -> CLExpr

skiTransform (LamVar x) = CLVar x --Rule 1

skiTransform (LamAbs y (s)) 
           | (free y s == False) = K (skiTransform(s)) --Rule 3

skiTransform (LamAbs x (LamVar y)) 
           | x == y     = I --Rule 4

skiTransform (LamAbs x (LamAbs y (s))) 
           | (free x s) = skiTransform 
                            (LamAbs x (skiTransform (LamAbs y (s)))) --Rule 5

free :: Int -> LamExpr -> Bool
free x (LamVar y) = x == y
free x (LamAbs y e) | x == y = False
free x (LamAbs y e) | x /= y = free x e
free x (LamApp e f) = (free x e) || (free x f)

The problem I have is, in rule 5, how to 'nest' my transformation functions as shown at the top. The inner transformation creates the type CLExpr, which then can't be used as an input for the outer transformation.

I also am not sure how to implement rule 2 and 6, which require seperating two expressions next to each other, but that isn't a priority yet.

Thanks!

Upvotes: 0

Views: 537

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33389

To handle this nesting, you can widen the source language to a superset of both the source and target language (or said another way, generalize LamExpr to include constants).

-- The "union" of LamExpr and CLExpr
data LamCLExpr = S' | K' | I' | LCLVar Int | LCLApp CLExpr CLExpr | LCLAbs Int LamCLExpr

Then you can define injections from the two languages

fromLam :: LamExpr -> LamCLExpr
fromCL :: CLExpr -> LamCLExpr

And that allows you to define the transformation

skiTransform :: LamCLExpr -> CLExpr

notably using fromCL in the nested case.

Upvotes: 4

Related Questions