转换计算固定点的函数

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用于什么？事实证明,通过添加fixlambda演算,我们可以指定递归函数的评估.考虑一下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找到了某 一种固定的点,该功能被指定在偏序集,即最小的可用固定点.