Spielen mit der Unendlichkeit - Lazy arithmetics

Question

Viele moderne Programmiersprachen erlauben uns, potentiell unendliche Listen zu handhaben und bestimmte Operationen an ihnen auszuführen.

Beispiel [Python]:

EvenSquareNumbers = (x * x for x in naturals() if x mod 2 == 0) 

Solche Listen, weil nur Elemente vorhanden sein können, die tatsächlich benötigt werden, berechnet. (Lazy evaluation)

Ich frage mich nur aus Interesse, ob es möglich ist (oder sogar in bestimmten Sprachen praktiziert), den Mechanismus der Lazy Evaluation auf Arithmetik zu erweitern.

Beispiel: Angesichts der unendlichen Liste von geraden Zahlen evens = [ x | x <- [1..], even x ] Wir nicht

length evens 

da die Berechnung wäre hier erforderlich berechnen konnte nie enden.

Aber wir konnten tatsächlich feststellen, dass

length evens > 42 

, ohne den gesamten length Begriff zu bewerten haben.

Ist das in jeder Sprache möglich? Was ist mit Haskell?

Edit: Um den Punkt klarer zu machen: Die Frage ist nicht, wie man feststellen kann, ob eine faule Liste kürzer ist als eine gegebene Zahl. Es geht darum, konventionelle eingebaute Funktionen so zu verwenden, dass die numerische Berechnung träge erfolgt.

sdcvvc eine Lösung für Haskell zeigte:

data Nat = Zero | Succ Nat deriving (Show, Eq, Ord) 

toLazy :: Integer -> Nat 
toLazy 0 = Zero 
toLazy n = Succ (toLazy (n-1)) 

instance Num Nat where 
    (+) (Succ x) y = Succ (x + y) 
    (+) Zero y = y 
    (*) Zero y = Zero 
    (*) x Zero = Zero 
    (*) (Succ x) y = y + (x * y) 
    fromInteger = toLazy 
    abs = id 
    negate = error "Natural only" 
    signum Zero = Zero 
    signum (Succ x) = Succ Zero 

