15

给定一个至少有n参数的函数，我想旋转第一个参数，使其成为第nth 个参数。例如（在无类型 lambda 演算中）：

r(λa. a)                   = λa. a
r(λa. λb. a b)             = λb. λa. a b
r(λa. λb. λc. a b c)       = λb. λc. λa. a b c
r(λa. λb. λc. λd. a b c d) = λb. λc. λd. λa. a b c d

等等。

你能用r一般的方式写吗？如果你知道n >= 2怎么办？

这是Scala中陈述的问题：

trait E
case class Lam(i: E => E) extends E
case class Lit(i: Int) extends E
case class Ap(e: E, e: E) extends E

例如，旋转应该采取Lam(a => Lam(b => Lam(c => Ap(Ap(a, b), c))))并返回Lam(b => Lam(c => Lam(a => Ap(Ap(a, b), c))))。

4

7 回答 7

7

诀窍是标记所涉及函数的“最终”值，因为对于普通的haskell，两者a -> b都a -> (b->c)只是单个变量的函数。但是，如果我们这样做，我们可以做到这一点。

{-# LANGUAGE TypeFamilies,FlexibleInstances,FlexibleContexts #-}
module Rotate where

data Result a = Result a

class Rotate f where
  type After f
  rotate :: f -> After f

instance Rotate (a -> Result b) where
  type After (a -> Result b) = a -> Result b
  rotate = id

instance Rotate (a -> c) => Rotate (a -> b -> c) where
  type After (a -> b -> c) = b -> After (a -> c)
  rotate = (rotate .) . flip

然后，查看它的实际效果：

f0 :: Result a
f0 = Result undefined

f1 :: Int -> Result a
f1 = const f0

f2 :: Char -> Int -> Result a
f2 = const f1

f3 :: Float -> Char -> Int -> Result a
f3 = const f2

f1' :: Int -> Result a
f1' = rotate f1

f2' :: Int -> Char -> Result a
f2' = rotate f2

f3' :: Char -> Int -> Float -> Result a
f3' = rotate f3
于 2011-03-04T18:14:34.487 回答
5

在不违反 HOAS 的“合法性”的情况下，这可能是不可能的，因为它E => E不仅必须用于对象语言中的绑定，还必须用于元语言中的计算。也就是说，这是 Haskell 中的一个解决方案。它滥用一个Literal节点来放入一个唯一的 ID 以供以后替换。享受！

import Control.Monad.State

-- HOAS representation
data Expr = Lam (Expr -> Expr)
          | App Expr Expr
          | Lit Integer

-- Rotate transformation
rot :: Expr -> Expr
rot e = case e of
  Lam f -> descend uniqueID (f (Lit uniqueID))
  _ -> e
  where uniqueID = 1 + maxLit e

descend :: Integer -> Expr -> Expr
descend i (Lam f) = Lam $ descend i . f
descend i e = Lam $ \a -> replace i a e

replace :: Integer -> Expr -> Expr -> Expr
replace i e (Lam f) = Lam $ replace i e . f
replace i e (App e1 e2) = App (replace i e e1) (replace i e e2)
replace i e (Lit j)
  | i == j = e
  | otherwise = Lit j

maxLit :: Expr -> Integer
maxLit e = execState (maxLit' e) (-2)
  where maxLit' (Lam f) = maxLit' (f (Lit 0))
        maxLit' (App e1 e2) = maxLit' e1 >> maxLit' e2
        maxLit' (Lit i) = get >>= \k -> when (i > k) (put i)

-- Output
toStr :: Integer -> Expr -> State Integer String
toStr k e = toStr' e
  where toStr' (Lit i)
          | i >= k = return $ 'x':show i -- variable
          | otherwise = return $ show i  -- literal
        toStr' (App e1 e2) = do
          s1 <- toStr' e1
          s2 <- toStr' e2
          return $ "(" ++ s1 ++ " " ++ s2 ++ ")"
        toStr' (Lam f) = do
          i <- get
          modify (+ 1)
          s <- toStr' (f (Lit i))
          return $ "\\x" ++ show i ++ " " ++ s

instance Show Expr where
  show e = evalState (toStr m e) m
    where m = 2 + maxLit e

-- Examples
ex2, ex3, ex4 :: Expr

ex2 = Lam(\a -> Lam(\b -> App a (App b (Lit 3))))
ex3 = Lam(\a -> Lam(\b -> Lam(\c -> App a (App b c))))
ex4 = Lam(\a -> Lam(\b -> Lam(\c -> Lam(\d -> App (App a b) (App c d)))))

check :: Expr -> IO ()
check e = putStrLn(show e ++ " ===> \n" ++ show (rot e) ++ "\n")

main = check ex2 >> check ex3 >> check ex4

结果如下：

\x5 \x6 (x5 (x6 3)) ===> 
\x5 \x6 (x6 (x5 3))

\x2 \x3 \x4 (x2 (x3 x4)) ===> 
\x2 \x3 \x4 (x4 (x2 x3))

\x2 \x3 \x4 \x5 ((x2 x3) (x4 x5)) ===> 
\x2 \x3 \x4 \x5 ((x5 x2) (x3 x4))

（不要被看起来相似的变量名所迷惑。这是您寻求的旋转，模 alpha 转换。）

于 2011-03-04T04:49:23.097 回答
4

是的，我正在发布另一个答案。而且它可能仍然不是您想要的。但我认为它可能仍然有用。它在哈斯克尔。

data LExpr = Lambda Char LExpr
           | Atom Char
           | App LExpr LExpr

instance Show LExpr where
    show (Atom c) = [c]
    show (App l r) = "(" ++ show l ++ " " ++ show r ++ ")"
    show (Lambda c expr) = "(λ" ++ [c] ++ ". " ++ show expr ++ ")"

所以在这里我设计了一个基本的代数数据类型来表达 lambda 演算。我添加了一个简单但有效的自定义 Show 实例。

ghci> App (Lambda 'a' (Atom 'a')) (Atom 'b')
((λa. a) b)

为了好玩，我使用了一个简单的reduce方法，使用 helper replace。警告：未经仔细考虑或测试。请勿用于工业用途。无法处理某些讨厌的表达。:P

reduce (App (Lambda c target) expr) = reduce $ replace c (reduce expr) target
reduce v = v

replace c expr av@(Atom v)
    | v == c    = expr
    | otherwise = av
replace c expr ap@(App l r)
                = App (replace c expr l) (replace c expr r)
replace c expr lv@(Lambda v e)
    | v == c    = lv
    | otherwise = (Lambda v (replace c expr e))

它似乎有效，尽管这真的只是我走神了。（it在 ghci 中是指在提示符处评估的最后一个值）

ghci> reduce it
b

所以现在是有趣的部分，rotate. 所以我想我可以剥掉第一层，如果是 Lambda，那太好了，我会保存标识符并继续向下钻取，直到遇到非 Lambda。然后我将把 Lambda 和标识符放回“最后”位置。如果它一开始就不是 Lambda，那么什么也不做。

rotate (Lambda c e) = drill e
    where drill (Lambda c' e') = Lambda c' (drill e') -- keep drilling
          drill e' = Lambda c e'       -- hit a non-Lambda, put c back
rotate e = e

原谅没有想象力的变量名称。通过 ghci 发送它显示出良好的迹象：

ghci> Lambda 'a' (Atom 'a')
(λa. a)
ghci> rotate it
(λa. a)
ghci> Lambda 'a' (Lambda 'b' (App (Atom 'a') (Atom 'b')))
(λa. (λb. (a b)))
ghci> rotate it
(λb. (λa. (a b)))
ghci> Lambda 'a' (Lambda 'b' (Lambda 'c' (App (App (Atom 'a') (Atom 'b')) (Atom 'c'))))
(λa. (λb. (λc. ((a b) c))))
ghci> rotate it
(λb. (λc. (λa. ((a b) c))))
于 2011-03-04T04:09:34.673 回答
3

使用模板 haskell 执行此操作的一种方法是：

有了这两个功能：

import Language.Haskell.TH

rotateFunc   :: Int -> Exp
rotateFunc n = LamE (map VarP vars) $ foldl1 AppE $ map VarE $ (f:vs) ++ [v]
    where vars@(f:v:vs) = map (\i -> mkName $ "x" ++ (show i)) [1..n]

getNumOfParams :: Info -> Int
getNumOfParams (VarI _ (ForallT xs _ _) _ _) = length xs + 1

然后对于myF具有可变数量参数的函数，您可以这样旋转它们：

$(return $ rotateFunc $ read $(stringE . show =<< (reify 'myF >>= return . getNumOfParams))) myF

使用 TH 肯定有更简洁的方法，我对它很陌生。

于 2011-03-05T00:15:50.663 回答
1

好的，感谢所有提供答案的人。这是我最终采用的解决方案。利用我知道的事实n：

rot :: Int -> [Expr] -> Expr
rot 0 xs = Lam $ \x -> foldl App x (reverse xs)
rot n xs = Lam $ \x -> rot (n - 1) (x : xs)

rot1 n = rot n []

我认为不给出就无法解决这个问题n，因为在 lambda 演算中，一个术语的数量可能取决于它的论点。即没有明确的“最后”论点。相应地改变了问题。

于 2011-03-04T22:16:08.813 回答
0

我认为您可以为此使用 Haskell 中的 An n-ary zipWith 论文中描述的技术。

于 2011-03-04T08:21:16.133 回答
-1

你能用r一般的方式写吗？如果你知道n怎么办？

哈斯克尔

不是普通的Haskell。您必须使用其他人（比我聪明得多）可能会发布的一些深层模板魔法。

在普通的 Haskell 中，让我们尝试编写一个类。

class Rotatable a where
    rotate :: a -> ???

到底是什么类型的旋转？如果您不能编写它的类型签名，那么您可能需要模板来在您正在寻找的通用级别上进行编程（无论如何，在 Haskell 中）。

不过，将这个想法转化为 Haskell 函数很容易。

r1 f = \a -> f a
r2 f = \b -> \a -> f a b
r3 f = \b -> \c -> \a -> f a b c

等等

Lisp

一些 Lispy 语言有apply函数 (linked: r5rs)，它接受一个函数和一个列表，并将列表的元素作为函数的参数应用。我想在这种情况下，只需取消轮换列表并将其发送出去就不会那么难了。我再次向大师们寻求更深层次的答案。

于 2011-03-04T01:54:51.213 回答