6

假设有一些数据类型来表达 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₁ E₂)] => (T[E₁] T[E₂])

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] => 我

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₁ E₂)] => (ST[λx.E₁] 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)正确表述呢？

4

4 回答 4

1

这里最好为组合器和 lambda 表达式提供一个通用的数据类型。请注意，您的类型已经有很大的重叠（Var, App），并且在 lambda 表达式中使用组合子并没有什么坏处。

我们要消除的唯一可能性是在组合子术语中使用 lambda 抽象。我们可以使用索引类型来禁止它们。

在下面的代码中，术语的类型由该术语中嵌套的 lambda 抽象的数量参数化。convert函数返回Term Z a，这里的Z意思是零，所以返回的项中没有 lambda 抽象。

有关单例类型的更多信息（此处使用了一点），请参阅论文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
于 2012-10-22T08:35:27.977 回答
1

让我们考虑方程 T[λx.λy.E] => T[λx.T[λy.E]]。

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

因此 T[λx.T[λy.E]] 中的外层 T 必须是情况 3 或 6 之一。您可以在代码中进行这种情况分析。对不起，我没有时间写出来。

于 2012-10-21T21:18:22.620 回答
1

关键的见解是 S、K 和 I 只是常数 Lam 项，就像 1、2 和 3 是常数 Ints 一样。通过对“转换”函数进行逆操作来进行规则 5 类型检查将非常容易：

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)

现在我们可以使用 'nvert' 来进行规则 5 类型检查：

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

我们可以看到左边和右边是相同的（我们将忽略守卫），除了左边的 'Abs y e' 被右边的 'nvert (convert (Abs ye))' 替换。由于 'convert' 和 'nvert' 互为倒数，我们总是可以用 'nvert (convert x)' 替换任何 Lam 'x' ，同样我们总是可以用 'convert (nvert x)' 替换任何 SKI 'x' ，所以这是一个有效的方程。

不幸的是，虽然它是一个有效的方程，但它不是一个有用的函数定义，因为它不会导致计算进行：我们只会永远来回转换'Abs y e'！

为了打破这个循环，我们可以用“提醒”替换对“nvert”的调用，我们应该稍后再做。我们通过向 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)

现在规则 5 使用这个提醒而不是“nvert”：

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

现在我们需要兑现我们回来的承诺，制定一个单独的规则，用对“nvert”的实际调用替换提醒，如下所示：

convert (Com c) = convert (nvert c)

现在我们终于可以打破循环了：我们知道 'convert (nvert c)' 总是与 'c' 相同，所以我们可以将上面的行替换为：

convert (Com c) = c

请注意，我们对“convert”的最终定义实际上根本没有使用“nvert”！不过，它仍然是一个方便的功能，因为涉及 Lam 的其他功能可以使用它来处理新的“Com”案例。

你可能已经注意到我实际上将这个构造函数命名为“Com”，因为它只是一个包装好的 COMbinator，但我认为采取稍微长一点的路线比仅仅说“在 Lams 中包装你的 SKI”更能提供信息:)

如果您想知道为什么我将该功能称为“nvert”，请参阅http://unapologetic.wordpress.com/2007/05/31/duality-terminology/ :)

于 2014-01-24T17:09:16.130 回答
1

Warbo 是对的，组合子是常数 lambda 项，因此转换函数是
T[ ]:L -> CL 是 lambda 项的集合，C 是组合项的集合，并且 C ⊂ L 。

所以规则没有打字问题T[λx.λy.E] => T[λx.T[λy.E]]

这是Scala中的一个实现。

于 2016-01-09T17:46:09.633 回答