User talk:I am islptng/Lambda Calculus Tutorial

My notation for lambda calculus:

1. Lambda:

!ab

2. Applyment:

`ab

Almost Interpreter:

def tostr(o,depth=1):
	a = "xyztpqrsfghijklmnoabcde"
	if isinstance(o,Apply): return "`%s%s" % (tostr(o.func,depth),tostr(o.arg,depth))
	if isinstance(o,Lambda): return "!%s%s" % (a[depth-1],tostr(o.body,depth+1))
	if isinstance(o,int): return a[depth-o-1]
	return o

def subst(o,repl,match=1):
	if isinstance(o,Apply): return Apply(subst(o.func,repl,match),subst(o.arg,repl,match))
	if isinstance(o,Lambda):
		if isinstance(repl,int):# and repl > match:
			return Lambda(subst(o.body,repl+1,match+1))
		return Lambda(subst(o.body,repl,match+1))
	if isinstance(o,int):
		if o == match: return repl
		if o > match: return o - 1
	return o

class Apply:
	def __init__(self,func,arg):
		self.func, self.arg = func, arg
	__repr__,__str__ = tostr,tostr
	__ne__ = lambda self,other: isinstance(other,Apply) and (self.func != other.func) and (self.arg != other.arg)

class Lambda:
	def __init__(self,body):
		self.body = body
	__repr__,__str__= tostr,tostr
	def __call__(self,arg): return subst(self.body,arg)
	__ne__ = lambda self,other: isinstance(other,Lambda) and (self.body != other.body)

def lc(s):
	s = list(s)
	def r(stk):
		nonlocal s
		stk = list(stk)
		if s[0] == "`":
			s.pop(0)
			a = r(stk)
			b = r(stk)
			return Apply(a,b)
		if s[0] == "!":
			s.pop(0)
			stk.append(s.pop(0))
			b = r(stk)
			return Lambda(b)
		if s[0] in stk:
			index = 1
			while stk[-index] != s[0]: index += 1
			s.pop(0)
			return index
		a = s.pop(0)
		return a
	return r([])

notlc = lambda t: not (isinstance(t,Apply) or isinstance(t,Lambda))

def betaonce(t):
	if isinstance(t,Lambda):
		if notlc(t.body): return t
		return Lambda(betaonce(t.body))
	if isinstance(t,Apply):
		try: return t.func(t.arg)
		except:pass
		if notlc(t.func):
			if notlc(t.arg): return Apply(t.func,t.arg)
			return Apply(t.func,betaonce(t.arg))
		if notlc(t.arg): return Apply(betaonce(t.func),t.arg)
		return Apply(betaonce(t.func),betaonce(t.arg))
	return t

def betareduce(t, prt = False):
	last = ""
	b = " "
	while str(last) != str(t):
		last,t = t,betaonce(t)
		if prt:
			print(b,last)
			b = "="
	return t

betareduce(lc(input().replace(" ","").replace("(","").replace(")","")),True)