Upgrade to Pro — share decks privately, control downloads, hide ads and more …

Lambda as JS, or A Flock of Functions: Combinat...

Lambda as JS, or A Flock of Functions: Combinators, Lambda Calculus, and Church Encodings in JavaScript

🔗 Repo: https://github.com/glebec/lambda-talk
🔗 Video Part I: https://youtu.be/3VQ382QG-y4
🔗 Video Part II: https://youtu.be/pAnLQ9jwN-E

A presentation given at Fullstack Academy, by instructor Gabriel Lebec. The Lambda Calculus is a symbol manipulation system which suffices to calculate anything calculable. Developed in the 1930s by Alonzo Church, this branch of pure math forms the basis of many functional programming languages (such as Scheme and Haskell), and is explained here through the familiar lens of JavaScript. Along the way, related concepts like combinatory logic (investigated by Haskell B. Curry) and encodings are examined, building up boolean logic and arithmetic from scratch.

(Errata: 307–311 & 313, the JS function `eq` should be written as `gt`.)

Gabriel Lebec

August 24, 2017
Tweet

More Decks by Gabriel Lebec

Other Decks in Programming

Transcript

  1. as.js A FL O C K of FU N C

    T I O N S COMBINATORS, LAMBDA CALCULUS, & CHURCH ENCODINGS in JAVASCRIPT
  2. λ JS I(x) === ? I x = ? I

    := a.a I = a => a
  3. λ JS I(x) === x I x = x I

    := a.a I = a => a
  4. λ JS I(I) === ? I I = ? I

    := a.a I = a => a
  5. λ JS I(I) === I I I = I I

    := a.a I = a => a
  6. ?

  7. -CALCULUS SYNTAX expression ::= variable identifier | expression expression application

    | variable . expression abstraction | ( expression ) grouping
  8. f a f(a) f a b f(a)(b) (f a) b

    (f(a))(b) f (a b) f(a(b)) APPLICATIONS
  9. a.b a => b a.b x a => b(x) a.(b

    x) a => (b(x)) (a.b) x (a => b)(x) a.b.a a => b => a a.(b.a) a => (b => a) ABSTRACTIONS
  10. ((a.a)b.c.b)(x)e.f = (b.c.b) (x)e.f = (c.x) e.f = x β-REDUCTION*

    β-NORMAL FORM *not covered: evaluation order, variable collision avoidance
  11. λ JS M(I) === I(I) && I(I) === ? M

    I = I I = ? M := f.ff
  12. λ JS M(I) === I(I) && I(I) === I M

    I = I I = I M := f.ff
  13. λ JS M M = M M = M M

    = Ω // stack overflow M := f.ff M(M) === M(M) === M(M) === M(M) === M M(M) === M(M) === M(M) === M(M) === M M(M) === M(M) === M(M) === M(M) === M M(M) === M(M) === M(M) === M(M) === M M(M) === M(M) === M(M) === M(M) === M
  14. λ JS ω ω = ω ω = ω ω

    = Ω // stack overflow M := f.ff M(M) === M(M) === M(M) === M(M) === M M(M) === M(M) === M(M) === M(M) === M M(M) === M(M) === M(M) === M(M) === M M(M) === M(M) === M(M) === M(M) === M M(M) === M(M) === M(M) === M(M) === M
  15. a.b.c.b a => b => c => b abc.b a

    => b => c => b (a, b, c) => b = ABSTRACTIONS, again
  16. λ JS K = a => b => a K

    := ab.a = a.b.a
  17. λ JS K = a => b => a K

    := ab.a = a.b.a
  18. λ JS K = a => b => a K

    := ab.a = a.b.a
  19. λ JS K = a => b => a K

    := ab.a = a.b.a
  20. λ JS K(M)(I) === ? K M I = ?

    K := ab.a K = a => b => a
  21. λ JS K(M)(I) === M K M I = M

    K := ab.a K = a => b => a
  22. λ JS K(M)(I) === M K(I)(M) === ? K M

    I = M K I M = ? K := ab.a K = a => b => a
  23. λ JS K(M)(I) === M K(I)(M) === I K M

    I = M K I M = I K := ab.a K = a => b => a
  24. λ JS K(I)(x) === I K I x = I

    K := ab.a K = a => b => a
  25. λ JS K(I)(x)(y) === I(y) && I(y) === ? K

    I x y = I y = ? K := ab.a K = a => b => a
  26. λ JS K I x y = I y =

    y K := ab.a K = a => b => a K(I)(x)(y) === I(y) && I(y) === y
  27. λ JS K I x y = I y =

    y K := ab.a K = a => b => a K(I)(x)(y) === I(y) && I(y) === y
  28. λ JS K I x y = I y =

    y K := ab.a K = a => b => a K(I)(x)(y) === I(y) && I(y) === y
  29. λ JS KI = a => b => b KI

    = K(I) KI := ab.b = K I
  30. λ JS KI(M)(K) === ? KI M K = ?

    KI := ab.b KI = a => b => b
  31. λ JS KI(M)(K) === K KI M K = K

    KI := ab.b KI = a => b => b
  32. λ JS KI(M)(K) === K KI(K)(M) === ? KI M

    K = K KI K M = ? KI := ab.b KI = a => b => b
  33. λ JS KI(M)(K) === K KI(K)(M) === M KI M

    K = K KI K M = M KI := ab.b KI = a => b => b
  34. ?

  35. ?

  36. PEANO FREGE RUSSELL SCHÖNFINKEL VON NEUMANN CURRY CHURCH GÖDEL TURING

    KLEENE ROSSER TH E FO R M A L I Z AT I O N O F MAT H E M AT I C A L LO G I C
  37. PEANO FREGE RUSSELL SCHÖNFINKEL VON NEUMANN CURRY CHURCH GÖDEL TURING

    KLEENE ROSSER FO R M A L NO TAT I O N FO R FU N C T I O N S 1889 PE A N O AR I T H M E T I C
  38. PEANO FREGE RUSSELL SCHÖNFINKEL VON NEUMANN CURRY CHURCH GÖDEL TURING

    KLEENE ROSSER AX I O M AT I C LO G I C · FN NO TAT I O N FU N C T I O N S A S GR A P H S · CU R RY I N G 1891
  39. PEANO FREGE RUSSELL SCHÖNFINKEL VON NEUMANN CURRY CHURCH GÖDEL TURING

    KLEENE ROSSER PR I N C I P I A MAT H E M AT I C A 1910 RU S S E L L ’S PA R A D OX · FN NO TAT I O N
  40. PEANO FREGE RUSSELL SCHÖNFINKEL VON NEUMANN CURRY CHURCH GÖDEL TURING

    KLEENE ROSSER CO M B I N AT O RY LO G I C CO M B I N AT O R S · CU R RY I N G 1920
  41. PEANO FREGE RUSSELL SCHÖNFINKEL VON NEUMANN CURRY CHURCH GÖDEL TURING

    KLEENE ROSSER FU N C T I O N A L SY S T E M O F SE T TH E O RY 1925 (OV E R L A P P E D W I T H CO M B I N AT O RY LO G I C )
  42. PEANO FREGE RUSSELL SCHÖNFINKEL VON NEUMANN CURRY CHURCH GÖDEL TURING

    KLEENE ROSSER CO M B I N AT O RY LO G I C (AG A I N ) CO M B I N AT O R S · M A N Y C O N T R I B U T I O N S 1926
  43. PEANO FREGE RUSSELL SCHÖNFINKEL VON NEUMANN CURRY CHURCH GÖDEL TURING

    KLEENE ROSSER D I S C OV E R S SC H Ö N F I N K E L “This paper anticipates much of what I have done.” 1927
  44. PEANO FREGE RUSSELL SCHÖNFINKEL VON NEUMANN CURRY CHURCH GÖDEL TURING

    KLEENE ROSSER IN C O M P L E T E N E S S TH E O R E M S 1931 EN D I N G T H E SE A RC H FO R SU F F I C I E N T AX I O M S
  45. PEANO FREGE RUSSELL SCHÖNFINKEL VON NEUMANN CURRY CHURCH GÖDEL TURING

    KLEENE ROSSER -CA L C U L U S AN EF F E C T I V E MO D E L O F CO M P U TAT I O N 1932
  46. PEANO FREGE RUSSELL SCHÖNFINKEL VON NEUMANN CURRY CHURCH GÖDEL TURING

    KLEENE ROSSER I N C O N S I S T E N C Y O F S P E C I A L I Z E D 1931–1936 C O N S I S T E N C Y O F P U R E
  47. PEANO FREGE RUSSELL SCHÖNFINKEL VON NEUMANN CURRY CHURCH GÖDEL TURING

    KLEENE ROSSER SO LV E S T H E DE C I S I O N PRO B L E M V I A T H E -CA L C U L U S 1936
  48. PEANO FREGE RUSSELL SCHÖNFINKEL VON NEUMANN CURRY CHURCH GÖDEL TURING

    KLEENE ROSSER SO LV E S T H E DE C I S I O N PRO B L E M 1936 V I A T H E TU R I N G MAC H I N E
  49. PEANO FREGE RUSSELL SCHÖNFINKEL VON NEUMANN CURRY CHURCH GÖDEL TURING

    KLEENE ROSSER ES TA B L I S H E S T H E CH U RC H -TU R I N G TH E S I S 1936 -CA L C U L U S 㱻 TU R I N G MAC H I N E
  50. PEANO FREGE RUSSELL SCHÖNFINKEL VON NEUMANN CURRY CHURCH GÖDEL TURING

    KLEENE ROSSER O B TA I N S PH D U N D E R CH U RC H 1936–1938 PU B L I S H E S 1S T FI X E D -PO I N T CO M B I N AT O R
  51. COMBINATORS functions with no free variables b.b combinator b.a not

    a combinator ab.a combinator a.ab not a combinator abc.c(e.b) combinator
  52. COMBINATORS Sym. Bird -Calculus Use Haskell I Idiot a.a identity

    id M Mockingbird f.ff self-application (cannot define) K Kestrel ab.a first, const const KI Kite ab.b = KI second const id C Cardinal fab.fba reverse arguments flip B Bluebird fga.f(ga) 1°-1° composition (.) B1 Blackbird fgab.f(gab) = BBB 1°-2° composition (.) . (.) Th Thrush af.fa = CI hold an argument flip id V Vireo abf.fab = BCT hold a pair of args flip . flip id
  53. λ JS C = f => a => b =>

    f(b)(a) C := fab.fba
  54. λ JS C(K)(I)(M) === ? C K I M =

    ? C := fab.fba C = f => a => b => f(b)(a)
  55. λ JS C(K)(I)(M) === M C K I M =

    M C := fab.fba C = f => a => b => f(b)(a)
  56. λ JS C(K)(I)(M) === M C K I M =

    M C := fab.fba C = f => a => b => f(b)(a)
  57. λ JS KI(I)(M) === M KI I M = M

    C := fab.fba C = f => a => b => f(b)(a)
  58. COMBINATORS Sym. Bird -Calculus Use Haskell I Idiot a.a identity

    id M Mockingbird f.ff self-application (cannot define) K Kestrel ab.a first, const const KI Kite ab.b = KI second const id C Cardinal fab.fba reverse arguments flip B Bluebird fga.f(ga) 1°-1° composition (.) B1 Blackbird fgab.f(gab) = BBB 1°-2° composition (.) . (.) Th Thrush af.fa = CI hold an argument flip id V Vireo abf.fab = BCT hold a pair of args flip . flip id
  59. COMBINATORS Sym. Bird -Calculus Use Haskell I Idiot a.a identity

    id M Mockingbird f.ff self-application (cannot define) K Kestrel ab.a first, const const KI Kite ab.b = KI = CK second const id C Cardinal fab.fba reverse arguments flip B Bluebird fga.f(ga) 1°-1° composition (.) B1 Blackbird fgab.f(gab) = BBB 1°-2° composition (.) . (.) Th Thrush af.fa = CI hold an argument flip id V Vireo abf.fab = BCT hold a pair of args flip . flip id
  60. -CALCULUS abstract symbol rewriting functional computation TURING MACHINE hypothetical device

    state-based computation (f.ff)a.a purely functional programming languages higher-level machine-centric languages assembly languages machine code higher-level abstract stateful languages real computers
  61. TM

  62. λ JS const result = bool ? exp1 : exp2

    result := bool ? exp1 : exp2
  63. λ JS const result = bool ? exp1 : exp2

    result := bool exp1 exp2
  64. λ JS result := func exp1 exp2 const result =

    bool (exp1) (exp2) // false
  65. λ JS const T = K const F = KI

    TRUE := K FALSE := KI = C K CHURCH ENCODINGS: BOOLEANS
  66. λ JS ( ) ( ) T F T F

    T T K K KI KI
  67. λ JS ( ) ( ) F F T F

    T F KI KI K K
  68. CHURCH ENCODINGS: BOOLEANS Sym. Name -Calculus Use T TRUE ab.a

    = K encoding for true F FALSE ab.b = KI = CK encoding for false NOT p.pFT negation AND pq.pqF or pq.pqp conjunction OR pq.pTq or pq.ppq disjunction BEQ pq.p q (NOT q) equality
  69. λ JS not(K) === KI not(KI) === K NOT K

    = KI NOT (KI) = K ab.a ba.a ba.a ab.a
  70. CHURCH ENCODINGS: BOOLEANS Sym. Name -Calculus Use T TRUE ab.a

    = K encoding for true F FALSE ab.b = KI = CK encoding for false NOT p.pFT negation AND pq.pqF or pq.pqp conjunction OR pq.pTq or pq.ppq disjunction BEQ pq.p q (NOT q) equality
  71. CHURCH ENCODINGS: BOOLEANS Sym. Name -Calculus Use T TRUE ab.a

    = K encoding for true F FALSE ab.b = KI = CK encoding for false NOT p.pFT or C negation AND pq.pqF or pq.pqp conjunction OR pq.pTq or pq.ppq disjunction BEQ pq.p q (NOT q) equality
  72. CHURCH ENCODINGS: BOOLEANS Sym. Name -Calculus Use T TRUE ab.a

    = K encoding for true F FALSE ab.b = KI = CK encoding for false NOT p.pFT or C negation AND pq.pqF or pq.pqp conjunction OR pq.pTq or pq.ppq disjunction BEQ pq.p q (NOT q) equality
  73. CHURCH ENCODINGS: BOOLEANS Sym. Name -Calculus Use T TRUE ab.a

    = K encoding for true F FALSE ab.b = KI = CK encoding for false NOT p.pFT or C negation AND pq.pqF or pq.pqp conjunction OR pq.pTq or pq.ppq disjunction BEQ pq.p q (NOT q) equality
  74. CHURCH ENCODINGS: BOOLEANS Sym. Name -Calculus Use T TRUE ab.a

    = K encoding for true F FALSE ab.b = KI = CK encoding for false NOT p.pFT or C negation AND pq.pqF or pq.pqp conjunction OR pq.pTq or pq.ppq disjunction BEQ pq.p q (NOT q) equality
  75. CHURCH ENCODINGS: BOOLEANS Sym. Name -Calculus Use T TRUE ab.a

    = K encoding for true F FALSE ab.b = KI = CK encoding for false NOT p.pFT or C negation AND pq.pqF or pq.pqp conjunction OR pq.pTq or pq.ppq = M* disjunction BEQ pq.p q (NOT q) equality
  76. ( ) pq.p( ) T T F F q q

    p => q => p(q(T)(F))(q(F)(T))
  77. ( ) pq.p ( ) T T F F q

    q BOOLEAN EQUALITY
  78. CHURCH ENCODINGS: BOOLEANS Sym. Name -Calculus Use T TRUE ab.a

    = K encoding for true F FALSE ab.b = KI = CK encoding for false NOT p.pFT or C negation AND pq.pqF or pq.pqp conjunction OR pq.pTq or pq.ppq = M* disjunction BEQ pq.p q (NOT q) equality
  79. (ONE OF) DE MORGAN'S LAWS ¬(P ∧ Q) = (¬P)

    ∨ (¬Q) BEQ (NOT (AND p q)) (OR (NOT p) (NOT q)) !(p && q) === (!p) || (!q)
  80. BEQ (NOT (AND p q)) (OR (NOT p) (NOT q))

    (xy.x y ((fab.fba) y))
 ((fab.fba) ((xy.xyx) p q))
 ((f.ff) ((fab.fba) p) ((fab.fba) q))
  81. BEQ (NOT (AND p q)) (OR (NOT p) (NOT q))

    (xy.x y ((fab.fba) y))
 ((fab.fba) ((xy.xyx) p q))
 ((f.ff) ((fab.fba) p) ((fab.fba) q))
  82. BEQ (NOT (AND p q)) (OR (NOT p) (NOT q))

    (xy.x y ((fab.fba) y))
 ((fab.fba) ((xy.xyx) p q))
 ((f.ff) ((fab.fba) p) ((fab.fba) q))
  83. BEQ (NOT (AND p q)) (OR (NOT p) (NOT q))

    (xy.x y ((fab.fba) y))
 ((fab.fba) ((xy.xyx) p q))
 ((f.ff) ((fab.fba) p) ((fab.fba) q))
  84. BEQ (NOT (AND p q)) (OR (NOT p) (NOT q))

    (xy.x y ((fab.fba) y))
 ((fab.fba) ((xy.xyx) p q))
 ((f.ff) ((fab.fba) p) ((fab.fba) q))
  85. BEQ (NOT (AND p q)) (OR (NOT p) (NOT q))

    (xy.x y ((fab.fba) y))
 ((fab.fba) ((xy.xyx) p q))
 ((f.ff) ((fab.fba) p) ((fab.fba) q))
  86. BEQ (NOT (AND p q)) (OR (NOT p) (NOT q))

    (xy.x y ((fab.fba) y))
 ((fab.fba) ((xy.xyx) p q))
 ((f.ff) ((fab.fba) p) ((fab.fba) q))
  87. λ JS n1 = f => a => f(a) n2

    = f => a => f(f(a)) n3 = f => a => f(f(f(a))) N1 := fa.fa N2 := fa.f(fa) N3 := fa.f(f(fa))
  88. λ JS n1(not)(T) = not(T) = ? N1 NOT T

    = NOT T = ? N1 := fa.fa N1 = f => a => f(a)
  89. λ JS n1(not)(T) = not(T) = F N1 NOT T

    = NOT T = F N1 := fa.fa N1 = f => a => f(a)
  90. λ JS n2(not)(T) = not(not(T)) = ? N2 NOT T

    = NOT (NOT T) = ? N2 := fa.f(fa) N2 = f => a => f(f(a))
  91. λ JS n2(not)(T) = not(not(T)) = T N2 NOT T

    = NOT (NOT T) = T N2 := fa.f(fa) N2 = f => a => f(f(a))
  92. λ JS n3(not)(T) = not(not(not(T))) = F N3 NOT T

    = NOT (NOT (NOT T))) = F N3 := fa.f(f(fa)) N3 = f => a => f(f(f(a)))
  93. λ JS n0 = f => a => a n1

    = f => a => f(a) n2 = f => a => f(f(a)) n3 = f => a => f(f(f(a))) N0 := fa.a N1 := fa.fa N2 := fa.f(fa) N3 := fa.f(f(fa))
  94. λ JS n0(not)(T) = ? N0 NOT T = ?

    N0 := fa.a N3 = f => a => a
  95. λ JS n0(not)(T) = T N0 NOT T = T

    N0 := fa.a N3 = f => a => a
  96. CHURCH ENCODINGS: NUMERALS Sym. Name -Calculus Use N0 ZERO fa.a

    = F apply f no times to a N1 ONCE fa.f a = I* apply f once to a N2 TWICE fa.f (f a) apply 2-fold f to a N3 THRICE fa.f (f (f a)) apply 3-fold f to a N4 FOURFOLD fa.f (f (f (f a))) apply 4-fold f to a N5 FIVEFOLD fa.f (f (f (f (f a))))) apply 5-fold f to a
  97. λ JS succ = n => ? SUCC := n.?

    SUCC fa.fa = fa.f(fa)
  98. λ JS succ = n => f => a =>

    f(n(f)(a)) SUCC := nfa.f(nfa) SUCC fa.fa = fa.f(fa)
  99. λ JS succ = n => f => a =>

    f(n(f)(a)) SUCC := nfa.f(nfa) SUCC fa.fa = fa.f(fa)
  100. λ JS succ = n => f => a =>

    f(n(f)(a)) SUCC := nfa.f(nfa) SUCC fa.fa = fa.f(fa)
  101. CHURCH ARITHMETIC Name -Calculus Use SUCC nfa.f(nfa) successor of n

    ADD nk.n SUCC k = nkf.B (n f) (k f) addition of n and k MULT nkf.n(kf) = B multiplication of n and k POW nk.kn = Th raise n to the power of k PRED n.n (g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n PRED n.FST (n Φ (PAIR N0 N0)) predecessor of n (easier) SUB nk.k PRED n subtract k from n
  102. λ JS B = f => g => a =>

    f(g(a)) B := fga.f(ga)
  103. λ JS B(not)(not)(T) === ? B NOT NOT T =

    ? B := fga.f(ga) B = f => g => a => f(g(a))
  104. λ JS B(not)(not)(T) === T B NOT NOT T =

    T B := fga.f(ga) B = f => g => a => f(g(a))
  105. COMBINATORS Sym. Bird -Calculus Use Haskell I Idiot a.a identity

    id M Mockingbird f.ff self-application (cannot define) K Kestrel ab.a true, first, const const KI Kite ab.b = KI = CK false, second const id C Cardinal fab.fba reverse arguments flip B Bluebird fga.f(ga) 1°←1° composition (.) B1 Blackbird fgab.f(gab) = BBB 1°-2° composition (.) . (.) Th Thrush af.fa = CI hold an argument flip id V Vireo abf.fab = BCT hold a pair of args flip . flip id
  106. λ JS succ = n => f => a =>

    f(n(f)(a)) SUCC := nfa.f(nfa)
  107. CHURCH ARITHMETIC Name -Calculus Use SUCC nf.B f (nf) =

    nfa.f(nfa) successor of n ADD nk.n SUCC k = nkf.B (n f) (k f) addition of n and k MULT nkf.n(kf) = B multiplication of n and k POW nk.kn = Th raise n to the power of k PRED n.n (g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n PRED n.FST (n Φ (PAIR N0 N0)) predecessor of n (easier) SUB nk.k PRED n subtract k from n
  108. λ JS add = n => k => ? ADD

    := nk.? ADD N3 N5 = SUCC (SUCC (SUCC N5))
  109. λ JS add = n => k => ? ADD

    := nk.? ADD N3 N5 = (SUCC ∘ SUCC ∘ SUCC) N5
  110. λ JS add = n => k => ? ADD

    := nk.? ADD N3 N5 = N3 SUCC N5
  111. λ JS add = n => k => n(succ)(k) ADD

    := nk.n SUCC k ADD N3 N5 = N3 SUCC N5
  112. ADD N3 N5 = N3 SUCC N5 = THRICE SUCC

    FIVEFOLD = SUCC (SUCC (SUCC FIVEFOLD))) = EIGHTFOLD
  113. CHURCH ARITHMETIC Name -Calculus Use SUCC nf.B f (nf) =

    nfa.f(nfa) successor of n ADD nk.n SUCC k = nkf.B (n f) (k f) addition of n and k MULT nkf.n(kf) = B multiplication of n and k POW nk.kn = Th raise n to the power of k PRED n.n (g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n PRED n.FST (n Φ (PAIR N0 N0)) predecessor of n (easier) SUB nk.k PRED n subtract k from n
  114. λ JS mult = n => k => ? MULT

    := nk.? MULT N2 N3 = N6
  115. λ JS mult = n => k => ? MULT

    := nk.? MULT N2 N3 f a = N6 f a
  116. λ JS mult = n => k => ? MULT

    := nk.? MULT N2 N3 f a = (f ∘ f ∘ f ∘ f ∘ f ∘ f) a
  117. λ JS mult = n => k => ? MULT

    := nk.? MULT N2 N3 f a = ((f ∘ f ∘ f) ∘ (f ∘ f ∘ f)) a
  118. λ JS mult = n => k => ? MULT

    := nk.? MULT N2 N3 f a = ((N3 f) ∘ (N3 f)) a
  119. λ JS mult = n => k => ? MULT

    := nk.? MULT N2 N3 f a = N2 (N3 f) a
  120. λ JS mult = n => k => ? MULT

    := nk.? MULT N2 N3 f a = N2 (N3 f) a
  121. λ JS mult = n => k => ? MULT

    := nk.? MULT N2 N3 f = N2 (N3 f)
  122. λ JS mult = n => k => n(k(f)) MULT

    := nkf.n(kf) MULT N2 N3 f = N2 (N3 f)
  123. MULT N2 N3 f = N2 (N3 f) = TWICE

    (THRICE f) = (f ∘ f ∘ f) ∘ (f ∘ f ∘ f) = SIXFOLD f
  124. CHURCH ARITHMETIC Name -Calculus Use SUCC nf.B f (nf) =

    nfa.f(nfa) successor of n ADD nk.n SUCC k = nkf.B (n f) (k f) addition of n and k MULT nkf.n(kf) multiplication of n and k POW nk.kn = Th raise n to the power of k PRED n.n (g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n PRED n.FST (n Φ (PAIR N0 N0)) predecessor of n (easier) SUB nk.k PRED n subtract k from n
  125. λ JS MULT := nkf.n(kf) MULT N2 N3 f =

    N2 (N3 f) mult = n => k => n(k(f))
  126. λ JS MULT := nkf.n(kf) MULT N2 N3 f =

    (N2 ∘ N3) f mult = n => k => n(k(f))
  127. λ JS MULT := nkf.n(kf) MULT N2 N3 f =

    (N2 ∘ N3) f mult = n => k => n(k(f))
  128. λ JS MULT := nkf.n(kf) MULT N2 N3 = N2

    ∘ N3 mult = n => k => n(k(f))
  129. λ JS MULT := nkf.n(kf) MULT N2 N3 = B

    N2 N3 mult = n => k => n(k(f))
  130. λ JS MULT := nkf.n(kf) MULT N2 N3 = B

    N2 N3 mult = n => k => n(k(f))
  131. Mult := n k f . n ( k f)

    = B = f g a . f ( g a) -EQUIVALENCE
  132. CHURCH ARITHMETIC Name -Calculus Use SUCC nf.B f (nf) =

    nfa.f(nfa) successor of n ADD nk.n SUCC k = nkf.B (n f) (k f) addition of n and k MULT nkf.n(kf) = B multiplication of n and k POW nk.kn = Th raise n to the power of k PRED n.n (g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n PRED n.FST (n Φ (PAIR N0 N0)) predecessor of n (easier) SUB nk.k PRED n subtract k from n
  133. λ JS pow = n => k => ? POW

    := nk.? POW N2 N3 = N8
  134. λ JS pow = n => k => ? POW

    := nk.? POW N2 N3 = N2 × N2 × N2
  135. λ JS pow = n => k => ? POW

    := nk.? POW N2 N3 = N2 ∘ N2 ∘ N2
  136. λ JS pow = n => k => ? POW

    := nk.? POW N2 N3 = N3 N2
  137. λ JS pow = n => k => k(n) POW

    := nk.kn POW N2 N3 = N3 N2
  138. POW N2 N3 = N3 N2 = THRICE TWICE =

    TWICE ∘ TWICE ∘ TWICE = EIGHTFOLD
  139. CHURCH ARITHMETIC Name -Calculus Use SUCC nf.B f (nf) =

    nfa.f(nfa) successor of n ADD nk.n SUCC k = nkf.B (n f) (k f) addition of n and k MULT nkf.n(kf) = B multiplication of n and k POW nk.kn raise n to the power of k PRED n.n (g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n PRED n.FST (n Φ (PAIR N0 N0)) predecessor of n (easier) SUB nk.k PRED n subtract k from n
  140. COMBINATORS Sym. Bird -Calculus Use Haskell I Idiot a.a identity

    id M Mockingbird f.ff self-application (cannot define) K Kestrel ab.a true, first, const const KI Kite ab.b = KI = CK false, second const id C Cardinal fab.fba reverse arguments flip B Bluebird fga.f(ga) 1°←1° composition (.) Th Thrush af.fa hold an argument V Vireo abf.fab = BCT hold a pair of args flip . flip id B1 Blackbird fgab.f(gab) = BBB 1°←2° composition (.) . (.)
  141. COMBINATORS Sym. Bird -Calculus Use Haskell I Idiot a.a identity

    id M Mockingbird f.ff self-application (cannot define) K Kestrel ab.a true, first, const const KI Kite ab.b = KI = CK false, second const id C Cardinal fab.fba reverse arguments flip B Bluebird fga.f(ga) 1°←1° composition (.) Th Thrush af.fa = CI hold an argument flip id V Vireo abf.fab = BCT hold a pair of args flip . flip id B1 Blackbird fgab.f(gab) = BBB 1°←2° composition (.) . (.)
  142. CHURCH ARITHMETIC Name -Calculus Use SUCC nf.B f (nf) =

    nfa.f(nfa) successor of n ADD nk.n SUCC k = nkf.B (n f) (k f) addition of n and k MULT nkf.n(kf) = B multiplication of n and k POW nk.kn raise n to the power of k PRED n.n (g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n PRED n.FST (n Φ (PAIR N0 N0)) predecessor of n (easier) SUB nk.k PRED n subtract k from n
  143. CHURCH ARITHMETIC Name -Calculus Use SUCC nf.B f (nf) =

    nfa.f(nfa) successor of n ADD nk.n SUCC k = nkf.B (n f) (k f) addition of n and k MULT nkf.n(kf) = B multiplication of n and k POW nk.kn = Th raise n to the power of k PRED n.n (g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n PRED n.FST (n Φ (PAIR N0 N0)) predecessor of n (easier) SUB nk.k PRED n subtract k from n
  144. λ JS is0 = n => n(K(F))(T) IS0 := n.n

    (KF) T IS0 N3 = KF(KF(KF(T))) = F
  145. λ JS is0 = n => n(K(F))(T) IS0 := n.n

    (KF) T IS0 N3 = KF(KF(KF(T))) = F
  146. λ JS is0 = n => n(K(F))(T) IS0 := n.n

    (KF) T IS0 N3 = KF(KF(KF(T))) = F
  147. CHURCH ARITHMETIC: BOOLEAN OPS Name -Calculus Use IS0 n.n (K

    F) T test if n = 0 LEQ nk.IS0 (SUB n k) test if n <= k EQ nk.AND (LEQ n k) (LEQ k n) test if n = k GT nk.B1 NOT LEQ test if n > k
  148. N0: N0 (g.IS0 (g N1) ) (K N0) N0 I

    (B SUCC g) N0 N1: N1 (g.IS0 (g N1) ) (K N0) N0 I (B SUCC g) N0 N2: N2 (g.IS0 (g N1) ) (K N0) N0 I (B SUCC g) N1 N3: N3 (g.IS0 (g N1) ) (K N0) N0 I (B SUCC g) N2 (K N0) I (SUCC ∘ I) PRED := n.n (g.IS0 (g N1) I (B SUCC g)) (K N0) N0
  149. λ JS V = a => b => f =>

    f(a)(b) V := abf.fab
  150. λ JS V(I)(M) // f => f(I)(M) V I M

    = (f.f I M) V := abf.fab V = a => b => f => f(a)(b)
  151. λ JS V(I)(M)(K) // (f => f(I)(M))(K) === ? V

    I M K = (f.f I M) K = ? V := abf.fab V = a => b => f => f(a)(b)
  152. λ JS V(I)(M)(K) // (f => f(I)(M))(K) === I V

    I M K = (f.f I M) K = I V := abf.fab V = a => b => f => f(a)(b)
  153. λ JS V I M KI = (f.f I M)

    KI = M V := abf.fab V = a => b => f => f(a)(b) V(I)(M)(KI) // (f => f(I)(M))(KI) === M
  154. COMBINATORS Sym. Bird -Calculus Use Haskell I Idiot a.a identity

    id M Mockingbird f.ff self-application (cannot define) K Kestrel ab.a true, first, const const KI Kite ab.b = KI = CK false, second const id C Cardinal fab.fba reverse arguments flip B Bluebird fga.f(ga) 1°←1° composition (.) Th Thrush af.fa = CI hold an argument flip id V Vireo abf.fab = BCT hold a pair of args flip . flip id B1 Blackbird fgab.f(gab) = BBB 1°←2° composition (.) . (.)
  155. CHURCH PAIRS Sym. Name -Calculus Use PAIR abf.fab = V

    pair two arguments FST p.pK extract first of pair SND p.p(KI) extract second of pair Φ PHI p.PAIR (SND p) (SUCC (SND p) copy 2nd to 1st, inc 2nd SET1ST cp.PAIR c (SND p) set first, immutably SET2ND cp.PAIR (FST p) c set second, immutably
  156. CHURCH PAIRS Sym. Name -Calculus Use PAIR abf.fab = V

    pair two arguments FST p.pK extract first of pair SND p.p(KI) extract second of pair Φ PHI p.PAIR (SND p) (SUCC (SND p) copy 2nd to 1st, inc 2nd SET1ST cp.PAIR c (SND p) set first, immutably SET2ND cp.PAIR (FST p) c set second, immutably
  157. Φ := p.PAIR (SND p) (SUCC (SND p)) Φ (M,

    N7) = (N7, N8) Φ (N9, N2) = (N2, N3)
  158. CHURCH PAIRS Sym. Name -Calculus Use PAIR abf.fab = V

    pair two arguments FST p.pK extract first of pair SND p.p(KI) extract second of pair Φ PHI p.PAIR (SND p) (SUCC (SND p) copy 2nd to 1st, inc 2nd SET1ST cp.PAIR c (SND p) set first, immutably SET2ND cp.PAIR (FST p) c set second, immutably
  159. Φ := p.PAIR (SND p) (SUCC (SND p)) Φ (M,

    N7) = (N7, N8) Φ (N9, N2) = (N2, N3) Φ (N0, N0) = (N0, N1)
  160. Φ := p.PAIR (SND p) (SUCC (SND p)) Φ (M,

    N7) = (N7, N8) Φ (N9, N2) = (N2, N3) Φ (N0, N0) = (N0, N1) Φ (N0, N1) = (N1, N2)
  161. Φ := p.PAIR (SND p) (SUCC (SND p)) Φ (M,

    N7) = (N7, N8) Φ (N9, N2) = (N2, N3) Φ (N0, N0) = (N0, N1) Φ (N0, N1) = (N1, N2) Φ (N1, N2) = (N2, N3)
  162. Φ := p.PAIR (SND p) (SUCC (SND p)) Φ (M,

    N7) = (N7, N8) Φ (N9, N2) = (N2, N3) Φ (N0, N0) = (N0, N1) Φ (N0, N1) = (N1, N2) Φ (N1, N2) = (N2, N3) N8 Φ (N0, N0) = ?
  163. Φ := p.PAIR (SND p) (SUCC (SND p)) Φ (M,

    N7) = (N7, N8) Φ (N9, N2) = (N2, N3) Φ (N0, N0) = (N0, N1) Φ (N0, N1) = (N1, N2) Φ (N1, N2) = (N2, N3) N8 Φ (N0, N0) = (N7, N8)
  164. FST ( ) Φ := p.PAIR (SND p) (SUCC (SND

    p)) Φ (M, N7) = (N7, N8) Φ (N9, N2) = (N2, N3) Φ (N0, N0) = (N0, N1) Φ (N0, N1) = (N1, N2) Φ (N1, N2) = (N2, N3) N8 Φ (N0, N0) = FST (N7, N8) = N7
  165. FST ( ) Φ := p.PAIR (SND p) (SUCC (SND

    p)) Φ (M, N7) = (N7, N8) Φ (N9, N2) = (N2, N3) Φ (N0, N0) = (N0, N1) Φ (N0, N1) = (N1, N2) Φ (N1, N2) = (N2, N3) N8 Φ (N0, N0) = FST (N7, N8) = N7
  166. CHURCH ARITHMETIC Name -Calculus Use SUCC nf.B f (nf) =

    nfa.f(nfa) successor of n ADD nk.n SUCC k = nkf.B (n f) (k f) addition of n and k MULT nkf.n(kf) = B multiplication of n and k POW nk.kn = Th raise n to the power of k PRED n.n (g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n PRED n.FST (n Φ (PAIR N0 N0)) predecessor of n (easier) SUB nk.k PRED n subtract k from n
  167. CHURCH ARITHMETIC Name -Calculus Use SUCC nf.B f (nf) =

    nfa.f(nfa) successor of n ADD nk.n SUCC k = nkf.B (n f) (k f) addition of n and k MULT nkf.n(kf) = B multiplication of n and k POW nk.kn = Th raise n to the power of k PRED n.n (g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n PRED n.FST (n Φ (PAIR N0 N0)) predecessor of n (easier) SUB nk.k PRED n subtract k from n
  168. CHURCH ARITHMETIC: BOOLEAN OPS Name -Calculus Use IS0 n.n (K

    F) T test if n = 0 LEQ nk.IS0 (SUB n k) test if n <= k EQ nk.AND (LEQ n k) (LEQ k n) test if n = k GT nk.B1 NOT LEQ test if n > k
  169. CHURCH ARITHMETIC: BOOLEAN OPS Name -Calculus Use IS0 n.n (K

    F) T test if n = 0 LEQ nk.IS0 (SUB n k) test if n <= k EQ nk.AND (LEQ n k) (LEQ k n) test if n = k GT nk.B1 NOT LEQ test if n > k
  170. COMBINATORS Sym. Bird -Calculus Use Haskell I Idiot a.a identity

    id M Mockingbird f.ff self-application (cannot define) K Kestrel ab.a true, first, const const KI Kite ab.b = KI = CK false, second const id C Cardinal fab.fba reverse arguments flip B Bluebird fga.f(ga) 1°←1° composition (.) Th Thrush af.fa = CI hold an argument flip id V Vireo abf.fab = BCT hold a pair of args flip . flip id B1 Blackbird fgab.f(gab) 1°←2° composition
  171. COMBINATORS Sym. Bird -Calculus Use Haskell I Idiot a.a identity

    id M Mockingbird f.ff self-application (cannot define) K Kestrel ab.a true, first, const const KI Kite ab.b = KI = CK false, second const id C Cardinal fab.fba reverse arguments flip B Bluebird fga.f(ga) 1°←1° composition (.) Th Thrush af.fa = CI hold an argument flip id V Vireo abf.fab = BCT hold a pair of args flip . flip id B1 Blackbird fgab.f(gab) = BBB 1°←2° composition (.) . (.)
  172. B C K I KI = K I = C

    K B1 = B B B Th = C I V = B C Th = B C (C I)
  173. COMBINATORS Sym. Bird -Calculus Use Haskell I Idiot a.a identity

    id M Mockingbird f.ff self-application (cannot define) K Kestrel ab.a true, first, const const KI Kite ab.b = KI = CK false, second const id C Cardinal fab.fba reverse arguments flip B Bluebird fga.f(ga) 1°←1° composition (.) Th Thrush af.fa = CI hold an argument flip id V Vireo abf.fab = BCT hold a pair of args flip . flip id B1 Blackbird fgab.f(gab) = BBB 1°←2° composition (.) . (.)
  174. CHURCH ENCODINGS: BOOLEANS Sym. Name -Calculus Use T TRUE ab.a

    = K = C(KI) encoding for true F FALSE ab.b = KI = CK encoding for false NOT p.pFT or C negation AND pq.pqF or pq.pqp conjunction OR pq.pTq or pq.ppq = M* disjunction BEQ pq.p q (NOT q) equality
  175. CHURCH ENCODINGS: NUMERALS Sym. Name -Calculus Use N0 ZERO fa.a

    = F apply f no times to a N1 ONCE fa.f a = I* apply f once to a N2 TWICE fa.f (f a) apply 2-fold f to a N3 THRICE fa.f (f (f a)) apply 3-fold f to a N4 FOURFOLD fa.f (f (f (f a))) apply 4-fold f to a N5 FIVEFOLD fa.f (f (f (f (f a))))) apply 5-fold f to a
  176. CHURCH ARITHMETIC Name -Calculus Use SUCC nf.B f (nf) =

    nfa.f(nfa) successor of n ADD nk.n SUCC k = nkf.B (n f) (k f) addition of n and k MULT nkf.n(kf) = B multiplication of n and k POW nk.kn = Th raise n to the power of k PRED n.n (g.IS0 (g N1) I (B SUCC g)) (K N0) N0 predecessor of n PRED n.FST (n Φ (PAIR N0 N0)) predecessor of n (easier) SUB nk.k PRED n subtract k from n
  177. CHURCH ARITHMETIC: BOOLEAN OPS Name -Calculus Use IS0 n.n (K

    F) T test if n = 0 LEQ nk.IS0 (SUB n k) test if n <= k EQ nk.AND (LEQ n k) (LEQ k n) test if n = k GT nk.B1 NOT LEQ test if n > k
  178. CHURCH PAIRS Sym. Name -Calculus Use PAIR abf.fab = V

    pair two arguments FST p.pK extract first of pair SND p.p(KI) extract second of pair Φ PHI p.PAIR (SND p) (SUCC (SND p) copy 2nd to 1st, inc 2nd SET1ST cp.PAIR c (SND p) set first, immutably SET2ND cp.PAIR (FST p) c set second, immutably
  179. EVALUATION STRATEGIES (ab.b)((f.ff)f.ff) x = (b.b) x = x (ab.b)((f.ff)f.ff)x

    = (ab.b)((f.ff)f.ff)x = (ab.b)((f.ff)f.ff)x = (ab.b)((f.ff)f.ff)x = (ab.b)((f.ff)f.ff)x C A L L B Y N A M E (apply to args before reduction) C A L L B Y VA L U E (reduce args before application) (AKA normal order; lazy) (AKA applicative order; strict)
  180. ADDITIONAL RESOURCES Combinator Birds · Rathman · http://bit.ly/2iudab9 To Mock

    a Mockingbird · Smullyan · http://amzn.to/2g9AlXl To Dissect a Mockingbird · Keenan · http://dkeenan.com/Lambda .:.
 A Tutorial Introduction to the Lambda Calculus · Rojas · http://bit.ly/1agRC97 Lambda Calculus · Wikipedia · http://bit.ly/1TsPkGn The Lambda Calculus · Stanford · http://stanford.io/2vtg8hp .:.
 History of Lambda-calculus and Combinatory Logic Cardone, Hindley · http://bit.ly/2wCxv4k .:.
 An Introduction to Functional Programming
 through Lambda Calculus · Michaelson · http://amzn.to/2vtts56