# -*- coding: utf-8 -*-

ur'''

Boring legal details
====================

This text is released under the terms of the Creative Commons
Attribution-Share-Alike License 3.0.

You can find this license here:
http://creativecommons.org/licenses/by-sa/3.0/

Introduction
============

This is a verbose introduction to fixed point combinators and a
introduction to the denotational semantic of loops. It uses python to
illustrate the examples. You can execute all the examples in this
docstring by running

$ python -m doctest -v y-combinator.py

or you can try it out interactively by running

$ python -i y-combinator.py
>>> Z(fact)(5)
120

I'd suggest to install ipython, the interactive python console
featuring tab completion, a nice online help and other goodies. Just
substitute ipython for python in the above command to use it.

Introducing fixed point combinators
===================================

Original text and example from
https://en.wikipedia.org/wiki/Fixed-point_combinator

A fixed point combinator (or fixpoint combinator) is a
higher-order function that computes a fixed point of other
functions. A fixed point of a function f is a value x such that f(x)
= x. For example, 0 and 1 are fixed points of the function f(x) =
x^2, because 0^2 = 0 and 1^2 = 1. Whereas a fixed-point of a
first-order function (a function on "simple" values such as
integers) is a first-order value, a fixed point of a higher-order
function f is another function p such that f(p) = p. A fixed point
combinator, then, is a function g which produces such a fixed point
p for any function f:

    p = g(f), f(p) = p

or, alternatively:

    f(g(f)) = g(f).

Because fixed-point combinators are higher-order functions, their
history is intimately related to the development of lambda calculus.
One well-known fixed point combinator in the untyped lambda calculus
is Haskell Curry's Y = λf (λx f (x x)) (λx f (x x)). The name of
this combinator is sometimes incorrectly used to refer to any fixed
point combinator. The untyped lambda calculus however, contains an
infinitude of fixed point combinators. Fixed point combinators do
not necessarily exist in more restrictive models of computation. For
instance, they do not exist in simply typed lambda calculus.

In programming languages that support function literals, fixed point
combinators allow the definition and use of anonymous recursive
functions, i.e. without having to bind such functions to
identifiers. In this setting, the use of fixed point combinators is
sometimes called anonymous recursion.

[...]

Other fixed point combinators

In untyped lambda calculus fixed point combinators are not
especially rare. In fact there are infinitely many of them. In 2005
Mayer Goldberg showed that the set of fixed point combinators of
untyped lambda calculus is recursively enumerable.[4]

A version of the Y combinator that can be used in call-by-value
(applicative-order) evaluation is given by η-expansion of part of
the ordinary Y combinator:

    Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))

Here is an example of this in Python:

>>> Z = lambda f: (lambda x: f(lambda *args: x(x)(*args)))(lambda x: f(lambda *args: x(x)(*args)))
>>> fact = lambda f: lambda x: 1 if x == 0 else x * f(x - 1)
>>> Z(fact)(5)
120

Interpretation
==============

[This is my own interpretation.]

Z(fact) computes the lowest fixed point of the fact function, let's
call this value p. Calling fact with this value p yields p:

p = Z(fact)
fact(p) == p

Let me introduce a function bottom which raises an exception when
called:

>>> bottom()
Traceback (most recent call last):
...
Bottom

In the context of denotational semantics bottom is interpreted as a
computation that does not terminate. Raising a runtime error is a good
approximation to illustrate this point.

Let's consider the sequence

fact^i(bottom)

where fact^i shall be read as i-many application of the function fact:

fact^0(bottom) => bottom
fact^1(bottom) => fact(bottom)
fact^2(bottom) => fact(fact(bottom))
...

The function i_many_application accomplishes the task of chaining
functions i times. See below for its definition.

Let's get back to our example Z(fact)(5) and compute fact^i (bottom)(5)
for a few i:

>>> fact(bottom)(5)
Traceback (most recent call last):
...
Bottom
>>> fact(fact(bottom))(5)
Traceback (most recent call last):
...
Bottom
>>> fact(fact(fact(bottom)))(5)
Traceback (most recent call last):
...
Bottom
>>> i_many_application(fact, 4)(bottom)(5)
Traceback (most recent call last):
...
Bottom
>>> i_many_application(fact, 5)(bottom)(5)
Traceback (most recent call last):
...
Bottom

No surprise here, on each invokation of fact its parameter is
decremented by one and has reached zero when we reach the bottom
function which raises the Bottom exception.

Let's try some more values for i:

>>> i_many_application(fact, 6)(bottom)(5)
120
>>> i_many_application(fact, 7)(bottom)(5)
120
>>> i_many_application(fact, 8)(bottom)(5)
120

For i > 5 the factorial of five is computed and this value does not
change if we increase i. The recursion stops at the depth of six when
fact's parameter reaches zero so intuitively for i > 5 we "don't
run into the bottom function".

Denotational semantic of loops
==============================

The sequence fact^i(bottom)(5) for arbitrary i starting at zero is

[⊥, ⊥, ⊥, ⊥, ⊥, ⊥, 120, 120, 120, ...]

120 is the lowest upper bound of this sequence:

∐_{i = 0}^{∞} fact^i(bottom)(5) = 120

and incidentally this is exactly what the fixed point combinator
defined above computes:

Z(fact) = ∐_{i = 0}^{∞} fact^i(bottom)
Z(fact)(5) = ∐_{i = 0}^{∞} fact^i(bottom)(5) = 120

If you are wondering where the loop is, it has been unrolled into a
series of recursive function calls. The non recursive variant of the
factorial function is

>>> def factorial(n):
...     result = n
...     while True:
...         if n == 1:
...             return result
...         else:
...             result = result * (n - 1)
...             n = n - 1
...     return result
>>> factorial(5)
120

Transforming this into a recursive function yields

>>> def factorial(x):
...     if x == 0:
...         return 1
...     else:
...         return x * factorial(x - 1)
>>> factorial(5)
120

or shorter
>>> def factorial(x):
...     return 1 if x == 0 else x * factorial(x - 1)
>>> factorial(5)
120

Note that we had to use the def statement to define factorial since
this function calls itself and thus needs itself to be bound to an
identifier. Can we avoid that?

The lambda statement allows us to define anonymous functions, functions
that aren't bound to an identifier:

>>> (lambda x: x * 2)(2)
4

But can we define anonymous functions that recursively compute a
value? The answer is yes and with the y-combinator we have the means
to do so:

>>> fact = lambda f: lambda x: 1 if x == 0 else x * f(x - 1)
>>> factorial = Z(fact)
>>> factorial(5)
120

Note that fact does some kind of recursion and at runtime the fact
function is bound to the formal parameter f. Let's write this even
shorter:

>>> Z(lambda f: lambda x: 1 if x == 0 else x * f(x - 1))(5)
120

And if we insert the very definition of the Z function we get a
purely functional expression that uses recursion without ever
binding a function to an identifier:

>>> (lambda f: (lambda x: f(lambda *args: x(x)(*args)))(lambda x: f(lambda *args: x(x)(*args))))(lambda f: lambda x: 1 if x == 0 else x * f(x - 1))(5)
120

This also demonstrates the lambda calculus' ability to do primitive
recursion (the same argument can be extended to µ-recursive
functions).
'''

class Bottom(RuntimeError): pass

def bottom(*args, **kwargs):
    raise Bottom()

def i_many_application(function, i):
    ur'''
    >>> s = lambda n: n + 1
    >>> s(0)
    1
    >>> i_many_application(s, 0)(0)
    0
    >>> i_many_application(s, 1)(0)
    1
    >>> i_many_application(s, 2)(0)
    2
    '''
    def callable(value):
        result = value
        for n in range(i):
            result = function(result)
        return result
    return callable

# definitions for Z and fact for interactive sessions
Z = lambda f: (lambda x: f(lambda *args: x(x)(*args)))(lambda x: f(lambda *args: x(x)(*args)))
fact = lambda f: lambda x: 1 if x == 0 else x * f(x - 1)