10

我有一个根据迭代计算固定点的函数：

equivalenceClosure :: (Ord a) => Relation a -> Relation a
equivalenceClosure = fst . List.head                -- "guaranteed" to exist 
                   . List.dropWhile (uncurry (/=))  -- removes pairs that are not equal
                   . U.List.pairwise (,)            -- applies (,) to adjacent list elements
                   . iterate ( reflexivity
                             . symmetry
                             . transitivity
                             )

请注意，我们可以从中抽象为：

findFixedPoint :: (a -> a) -> a -> a
findFixedPoint f = fst . List.head
                 . List.dropWhile (uncurry (/=))  -- dropWhile we have not reached the fixed point
                 . U.List.pairwise (,)            -- applies (,) to adjacent list elements
                 . iterate
                 $ f

这个函数可以用fix来写吗？似乎应该从这个方案转变为有修复的东西，但我没有看到。

4

2 回答 2

11

这里有很多东西，从惰性求值的机制，到固定点的定义，再到找到固定点的方法。简而言之，我相信您可能错误地将 lambda 演算中函数应用的固定点与您的需求互换。

请注意，查找定点（利用iterate）的实现需要函数应用序列的起始值，这可能会有所帮助。将此与不需要此类起始值的函数进行对比fix（作为提醒，类型已经放弃了：findFixedPointis of type (a -> a) -> a -> a，而fixhas type (a -> a) -> a）。这本质上是因为这两个函数做了微妙的不同的事情。

让我们更深入地研究一下。首先，我应该说您可能需要提供更多信息（例如，您对成对的实现），但首先要天真地尝试，并且我（可能有缺陷）对我认为您想要成对的实现, 你的findFixedPoint函数在结果上等价于fix,仅适用于某类函数

让我们看一些代码：

{-# LANGUAGE RankNTypes #-}                                                      

import Control.Monad.Fix                                                                              
import qualified Data.List as List                                                                   

findFixedPoint :: forall a. Eq a => (a -> a) -> a -> a                                                
findFixedPoint f = fst . List.head                                                                    
                 . List.dropWhile (uncurry (/=))  -- dropWhile we have not reached the fixed point    
                 . pairwise (,)                   -- applies (,) to adjacent list elements            
                 . iterate f                                                                          

pairwise :: (a -> a -> b) -> [a] -> [b]                                                             
pairwise f []           = []                                                                        
pairwise f (x:[])       = []                                                                        
pairwise f (x:(xs:xss)) = f x xs:pairwise f xss

将此与 的定义进行对比fix：

fix :: (a -> a) -> a
fix f = let x = f x in x

你会注意到我们正在寻找一种非常不同的定点（即，我们滥用惰性求值来为数学意义上的函数应用生成一个定点，我们只在结果函数应用到本身，评估为相同的功能）。

为了说明，让我们定义一些函数：

lambdaA = const 3
lambdaB = (*)3

fix让我们看看和之间的区别findFixedPoint：

*Main> fix lambdaA               -- evaluates to const 3 (const 3) = const 3
                                 -- fixed point after one iteration           
3                                  
*Main> findFixedPoint lambdaA 0  -- evaluates to [const 3 0, const 3 (const 3 0), ... thunks]
                                 -- followed by grabbing the head.
3                                  
*Main> fix lambdaB               -- does not stop evaluating      
^CInterrupted.                   
*Main> findFixedPoint lambdaB 0  -- evaluates to [0, 0, ...thunks]
                                 -- followed by grabbing the head
0

现在如果我们不能指定起始值，那有什么fix用呢？事实证明，通过添加fixlambda 演算，我们获得了指定递归函数求值的能力。考虑fact' = \rec n -> if n == 0 then 1 else n * rec (n-1)，我们可以计算 的不动点fact'：

*Main> (fix fact') 5
120

where in evaluate(fix fact')重复应用fact'，直到我们到达同一个 函数，然后我们用 value 调用它5。我们可以看到这一点：

  fix fact'
= fact' (fix fact')
= (\rec n -> if n == 0 then 1 else n * rec (n-1)) (fix fact')
= \n -> if n == 0 then 1 else n * fix fact' (n-1)
= \n -> if n == 0 then 1 else n * fact' (fix fact') (n-1)
= \n -> if n == 0 then 1
        else n * (\rec n' -> if n' == 0 then 1 else n' * rec (n'-1)) (fix fact') (n-1)
= \n -> if n == 0 then 1
        else n * (if n-1 == 0 then 1 else (n-1) * fix fact' (n-2))
= \n -> if n == 0 then 1
        else n * (if n-1 == 0 then 1
                  else (n-1) * (if n-2 == 0 then 1
                                else (n-2) * fix fact' (n-3)))
= ...

那么，这意味着什么？根据您正在处理的功能，您不一定能够用来fix计算您想要的固定点类型。据我所知，这取决于所讨论的功能。并非所有函数都具有由fix!

*我避免谈论领域理论，因为我相信它只会混淆一个已经很微妙的话题。如果你很好奇，可以fix找到某种 固定点，即指定函数的poset 中最不可用的固定点。

于 2011-06-10T01:22:27.207 回答
2

仅作记录，可以findFixedPoint使用fix. 正如 Raeez 所指出的，递归函数可以用fix. 您感兴趣的函数可以递归定义为：

findFixedPoint :: Eq a => (a -> a) -> a -> a
findFixedPoint f x = 
   case (f x) == x of
       True  -> x
       False -> findFixedPoint f (f x)

这意味着我们可以将其定义为fix ffpwhere ffpis：

ffp :: Eq a => ((a -> a) -> a -> a) -> (a -> a) -> a -> a
ffp g f x = 
   case (f x) == x of
       True  -> x
       False -> g f (f x)

对于一个具体的例子，让我们假设f定义为

f = drop 1

很容易看出，对于l我们拥有的每个有限列表findFixedPoint f l == []。以下是fix ffp“值参数”为 [] 时的工作方式：

(fix ffp) f []
    = { definition of fix }
ffp (fix ffp) f []
    = { f [] = [] and definition of ffp }
[]

另一方面，如果“值参数”是 [42]，我们将有：

fix ffp f [42]
    = { definition of fix }
ffp (fix ffp) f [42]
    = { f [42] =/= [42] and definition of ffp }
(fix ffp) f (f [42])
    = { f [42] = [] }
(fix ffp) f []
    = { see above }
[]
于 2013-03-05T11:23:06.443 回答