# User:Hakerh400/How to convert a lambda expression to SKI expressions

In this tutorial we show the most intuitive (but not the most efficient) algorithm for converting lambda expressions to SKI expressions.

## Definitions

A lambda expression can be either an identifier, an abstraction, or an application. Identifier consists of a string representing the identifier's name. Abstraction consists of a string representing the abstraction's argument, and abstraction's expression. Application consists of two expressions.

Identifier that is not bound to any abstraction is called a combinator. We recognize three combinators: `I`

, `K`

and `S`

. Combinator `I`

takes one argument and returns the argument itself. Combinator `K`

takes two arguments and returns the first one. Combinator `S`

takes three arguments `x`

, `y`

, and `z`

and returns `(xz)(yz)`

. The main difference between general lambda expressions and SKI expressions is that SKI does not contain abstractions. Our goal is to replace each abstraction with combinators `I`

, `K`

, `S`

and applications.

## Algorithm

Given a lambda expression. We consider the following cases:

- If it is an application, then convert both of its expressions to SKI
- If it is an abstraction and its expression is the abstraction's argument (for example
`(λa.a)`

), then return`I`

- If it is an abstraction and its expression is an identifier which is not the abstraction's argument (for example
`(λa.X)`

), then return`(K X)`

- If it is an abstraction and its expression is an application (for example
`(λa.XY)`

), then split the abstraction into two abstractions and move them into the application and prepend`S`

(resulting in`S(λa.X)(λa.Y)`

) - If it is an abstraction and its expression is an abstraction (for example
`(λa.λb.X)`

), then first convert the inner abstraction to SKi and then the outer one - If it is an abstraction and its expression is anything else, then remove the abstraction and prepend
`K`

before the expression - If it is anything else, then return it unchanged

## Implementation

Implementation in Haskell:

data Expr =
S | K | I |
Ide String |
Abs String Expr |
App Expr Expr
lam2ski :: *Expr* -> *Expr*
lam2ski (Abs a e) = case e of
Ide b -> if b == a then I else App K (Ide b)
Abs b c -> lam2ski (Abs a (lam2ski (Abs b c)))
App e1 e2 -> App (App S (lam2ski (Abs a e1))) (lam2ski (Abs a e2))
a -> App K a
lam2ski (App e1 e2) = App (lam2ski e1) (lam2ski e2)
lam2ski a = a

## Example

In this example we convert lambda expression `(λa.λb.ba)`

to SKI and display the result as string:

main :: *IO* *()*
main = *putStrLn* (*show* output)
input :: *Expr*
input = Abs "a" (Abs "b" (App (Ide "b") (Ide "a")))
output :: *Expr*
output = lam2ski input
instance *Show* *Expr* where
*show* x = show' x False where
show' x y = case x of
S -> "S"
K -> "K"
I -> "I"
(Ide a) -> s a
(Abs a e) -> t (s a ++ " -> " ++ *show* e)
(App e1 e2) -> if y then t r else r where
r :: *String*
r = *show* e1 ++ show' e2 True
where
m :: *String* -> *String* -> *String* -> *String*
m a b c = a ++ b ++ c
t :: *String* -> *String*
t a = m "(" a ")"
s :: *String* -> *String*
s a = m "[" a "]"

Output:

S(S(KS)(KI))(S(KK)I)