#!/usr/bin/env python
# coding: utf-8

# ### Finding Fibonacci Numbers Using Lambda Calculus

# Inspired by this article on github (posted on HN): https://gitlab.com/snippets/1879264, I, as a kind of experiment, did something different: wrote a Fibonacci numbers function using Lambda Calculus on it's own. 
# So, no numbers, no data structures, just anonymous functions. I have to do it in some language, for the sake of convenience I've choosen Python. The lambda function is a function of one variable (this variable could be also a function). That's how it looks: 

# In[1]:


lambda x: x + 41


# It's used in stright forward way:

# In[2]:


(lambda x: x + 41)(1)


# We bring the original, famous, Fibonacci function, and start to refactor it:

# In[3]:


def fibo(n):
    if n < 2:
        return 1
    else:
        return fibo(n - 1) + fibo (n - 2)


# As a sanity check, we will be checking that: fibo(5) == 8:

# In[4]:


fibo(5)


# #### Refactoring
# The first task: a few changes to functions.

# In[5]:


ONE = 1
SUB1 = lambda x: x - 1
SUB2 = lambda x: x - 2
ADD = lambda x, y: x + y
LESS_TWO = lambda x: x < 2

def fibo(n):
    if LESS_TWO(n):
        return ONE
    return ADD(fibo(SUB1(n)), fibo(SUB2(n)))


# In[6]:


fibo(5)


# We're changing ```if``` now, definining it as a function which takes three expressions: cond, true_exp, false_exp and evaluates it similar to Python's ```if```.

# In[7]:


IF = lambda cond, true_exp, false_exp: true_exp if cond else false_exp

def fibo(n):
    return IF(
        LESS_TWO(n),
        ONE,
        ADD(fibo(SUB1(n)), fibo(SUB2(n)))
        )


# In[8]:


fibo(5) # -> !$%!@


# Unfortunately this function blow up stack (RecursionError), because of Python's default parameter evaluation - before function computes it's body the all parameters are evaluated; but there is, in the third parameter, recurrence passed, so we ends in infinite loop. Normally Python's ```if``` (like many other imperative languages) doesn't work like that, it has a short circuit evaluation: parameters are evaluated only if necessery, here in the case of ```cond = true```, only the ```true_exp``` is evaluated. 
# The solution would be simulate in some way lazy evaluation, make thunks from parameters passed (i.e. surround them by lambdas) and functions from formal parametrs. Now the ```IF``` will call ```true_fun``` and ```false_fun``` if needed:

# In[10]:


IF = lambda cond, true_fun, false_fun: true_fun() if cond else false_fun()

def fibo(n):
    return IF(
        LESS_TWO(n),
        lambda: ONE,
        lambda: ADD(fibo(SUB1(n)), fibo(SUB2(n)))
        )


# In[11]:


fibo(5)


# Let's get rid of two argument functions; now we have:

# In[12]:


add = lambda x, y: x + y
add(40, 2)


# Refactoring in that way:

# In[13]:


add = lambda x: lambda y: x + y;
add(40)


# In[14]:


add(40)(2)


# Time to add it to ```fibo```:

# In[15]:


ONE = 1
SUB1 = lambda x: x - 1
SUB2 = lambda x: x - 2
ADD = lambda x: lambda y: x + y
LESS_TWO = lambda x: x < 2
IF = lambda cond, true_fun, false_fun: true_fun() if cond else false_fun()

def fibo(n):
    return IF(
        LESS_TWO(n),
        lambda: ONE,
        lambda: ADD(fibo(SUB1(n)))(fibo(SUB2(n)))
    )


# In[16]:


fibo(5)


# Refactoring ```IF``` in that way gives:

# In[17]:


ONE = 1
SUB1 = lambda x: x - 1
SUB2 = lambda x: x - 2
ADD = lambda x: lambda y: x + y
LESS_TWO = lambda x: x < 2
IF = lambda cond: lambda true_fun: lambda false_fun: true_fun(None) if cond else false_fun(None)

def fibo(n):
    return IF(
        LESS_TWO(n)
    )(
        lambda _: ONE
    )(
        lambda _: ADD(fibo(SUB1(n)))(fibo(SUB2(n)))
    )


# In[18]:


fibo(5)


# Function ```fibo```, still works, good. In the meantime, I've changed ```lambda expr``` to ```lambda _: expr``` - there is no "zero argument lambda" in Lambda Calcullus (underscore is not used variable in Python) and following, I'm calling functions from ```None``` - ```Null``` in Python in lambda definition.
# 
# Now ```def``` keyword (if all we have are lambdas, what's the point to edfine anything?:)), we change to simple assignment:

# In[19]:


fibo = lambda n: (
    IF(
        LESS_TWO(n)
    )(
        lambda _: ONE
    )(
        lambda _: ADD(fibo(SUB1(n)))(fibo(SUB2(n)))
    )
)


