Conversion from lambda term to combinatorial term

Question

Suppose there are some data types to express lambda and combinatorial terms:

data Lam α = Var α                   -- v
           | Abs α (Lam α)           -- λv . e1
           | App (Lam α) (Lam α)     -- e1 e2
             deriving (Eq, Show)

infixl 0 :@
data SKI α = V α                     -- x
           | SKI α :@ SKI α          -- e1 e2
           | I                       -- I
           | K                       -- K
           | S                       -- S
             deriving (Eq, Show)

There is also a function to get a list of lambda term's free variables:

fv ∷ Eq α ⇒ Lam α → [α]
fv (Var v) = [v]
fv (Abs x e) = filter (/= x) $ fv e
fv (App e1 e2) = fv e1 ++ fv e2

To convert lambda term to combinatorial term abstract elimination rules could be usefull:

convert ∷ Eq α ⇒ Lam α → SKI α

1) T[x] => x

convert (Var x) = V x

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

convert (App e1 e2) = (convert e1) :@ (convert e2)

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

convert (Abs x e) | x `notElem` fv e = K :@ (convert e)

4) T[λx.x] => I

convert (Abs x (Var y)) = if x == y then I else K :@ V y

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

convert (Abs x (Abs y e)) | x `elem` fv e = convert (Abs x (convert (Abs y e)))

6) T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂])

convert (Abs x (App y z)) = S :@ (convert (Abs x y)) :@ (convert (Abs x z))

convert  _ = error ":["

This definition is not valid because of 5):

Couldn't match expected type `Lam α' with actual type `SKI α'
In the return type of a call of `convert'
In the second argument of `Abs', namely `(convert (Abs y e))'
In the first argument of `convert', namely
  `(Abs x (convert (Abs y e)))'

So, what I have now is:

> convert $ Abs "x" $ Abs "y" $ App (Var "y") (Var "x")
*** Exception: :[

What I want is (hope I calculate it right):

> convert $ Abs "x" $ Abs "y" $ App (Var "y") (Var "x")
S :@ (S (KS) (S (KK) I)) (S (KK) I)

Question:

If lambda term and combinatorial term have a different types of expression, how 5) could be formulated right?

Pelota

Your fv is wrong, btw: it should be fv (Abs x e) = filter (/= x) $ fv e – Can

Your fix is not sufficient: consider the term \x -> x x. – Can

Answer 1

Let's consider the equation T[λx.λy.E] => T[λx.T[λy.E]].

We know the result of T[λy.E] is an SKI expression. Since it has been produced by one of the cases 3, 4 or 6, it is either I or an application (:@).

Thus the outer T in T[λx.T[λy.E]] must be one of the cases 3 or 6. You can perform this case analysis in the code. I'm sorry but I don't have the time to write it out.

Crepuscule

Answer 2

Here it's better to have a common data type for combinators and lambda expressions. Notice that your types already have significant overlap (Var, App), and it doesn't hurt to have combinators in lambda expressions.

The only possibility we want to eliminate is having lambda abstractions in combinator terms. We can forbid them using indexed types.

In the following code the type of a term is parameterised by the number of nested lambda abstractions in that term. The convert function returns Term Z a, where Z means zero, so there are no lambda abstractions in the returned term.

For more information about singleton types (which are used a bit here), see the paper Dependently Typed Programming with Singletons.

