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

この関数は修正の観点から書くことができますか？このスキームから修正されたものへの変換があるはずのようですが、私にはわかりません。

4

2 に答える 2

11

ここでは、遅延評価のメカニズムから、固定小数点の定義、固定小数点の検索方法まで、かなりのことが行われています。要するに、ラムダ計算の関数適用の不動点をニーズと誤って交換している可能性があると思います。

iterate固定小数点を見つける（を利用する）実装には、関数適用のシーケンスの開始値が必要であることに注意してください。これを、fixそのような開始値を必要としない関数と比較してください（ヘッドアップとして、タイプはすでにこれを提供しています：findFixedPointはタイプですが、タイプ(a -> a) -> a -> aはありfixます(a -> a) -> a）。これは本質的に、2つの関数が微妙に異なることを行うためです。

これをもう少し深く掘り下げてみましょう。まず、もう少し情報を提供する必要があるかもしれませんが（たとえば、ペアワイズの実装）、素朴な最初の試みと、ペアワイズから望むと私が信じているものの私の（おそらく欠陥のある）実装を使用します、関数は、特定のクラスの関数についてのみ、結果としてと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使用されますか？ラムダ計算に追加fixすることで、再帰関数の評価を指定できるようになります。を考え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を見つけます。

于 2011-06-10T01:22:27.207 に答える
2

念のため、を使用して関数を定義することができます。Raeezが指摘しているように、再帰関数は。で定義できます。関心のある関数は、再帰的に次のように定義できます。findFixedPointfixfix

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 }
[]
于 2013-03-05T11:23:06.443 に答える