# 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?

• Read the book: microsoft.com/en-us/research/publication/… Sep 28, 2021 at 4:22
• What is the theory behind what? The compiler methods used in Haskell? Or something else? Sep 28, 2021 at 6:35
• @AndrejBauer I cannot translate it to lambda calculus or combinatory logic with same complexity. Is it just an optimization of the compiler? Is there any formal system that can achieve the same thing? Sep 28, 2021 at 6:52
• What notion of time complexity are you using for combinatory logic and $\lambda$-calculus? Sep 28, 2021 at 7:06
• That's not a proof of anything, and there are many more possibilities than using $Y$, so it's not clear at all that "it canno be done in $\lambda$-calculus". I think it would be better to rephrase your question to "how, if possible, can we efficiently compute with lazy data structures in $\lambda$-calculus?" And then people would point you to various encodings of data structures etc. The way the question stands, it's just makes unwarranted claims, so the answer is almost by necessity "that's not how things are". Sep 28, 2021 at 10:21

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 =>
);

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 =>
);

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.

In terms of the combinators $$S = λxλyλz·xz(yz)$$, $$K = λxλy·x$$, $$I = λx·x$$ and $$B = λxλyλz·x(yz)$$ and letting $$C_n$$ denote the Church numerals, with $$C_0 = K I$$, $$C_1 = I$$, $$C_{n+1} = S B C_n$$, for $$n = 1, 2, 3, ...$$ (noting also that $$S B (K I) = I$$ under η-equivalence), something that is closer to what you're looking for is also a typical example showing how to deal with primitive recursion. The Fibonacci sequence is $$1, 1, 2 = 1 + 1, 3 = 1 + 2, 5 = 2 + 3, 8 = 3 + 5, ⋯.$$

The Church numerals have the property that $$C_n f x = f^n x$$, where $$f^n$$ denotes the $$n$$-fold composition of $$f$$ with itself, e.g. $$C_2 f x = f (f x)$$ and $$C_3 f x = f (f (f x))$$. Since the Fibonacci sequence's recursive definition also involves the addition operator, we'll also need the operator for adding Church numerals, $$C_{m+n} f x = C_m f (C_n f x)$$. Up to η-equivalence $$C_{m+n} = B S (B B) C_m C_n$$. Let $$A = B S (B B)$$

Then $$K C_1 C_1 = C_1,\\ J K C_1 C_1 = K C_1 (A C_1 C_1) = K C_1 C_2 = C_1,\\ J^2 K C_1 C_1 = J K C_1 C_2 = K C_2 (A C_1 C_2) = K C_2 C_3 = C_2,\\ J^3 K C_1 C_1 = J^2 K C_1 C_2 = J K C_2 C_3 = K C_3 (A C_2 C_3) = K C_3 C_5 = C_3,$$ and so on ... where $$J k u v = k v (A u v) = S k (A u) v = B (S k) A u v = C B A (S k) u v = B (C B A) S k u v,$$ which also uses the combinator $$C = λxλyλz·xzy$$. Therefore, the $$n$$-th Fibonacci number, presented as a Church numeral, is $$C_n J K C_1 C_1$$, where $$J = B (C B A) S$$ and $$A = B S (B B)$$.

Running this in Combo (which I put up on GitHub), with the η-rule turned on, e.g. $$A = B\ S\ (B\ B),\ J = B\ (C\ B\ A)\ S,\ SB = S\ B,\\ C1 = I,\ C2 = SB\ I,\ C3 = SB\ C2,\ C4 = SB\ C3,\\ C4\ J\ K\ C1\ C1$$ for the $$4$$-th Fibonacci number, I get $$4, 7, 18, 26, 37, 49, 63, 80, 102, 132, ...$$ steps for the cases $$n = 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, ...$$. So, it's probably quadratic, but not exponential. It can't be linear with Church numerals, since the numerals, themselves, are already linear (instead of logarithmic); i.e. they're essentially numerals in base $$1$$. You need positional numerals in base $$2$$ or higher. Then, it might become $$n \log n$$.

Further, you can probably roll up the first $$n$$ factor into a $$\log n$$ factor, too, if you exponentiate the iteration. The $$1$$-step iteration of $$u v$$ is into $$v (u + v)$$, which can be presented in vector-matrix form as $$A w$$, where $$w$$ is the vector for $$u v$$ and $$A$$ is a suitably-defined matrix. So, then, the $$2$$-step iteration is $$A^2 w$$, $$4$$-steps is $$(A^2)^2 w$$, $$8$$-steps is $$((A^2)^2)^2 w$$, and - in general - the $$2^k$$-step iteration is $$A^{2^k} w$$.

• There's a bug in this Stack Exchange. When logged in, this reply displays fine. When logged out, parts of the reply register as "math errors" and don't display properly. Mar 14 at 7:47