Here is a Python notebook 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 $\lambda$ calculus itself.
One note is that the code is quite sensitive to spaces and parenthesis placements. In particular because, following Matt Might, we'll use Python's lambda expressions mechanisms, we'll need to wrap everything with extra parenthesis.
You can find better lambda evaluators online such as this one
There are also some annoying issues due to the fact that Python is an eager language which means that if we have a lambda expression such as $(\lambda x,y.x) (e)(f)$ then Python will evaluate $f$ even though it is not necessary for the computation. It is probably easy to avoid this (indeed maybe even using Matt Might's ideas above) but at the moment I just used a simple hack to handle this (which unfortuantely does not work for the Y combinator yet)
If you want to use the λ character you can copy paste it from here: λ
# convert lambda expression to python code
# all it amounts to is replacing λ with lambda and . with :
def ltop(exp):
return eval("("+exp.replace('λ','lambda ').replace('.',': ')+")")
# evaluate whether Python code corresponds to 0 or 1
def boolp(code):
res = code("first")("second")
if res=='first': return 1
if res=='second': return 0
return code
OK now that we got Python out of the way, let us play with this and see if it works
ltop("(λx.(λy.(y))) ('hello')('world')")
'world'
one = ltop("λx.(λy.(x))")
zero = ltop("λx.(λy.(y))")
one("first")("second")
'first'
Recall the following question from lecture:
We had the following question:
Question: Suppose that $F = \lambda f. (\lambda x. (f x)f)$, $1 = \lambda x.(\lambda y.x)$ and $0=\lambda x.(\lambda y.y)$. What is $F \; 1\; 0$?
a. $1$
b. $0$
c. $\lambda x.1$
d. $\lambda x.0$
Let's evaluate the answer
mystery=ltop("(λf.(λx.((f (x) (f)))))")
mystery (one)(zero)
<function __main__.ltop.<locals>.myfunc>
This is not very informative, but we can test if this is the zero function $\lambda x,y.y$ or the one function $\lambda y,x.y$ or something else
boolp(_)
0
NIL=ltop("λf.(one)")
PAIR =ltop("λx.(λy.(λf.((f (x)) (y))))")
ISEMPTY=ltop("λP.(P (λx.(λy.(zero))))")
HEAD = ltop("λP.(P (one))")
TAIL =ltop("λP.(P (zero))")
boolp(ISEMPTY(NIL))
1
HEAD(PAIR("first")("second"))
'first'
Now let's try something a little more interesting
Recall that we defined
$$APAR \;\;\; = \lambda f,L. (ISNIL \; L)\; 0 \; (XOR \; (HEAD \; L) \; (f \; f \; (TAIL \; L)) \color{green}{(**)}$$and claimed that $APAR \; APAR$ (i.e., $APAR$ applied to itself) is the parity function. Let's try this out
The following is the definition of XOR - can you see why?
XOR = ltop("λa.(λb.(a (b (zero) (one)) (b)))")
boolp(XOR(one)(one))
0
APAR=ltop("λf.(λL.((ISEMPTY (L)) (zero) (XOR (HEAD (L) ) ((f (f) ) (TAIL (L) )))))")
The code we used for ltop
above works perfectly fine for non recursive functions. However, because Python is an "eager" programming language, we have to be a little more careful in programming functions that do not necessarily halt. Below is a very crude hack where we simply stop the recursion if it goes on too deep, with the hope that we'll never care about the result of this branch. If you have a simpler/better way to do it, then please let me know.
Please skip ahead and ignore this cell: this is about details that are more specific to Python than to the λ calculus.
If you actually run this notebook, you'd want to use this definition of ltop
and rerun all the cells above using it.
# a little fancier version of ltop that keeps track of the lambda expression
# you can safely ignore this code
import inspect
from inspect import getouterframes, currentframe
MAX_RECURSION_DEPTH = 40
def ltop(exp):
global MAX_RECURSION_DEPTH
code = eval("("+exp.replace('λ','lambda ').replace('.',': ')+")")
if not callable(code): return code
def myfunc(x):
# if len(getouterframes(currentframe())) > MAX_RECURSION_DEPTH: # chop off
if len(inspect.stack()) > MAX_RECURSION_DEPTH:
return lambda x: (lambda y: y)
return code(x)
myfunc.lambdaexp = exp
return myfunc
The following will be slow because Python will go into unnecessary branches of the recursion.
par = APAR(APAR)
par(NIL)
<function __main__.ltop.<locals>.myfunc>
But at least we get the correct answer (0):
boolp(_)
0
Similarly we get the correct answers for the list $(1)$ and $(1,1)$, see below:
boolp(par (PAIR(one)(NIL)))
1
boolp(par (PAIR(one)(PAIR (one)(NIL) )))
0
The cells below correspond to a rough and still buggy part of the notebook. Feel free to ignore, and if you are a Python expert, feel free to tell me how to fix this.
Let's try to see if we can avoid some of these issues by defining IF which will do the "shortcut" evaluation
IF = ltop("λf.(λx.(λy.((f (λignore.x) (λignore.y)) (zero) )))")
#lambda f: lambda x: lambda y: (f (lambda ignore: x) (lambda ignore: y))("nonsense")
IF(zero)("hello")("world")
'world'
def nothalt():
x =0
while True:
x += 1
IF(one)("hello")(nothalt)
'hello'
APAR=ltop("λf.(λL.(IF (ISEMPTY (L)) (zero) (XOR (HEAD (L) ) ((f (f) ) (TAIL (L) )))))")
APAR(APAR)(NIL)
<function __main__.ltop.<locals>.myfunc>
boolp(_)
0
Wasn't any quicker but at least it's still correct. Let's now try to do the same thing via the Y combinator
PARREC = ltop("λf.(λL.((IF (ISEMPTY (L) ) (zero) (XOR (HEAD (L) ) (f (TAIL (L) ))))))")
Y = ltop("λf.((λx.(f (x (x)) )) (λy.(f (y (y) ))))")
par = Y(PARREC)
--------------------------------------------------------------------------- RecursionError Traceback (most recent call last) <ipython-input-310-d1e7ed7fffee> in <module>() ----> 1 par = Y(PARREC) <ipython-input-267-7b59671caeb1> in myfunc(x) 16 if len(inspect.stack()) > MAX_RECURSION_DEPTH: 17 return lambda x:x ---> 18 return code(x) 19 myfunc.lambdaexp = exp 20 return myfunc <string> in <lambda>(f) ... last 1 frames repeated, from the frame below ... <string> in <lambda>(x) RecursionError: maximum recursion depth exceeded
Well, might need a better hack for handling recursion .. if anyone has suggestions please let me know...
Please ignore the cells below, they are renmants from my attempt to evaluate the lambda expressions myself before I decided to use native Python
from inspect import getouterframes, currentframe # only for printing
# import os
import sys
sys.setrecursionlimit(3000)
OFFSET = len(getouterframes(currentframe()))
def list_lambdas(exp):
if not exp: return []
exp = exp.strip()
#print("Expression is:"+exp)
if not exp: return []
firstspace = exp.find(' ')
begin = exp.find('(')
if begin==-1 and firstspace==-1:
#print(exp+"->"+exp)
return [exp]
if (begin==-1) or (firstspace>-1 and firstspace<begin):
#print (exp + "->"+ str([exp[:firstspace]]+list_lambdas(exp[firstspace+1:])))
return [exp[:firstspace]]+list_lambdas(exp[firstspace+1:])
if begin>0 and exp[0]!='λ':
return [exp[:begin]]+list_lambdas(exp[begin:])
end = matchparen(exp,begin)
#print (exp +"->"+str([exp[:end+1]] +list_lambdas(exp[end+1:])))
return [exp[:end+1]] +list_lambdas(exp[end+1:])
uniquectr =0
def my_eval(exp,table={},debug=False):
def getunique():
global uniquectr
uniquectr +=1
return "u<"+str(uniquectr)+">"
def pr(s):
if debug: print(" "*(4*(len(getouterframes(currentframe()))-OFFSET))+s)
# pr(exp)
L = list_lambdas(exp)
if len(L)==0: return ""
if len(L)>1:
func = L[0]
if is_lambda(func):
e = beta_reduce(func,L[1],table,debug)
if len(L)>2: return my_eval(e+" "+" ".join(L[2:]),table,debug)
return e
func = my_eval(L[0],table,debug)
if is_lambda(func):
return my_eval(func+" "+" ".join(L[1:]),table,debug)
return func+" "+" ".join([my_eval(tmp,table,debug) for tmp in L[1:]])
exp = L[0]
if exp in table:
newtable = dict(table)
del newtable[exp]
pr(exp+"<-"+table[exp])
return my_eval(table[exp],newtable,debug)
if exp[0]=='(':
return my_eval(is_paren(exp),table,debug)
if is_lambda(exp):
[var,subexp] = is_lambda(exp)
newtable = dict(table)
if var in newtable: del newtable[var]
return "λ"+var+".("+my_eval(subexp,newtable,debug)+")"
#if table:
# [myexp,newtable,found] = replacevars(exp,table)
# if found:
# return my_eval(myexp,newtable,debug)
pr("Unparsed: "+exp)
return exp
def beta_reduce(func,arg,table,debug):
def pr(s):
if debug: print(" "*(4*(len(getouterframes(currentframe()))-OFFSET))+s)
if not is_lambda(func): raise Exception()
[var,subexp] = is_lambda(func)
newtable = dict(table)
if len(list_lambdas(arg))>1:
arg = "("+arg+")"
newtable[var] = arg
pr(subexp+" ["+var+"->"+arg+"]...")
res = my_eval(subexp,newtable,debug)
pr(subexp+"["+var+"->"+arg+ "] = "+ res)
return res
def is_lambda(exp):
if exp[0]!='λ': return False
varend = exp.find('.')
begin = varend+1
if exp[begin]=='(':
end = matchparen(exp,begin)
else:
begin = varend
end=len(exp)
var = exp[1:varend].strip()
subexp = exp[begin+1:end]
return [var,subexp]
def is_paren(exp):
if exp[0]!='(': return False
end = matchparen(exp,0)
return exp[1:end]
def matchparen(s,i):
depth = 1
if s[i]!='(': raise Exception()
j = i+1
while depth>0:
if s[j]=='(': depth += 1
if s[j]==')': depth -= 1
j += 1
if s[j-1]!=')': raise Exception()
return j-1
def replacevars(s,table):
newtable = dict(table)
found = False
for v in table:
if v!=table[v] and s.find(v)>-1:
s = s.replace(v,table[v])
del newtable[v]
found = True
return [s,newtable,found]
my_eval("λx.(x+y) 7",debug=True)
x+y [x->7]... x+y[x->7] = x+y
'x+y'
We will now go over the examples in the lecture. We use table
for our table of names.
We had the following question:
Question: Suppose that $F = \lambda f. (\lambda x. (f x)f)$, $1 = \lambda x.(\lambda y.x)$ and $0=\lambda x.(\lambda y.y)$. What is $F \; 1\; 0$?
a. $1$
b. $0$
c. $\lambda x.1$
d. $\lambda x.0$
We can answer this question by trying this out
table = {}
table["0"]="λx.(λy.(y))"
table["1"]="λx.(λy.(x))"
table["F"]="λf.(λx.((f x) f))"
my_eval("(F 1) 0",table,False)
'λx.(λy.(y))'
Which is the same as $0$
table = {}
table["0"]="λx.(λy.(y))"
table["1"]="λx.(λy.(x))"
table["NIL"]="λf.(1)"
table["PAIR"]="λx.(λy.(λf.((f x) y)))"
table["ISEMPTY"]="λP.(P (λx.(λy.(0))))"
table["HEAD"]="λP.(P 1)"
table["TAIL"]="λP.(P 0)"
my_eval("0 1 0",table,False)
'λx.(λy.(y))'
Now for the parity example.
Recall that we defined
$$APAR \;\;\; = \lambda f,L. (ISNIL \; L)\; 0 \; (XOR \; (HEAD \; L) \; (f \; f \; (TAIL \; L)) \color{green}{(**)}$$We first note that we can define XOR in the lambda calculus as follows
$$XOR = \lambda a,b.a(b 1 0)b$$# table["XOR"]="λvar.(λb.(var (b 0 1) b))"
table["XOR"]="λvar.(λb.(var (b λz.(λw.w) λt.(λs.t)) b))"
my_eval("(XOR 1) 1",table,False)
'λt.(λs.(t))'
my_eval("(λb.(1 (b 0 1) b))",table)
'λb.(b λx.(λy.(y)) λx.(λy.(x)))'
my_eval("λhello.(hello λx.(λy.(x)) hello) 0",table)
'λx.(λy.(y))'
my_eval("(0 λx.(λy.(x)) 0)",table)
'λx.(λy.(y))'
table["APAR"]="λf.(λL.((ISEMPTY L) 0 (XOR (HEAD L) ((f f) (TAIL L)))))"
my_eval("TAIL (PAIR 1 0)",table)
'λx.(λy.(y))'
table
{'0': 'λx.(λy.(y))', '1': 'λx.(λy.(x))', 'APAR': 'λf.(λL.((ISEMPTY L) 0 (XOR (HEAD L) ((f f) (TAIL L)))))', 'HEAD': 'λP.(P 1)', 'ISEMPTY': 'λP.(P (λx.(λy.(0))))', 'NIL': 'λf.(1)', 'PAIR': 'λx.(λy.(λf.((f x) y)))', 'TAIL': 'λP.(P 0)', 'XOR': 'λvar.(λb.(var (b λz.(λw.w) λt.(λs.t)) b))'}
my_eval("1",table)
'λx.(λy.(x))'
my_eval("ISEMPTY (PAIR 0 1) a b",table)
'b'
my_eval("APAR APAR",table,False)
'λL.(L λx.(λy.(λx.(λy.(y)))) λx.(λy.(y)) L λx.(λy.(x)) λf.(λL.(L λx.(λy.(λx.(λy.(y)))) λx.(λy.(y)) L λx.(λy.(x)) f f L λx.(λy.(y)) λz.(λw.(w)) λt.(λs.(t)) f f L λx.(λy.(y)))) λf.(λL.(L λx.(λy.(λx.(λy.(y)))) λx.(λy.(y)) L λx.(λy.(x)) f f L λx.(λy.(y)) λz.(λw.(w)) λt.(λs.(t)) f f L λx.(λy.(y)))) L λx.(λy.(y)) λz.(λw.(w)) λt.(λs.(t)) λf.(λL.(L λx.(λy.(λx.(λy.(y)))) λx.(λy.(y)) L λx.(λy.(x)) f f L λx.(λy.(y)) λz.(λw.(w)) λt.(λs.(t)) f f L λx.(λy.(y)))) λf.(λL.(L λx.(λy.(λx.(λy.(y)))) λx.(λy.(y)) L λx.(λy.(x)) f f L λx.(λy.(y)) λz.(λw.(w)) λt.(λs.(t)) f f L λx.(λy.(y)))) L λx.(λy.(y)))'
my_eval("(APAR APAR) NIL",table)
my_eval("(APAR APAR) (PAIR 0 (PAIR 1 NIL))",table, False)
'λx.(λy.(y))'
list_lambdas('f λx.(λy.(x))')
eval_lambda("NIL",table)
table["YCOMB"] = "λf.((λx.(f (x x))) (λy.(f (y y))))"
table["REC"] = "λf.(λL.(((ISEMPTY L) 0) (XOR (HEAD L) (f (TAIL L)))))"
my_eval("YCOMB REC",table)
'λx.(λy.(y))'
my_eval("(XOR 0 0)",table)
'λx.(λy.(y))'
my_eval("TAIL (PAIR 7 (PAIR 9 (PAIR 11 12)))",table)
'λf.(f 9 λf.(f 11 12))'
my_eval("ISEMPTY (PAIR 0 1)",table)
'λx.(λy.(y))'
my_eval("(YCOMB REC) (PAIR 0 NIL)",table)
'λy.(y)'