Church Python

pythedral.py

# Void

VOID = lambda void: void



# Booleans / Conditionals

IF = lambda c: lambda t: lambda f: c(t)(f)

TRUE = lambda t: lambda f: t

FALSE  = lambda t: lambda f: f

print (IF (TRUE) ("true") ("false"))
print (IF (FALSE) ("true") ("false"))


TRUE = lambda t: lambda f: t()

FALSE = lambda t: lambda f: f()

print (IF (TRUE) (lambda: "true") (lambda: "false"))
print (IF (FALSE) (lambda: "true") (lambda: "false"))



# Numerals

ZERO = lambda f: lambda z: z

SUCC = lambda n: lambda f: lambda z: (f(n(f)(z)))

SUM = (lambda a: lambda b: lambda f: lambda z:
  a(f)(b(f)(z)))

MUL = (lambda a: lambda b: lambda f: lambda z:
  a(lambda z:b(f)(z))(z))

natify = lambda n: n (lambda x: x + 1) (0)

print (natify(ZERO))

print (natify(SUCC(ZERO)))

print (natify(SUCC(SUCC(ZERO))))

ONE = SUCC(ZERO)

TWO = SUCC(ONE)

FOUR = SUM(TWO)(TWO)

SIXTEEN = MUL(FOUR)(FOUR)

print (natify(FOUR))

print (natify(SIXTEEN))



# Pairs

PAIR = lambda l: lambda r: lambda f: f(l)(r)

LEFT = lambda p: p(lambda l: lambda r: l)

RIGHT = lambda p: p(lambda l: lambda r: r)

print (LEFT (PAIR ("left") ("right")))

print (RIGHT (PAIR ("left") ("right")))



# Lists

NIL = lambda oncons: lambda onnil: onnil(VOID)

CONS = (lambda hd: lambda tl:
         lambda oncons: lambda onnil: 
          oncons(hd)(tl))

CONSP = lambda l: l (lambda hd: lambda tl: TRUE) (lambda void: FALSE)

NILP = lambda l: l (lambda hd: lambda tl: FALSE) (lambda void: TRUE)

HEAD = lambda l: l (lambda hd: lambda tl: hd) (VOID)

TAIL = lambda l: l (lambda hd: lambda tl: tl) (VOID)


print (IF (CONSP(NIL)) (lambda: "cons") (lambda: "nil"))

print (IF (CONSP(CONS(10)(20))) (lambda: "cons") (lambda: "nil"))

print (HEAD (CONS ("head") ("tail")))

print (TAIL (CONS ("head") ("tail")))



# Non-termination

U = lambda f: f(f)

# Omega = U(U)  # Stack over-flow from infinite loop



# Factorial

fact = U(lambda h: lambda n: 1 if n <= 0 else n * (U(h))(n-1))

print (fact(5))



# Y combinator

# Y(F) = x   such that   x = F(x)

# Y(F) = x   such that   x = F(Y(F))

# Y(F) = F(Y(F))

# Y = lambda F: F(Y(F))  # works for call-by-name

Y = lambda F: F(lambda x: Y(F)(x))

fact = Y(lambda f: lambda n: 1 if n <= 0 else n * f(n-1))

print (fact(6))


Y = U(lambda h: lambda F: F(lambda x: U(h)(F)(x)))

fact = Y(lambda f: lambda n: 1 if n <= 0 else n * f(n-1))

print (fact(7))


Y = (lambda h: lambda F: F(lambda x: h(h)(F)(x)))(lambda h: lambda F: F(lambda x: h(h)(F)(x)))

fact = Y(lambda f: lambda n: 1 if n <= 0 else n * f(n-1))

print (fact(8))

R1 = (((lambda f: (((f)((lambda f: ((lambda z: (((f)(((f)(((f)(((f)(((f)(z)))))))))))))))))))((((((lambda y: ((lambda F: (((F)((lambda x: (((((((y)(y)))(F)))(x)))))))))))((lambda y: ((lambda F: (((F)((lambda x: (((((((y)(y)))(F)))(x)))))))))))))((lambda f: ((lambda n: ((((((((((((lambda n: (((((n)((lambda _: ((lambda t: ((lambda f: (((f)((lambda void: (void)))))))))))))((lambda t: ((lambda f: (((t)((lambda void: (void)))))))))))))((((((lambda n: ((lambda m: (((((m)((lambda n: ((lambda f: ((lambda z: (((((((n)((lambda g: ((lambda h: (((h)(((g)(f)))))))))))((lambda u: (z)))))((lambda u: (u)))))))))))))(n)))))))(n)))((lambda f: ((lambda z: (z)))))))))((lambda _: ((((lambda n: (((((n)((lambda _: ((lambda t: ((lambda f: (((f)((lambda void: (void)))))))))))))((lambda t: ((lambda f: (((t)((lambda void: (void)))))))))))))((((((lambda n: ((lambda m: (((((m)((lambda n: ((lambda f: ((lambda z: (((((((n)((lambda g: ((lambda h: (((h)(((g)(f)))))))))))((lambda u: (z)))))((lambda u: (u)))))))))))))(n)))))))((lambda f: ((lambda z: (z)))))))(n)))))))))((lambda _: ((lambda t: ((lambda f: (((f)((lambda void: (void)))))))))))))((lambda _: ((lambda f: ((lambda z: (((f)(z)))))))))))((lambda _: ((((((lambda n: ((lambda m: ((lambda f: ((lambda z: (((((m)(((n)(f)))))(z)))))))))))(n)))(((f)((((((lambda n: ((lambda m: (((((m)((lambda n: ((lambda f: ((lambda z: (((((((n)((lambda g: ((lambda h: (((h)(((g)(f)))))))))))((lambda u: (z)))))((lambda u: (u)))))))))))))(n)))))))(n)))((lambda f: ((lambda z: (((f)(z))))))))))))))))))))))))

print (natify(R1))