转换计算固定点的函数

Question

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

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

可以用修复程序编写此功能吗？似乎应该从该方案转变为“修复程序”，但我看不到。

Answer 1

从懒惰评估的机制到固定点的定义到 方法 找到一个固定点。简而言之，我相信您可能正在错误地互换 在lambda演奏中申请功能点的固定点 满足您的需求。

可能会注意到您找到定点的实施（利用 iterate）需要函数应用程序序列的起始值。与此对比 fix 功能，不需要这样的起始值（作为抬头，类型已经放弃了： findFixedPoint 是类型 (a -> a) -> a -> a, ， 然而 fix 有类型 (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

您会注意到我们发现了一种非常不同的 固定点 （即，我们滥用懒惰评估以生成用于功能应用程序的固定点 数学意义, ，我们只停止评估 iff* 应用于自身的结果函数评估到相同的函数）。

插图，让我们定义一些功能：

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 用于？事实证明，通过添加 fix 对于lambda演算，我们获得了指定递归函数评估的能力。考虑 fact' = \rec n -> if n == 0 then 1 else n * rec (n-1), ，我们可以计算 fact' 作为：

*Main> (fix fact') 5
120      

在哪里评估 (fix fact') 反复适用 fact' 本身直到我们到达 相同的 功能, ，然后我们将其称为值 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的最低可用固定点，该函数被指定。

Answer 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 ffp 在哪里 ffp 是：

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 }
[]