转换计算定点的函数

| 我有一个函数，它根据迭代来计算固定点：

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来编写此功能吗？似乎应该从该方案向其中已修复的事物进行转换，但是我没有看到它。

已邀请:

2 个回复

念炯

从惰性评估的原理到固定点的定义再到找到固定点的方法，这里有很多事情要做。简而言之，我相信您可能会根据需要错误地交换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

将此与“ 3”的定义进行对比：

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的作用是什么？事实证明，通过在λ微积分中添加ѭ3，我们可以指定递归函数的求值。考虑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)))
= ...

那么，这意味着什么？根据要处理的功能，您不一定能够使用ѭ3来计算所需的不动点类型。据我所知，这取决于所讨论的功能。并非所有函数都具有fix计算的定点！ *我避免谈论领域理论，因为我相信这只会混淆本来就很细微的话题。如果您很好奇，ѭ3会找到某种固定点，即函数所指定的位姿的最小可用固定点。

厦惫

仅出于记录目的，可以使用fix定义函数function4ѭ。正如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 == []。这是当\“ value参数\”为[]时，fix ffp的工作方式：

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

另一方面，如果\“ value参数\”为[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 }
[]

要回复问题请先登录或注册

转换计算定点的函数

2 个回复

发起人

fixpoint_combinators

haskell

y_combinator

letrec

问题状态

转换计算定点的函数

与内容相关的链接

2 个回复

发起人

fixpoint_combinators

haskell

y_combinator

letrec

问题状态