CODEWITHSUNDEEP
haskell
Student
Student

Reputation: 1

Converting numerical expressions to lambda calculus in Haskell

Trying to make a function that converts any given numerical expression to its lambda calculus equivalent.

To do this, I've made two functions; an encode function and subst. Below are the relevant bits of my code. However, when I run my encode function, it doesn't encode multiplication expressions properly; i.e I think I've written my Add/Mul lines of code in the encode function wrong. However, I can't work out how to fix this. When I run encode (ArithmeticNum 2) and encode (SecApp (Section (ArithmeticNum 1)) (ArithmeticNum 1)) , it produces the expected output, however. Can someone help me on fixing the Add/Mul bits of the encode function so it works in all cases?

I know the multiplication syntax for encoding would look like mul n m = \s -> \z -> n (m s) z, but I'm not sure how I would write this in my encode function. Could someone help me with this bit? Thanks.

data Lambda = LamdaApp Lambda Lambda | LambdaAbs Int Lambda | LambdaVar Int deriving (Show,Eq)

data ArithmeticExpr = Add ArithmeticExpr ArithmeticExpr | Mul ArithmeticExpr ArithmeticExpr | Section ArithmeticExpr | SecApp ArithmeticExpr ArithmeticExpr | ArithmeticNum Int deriving (Show, Eq,Read)

subst :: LambdaExpr -> Int -> LambdaExpr -> LambdaExpr
subst (LambdaVar x) y e | x == y = e
subst (LambdaVar x) y e | x /= y = LambdaVar x
subst (LambdaAbs x e1) y e |  
  x /= y && not (free x e) = LambdaAbs x (subst e1 y e)
subst (LambdaAbs x e1) y e |
    x /=y && (free x e) = let x' = rename x y in
          subst (LambdaAbs x' (subst e1 x (LambdaVar x'))) y e

subst (LambdaAbs x e1) y e | x == y = LambdaAbs x e1
subst (LambdaApp e1 e2) y e = LambdaApp (subst e1 y e) (subst e2 y e)


free :: Int -> LambdaExpr -> Bool
free x (LambdaVar y) = x == y
free x (LambdaAbs y e) | x == y = False
free x (LambdaAbs y e) | x /= y = free x e
free x (LambdaApp e1 e2) = (free x e1) || (free x e2)


rename :: Int -> Int -> Int
rename x y = (max x y) + 1

encode:: ArithmeticExpr -> LambdaExpr
encode(ArithmeticNum 0) = LambdaAbs 0 (LambdaAbs 1 (LambdaVar 1))
encode(ArithmeticNum n) = LambdaAbs 0 (LambdaAbs 1 (helper n 0 1))
    where helper :: Int -> Int -> Int -> LambdaExpr
          helper 0 _ _ = LambdaVar 1
          helper n f x = LambdaApp (LambdaVar f) (helper (n - 1) f x)

encode (Add e1 e2) = LambdaAbs 0 (LambdaAbs 1 ( LambdaApp (LambdaApp (encode e1) (LambdaVar 0)) (LambdaApp (LambdaApp (encode e2) (LambdaVar 0)) (LambdaVar 1))))
encode (Mul e1 e2) = LambdaAbs 0 (LambdaAbs 1 (LambdaAbs 2 (LambdaAbs 3 (LambdaApp (LambdaApp (LambdaVar 0) (encode e1)) (LambdaApp (LambdaVar 1) (encode e2))))))  
encode (SecApp (Section op) e1) = LambdaApp (LambdaApp (encode op) (encode e1)) (encode (ArithmeticNum 1))
encode (Section (ArithmeticNum n)) = LambdaAbs 0 (LambdaAbs 1 (LambdaApp (LambdaVar 0) (encode (ArithmeticNum n))))

Upvotes: 0

Views: 224

Answers (1)

Noughtmare
Noughtmare

Reputation: 10645

As you say, multiplication in the Church Encoding (there are other encodings) is done as follows:

mul n m = \s -> \z -> n (m s) z

Just taking this line:

encode (Mul e1 e2) = LambdaAbs 0 (LambdaAbs 1 (LambdaAbs 2 (LambdaAbs 3 (LambdaApp (LambdaApp (LambdaVar 0) (encode e1)) (LambdaApp (LambdaVar 1) (encode e2))))))

I'd say it corresponds to this in the more direct notation (assuming numbers are valid variable names):

mul e1 e2 = \0 -> \1 -> \2 -> \3 -> (0 e1) (1 e2)

So, I'd say one mistake is to have the encoded multiplication take four arguments where it should only take two. Multiplication on its own should indeed take four arguments, but in this case you are translating a multiplication that is already applied to the arguments e1 and e2, so there are only two left. And the inner body of the lambda is also incorrect. You'd want this:

mul e1 e2 = \0 -> \1 -> e1 (e2 0) 1

Which is equivalant to the equation at the top of this answer.

Upvotes: 1

Related Questions