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)