{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## λ calculus\n",
    "\n",
    "This is an appendix to upcoming book [\"Introduction to Theoretical Computer Science\"](http://introtcs.org), which is also available online as a Jupyter notebook in the  [boazbk/nandnotebooks](https://github.com/boazbk/nandnotebooks) on Github. You can also try the [live binder version](https://mybinder.org/v2/gh/boazbk/nandnotebooks/master?filepath=lambda.ipynb).\n",
    "\n",
    "The λ calculus is discussed in  [Chapter 7: \"Equivalent Models of Computation\"](http://introtcs.org/public/lec_07_other_models.html)\n",
    "\n",
    "[Click here](https://mybinder.org/v2/gh/boazbk/nandnotebooks/master?filepath=lambda.ipynb) for the live Binder version. (Service can sometimes be slow.)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This Python notebook provides a way to play with the lamdba calculus and  evaluate lambda expressions of the form `λvar1(exp1) λvar2(exp2) ...`. If you don't know Python you can safely ignore the Ptyhon code and skip below to where we actually talk about the λ calculus itself.\n",
    "\n",
    "To better fit with python there are two main differences:\n",
    "\n",
    "* Instead of writing `λvar.exp` we write `λvar(exp)`\n",
    "\n",
    "* Instead of simply concatenating two expressions `exp1 exp2` we use the `*` operator and write `exp1 * exp2`. We can also use `exp1, exp2` if they are inside a function call or a variable binding parenthesis.\n",
    "\n",
    "* To reduce an expression `exp`, use `exp.reduce()`\n",
    "\n",
    "* Since Python does not allow us to override the default `0` and `1` we use `_0` for `λx(y(y))` and `_1` for `λx(y(x))`. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Python code (can skip at first read)\n",
    "\n",
    "If you don't know Python feel free to skip ahead to the part where we play with the $\\lambda$ calculus itself.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "# We define an abstract base class Lambdaexp for lambda expressions\n",
    "# It has the following subclasses:\n",
    "# Applicableexp: an expression of the form λx.exp\n",
    "# Combinedexp: an expression of the form (exp,exp')\n",
    "# Boundvar: an expression corresponding to a bounded variable\n",
    "# Unboundvar: an expression corresponding to a free variable\n",
    "#\n",
    "# The main operations in a Lambdaexp are:\n",
    "# 1. Replace: given exp,x and exp', obtain the expression exp[x-->exp']\n",
    "# 2. Reduce: continuously evaluate expressions to obtain a simpler form\n",
    "# 3. Apply: given exp,exp', if exp is applicable then apply it to exp', otherwise combine the two \n",
    "# (we also use the * operator for it)\n",
    "\n",
    "\n",
    "\n",
    "import operator ,functools\n",
    "\n",
    "class Lambdaexp:\n",
    "    \"\"\"Lambda expressions base class\"\"\"\n",
    "    \n",
    "    counter = 0\n",
    "    call_by_name = True  # if False then do normal form evaluation.\n",
    "    \n",
    "    def __init__(self):\n",
    "        self.mykey = {}\n",
    "    \n",
    "    def apply(self,other): \n",
    "        \"\"\"Apply expression on an argument\"\"\"\n",
    "        return self*other\n",
    "        \n",
    "    def _reduce(self,maxlevel=100): \n",
    "        \"\"\"Reduce expression\"\"\"\n",
    "        return self\n",
    "    \n",
    "    def replace(self,old,new): \n",
    "        \"\"\"Replace all occurences of old with new\"\"\"\n",
    "        raise NotImplemented\n",
    "\n",
    "    \n",
    "    def bounded(self): \n",
    "        \"\"\"Set of bounded variables inside expression\"\"\"\n",
    "        return set()\n",
    "\n",
    "    def asstring(self, m,pretty=False):\n",
    "        \"\"\"Represent self as a string mapping bounded variables to particular numbers.\"\"\"\n",
    "        raise NotImplemented\n",
    "\n",
    "    #------------------------------------------------------------------------------#\n",
    "    # Ignore this code  in first read: Python specific details\n",
    "\n",
    "    lambdanames = {}\n",
    "    reducedstrings = {}\n",
    "   \n",
    "    def reduce(self,maxlevel=100):\n",
    "        if not maxlevel: return self\n",
    "        #m = {b:b for b in self.bounded() }\n",
    "        #t = Lambdaexp.reducedstrings.get((self.asstring(m),maxlevel),None)\n",
    "        #if t: return t\n",
    "        return self._reduce(maxlevel)\n",
    "        #k = t.asstring(m)\n",
    "        #for i in range(maxlevel+1):  \n",
    "        #    Lambdaexp.reducedstrings[(k,i)] = t\n",
    "        #return t\n",
    "            \n",
    "            \n",
    "        \n",
    "    def __mul__(self,other):\n",
    "        \"\"\"Use * for combining.\"\"\"\n",
    "        return Combinedexp(self,other) if other else self\n",
    "    \n",
    "    def __call__(self,*args): \n",
    "        \"\"\"Use function call for application\"\"\"\n",
    "        return functools.reduce(operator.mul,args,self)\n",
    "    \n",
    "    def _key(self,maxlevel=100): \n",
    "        #if maxlevel not in self.mykey: \n",
    "        return self.reduce(maxlevel).__repr__()\n",
    "            # for i in range(maxlevel+1): self.mykey[i] = s \n",
    "        # return self.mykey[maxlevel]\n",
    "\n",
    "    def __eq__(self,other): return self._key()==other._key() if isinstance(other,Lambdaexp) else False\n",
    "    def __hash__(self): return hash(self._key())\n",
    "    \n",
    "        \n",
    "        \n",
    "    def __repr__(self,pretty=False):\n",
    "        B = sorted(self.bounded())\n",
    "        m ={}\n",
    "        for v in B: m[v] = len(m)\n",
    "        return self.asstring(m,pretty)\n",
    "    \n",
    "    \n",
    "    def _repr_pretty_(self, p, cycle):\n",
    "        if cycle: p.text( self._repr())\n",
    "        p.text( self.reduce().__repr__(True))     \n",
    "        \n",
    "    def addconst(self,srep):\n",
    "        \"\"\"Return either exp.string or replaced with a keyword if it's in table.\"\"\"\n",
    "        if self in Lambdaexp.lambdanames:  return blue(Lambdaexp.lambdanames[self])\n",
    "        return srep\n",
    "\n",
    "      #------------------------------------------------------------------------------#\n",
    "\n",
    "\n",
    "    \n",
    "    \n",
    " "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "#-------------------------------------------------#\n",
    "# Utility functions: print color\n",
    "def bold(s,justify=0):\n",
    "    return \"\\x1b[1m\"+s.ljust(justify)+\"\\x1b[21m\"\n",
    "\n",
    "def underline(s,justify=0):\n",
    "    return \"\\x1b[4m\"+s.ljust(justify)+\"\\x1b[24m\"\n",
    "\n",
    "def red(s,justify=0):\n",
    "    return  \"\\x1b[31m\"+s.ljust(justify)+\"\\x1b[0m\"\n",
    "\n",
    "\n",
    "def green(s,justify=0):\n",
    "    return  \"\\x1b[32m\"+s.ljust(justify)+\"\\x1b[0m\"\n",
    "\n",
    "\n",
    "def blue(s,justify=0):\n",
    "    return  \"\\x1b[34m\"+s.ljust(justify)+\"\\x1b[0m\"\n",
    "#--------------------------------------------------#"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "  \n",
    "    \n",
    "    \n",
    "\n",
    "        \n",
    "class Applicableexp(Lambdaexp):\n",
    "    \"\"\"Lambda expression that can be applied\"\"\"\n",
    "    \n",
    "    def __init__(self,exp,name):\n",
    "        Lambdaexp.counter += 1\n",
    "        self.arg =  Lambdaexp.counter\n",
    "        self.inner = exp.replace(name,Boundvar(self.arg))\n",
    "        super().__init__()    \n",
    "    \n",
    "    def apply(self,other): \n",
    "        return self.inner.replace(self.arg,other)\n",
    "    \n",
    "    def replace(self,old,new): \n",
    "        if self.arg==old: self.arg = new.myid\n",
    "        return Applicableexp(self.inner.replace(old,new),self.arg)\n",
    "    \n",
    "    def bounded(self): return self.inner.bounded()|{self.arg}\n",
    "    \n",
    "    def _reduce(self,maxlevel=100):\n",
    "        if Lambdaexp.call_by_name: return self \n",
    "        # in call by name there are no reductions inside abstractions\n",
    "        inner = self.inner.reduce(maxlevel-1)\n",
    "        return Applicableexp(inner,self.arg)\n",
    "    \n",
    "    def asstring(self, m,pretty=False):\n",
    "        if not pretty: return \"λ\"+Boundvar(self.arg).asstring(m,False)+\".(\"+self.inner.asstring(m)+\")\"\n",
    "        return self.addconst(green(\"λ\")+Boundvar(self.arg).asstring(m,True)+\".(\"+self.inner.asstring(m,True)+\")\")\n",
    "        \n",
    "        \n",
    " \n",
    "  "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "class Boundvar(Lambdaexp):\n",
    "    \"\"\"Bounded variable\"\"\"\n",
    "    def __init__(self,arg): \n",
    "        self.myid = arg\n",
    "        super().__init__()\n",
    "        \n",
    "    def replace(self,argnum,exp): return exp if argnum==self.myid else self\n",
    "    \n",
    "    def bounded(self): return { self.myid }\n",
    "\n",
    "    def asstring(self, m,pretty=False):\n",
    "        arg = m.get(self.myid,self.myid) \n",
    "        return chr(ord('α')+arg)\n",
    "    \n",
    "\n",
    "class Unboundvar(Lambdaexp):\n",
    "    \"\"\"Unbounded (free) variable.\"\"\"\n",
    "    def __init__(self,name): \n",
    "        self.name = name\n",
    "        super().__init__()\n",
    "        \n",
    "    def replace(self,name,arg): return arg if name==self.name else self\n",
    "    \n",
    "    def asstring(self, m,pretty=False):\n",
    "        return self.addconst(self.name) if pretty else self.name\n",
    "\n",
    "   \n",
    "    \n",
    "class Combinedexp(Lambdaexp):\n",
    "    \"\"\"Combined expression of two expressions.\"\"\"\n",
    "    def __init__(self,exp1,exp2):\n",
    "        self.exp1 = exp1\n",
    "        self.exp2 = exp2\n",
    "        super().__init__()\n",
    "    \n",
    "    def replace(self,arg,exp): \n",
    "        return Combinedexp(self.exp1.replace(arg,exp),self.exp2.replace(arg,exp))\n",
    "    \n",
    "    def bounded(self): return self.exp1.bounded()|self.exp2.bounded()\n",
    "    \n",
    "    \n",
    "    def _reduce(self,maxlevel=100):\n",
    "        if not maxlevel: return self\n",
    "        e1 = self.exp1.reduce(maxlevel-1)\n",
    "        if isinstance(e1,Applicableexp): \n",
    "            return  e1.apply(self.exp2).reduce(maxlevel-1)\n",
    "        return Combinedexp(e1,self.exp2)\n",
    "    \n",
    "    def asstring(self, m,pretty=False):\n",
    "        s = f\"({self.exp1.asstring(m,False)} {self.exp2.asstring(m,False)})\"\n",
    "        if not pretty: return s\n",
    "        return f\"({self.exp1.asstring(m,True)} {self.exp2.asstring(m,True)})\"\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "class λ:\n",
    "    \"\"\"Binds a variable name in a lambda expression\"\"\"\n",
    "\n",
    "    def __init__(self,*varlist): \n",
    "        \"\"\"\n",
    "        Get list of unbounded variables (for example a,b,c) and returns an operator that binds an expresion exp to\n",
    "        λa(λb(λc(exp))) and so on.\"\"\"\n",
    "        if not varlist: raise Exception(\"Need to bind at least one variable\")\n",
    "        self.varlist = varlist[::-1]\n",
    "        \n",
    "    \n",
    "    def bindexp(self,exp):\n",
    "        res = exp\n",
    "        for v in self.varlist: \n",
    "            res = Applicableexp(res,v.name)\n",
    "        return res\n",
    "    \n",
    "    #------------------------------------------------------------------------------#\n",
    "    # Ignore this code  in first read: Python specific details\n",
    "\n",
    "    \n",
    "    def __call__(self,*args):\n",
    "        exp = functools.reduce(operator.mul,args[1:],args[0])\n",
    "        return self.bindexp(exp)\n",
    "    #------------------------------------------------------------------------------#"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Initalization \n",
    "\n",
    "The above is all the code for implementing the λ calculus. We now add some convenient global variables: \n",
    "λa .... λz and a ... z for variables, and 0 and 1."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [],
   "source": [
    "Lambdaexp.lambdanames  = {}\n",
    "import string\n",
    "\n",
    "def initids(g):\n",
    "    \"\"\"Set up parameters a...z and correpsonding Binder objects λa..λz\"\"\"\n",
    "    lcase = list(string.ascii_lowercase)\n",
    "    ids = lcase + [n+\"_\" for n in lcase]\n",
    "    for name in ids:\n",
    "        var =  Unboundvar(name)\n",
    "        g[name] = var\n",
    "        g[\"λ\"+name] = λ(var)\n",
    "        Lambdaexp.lambdanames[var] = name"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [],
   "source": [
    "initids(globals())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[32mλ\u001b[0mα.(α)"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# testing...\n",
    "λy(y)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[32mλ\u001b[0mα.(\u001b[32mλ\u001b[0mβ.(α))"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "λ(a,b)(a)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [],
   "source": [
    "def setconstants(g,consts):\n",
    "    \"\"\"Set up constants for easier typing and printing.\"\"\"\n",
    "   \n",
    "    for name in consts:\n",
    "        Lambdaexp.lambdanames[consts[name]] = name\n",
    "        if name[0].isalpha(): \n",
    "            g[name]=consts[name]\n",
    "            \n",
    "        else: # Numeric constants such as 0 and 1 are replaced by _0 and _1\n",
    "            g[\"_\"+name] = consts[name]\n",
    "    \n",
    "setconstants(globals(),{\"1\" : λ(x,y)(x) , \"0\" : λ(x,y)(y)  })\n",
    "\n",
    "def register(g,*args):\n",
    "    for name in args:\n",
    "        Lambdaexp.lambdanames[g[name]] = name"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34m1\u001b[0m"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# testing\n",
    "λa(λz(a))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## λ calculus playground\n",
    "\n",
    "We can now start playing with the λ calculus\n",
    "\n",
    "If you want to use the λ character you can copy paste it from here:  λ"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let's start with the function λx,y.y, also known as 0 "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34m0\u001b[0m"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "λa(λb(b))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Our string representation recognizes that this is the 0 function and so \"pretty prints\" it. To see the underlying λ expression you can use `__repr__()`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'λα.(λβ.(β))'"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "λa(λb(b)).__repr__()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let's check that `_0` and `_1` behave as expected"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34ma\u001b[0m"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "_1(a,b)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34mb\u001b[0m"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "_0(a,b)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34m1\u001b[0m"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "_1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[32mλ\u001b[0mα.(\u001b[34m0\u001b[0m)"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "_1(_0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'λα.(λβ.(α))'"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "_1.__repr__()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Here is an exercise:\n",
    "\n",
    "__Question:__ Suppose that $F = \\lambda f. (\\lambda x. (f x)f)$, $1 = \\lambda x.(\\lambda y.x)$ and $0=\\lambda x.(\\lambda y.y)$.\n",
    "What is $F \\; 1\\; 0$?\n",
    "\n",
    "__a.__ $1$\n",
    "\n",
    "__b.__ $0$\n",
    "\n",
    "__c.__ $\\lambda x.1$\n",
    "\n",
    "__d.__ $\\lambda x.0$"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let's evaluate the answer"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {
    "collapsed": true
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[32mλ\u001b[0mα.(\u001b[32mλ\u001b[0mβ.(((α β) α)))"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "F=λf(λx((f*x)*f))\n",
    "F"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[32mλ\u001b[0mα.(((\u001b[34m1\u001b[0m α) \u001b[34m1\u001b[0m))"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "F(_1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34m0\u001b[0m"
      ]
     },
     "execution_count": 21,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "F(_1,_0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [],
   "source": [
    "ID = λa(a)\n",
    "register(globals(),\"ID\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Some useful functions\n",
    "\n",
    "Let us now add some of the basic functions in the λ calculus"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "NIL= λf(_1)\n",
    "PAIR =λx(λy(λf(f*x*y)))\n",
    "ISEMPTY= λp(p *(λx(λy(_0))))\n",
    "HEAD = λp(p(_1))\n",
    "TAIL  =λp(p * _0)\n",
    "IF = λ(a,b,c)(a * b * c)\n",
    "\n",
    "register(globals(),\"NIL\", \"PAIR\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "And test them out"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34m1\u001b[0m"
      ]
     },
     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "ISEMPTY(NIL)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34mb\u001b[0m"
      ]
     },
     "execution_count": 25,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "IF(_0,a,b)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34ma\u001b[0m"
      ]
     },
     "execution_count": 26,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "IF(_1,a,b)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {},
   "outputs": [],
   "source": [
    "P=PAIR(_0,_1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34m0\u001b[0m"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "HEAD(P)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34m1\u001b[0m"
      ]
     },
     "execution_count": 29,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "TAIL(P)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can make lists of bits as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "metadata": {},
   "outputs": [],
   "source": [
    "def makelist(*L):\n",
    "    \"\"\"Construct a λ list of _0's and _1's.\"\"\"\n",
    "    if not L: return NIL\n",
    "    h = _1 if L[0]   else _0\n",
    "    return PAIR(h,makelist(*L[1:]))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[32mλ\u001b[0mα.(((α \u001b[34m1\u001b[0m) ((\u001b[34mPAIR\u001b[0m \u001b[34m0\u001b[0m) ((\u001b[34mPAIR\u001b[0m \u001b[34m1\u001b[0m) \u001b[34mNIL\u001b[0m))))"
      ]
     },
     "execution_count": 31,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "L=makelist(1,0,1)\n",
    "L"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34m1\u001b[0m"
      ]
     },
     "execution_count": 32,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "HEAD(L)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[32mλ\u001b[0mα.(((α \u001b[34m0\u001b[0m) ((\u001b[34mPAIR\u001b[0m \u001b[34m1\u001b[0m) \u001b[34mNIL\u001b[0m)))"
      ]
     },
     "execution_count": 33,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "TAIL(L)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34m0\u001b[0m"
      ]
     },
     "execution_count": 34,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "HEAD(TAIL(L))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34m1\u001b[0m"
      ]
     },
     "execution_count": 35,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "HEAD(TAIL(TAIL(L)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Recursion\n",
    "\n",
    "We now show how we can implement recursion in the λ calculus. We start by doing this in Python.\n",
    "Let's try to define XOR in a recursive way and then avoid recursion"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "1"
      ]
     },
     "execution_count": 36,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# XOR of 2 bits\n",
    "def xor2(a,b): return 1-b if a else b\n",
    "\n",
    "# XOR of a list - recursive definition\n",
    "def xor(L): return xor2(L[0],xor(L[1:])) if L else 0\n",
    "\n",
    "xor([1,0,0,1,1])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now let's try to make a _non recursive_ definition, by replacing the recursive call with a call to `me` which is a function that is given as an extra argument:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "metadata": {},
   "outputs": [],
   "source": [
    "def myxor(me,L): return 0 if not L else xor2(L[0],me(L[1:]))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The first idea is to try to implement `xor(L)` as `myxor(myxor,L)` but this will not work:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "myxor() missing 1 required positional argument: 'L'\n"
     ]
    }
   ],
   "source": [
    "def xor(L): return myxor(myxor,L)\n",
    "\n",
    "try: \n",
    "    xor([0,1,1])\n",
    "except Exception as e:\n",
    "    print(e)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The issue is that `myxor` takes _two_ arguments, while in `me` we only supply one.\n",
    "Thus, we will modify `myxor` to `tempxor` where we replace the call `me(x)` with `me(me,x)`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "metadata": {},
   "outputs": [],
   "source": [
    "def tempxor(me,L): return myxor(lambda x: me(me,x),L)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let's check this out:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "1"
      ]
     },
     "execution_count": 40,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def xor(L): return tempxor(tempxor,L)\n",
    "\n",
    "xor([1,0,1,1])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This works!\n",
    "\n",
    "Let's now generatlize this to any function. The `RECURSE` operator will take a function `f` that takes two arguments `me` and `x` and return a function `g`  where the calls to  `me` are replaced with calls to `g`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "0"
      ]
     },
     "execution_count": 41,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def RECURSE(f):\n",
    "    def ftemp(me,x): return f(lambda x: me(me,x),x)\n",
    "    return lambda x: ftemp(ftemp,x)\n",
    "\n",
    "xor = RECURSE(myxor)\n",
    "\n",
    "xor([1,1,0])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### The λ version\n",
    "\n",
    "We now repeat the same arguments with the λ calculus:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "metadata": {},
   "outputs": [],
   "source": [
    "# XOR of two bits\n",
    "XOR2 = λ(a,b)(IF(a,IF(b,_0,_1),b))\n",
    "\n",
    "# Recursive XOR with recursive calls replaced by m parameter\n",
    "myXOR = λ(m,l)(IF(ISEMPTY(l),_0,XOR2(HEAD(l),m(TAIL(l)))))\n",
    "\n",
    "# Recurse operator (aka Y combinator)\n",
    "RECURSE = λf((λm(f(m*m)))(λm(f(m*m))))\n",
    "\n",
    "# XOR function\n",
    "XOR = RECURSE(myXOR)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let's test this out:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 43,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34m1\u001b[0m"
      ]
     },
     "execution_count": 43,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "XOR(PAIR(_1,NIL)) # List [1]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 44,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34m0\u001b[0m"
      ]
     },
     "execution_count": 44,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "XOR(PAIR(_1,PAIR(_0,PAIR(_1,NIL)))) # List [1,0,1]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 45,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34m0\u001b[0m"
      ]
     },
     "execution_count": 45,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "XOR(makelist(1,0,1))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 46,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "\u001b[34m1\u001b[0m"
      ]
     },
     "execution_count": 46,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "XOR(makelist(1,0,0,1,1))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.6.5"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}