Totalität und Suche nach Elementen in Streams

Question

Ich möchte eine find Funktion für Streams von Größe-gebundenen Typen, die analog zu den Suchfunktionen für Lists und Vects ist.

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

Die Herausforderung ist es, es zu machen:

1. insgesamt sein
2. verbrauchen nicht mehr als konstant log_2 N Raum, wobei N die Anzahl der Bits ist erforderlich, um die größte a zu kodieren.
3. nicht länger als eine Minute bei der Kompilierung
4. zu überprüfen, keine Laufzeit Kosten auferlegen

Allgemeinen insgesamt finden Implementierung für Streams klingt absurd. Streams sind unendlich und ein Prädikat von const False würde die Suche für immer weitergehen lassen. Eine gute Möglichkeit, diesen allgemeinen Fall zu behandeln, ist die Technik des unendlichen Treibstoffs.

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 

, die gut für meinen Anwendungsfall funktioniert, aber ich frage mich, ob in bestimmten spezialisierten Fällen die Gesamtheit Prüfung ohne forever mit überzeugt sein könnte. Ansonsten kann jemand ein langweiliges Leben lang warten, bis find forever ?predicateWhichHappensToAlwaysReturnFalse (iterate S Z) fertig ist.

Betrachten Sie den speziellen Fall, in dem aBits32 ist.

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

Zwei Probleme: es ist nicht total ist, und es kann möglicherweise nicht Nothing selbst zurückkehren, obwohl es eine endliche Anzahl von Bits32 Einwohnern ist zu versuchen. Vielleicht könnte ich take (pow 2 32) verwenden, um eine Liste zu erstellen und dann Lists Suche zu verwenden ... uh, warte ... die Liste würde nur GBs Speicherplatz belegen.

Im Prinzip scheint es nicht so schwierig zu sein. Es gibt endlich viele Einwohner, die man ausprobieren kann, und ein moderner Computer kann alle 32-Bit-Permutationen in Sekunden durchlaufen. Gibt es eine Möglichkeit, die Vollständigkeitsprüfung überprüfen zu lassen the (Stream Bits32) $ iterate (+1) 0 schließlich zurück zu 0 und sobald es behauptet, dass alle Elemente ausprobiert worden sind, seit (+1) ist rein?

Hier ist ein Anfang, obwohl ich nicht sicher bin, wie man die Löcher füllt und find genug spezialisiert, um es total zu machen. Vielleicht würde eine Schnittstelle helfen?

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} 

Gibt es eine Möglichkeit, die Gesamtheit checker zu sagen, unendlich Kraftstoff zu verwenden, um eine Suche über einen bestimmten Strom Verifizieren ist insgesamt?

Answer 1

wir definieren, was es bedeutet, für eine Folge zyklisch zu sein:

%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) 

Die oben bedeutet, dass wir eine Situation haben, die wie folgt dargestellt werden kann:

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

wo m streng ist weniger als n (aber m kann gleich Null sein).n ist eine Anzahl von Schritten, nach denen wir ein Element der Sequenz erhalten, die wir zuvor kennengelernt haben.

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

Als nächstes wollen wir eine Hilfsfunktion definieren, die verwendet eine obere Schranke fuel genannt von der Schleife auszubrechen:

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 

Jetzt find kann wie so definiert werden:

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

Hier sind einige 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