# Of course, there is not assignemnt in Lambda Calculus, i.e. we can't save name and call it later, the only way to create a new name is: ```lambda name```. So, we create a function and another function ```fibo``` inside it and double calls - now ```fibo``` calls function ```fibo```:

# In[20]:


fibo = lambda fibo: (
    lambda n: (
    IF(
        LESS_TWO(n)
    )(
        lambda _: ONE
    )(
        lambda _: ADD(fibo(fibo)(SUB1(n)))(fibo(fibo)(SUB2(n)))
    )
  )
)


# In[22]:


fibo(fibo)(5)


# We don't need name ```fibo```. let's change it, to, for example, ```Y```:-)

# In[23]:


fibo = lambda Y: (
    lambda n: (
    IF(
        LESS_TWO(n)
    )(
        lambda _: ONE
    )(
        lambda _: ADD(Y(Y)(SUB1(n)))(Y(Y)(SUB2(n)))
    )
  )
)


# In[24]:


fibo(fibo)(5)


# I've deleted name ```fibo```, so I don't need assignment now, the only thing is classical refactoring: body of a function in the place of it's name:

# In[25]:


(
lambda Y: (
    lambda n: (
    IF(
        LESS_TWO(n)
    )(
        lambda _: ONE
    )(
        lambda _: ADD(Y(Y)(SUB1(n)))(Y(Y)(SUB2(n)))
    )
  )
)
    )(
lambda Y: (
    lambda n: (
    IF(
        LESS_TWO(n)
    )(
        lambda _: ONE
    )(
        lambda _: ADD(Y(Y)(SUB1(n)))(Y(Y)(SUB2(n)))
    )
  )
)
    )(5)


# Nice, works, looks less like programming - that's what we aim for:) But still many things to get rid of: booleans, numbers, arithmetic and logic operators...
# 
# We focus on numbers first, switching attention to Church Numerals, it's nothing wrong with it, the same like binary numbers in Python, they satisfy Peano Arithmetic axioms - means they are equally good to express arithmetic. 
# This what we see on screen: ```1, 3, 42, 1000``` are just numerals, under the hood, in Python are binary, here will be lambdas.
# So, numbers from scratch (from functions): number will be: function, which takes function and element (of course there is no two valued functions - it's function from function) and returns that function appriopriate number of times - zero for zero, one for one, etc...

# In[26]:


ZERO = lambda f: lambda x: x
ONE = lambda f: lambda x: f(x)
TWO = lambda f: lambda x: f(f(x))


# We also need a trick to compel Python to print it as a number:

# In[28]:


ZERO(lambda x: x + 1)(0)


# Cool, so we define more numbers and some functions:

# In[29]:


ZERO = lambda f: lambda x: x
ONE = (lambda f: lambda x: f(x))
TWO = (lambda f: lambda x: f(f(x)))
THREE = lambda f: lambda x: f(f(f(x)))
FIVE = lambda f: lambda x: f(f(f(f(f(x)))))
EIGHT = lambda f: lambda x: f(f(f(f(f(f(f(f(x)))))))) 
IDENTITY = lambda n: (lambda f: lambda x: n(f)(x))
INCREMENT = (lambda n: (lambda f: lambda x: f(n(f)(x))))
ADD = (lambda n: lambda m: n(INCREMENT)(m))  # use increment on m n times
SUBSTRACT = (lambda m: lambda n: n(DECREMENT)(m))
MULT = lambda n: lambda m: n(lambda a: ADD(m)(a))(ZERO)
DECREMENT = \
    (
    (lambda n:
     lambda f:
     lambda x: n(lambda g: lambda h: h(g(f)))
     (lambda u: x)
     (lambda u: u))
)


# There is crucial and looking odd function ```IDENTITY```, but it's correct: when applied to one numeral returns it as we want, cause ```n``` and ```f``` will just passed, but appllied to more arguments returns different result:

# In[30]:


IDENTITY(TWO)(lambda x: x + 1)(0)


# In[31]:


IDENTITY(TWO)(TWO)(lambda x: x + 1)(0)


# So, OK, ```IDENTITY``` changes easily to incrementation (by 1): to make 2 from 1, etc... we need to wrap the body of a function with ```f```.
# Having the incrementation we have the addition: ```m + n``` is incrementation of ```m``` ```n``` times.
# Alsa, we have multiplication: it's ```n``` times addition:

# In[32]:


ADD(ONE)(TWO)(lambda x: x + 1)(0)


# The same from the ```DECREMENT``` we have the substraction:
# 

# In[33]:


SUBSTRACT(ADD(ONE)(ONE))((ONE))(lambda x: x + 1)(0)


# That's great, we have the arithmetic, time for boolean, true and false first:

# In[34]:


NONE = (lambda a: a)
TRUE = (lambda m: lambda n: m(NONE))
FALSE = (lambda m: lambda n: n(NONE))


# True and False are just conditionals retrurns their, appriopriate, the first and the second element, called on ```NONE``` it's Python, will refactor later. 
# We have, also, ```to_bool``` function to cooperate with Python:

# In[35]:


