从lambda项转换为组合项

Question

假设有一些数据类型来表达lambda和组合术语:

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)

还有一个函数来获取lambda术语的自由变量列表:

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

要将lambda术语转换为组合术语,抽象消除规则可能很有用:

convert ? Eq ? ? Lam ? ? SKI ?

1)T [x] => x

convert (Var x) = V x

2)T [(E 1 E 2)] =>(T [E 1] T [E 2])

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

3)T [λx.E] =>(KT [E])(如果x在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]](如果x在E中自由出现)

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

6)T [λx.(E 1 E 2)] =>(ST [λx.E1] T [λx.E₂])

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

convert  _ = error ":["

此定义无效,因为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)))'

那么,我现在拥有的是:

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

我想要的是(希望我算得对):

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

问题:

如果lambda术语和组合术语具有不同类型的表达式,那么如何5)正确表达？

Answer 1

让我们考虑方程 T[\xce\xbbx.\xce\xbby.E] => T[\xce\xbbx.T[\xce\xbby.E]]。

\n\n

我们知道 T[\xce\xbby.E] 的结果是一个 SKI 表达式。由于它是由情况 3、4 或 6 之一产生的，因此它要么是 I，要么是应用程序 ( :@)。

\n\n

因此 T[\xce\xbbx.T[\xce\xbby.E]] 中的外层 T 一定是情况 3 或 6 之一。您可以在代码中进行这种情况分析。抱歉，我没有时间写出来。

\n