Trasformando una funzione che calcola un punto fisso

Question

Ho una funzione che calcola un punto fisso in termini di iterata:

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
                             )

Si noti che si può astrarre da questo a:

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

Può questa funzione essere scritta in termini di correzione? Sembra che ci dovrebbe essere una trasformazione di questo regime a qualcosa con correzione in esso, ma io non lo vedo.

Answer 1

C'è un po 'sta succedendo qui, dalla meccanica di valutazione pigra, alla definizione di un punto fisso per il metodo di di trovare un punto fisso. In breve, credo che si può essere intercambiabili in modo errato il punto fisso di applicazione funzione nel lambda calcolo con le vostre esigenze.

Può essere utile notare che l'implementazione di trovare il tempo determinato punto (utilizzando iterate) richiede un valore di partenza per la sequenza di applicazione funzioni. Contrastare questo alla funzione fix, che richiede tale valore iniziale (in un teste, i tipi di danno alla distanza già: findFixedPoint è di tipo (a -> a) -> a -> a, che ha fix tipo (a -> a) -> a). Questo è di per sé, perché le due funzioni fanno cose sottilmente diverse.

dig Let in questo un po 'più in profondità. In primo luogo, devo dire che potrebbe essere necessario per dare un po 'di più informazioni (l'implementazione di due a due, per esempio), ma con un ingenuo primo tentativo, e la mia (forse viziata) l'attuazione di quello che credo si desidera fuori di coppie , la funzione findFixedPoint è equivalente a risultato per fix, per un certa classe di funzioni solo

Diamo uno sguardo ad alcuni di codice:

{-# 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

Questo contrasto alla definizione di fix:

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

e si noterà che stiamo trovando un tipo molto diverso di -punto fisso (cioè abusiamo valutazione pigra per generare un punto fisso per l'applicazione funzione nel matematico senso , dove solo valutazione arresto sse * la funzione risultante, applicata a se stessa, restituisce la stessa funzione).

Per l'illustrazione, definiamo alcune funzioni:

lambdaA = const 3
lambdaB = (*)3          

E vediamo la differenza tra fix e 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                            

Ora, se non siamo in grado di specificare il valore di partenza, quello che viene utilizzato per fix? Si scopre che con l'aggiunta di fix al lambda calcolo, otteniamo la possibilità di specificare la valutazione delle funzioni ricorsive. Considerate fact' = \rec n -> if n == 0 then 1 else n * rec (n-1), siamo in grado di calcolare il punto fisso di fact' come:

*Main> (fix fact') 5
120      

dove nella valutazione (fix fact') applica ripetutamente fact' stesso fino a raggiungere il stesso funzione , che poi chiamiamo con il 5 valore. Possiamo vedere questo in:

  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)))
= ...

Che cosa significa tutto questo? a seconda della funzione hai a che fare con, non sarà necessariamente in grado di utilizzare fix per calcolare il tipo di punto fisso che si desidera. Questo è, per quanto ne so, dipende dalla funzione (s) in questione. Non tutte le funzioni hanno il tipo di punto fisso calcolato dal fix!

* ho evitato parlando di teoria dei domini, come credo che sarebbe solo confondere un argomento già sottile. Se siete curiosi, fix trova un certa tipo di punto fisso, vale a dire il minimo punto fisso a disposizione del poset la funzione è specificato sopra.

Answer 2

Per la cronaca, è possibile per definire la findFixedPoint funzione utilizzando fix. Come Raeez ha sottolineato, funzioni ricorsive possono essere definite in termini di fix. La funzione che ti interessa può essere ricorsivamente definito come:

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

Questo significa che siamo in grado di definirlo come fix ffp dove 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)

Per un esempio concreto, supponiamo che f è definito come

f = drop 1

E 'facile vedere che per ogni lista l finita abbiamo findFixedPoint f l == []. Ecco come fix ffp avrebbe funziona quando il "valore dell'argomento" è []:

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

D'altra parte, se il "valore dell'argomento" è [42], avremmo:

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