Search code examples
haskelllambda-calculus

How to turn Integer-List Generator [m ...] in Lambda Calculus in Haskell

I have given a task to make the Integer-List Generator [m...] in lambda calculus. So it should fullfill this definition.

Y F m ≡ : m (Y F (+ m 1))

Therefor a lambda calculus F is needed. I don't know how to find which lambda calculus F should be. Does anyone have any suggestions for F?

Solution

  • Equational reasoning gets you where you need to go. We have these two equations:

    Y F = F (Y F) -- the basic useful property of Y
Y F m = : m (Y F (+ m 1))

    So now we just solve. We replace the Y F in Y F m = ... with the thing it's equal to:

    F (Y F) m = : m (Y F (+ m 1))

    One solution to this equation is to generalize from Y F to an arbitrary variable g everywhere:

    F g m = : m (g (+ m 1))

    Done. This is now a fine defining equation for F. If you don't like the syntax sugar, you could instead write it as a lambda:

    F = \g m -> : m (g (+ m 1))

    Of course, when you practice this yourself on other problems, be kind to yourself: there are lots of different choices of how to rewrite things at each step, and you might have to play with a couple different ways before you stumble on one that gets you where you want to go, rather than following such a straight-line path as I've outlined here where I had already tried and eliminated a bunch of wrong ways. Persevere, and you can learn to do it.