def to_bool(p):  
    return IF(p)(lambda _: True)(lambda _: False)


# In[36]:


to_bool(TRUE)


# Time to ```IF```:

# In[37]:


IF = lambda b: lambda x: lambda y: b(x)(y)


# Works as intended:

# In[38]:


IF(TRUE)(lambda _ : 1)(lambda _: 2)


# Cool, switch to predicates, we change less than to less or equal, build first:

# In[39]:


IS_ZERO = lambda a: a(lambda x: FALSE)(TRUE)


# And, base on it:

# In[41]:


LESS_OR_EQ = lambda m: lambda n: IS_ZERO(SUBSTRACT(m)(n))


# Substraction returns zero if we substract greater number from smaller:
# 

# In[42]:


SUBSTRACT(ONE)(TWO)(lambda x: x + 1)(0)


# ```IS_ZERO``` called from zero returns true, from everything else false, so ```LESS_OR_EQ```works correct: check if difference is not zero:

# In[43]:


to_bool(LESS_OR_EQ(ONE)(TWO))


# #### Final Refactorings
# So now, we have all blocks:

# In[44]:


print(
    (
lambda Y : (
    lambda n:
    IF(
        LESS_OR_EQ(n)(ONE)
    )(
        lambda _: ONE
    )(
        lambda _: ADD(Y(Y)(SUBSTRACT(n)(ONE)))(Y(Y)(SUBSTRACT(n)(TWO))))
)
    )(
lambda Y : (
    lambda n:
    IF(
        LESS_OR_EQ(n)(ONE)
    )(
        lambda _: ONE
    )(
        lambda _: ADD(Y(Y)(SUBSTRACT(n)(ONE)))(Y(Y)(SUBSTRACT(n)(TWO))))
)
    )
    (FIVE)
    (lambda x: x + 1)(0)
) 


# Cool, but there is no names in Lambda Calculus (```ONE = lambda f: lambda x: f(x)```), so simply putting, again, function body instead of the name, we, finally have:

# In[45]:


print(
    (
lambda Y : (
    lambda n:
    (lambda b: lambda x: lambda y: b(x)(y))(
    (lambda m: lambda n: (lambda a: a(lambda x: (lambda m: lambda n: n((lambda a: a))))
    ((lambda m: lambda n: m((lambda a: a)))))((lambda m: lambda n: n((
    (lambda n:
     lambda f:
     lambda x: n(lambda g: lambda h: h(g(f)))
     (lambda u: x)
     (lambda u: u))
))(m))(m)(n)))(n)((lambda f: lambda x: f(x)))
    )(
        lambda _: (lambda f: lambda x: f(x))
    )(
        lambda _: (lambda n: lambda m: n((lambda n: (lambda f: lambda x: f(n(f)(x)))))(m))(Y(Y)((lambda m: lambda n: n((
    (lambda n:
     lambda f:
     lambda x: n(lambda g: lambda h: h(g(f)))
     (lambda u: x)
     (lambda u: u))
))(m))(n)
        ((lambda f: lambda x: f(x)))))(Y(Y)((lambda m: lambda n: n((
    (lambda n:
     lambda f:
     lambda x: n(lambda g: lambda h: h(g(f)))
     (lambda u: x)
     (lambda u: u))
))(m))(n)
        ((lambda f: lambda x: f(f(x)))))))
)
    )(
lambda Y : (
    lambda n:
    (lambda b: lambda x: lambda y: b(x)(y))(
        (lambda m: lambda n: (lambda a: a(lambda x: (lambda m: lambda n: n((lambda a: a))))
        ((lambda m: lambda n: m((lambda a: a)))))((lambda m: lambda n: n((
    (lambda n:
     lambda f:
     lambda x: n(lambda g: lambda h: h(g(f)))
     (lambda u: x)
     (lambda u: u))
))(m))(m)(n)))(n)((lambda f: lambda x: f(x)))
    )(
        lambda _: (lambda f: lambda x: f(x))
    )(
        lambda _: (lambda n: lambda m: n((lambda n: (lambda f: lambda x: f(n(f)(x)))))(m))(Y(Y)((lambda m: lambda n: n((
    (lambda n:
     lambda f:
     lambda x: n(lambda g: lambda h: h(g(f)))
     (lambda u: x)
     (lambda u: u))
))(m))(n)
        ((lambda f: lambda x: f(x)))))(Y(Y)((lambda m: lambda n: n((
    (lambda n:
     lambda f:
     lambda x: n(lambda g: lambda h: h(g(f)))
     (lambda u: x)
     (lambda u: u))
))(m))(n)
        ((lambda f: lambda x: f(f(x)))))))
)
    )
    (lambda f: lambda x: f(f(f(f(f(x))))))
    (lambda x: x + 1)(0)
) 


# I've added ```print``` instruction in the last two, due to some Python indentation mess (but it's not invalidate the main  argument). 
# Job's done, building from something small, like lambda functions, we have fairly complicated function (Fibonacci). 
# Salute to Lambda Calculus!
# Thanks for reading!