{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, GADTs, TypeOperators,
    ScopedTypeVariables, MultiParamTypeClasses, FlexibleInstances #-}

data Nat = Z | Inc Nat

data SNat :: Nat -> * where
  SZ :: SNat Z
  SInc :: NatSingleton n => SNat n -> SNat (Inc n)

class NatSingleton (a :: Nat) where
  sing :: SNat a

instance NatSingleton Z where sing = SZ
instance NatSingleton a => NatSingleton (Inc a) where sing = SInc sing

type family Max (a :: Nat) (b :: Nat) :: Nat
type instance Max Z a = a
type instance Max a Z = a
type instance Max (Inc a) (Inc b) = Inc (Max a b)

data Term (l :: Nat) a where
  Var :: a -> Term Z a
  Abs :: NatSingleton l => a -> Term l a -> Term (Inc l) a
  App :: (NatSingleton l1, NatSingleton l2)
      => Term l1 a -> Term l2 a -> Term (Max l1 l2) a
  I   :: Term Z a
  K   :: Term Z a
  S   :: Term Z a

fv :: Eq a => Term l a -> [a]
fv (Var v) = [v]
fv (Abs x e) = filter (/= x) $ fv e
fv (App e1 e2) = fv e1 ++ fv e2
fv _ = []

eliminateLambda :: (Eq a, NatSingleton l) => Term (Inc l) a -> Term l a
eliminateLambda t =
  case t of
    Abs x t ->
      case t of
        Var y
          | y == x -> I
          | otherwise -> App K (Var y)
        Abs {} -> Abs x $ eliminateLambda t
        App a b -> S `App` (eliminateLambda $ Abs x a)
                     `App` (eliminateLambda $ Abs x b)
    App a b -> eliminateLambdaApp a b

eliminateLambdaApp
  :: forall a l1 l2 l . 
     (Eq a, Max l1 l2 ~ Inc l,
      NatSingleton l1,
      NatSingleton l2)
  => Term l1 a -> Term l2 a -> Term l a
eliminateLambdaApp a b =
  case (sing :: SNat l1, sing :: SNat l2) of
    (SInc _, SZ    ) -> App (eliminateLambda a) b
    (SZ    , SInc _) -> App a (eliminateLambda b)
    (SInc _, SInc _) -> App (eliminateLambda a) (eliminateLambda b)

convert :: forall a l . Eq a => NatSingleton l => Term l a -> Term Z a
convert t =
  case sing :: SNat l of
    SZ -> t
    SInc _ -> convert $ eliminateLambda t

Can

it typechecks well :t convert $ Abs "x" $ Abs "y" $ App (Var "y") (Var "x") :: (Eq a, Data.String.IsString a) => Term 'Z a, but how it could be evaluated? – Hendiadys

Answer 3

The key insight is that S, K and I are just constant Lam terms, in the same way that 1, 2 and 3 are constant Ints. It would be pretty easy to make rule 5 type-check by making an inverse to the 'convert' function:

nvert :: SKI a -> Lam a
nvert S = Abs "x" (Abs "y" (Abs "z" (App (App (Var "x") (Var "z")) (App (Var "y") (Var "z")))))
nvert K = Abs "x" (Abs "y" (Var "x"))
nvert I = Abs "x" (Var "x")
nvert (V x) = Var x
nvert (x :@ y) = App (nvert x) (nvert y)

Now we can use 'nvert' to make rule 5 type-check:

convert (Abs x (Abs y e)) | x `elem` fv e = convert (Abs x (nvert (convert (Abs y e))))

We can see that the left and the right are identical (we'll ignore the guard), except that 'Abs y e' on the left is replaced by 'nvert (convert (Abs y e))' on the right. Since 'convert' and 'nvert' are each others' inverse, we can always replace any Lam 'x' with 'nvert (convert x)' and likewise we can always replace any SKI 'x' with 'convert (nvert x)', so this is a valid equation.

Unfortunately, while it's a valid equation it's not a useful function definition because it won't cause the computation to progress: we'll just convert 'Abs y e' back and forth forever!

To break this loop we can replace the call to 'nvert' with a 'reminder' that we should do it later. We do this by adding a new constructor to Lam:

data Lam a = Var a                   -- v
           | Abs a (Lam a)           -- \v . e1
           | App (Lam a) (Lam a)     -- e1 e2
           | Com (SKI a)             -- Reminder to COMe back later and nvert
             deriving (Eq, Show)

Now rule 5 uses this reminder instead of 'nvert':

convert (Abs x (Abs y e)) | x `elem` fv e = convert (Abs x (Com (convert (Abs y e))))

Now we need to make good our promise to come back, by making a separate rule to replace reminders with actual calls to 'nvert', like this:

convert (Com c) = convert (nvert c)

Now we can finally break the loop: we know that 'convert (nvert c)' is always identical to 'c', so we can replace the above line with this:

convert (Com c) = c

Notice that our final definition of 'convert' doesn't actually use 'nvert' at all! It's still a handy function though, since other functions involving Lam can use it to handle the new 'Com' case.

You've probably noticed that I've actually named this constructor 'Com' because it's just a wrapped-up COMbinator, but I thought it would be more informative to take a slightly longer route than just saying "wrap up your SKIs in Lams" :)

If you're wondering why I called that function "nvert", see http://unapologetic.wordpress.com/2007/05/31/duality-terminology/ :)

Closer

Answer 4

Warbo is right, combinators are constant lambda terms, consequently the conversion function is
T[ ]:L -> C with L the set of lambda terms and C that of combinatory terms and with C ⊂ L .

So there is no typing problem for the rule T[λx.λy.E] => T[λx.T[λy.E]]

Here an implementation in Scala.

Valida