Totalité et recherche d'éléments dans les flux

Question

Je souhaite une fonction find pour les flux de types liés à la taille, similaire aux fonctions de recherche de listes et de vecteurs.

total 
find : MaxBound a => (a -> Bool) -> Stream a -> Maybe a 

Le défi est à faire:

1. être totale
2. ne consomment pas plus constant espace N de log_2 où N est le nombre de bits requis pour coder le plus grand a.
3. pas prendre plus d'une minute pour vérifier au moment de la compilation
4. imposer sans frais d'exécution

En général, une mise en œuvre de découverte totale pour les flux semble absurde. Les flux sont infinis et un prédicat de const False rendrait la recherche éternelle. Une bonne façon de gérer ce cas général est la technique du carburant infini.

data Fuel = Dry | More (Lazy Fuel) 

partial 
forever : Fuel 
forever = More forever 

total 
find : Fuel -> (a -> Bool) -> Stream a -> Maybe a 
find Dry _ _ = Nothing 
find (More fuel) f (value :: xs) = if f value 
            then Just value 
            else find fuel f xs 

qui fonctionne bien pour mon cas d'utilisation, mais je me demande si, dans certains cas spécialisés le vérificateur de la totalité pourrait être convaincu sans utiliser forever. Sinon, quelqu'un risque de subir une vie ennuyeuse en attendant find forever ?predicateWhichHappensToAlwaysReturnFalse (iterate S Z) pour finir. Considérons le cas particulier où a est Bits32.

find32 : (Bits32 -> Bool) -> Stream Bits32 -> Maybe Bits32 
find32 f (value :: xs) = if f value then Just value else find32 f xs 

Deux problèmes: ce n'est pas totale et cela ne peut pas revenir Nothing même si il y a un nombre fini de Bits32 habitants à essayer. Peut-être que je pourrais utiliser take (pow 2 32) pour créer une liste, puis utiliser la recherche de liste ... euh, attendez ... la liste à elle seule prendrait des Go d'espace.

En principe, cela ne devrait pas être difficile. Il y a un nombre fini d'habitants à essayer, et un ordinateur moderne peut parcourir toutes les permutations 32 bits en quelques secondes. Y at-il un moyen d'avoir le vérificateur de totalité the (Stream Bits32) $ iterate (+1) 0 cycles éventuellement revenir à 0 et une fois qu'il affirme que tous les éléments ont été essayés depuis (+1) est pur?

Voici un début, même si je ne suis pas sûr de savoir comment remplir les trous et de spécialiser find assez pour le rendre total. Peut-être qu'une interface aiderait?

total 
IsCyclic : (init : a) -> (succ : a -> a) -> Type 

data FinStream : Type -> Type where 
    MkFinStream : (init : a) -> 
       (succ : a -> a) -> 
       {prf : IsCyclic init succ} -> 
       FinStream a 

partial 
find : Eq a => (a -> Bool) -> FinStream a -> Maybe a 
find pred (MkFinStream {prf} init succ) = if pred init 
              then Just init 
              else find' (succ init) 
    where 
    partial 
    find' : a -> Maybe a 
    find' x = if x == init 
       then Nothing 
       else 
       if pred x 
       then Just x 
       else find' (succ x) 

total 
all32bits : FinStream Bits32 
all32bits = MkFinStream 0 (+1) {prf=?prf} 

est-il un moyen de dire le vérificateur de la totalité d'utiliser du carburant infini vérifier une recherche sur un flux particulier est total?

Answer 1

Définissons ce que cela signifie pour une séquence soit cyclique:

%default total 

iter : (n : Nat) -> (a -> a) -> (a -> a) 
iter Z f = id 
iter (S k) f = f . iter k f 

isCyclic : (init : a) -> (next : a -> a) -> Type 
isCyclic init next = DPair (Nat, Nat) $ \(m, n) => (m `LT` n, iter m next init = iter n next init) 

Les moyens ci-dessus que nous avons une situation qui peut être décrite comme suit:

-- x0 -> x1 -> ... -> xm -> ... -> x(n-1) -- 
--     ^     | 
--      |--------------------- 

où m est strictement inférieur à n (mais m peut être égal à zéro).n est un certain nombre d'étapes après lesquelles nous obtenons un élément de la séquence que nous avons précédemment rencontrée.

data FinStream : Type -> Type where 
    MkFinStream : (init : a) -> 
       (next : a -> a) -> 
       {prf : isCyclic init next} -> 
       FinStream a 

Ensuite, nous allons définir une fonction d'assistance, qui utilise une appelée borne supérieure fuel pour sortir de la boucle:

findLimited : (p : a -> Bool) -> (next : a -> a) -> (init : a) -> (fuel : Nat) -> Maybe a 
findLimited p next x Z = Nothing 
findLimited p next x (S k) = if p x then Just x 
           else findLimited pred next (next x) k 

Maintenant find peut être défini comme ceci:

find : (a -> Bool) -> FinStream a -> Maybe a 
find p (MkFinStream init next {prf = ((_,n) ** _)}) = 
    findLimited p next init n 

Voici quelques tests:

-- I don't have patience to wait until all32bits typechecks 
all8bits : FinStream Bits8 
all8bits = MkFinStream 0 (+1) {prf=((0, 256) ** (LTESucc LTEZero, Refl))} 

exampleNothing : Maybe Bits8 
exampleNothing = find (const False) all8bits    -- Nothing 

exampleChosenByFairDiceRoll : Maybe Bits8 
exampleChosenByFairDiceRoll = find ((==) 4) all8bits  -- Just 4 

exampleLast : Maybe Bits8 
exampleLast = find ((==) 255) all8bits      -- Just 255