How, if possible, can we efficiently compute with lazy data structures in -calculus?

In Haskell, we can use the following code to define fibonacci numbers,

fibs = 1 : 1 : zipWith (+) fibs (tail fibs)

And its time complexity is linear.

I cannot find a way to do it in lambda calculus or combinatory logic.

With Y combinator, it leads to exponential steps to evaluate.

Is it possible in lambda calculus? Is there any formal system that can evaluate it in linear steps?

Although Haskell of course has native recursion, we can ignore it and implement the Y combinator $λf. (λx. f (x x)) (λx. f (x x))$ literally, using a newtype to get it through the type system, and a NOINLINE pragma to work around a GHC bug.

A fibs implementation based on the Y combinator runs in a quadratic number of steps, not exponential. This effectively builds the list a linear number of times, with each list depending only on the single list at the next level (try it online):
newtype Mu t = Mu (Mu t -> t)
{-# NOINLINE yStep #-}
yStep f (Mu x) = f (x (Mu x))
y f = yStep f (Mu (yStep f))
fibs = y (\f -> 1 : 1 : zipWith (+) f (tail f))
main = mapM_ print fibs


Just to see that nothing funny is going on, we can ignore Haskell’s builtin lists too and encode everything with functions (try it online):
{-# LANGUAGE RankNTypes #-}
newtype Mu t = Mu (Mu t -> t)
newtype List t = List (forall r. (t -> List t -> r) -> r)
{-# NOINLINE yStep #-}
yStep f (Mu x) = f (x (Mu x))
y f = yStep f (Mu (yStep f))
cons x xs = List (\f -> f x xs)
car (List xs) = xs (\x _ -> x)
cdr (List xs) = xs (\_ xs' -> xs')
zipWith' f = y (\go xs ys -> cons (f (car xs) (car ys)) (go (cdr xs) (cdr ys)))
fibs = y (\f -> cons 1 (cons 1 (zipWith' (+) f (cdr f))))
main = y (\go xs -> print (car xs) >> go (cdr xs)) fibs


We’re still relying on Haskell’s lazy evaluation. That’s not a problem—we can use a call-by-need lambda calculus interpreter. But alternatively, we can add an explicit laziness primitive to a call-by-value language, like in this JavaScript translation that still runs in quadratic steps (try it online):
const dummy = x => x;
const lazy = f => {
let value;
let evaluated = false;
return () => {
if (!evaluated) {
value = f(dummy);
evaluated = true;
}
return value;
};
};
const force = l => l(dummy);

const add = x => y => x + y;

const fix = f => (x => x(x))(x => f(y => x(x)(y)));
const lazyFix = f => (x => lazy(() => x(x)))(x => f(lazy(() => x(x))));
const cons = x => xs => f => f(x)(xs);
const car = xs => xs(x => xs1 => x);
const cdr = xs => xs(x => xs1 => xs1);
const zipWith = f =>
fix(
go => xs => ys =>
lazy(() =>
cons(f(car(force(xs)))(car(force(ys))))(
go(cdr(force(xs)))(cdr(force(ys)))
)
)
);
const fibs = lazyFix(p =>
cons(1n)(lazy(() => cons(1n)(zipWith(add)(p)(cdr(force(p))))))
);

for (let p = force(fibs); ; p = force(cdr(p))) console.log(car(p));


Of course, if we’re going to add laziness primitives, we might as well directly add an efficient primitive lazy fixed-point combinator, so we can write the solution that runs in a linear number of steps (try it online).
const dummy = x => x;
const lazyFix = f => {
let value;
let evaluated = false;
const lazyValue = () => {
if (!evaluated) {
value = f(lazyValue);
evaluated = true;
}
return value;
};
return lazyValue;
};
const lazy = lazyFix;
const force = l => l(dummy);

const add = x => y => x + y;

const fix = f => (x => x(x))(x => f(y => x(x)(y)));
const cons = x => xs => f => f(x)(xs);
const car = xs => xs(x => xs1 => x);
const cdr = xs => xs(x => xs1 => xs1);
const zipWith = f =>
fix(
go => xs => ys =>
lazy(() =>
cons(f(car(force(xs)))(car(force(ys))))(
go(cdr(force(xs)))(cdr(force(ys)))
)
)
);
const fibs = lazyFix(p =>
cons(1n)(lazy(() => cons(1n)(zipWith(add)(p)(cdr(force(p))))))
);

for (let p = force(fibs); ; p = force(cdr(p))) console.log(car(p));


So I guess the formal system you’re looking for is lambda calculus with a primitive lazy fixed-point combinator.

StackExchange Computer Science Q#144310, answer score: 3