len [] = Zero 
len (_:x') = Succ $ len x' 

-- Test 

len [1..] < 42 

Ist dies auch in anderen Sprachen möglich?

Answer 1

Sie Ihre eigenen natürlichen Zahlen erstellen können ...

data Nat = Zero | Succ Nat deriving (Show, Eq, Ord) 

len :: [a] -> Nat 
len = foldr (const Succ) Zero 

toLazy :: Int -> Nat 
toLazy 0 = Zero 
toLazy n = Succ (toLazy (n-1)) 

a = len [1..] > toLazy 42 

Dann wird ein True , dank fauler Bewertung. Es ist wichtig, dass Len foldr verwendet, fulll funktioniert nicht auf unendlichen Listen.Und Sie können auch einige Arithmetik (nicht getestet):

instance Num Nat where 
    (+) (Succ x) y = Succ (x + y) 
    (+) Zero y = y 
    (*) Zero y = Zero 
    (*) x Zero = Zero 
    (*) (Succ x) y = y + (x * y) 
    fromInteger = toLazy 
    abs = id 
    negate = error "Natural only" 
    signum Zero = Zero 
    signum (Succ x) = Succ Zero 

Zum Beispiel 2 * unendlich + 3 ist unendlich:

let infinity = Succ infinity 

*Main> 2 * infinity + 3 
(Succ (Succ (Succ ^cCc (Succ (Succ (SuccInterrupted. 

Zweite Lösung

Eine andere Lösung ist die Verwendung Listen von() als faule natürliche Zahlen.

Überprüfen Hackage.

Bearbeiten: Hinzugefügt Instanz Num.

Edit2:

Übersetzung zweite Lösung Python:

import itertools 

def length(x): 
    return itertools.imap(lambda:(), x) 

def to_lazy(n): 
    return itertools.chain([()] * n) 

Zahlen hinzuzufügen, verwenden Sie itertools.chain, sich zu vermehren, verwenden itertools.product. Das ist nicht so schön wie in Haskell, aber es funktioniert.

In jeder anderen strengen Sprache mit Schließungen können Sie Faulheit mit dem Typ() -> a anstelle von a simulieren. Damit ist es möglich, die erste Lösung von Haskell in andere Sprachen zu übersetzen. Dies wird jedoch schnell unlesbar werden.

Siehe auch a nice article on Python one-liners.

Answer 2

Sie können wahrscheinlich erreichen, was Sie wollen, indem Sie versuchen, mehr als 42 Elemente aus evens zu bekommen.

Answer 3

Nicht sicher, ich verstehe Ihre Frage, aber lassen Sie uns dies versuchen. Vielleicht suchst du Streams. Ich spreche nur Erlang, aus dem FP-Sprachfamilie, also ...

esn_stream() -> 
    fun() -> esn_stream(1) end. 

esn_stream(N) -> 
    {N*N, fun() -> esn_stream(N+2) end}. 

Aufruf der Strom immer das nächste Element zurückgibt, und ein Spaß sollten Sie das nächste Element abzurufen aufrufen. Auf diese Weise erreichen Sie eine faule Bewertung.

Dann können Sie eine is_stream_longer_than Funktion definieren als:

is_stream_longer_than(end_of_stream, 0) -> 
    false; 
is_stream_longer_than(_, 0) -> 
    true; 
is_stream_longer_than(Stream, N) -> 
    {_, NextStream} = Stream(), 
    is_stream_longer_than(NextStream, N-1). 

Ergebnis:

1> e:is_stream_longer_than(e:esn_stream(), 42). 
true 

2> S0 = e:esn_stream(). 
#Fun<e.0.6417874> 

3> {E1, S1} = S0(). 
{1,#Fun<e.1.62636971>} 
4> {E2, S2} = S1(). 
{9,#Fun<e.1.62636971>} 
5> {E3, S3} = S2(). 
{25,#Fun<e.1.62636971>} 

Answer 4

Wenn es nicht für Faulheit waren, ich denke, das in F # funktionieren würde:

type Nat = Zero | Succ of Nat 

let rec toLazy x = 
    if x = 0 then Zero 
    else Succ(toLazy(x-1)) 

type Nat with 
    static member (+)(x:Nat, y:Nat) = 
     match x with 
     | Succ(a) -> Succ(a+y) 
     | Zero -> y 
    static member (*)(x:Nat, y:Nat) = 
     match x,y with 
     | _, Zero -> Zero 
     | Zero, _ -> Zero 
     | Succ(a), b -> b + a*b 

module NumericLiteralQ = 
    let FromZero()   = toLazy 0 
    let FromOne()   = toLazy 1 
    let FromInt32(x:int) = toLazy x 

let rec len = function 
    | [] -> 0Q 
    | _::t -> 1Q + len t 

printfn "%A" (len [1..42] < 100Q) 
printfn "%A" (len [while true do yield 1] < 100Q) 

Aber da wir faul sein müssen, es dehnt sich so aus:

let eqLazy<'T> (x:Lazy<'T>) (y:Lazy<'T>) : bool = //' 
    let a = x.Force() 
    let b = y.Force() 
    a = b 

type Nat = Zero | Succ of LazyNat 
and [<StructuralComparison(false); StructuralEqualityAttribute(false)>] 
    LazyNat = LN of Lazy<Nat> with 
     override this.GetHashCode() = 0 
     override this.Equals(o) = 
      match o with 
      | :? LazyNat as other -> 
       let (LN(a)) = this 
       let (LN(b)) = other 
       eqLazy a b 
      | _ -> false 
     interface System.IComparable with 
      member this.CompareTo(o) = 
       match o with 
       | :? LazyNat as other -> 
        let (LN(a)) = this 
        let (LN(b)) = other 
        match a.Force(),b.Force() with 
        | Zero, Zero -> 0 
        | Succ _, Zero -> 1 
        | Zero, Succ _ -> -1 
        | Succ(a), Succ(b) -> compare a b 
       | _ -> failwith "bad" 

let (|Force|) (ln : LazyNat) = 
    match ln with LN(x) -> x.Force() 

let rec toLazyNat x = 
    if x = 0 then LN(lazy Zero) 
    else LN(lazy Succ(toLazyNat(x-1))) 

type LazyNat with 
    static member (+)(((Force x) as lx), ((Force y) as ly)) = 
     match x with 
     | Succ(a) -> LN(lazy Succ(a+ly)) 
     | Zero -> lx 

module NumericLiteralQ = 
    let FromZero()   = toLazyNat 0 
    let FromOne()   = toLazyNat 1 
    let FromInt32(x:int) = toLazyNat x 

let rec len = function 
    | LazyList.Nil -> 0Q 
    | LazyList.Cons(_,t) -> LN(lazy Succ(len t)) 

let shortList = LazyList.of_list [1..42] 
let infiniteList = LazyList.of_seq (seq {while true do yield 1}) 
printfn "%A" (len shortList < 100Q)  // true 
printfn "%A" (len infiniteList < 100Q) // false 

Dies zeigt, warum die Leute schreibe dieses Zeug nur in Haskell.