Gra z nieskończonością - Leniwa arytmetyka

Question

Wiele współczesnych języków programowania pozwala nam obsługiwać potencjalnie nieskończone listy i wykonywać na nich określone operacje.

Przykład [Python]

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

Te listy mogą istnieć ze względu jedynie elementy, które są rzeczywiście wymagane są obliczane. (Leniwa ocena)

Po prostu zastanawiałem się, czy nie jest interesujące, czy możliwe jest (lub nawet praktykowane w niektórych językach) rozszerzenie mechanizmu leniwego oceniania na arytmetykę.

Przykład: względu na nieskończoną listę liczb parzystych evens = [ x | x <- [1..], even x ] Nie mogliśmy obliczyć

length evens 

od obliczania wymaganej tutaj nigdy nie zakończyć.

Ale moglibyśmy stwierdzić, że

length evens > 42 

bez konieczności oceniać cały length termin.

Czy jest to możliwe w dowolnym języku? A co z Haskellem?

Edytuj: Aby uczynić punkt jaśniejszym: Pytanie nie dotyczy tego, jak ustalić, czy lista leniwych jest krótsza niż podana liczba. Chodzi o używanie konwencjonalnych funkcji wbudowanych w taki sposób, że obliczenia numeryczne odbywają się leniwie.

sdcvvc pokazał rozwiązanie Haskell:

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 

Czy to możliwe również w innych językach?

Answer 1

Można tworzyć własne liczby naturalne ...

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 

Wtedy to prawda , dzięki leniwej ocenie. Ważne jest, aby len używał foldr, foldl nie działa na nieskończonych listach.I można to zrobić trochę arytmetyki zbyt (nie testowane):

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 

Na przykład, 2 * nieskończoność + 3 jest nieskończoność:

let infinity = Succ infinity 

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

drugie rozwiązanie

Innym rozwiązaniem jest użycie listy() jako leniwych liczb naturalnych.

len = map (const()) 
toLazy n = replicate n() 
a = len [1..] > toLazy 42 

Sprawdź Hackage.

Edytuj: Dodano instancję Num.

Edit2:

Tłumaczenie drugiego roztworu Pythonie

import itertools 

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

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

dodać numery użyć itertools.chain do mnożenia użyciu itertools.product. To nie jest tak piękne jak w Haskell, ale działa.

W każdym innym ścisłym języku z zamknięciami można symulować lenistwo za pomocą typu() -> a zamiast a. Za pomocą tego można przetłumaczyć pierwsze rozwiązanie z Haskella na inne języki. To jednak szybko stanie się nieczytelne.

Zobacz także a nice article on Python one-liners.

Answer 2

Prawdopodobnie możesz osiągnąć to, czego szukasz, próbując uzyskać ponad 42 elementy z każdego dnia.

Answer 3

Nie jestem pewien, czy rozumiem twoje pytanie, ale spróbujmy. Być może szukasz strumieni. I tylko mówić Erlang, z rodziny języków FP, więc ...

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

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

Wywołanie strumień zawsze zwraca następny element, a zabawa należy zadzwonić, aby pobrać następny element. W ten sposób osiągniesz leniwą ocenę.

Następnie można zdefiniować is_stream_longer_than funkcję:

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

Wynik:

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

Gdyby nie do lenistwa, myślę, że to będzie działać w F #:

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) 

Ale ponieważ musimy być leniwy, rozszerza się następująco:

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 

To pokazuje, dlaczego ludzie pisz tylko te rzeczy w Haskell.