Lambda & javascript

lambda.js

// # Lambda as JS, or A Flock of Functions

// ### Combinators, Lambda Calculus, and Church Encodings in JavaScript

// #### Notes for [a talk by Gabriel Lebec 
// (click for videos and slides)](https://www.youtube.com/watch?v=3VQ382QG-y4&list=PLpkHU923F2XFWv-XfVuvWuxq41h21nOPK&index=1)

const chalk = require('chalk')
const green = chalk.green.bind(chalk)
const red = chalk.red.bind(chalk)

const errs = []

function demo (msg, bool) {
	if (typeof bool === 'function') bool = bool(true)(false)
	if (!!bool !== bool) throw TypeError('second arg must be boolean (JS or LC)')
	console.log(`${bool ? green('✔') : red('✖')} ${msg}`)
	if (!bool) errs.push(Error(red(`Spec fail: ${msg} -> ${bool}`)))
}

function logErrsAndSetExitCode () {
	errs.forEach(err => console.error(err))
	if (errs.length) process.exitCode = 1
}

function header (str) {
	console.log('\n' + str + '\n')
}

// ## Introduction

// The Lambda Calculus is a symbol manipulation framework developed by the mathematician Alonzo Church in the 1930s. 
// It was intended to be an extremely tiny syntax which could nevertheless suffice to calculate anything computable.
// The mathematical advantage of such a syntax is that with such extreme simplicity, it becomes easier to write formal proofs 
// about computational logic – demonstrated when Church solved David Hilbert's famous Decision Problem using LC.

// Another famous mathematician, Alan Turing, formulated a different model of universal computation – the eponymous
// Turing Machine. A TM is a hypothetical device, again of extreme simplicity;
// it can read or write to cells on an infinite tape, each cell containing data or instructions.
// Turing published a paper also solving the Decision Problem, mere months after Church.

// Turing proved that the Turing Machine and Lambda Calculus are totally equivalent.
// Everything that one can calculate, the other can. Not only this, but Turing and Church posited (in the "Church-Turing 
// Thesis") that these systems capture the definition of computability in a universal way.

// Turing Machines are exciting because if a hypothetical machine can compute anything computable, 
// then perhaps a real machine can as well. Modern computers add many features and optimizations beyond what is featured in 
// an actual Turing Machine; these features make the machine more convenient and performant, but do not compromise 
// its essential nature as a universal computing device.

// As machine codes, assemblers, compilers, and higher-level languages have developed to program these real machines, they 
// have largely evolved with a focus on the essence of the machine – memory, statefulness, effects, imperative instructions 
// and so forth. Over time, some of these languages have shifted ever farther into pure abstractions and conceptual 
// description over more machine-centric and stateful models.

// However, mathematicians and computer scientists have long known that the entirely abstract lambda calculus, 
// being equivalent to a TM, meant that computations could be expressed in a style totally independent from machine 
// instructions. Instead, a language consisting of first-class function expressions – aka lambda abstractions – could 
// be subsequently compiled into machine code. Such a language would benefit from decades of mathematical research.
// And just as real computers extend Turing Machines with extra power and convenience, these _functional languages_ would 
// extend the lambda calculus with additional features and under-the-hood shortcuts (such as hardware-based arithmetic).

// What follows is a demonstration, mostly for enjoyment and insight, of the surprising and delightful omnipotence of 
// the lambda calculus. JavaScript, like any functional language, is closely related to LC; it contains the necessary 
// ingredients (variables, parentheses, first-class functions) nestled among the additional luxuries most programmers 
// take for granted.

// # First steps with simple combinators

// Starting simple. A lambda abstraction is simply an anonymous unary function. In LC there are no named functions,
// but for convenience we will use names. In mathematical notation, `:=` means "is defined as".


// ## Identity

// Here is an almost trivial function: Identity, defined as `λx.x`. `λ` is used to indicate the start of a lambda 
// abstraction (read: function expression). The sole parameter is listed to the left of the `.`, and 
// the return expression is written after the `.`.

header('I := λx.x')
const I = x => x

// In LC, variables may be static tokens that stand for whatever you want. We'll use ES2015 Symbols for this.

const tweet = Symbol('tweet')
const chirp = Symbol('chirp')

// In LC, juxtaposition is function application. That is, `M I` means "apply the `M` function to the `I` argument". 
// A space is not strictly necessary; `fx` usually means "apply `f` to `x`". Some of our examples will use multi-letter 
// variables; to disambiguate them from multiple single-letter variables, we will frequently use SPACED UPPERCASE.

// ```lc
// I tweet
// = (λx.x) tweet
// = tweet
// ```

demo('I tweet = tweet', I(tweet) === tweet)
demo('I chirp = chirp', I(chirp) === chirp)

// in LC, valid arguments include other lambda abstractions. This is the meaning of "first-class" in the phrase 
// "first-class functions"; functions are values which may be passed into or returned from other functions. 
// In this sense, functions are both like verbs (they can perform a calculation) and nouns (they can be the subject or object 
// of a calculation).

// ```lc
// I I
// = (λx.x)(λx.x)
// = λx.x
// ```

demo('I I = I', I(I) === I)

// of course we can build up more complex expressions. In LC, function application associates left; that is, 
// `a b c d` = `((a b) c) d`. Evaluating terms by substituting arguments into function bodies has the fancy term of 
// "β-reduction". A reducible expression (or "redex") that has been completely simplified in this fashion is said to be 
// in its "β-normal" or just "normal" form.

// ```lc
//      id    id       id    id  tweet   <--- the initial reducible expression ("redex")
// = (((id    id)      id)   id) tweet   <--- application associates left
// = ((    id          id)   id) tweet   <--- evaluating function applications ("β-reduction")
// = (           id          id) tweet   <--- continuing β-reduction
// =                    id       tweet   <--- more β-reduction
// =                             tweet   <--- normal form of the original redex
// ```

// LC has great overlap with combinatory logic. A pioneer of CL was the mathematician Haskell Curry, whose name now adorns
// the Haskell language as well as the functional concept of currying. (Curry actually cited the technique from Schönfinkel,
// and Frege used it even earlier.) Combinatory logic is concerned with combinators, that is, functions which
// operate only on their inputs. The Identity function is a combinator, often abbreviated I, sometimes called the Idiot bird.

header('Idiot := I')
const Idiot = I


// ## Self-Application

// Curry was an avid birdwatcher, and the logician Raymond Smullyan named many combinators after birds in his honor.
// The self-application combinator M (for "Mockingbird"), aka ω (lowercase omega), looks like this:

header('Mockingbird := M := ω := λf.ff')
// Remember, `fx` means "apply f to x." So `ff` means "apply f to itself".
const ω = fn => fn(fn)
const M = ω
const Mockingbird = M

// Can you guess what the Mockingbird of Identity is?

// ```lc
// M I
// = (λf.ff)(λx.x)
// = (λx.x)(λx.x) = I I
// = λx.x = I
// ```

// That's right, it's the same as Identity of Identity… which is Identity.

demo('M I = I I = I', M(I) === I(I) && I(I) === I)

// What about… the Mockingbird of Mockingbird?

// That's the Ω (big Omega) Combinator. It diverges (goes on forever).

// ```lc
// M M
// = (λf.ff)(λf.ff)
// = (λf.ff)(λf.ff)
// = (λf.ff)(λf.ff)
// = (λf.ff)(λf.ff)
// ...
// ```

try {
  M(M)
} catch (err) {
  demo('M M = M M = M M = ' + err.message, true)
}


// ## Church Encodings: Booleans

header('First encodings: boolean value functions')

// OK this is nice and all, but how can we do anything real with only functions? Let's start with booleans.
// Here we need some multi-arg functions… in lambda calc, `λabc.a` is just shorthand for `λa.λb.λc.a`, or `λa.(λb.(λc.a)))`.
// In other words, all functions are curried.

// ### True and False

header('T := λxy.x')
const T = thn => els => thn

header('F := λxy.y')
const F = thn => els => els

// Hm. How can "true" and "false" be functions? Well, the point of booleans is to _select_ between a then-case and 
// an else-case. The LC booleans are just functions which do that! `T` takes two vals and returns the first; `F` 
// takes two vals and returns the second. If you apply an unknown bool func to two vals, the first val will be returned if 
// the bool was true, else the second val will be returned.

demo('T tweet chirp = tweet', T(tweet)(chirp) === tweet)
demo('F tweet chirp = chirp', F(tweet)(chirp) === chirp)

// ### Flipping Arguments

// Another fun way we could have produced F was with the Cardinal combinator. The Cardinal, aka `C`, aka `flip`, 
// takes a binary (two-argument) function, and produces a function with reversed argument order.

header('Cardinal := C := flip := λfab.fba')
const flip = func => a => b => func(b)(a)
const C = flip
const Cardinal = C

// With the Cardinal, we can derive `F` from the flip of `T`:

header('F = C T')

demo('flip T tweet chirp = chirp', flip(T)(tweet)(chirp) === chirp)

// Regardless of whether you define `F` manually, or as the flip of `T`, these functions are _encodings_ of boolean values.
// They represent booleans in useful and meaningful ways, which preserve the behavior of the values. Specifically, 
// they are Church encodings – representations developed / discovered by Alonzo Church. Their real power is revealed 
// when we start defining logical operations on them.

// ### Negation

header('NOT := λb.bFT')
const NOT = chooseOne => chooseOne(F)(T)

// Remember, booleans in the LC are really functions which select one of two arguments. Try reducing the expression `NOT T`
// yourself, then check your work below.

// NOT T
// = (λb.bFT) T
// = TFT
// = (λxy.x) F T
// = F

demo('NOT T = F', NOT(T) === F)
demo('NOT F = T', NOT(F) === T)

// There's another way we could define `NOT`, however, and we've already seen it. Remember how the flip of `T`
// (aka the Cardinal of `T`) is `F`? It works the other way too – `C F = T`! At least, `C F` yields a function 
// that behaves identically to `T`:

demo('CF = T', C(F)(tweet)(chirp) === tweet)
demo('CT = F', C(T)(tweet)(chirp) === chirp)

// This means that when it comes to Church encodings of booleans, the Cardinal behaves just like our manually-defined `NOT`.

// ### Conjunction and Disjunction

// Can you construct a function for boolean `AND`? It will have to take two unknown boolean functions as parameters,
// and route to an output of the correct boolean result. Give it a try.

header('AND := λpq.pqF')

// (λpq.pqp also works; can you see why?)

const AND = p => q => p(q)(F)

demo('AND F F = F', AND(F)(F) === F)
demo('AND T F = F', AND(T)(F) === F)
demo('AND F T = F', AND(F)(T) === F)
demo('AND T T = T', AND(T)(T) === T)

// If you work through the logic, you might notice that this function exhibits short-circuiting. If `p = F`,
// we don't bother using `q`. Similarly, our `OR` function below short circuits; if `p = T`, we don't bother using `q`.

header('OR := λpq.pTq')

// (λpq.ppq also works)

const OR = p => q => p(T)(q)

demo('OR F F = F', OR(F)(F) === F)
demo('OR T F = T', OR(T)(F) === T)
demo('OR F T = T', OR(F)(T) === T)
demo('OR T T = T', OR(T)(T) === T)

// `λpq.ppq` also works because if `p` is true, it is supposed to select `T`, but `p = T`, so we can just reuse it.
// Notice something interesting here: `λpq.ppq` behaves exactly like the Mockingbird. It takes a value, `p`, 
// and self-applies `p` (producing `pp`). Well, `Mp = pp`, and you can apply that result to another value `q`,
// to get `ppq`; therefore, `Mpq = ppq`. So `M` and `λpq.ppq` behave identically (i.e. they are "extensionally equivalent",
// and in fact `λpq.ppq` is sometimes called `M*` or "the Mockinbird once-removed". The Mockingbird works as a boolean
// `OR` function:

demo('M F F = F', M(F)(F) === F)
demo('M T F = T', M(T)(F) === T)
demo('M F T = T', M(F)(T) === T)
demo('M T T = T', M(T)(T) === T)

// ### Demo: De Morgan's Laws

// With working booleans, we can illustrate some more complex logic, such as one of De Morgan's Laws: 
// `!(p && q) === (!p) || (!q)`.

header('De Morgan: not (and P Q) = or (not P) (not Q)')

function deMorgansLawDemo (p, q) { return NOT(AND(p)(q)) === OR(NOT(p))(NOT(q)) }

demo('NOT (AND F F) = OR (NOT F) (NOT F)', deMorgansLawDemo(F, F))
demo('NOT (AND T F) = OR (NOT T) (NOT F)', deMorgansLawDemo(T, F))
demo('NOT (AND F T) = OR (NOT F) (NOT T)', deMorgansLawDemo(F, T))
demo('NOT (AND T T) = OR (NOT T) (NOT T)', deMorgansLawDemo(T, T))

// ### Boolean Equality

// However, this whole time we have been cheating in the demonstrations. Lambda calculus doesn't have any `===` 
// operator to check for equality! Don't fret though, everything is functions. We can define our own equality 
// function for booleans.

header('BEQ := λpq.p (qTF) (qFT)')
const BEQ = p => q => p( q(T)(F) )( q(F)(T) )

demo('BEQ F F = T', BEQ( BEQ(F)(F) )(T))
demo('BEQ F T = F', BEQ( BEQ(F)(T) )(F))
demo('BEQ T F = F', BEQ( BEQ(T)(F) )(F))
demo('BEQ T T = T', BEQ( BEQ(T)(T) )(T))

// Not a JS operator in sight (our `demo` function accepts church encodings). But for clarity's sake, we'll go back to 
// using JS's equality operator in our `demo` calls.


// ## Church Encodings: Numerals

header('Numbers')

// Booleans are neat, but surely to compute arithmetic you need language-supported math. Right? …Nah. You can construct 
// math from scratch.

// The Church encoding for a natural number n is an n-fold "compositor" (composing combinator). In other words, "2" 
// is a function that composes a function `f` twice: `2 f x = f(f(x))`. Whereas "4" is a function that composes any `f` 
// four times: `4 f x = f(f(f(f(x)`. In this sense, 2 and 3 can be read more like "two-fold" and "three-fold", or 
// "twice" and "thrice".

// ### Hard-Coded Numbers

// In this system, `ZERO` is a function which applies a function `f` zero times to `x`. So… `ZERO`
// ignores the function argument, just returning `x`; `0 f x = x`.

header('0 := λfx.x')
// (fun fact, `0 = F`)
const ZERO = fn => x => x

// Zero applications of Mockingbird to `tweet` is just `tweet`. Good thing too, because applying Mockingbird to `tweet`
// would throw an error in JS (though it would work fine in LC, just by not simplifying further).

demo('0 M tweet = tweet', ZERO(M)(tweet) === tweet)

// We could hard-code `ONCE` as a single application of `f`…

header('hard-coded 1 and 2')

header('1 := λfx.fx')
const ONCE = fn => x => fn(x)

// Another fun fact – this is one step removed from `I`, called `I*` ("I-star").
// In fact we could have shortened this to be `1 := I`. So 0 is false and 1 is identity, how nice!

demo('1 I tweet = tweet', ONCE(I)(tweet) === tweet)

// Identity is a bit boring, however, because the n-fold composition of `I` is always `I`, even for n = 0.
// The above example doesn't really prove our function is doing anything interesting. Let's cheat a bit with
// some string ops (note, this is polluting LC with some JS, but it's just for demonstration):

const λ = 'λ'
const yell = str => str + '!'

demo('0 yell λ = λ', ZERO(yell)(λ) === 'λ')
demo('1 yell λ = yell λ = λ!', ONCE(yell)(λ) === 'λ!')

// we could also hard-code `TWICE`.

header('2 := λfx.f(fx)')
const TWICE = fn => x => fn(fn(x))

demo('2 yell λ = yell (yell λ) = λ!!', TWICE(yell)(λ) === 'λ!!')

// ### Successor

// This hard-coding works, but is very limiting. We can't do true arithmetic like this,
// where operations on numbers generate other numbers. What we need is a way to count up.

header('SUCCESSOR')

header('SUCCESSOR := λnfx.f(nfx)')
const SUCCESSOR = num => fn => x => fn(num(fn)(x))

// Don't get lost in the weeds. All we are saying is that the successor of `n` does `n` compositions of `f` to a value `x`,
// and then it does _one more_ application of `f` to the result. Therefore, it ends up doing 1 + n compositions of `f`
// in total.

const newOnce   = SUCCESSOR(ZERO)
const newTwice  = SUCCESSOR(SUCCESSOR(ZERO)) // we can use multiple successors on zero, or…
const newThrice = SUCCESSOR(newTwice) // …apply successor to already-obtained numbers.

demo('1 yell λ = λ!',     newOnce(yell)(λ) === 'λ!')
demo('2 yell λ = λ!!',   newTwice(yell)(λ) === 'λ!!')
demo('3 yell λ = λ!!!', newThrice(yell)(λ) === 'λ!!!')

// ### Composition and Point-Free Notation

// There is another way to write successor. Point-free (some joke "point-less") notation means to define a function
// purely as a combination of other functions, without explicitly writing final arguments. Sometimes this style reveals
// what a function *is* rather than what explain what it *does*. Other times it can be abused to produce 
// incomprehensible gibberish. Successor is a reasonable candidate for it, however.

// We are doing n-fold compositions, so let's define an actual `compose` function to help. 
// Composition is often notated as `∘` in infix position: `(f ∘ g) x = f(g(x))`. 
// However, Lambda Calculus only includes prefix position function application. Smullyan named this the Bluebird
// after Curry's `B` combinator.

header('Bluebird := B := (∘) := compose := λfgx.f(gx)')
const compose = f => g => x => f(g(x))
const B = compose
const Bluebird = B

demo('(B NOT NOT)  T =  NOT (NOT T)', (B(NOT)(NOT))(T)  === NOT(NOT(T)))
demo('(B yell NOT) F = yell (NOT F)', (B(yell)(NOT))(F) === yell(NOT(F)))

// Now that we have an actual composition function, we can define successor without mentioning the final `x` value argument.

header('SUCC := λnf.f∘(nf) = λnf.Bf(nf)')
const SUCC = num => fn => compose( fn )( num(fn) )

// This is just a terse way of repeating what we already know: if a given `n` composes some function `f` n times,
// then the successor of n is a function which composes one additional `f`, for a total of 1 + n compositions.

const n0 = ZERO
const n1 = SUCC(n0)
const n2 = SUCC(SUCC(n0))
const n3 = SUCC(SUCC(SUCC(n0)))
const n4 = SUCC(n3)

demo('1 yell λ = λ!',    n1(yell)(λ) === 'λ!')
demo('2 yell λ = λ!!',   n2(yell)(λ) === 'λ!!')
demo('3 yell λ = λ!!!',  n3(yell)(λ) === 'λ!!!')
demo('4 yell λ = λ!!!!', n4(yell)(λ) === 'λ!!!!')

// ### Arithemtic

// #### Addition

// Things will get pretty slow if we can only increment by 1. Let's add addition.

header('ADD := λab.a(succ)b')
const ADD = numA => numB => numA(SUCC)(numB)

// Aha, addition is just the Ath successor of B. Makes sense. For example, `ADD 3 2 = 3 SUCC 2`,
// which could be read as "thrice successor of twice".

const n5 = ADD(n2)(n3)
const n6 = ADD(n3)(n3)

demo('ADD 5 2 yell λ = λ!!!!!!!', ADD(n5)(n2)(yell)(λ) === 'λ!!!!!!!')
demo('ADD 0 3 yell λ = λ!!!',     ADD(n0)(n3)(yell)(λ) === 'λ!!!')
demo('ADD 2 2 = 4',               ADD(n2)(n2)(yell)(λ) === n4(yell)(λ))

// These equivalence checks using `yell` and `'λ'` are a bit verbose. It's annoying, but a mathematical truth,
// that there can be no general algorithm to decide if two functions are equivalent – and we cannot rely on JS
// function equality because we are generating independent function objects. Since `yell` and `'λ'`
// are already impure non-LC code, we might as well go all the way and define `church` and `jsnum`
// to convert between Church encodings and JS numbers.

header('LC <-> JS: church & jsnum')

function church (n) { return n === 0 ? n0 : SUCC(church(n - 1)) }
function jsnum (c) { return c(x => x + 1)(0) }

demo(        'church(5) = n5', church(5)(yell)(λ) === n5(yell)(λ))
demo(       'jsnum(n5) === 5',          jsnum(n5) === 5)
demo('jsnum(church(2)) === 2',   jsnum(church(2)) === 2)

// #### Multiplication

// Back to math. How about multiplication?

header('MULT := λab.a∘b = compose')
const MULT = compose

// How beautiful! Multiplication is the composition of numbers. For example, `MULT 3 2 = 3 ∘ 2`, which could be
// read as "thrice of twice", or "three of (two of (someFn))". If you compose a function `f` two times — `f ∘ f` — and
// then you compose that result three times — `(f∘f) ∘ (f∘f) ∘ (f∘f)` — 
// you get the six-fold composition of f: `f ∘ f ∘ f ∘ f ∘ f ∘ f`. 
// It helps to know that composition is associative — `f ∘ (g ∘ h) = (f ∘ g) ∘ h`.

demo('MULT 1 5 = 5', jsnum( MULT(n1)(n5) ) === 5)
demo('MULT 3 2 = 6', jsnum( MULT(n3)(n2) ) === 6)
demo('MULT 4 0 = 0', jsnum( MULT(n4)(n0) ) === 0)
demo('MULT 6 2 yell λ = λ!!!!!!!!!!!!', MULT(n6)(n2)(yell)(λ) === 'λ!!!!!!!!!!!!')

const n8 = MULT(n4)(n2)
const n9 = SUCC(n8)

// #### Exponentiation

// Exponentiation is remarkably clean too. When we say 2^3, we are saying "multiply two by itself three times";
// or putting it another way, "twice of twice of twice". So for any base and power,
// the result is the power-fold composition of the base:

header('Thrush := POW := λab.ba')
const POW = numA => numB => numB(numA)

// As you can see, we also call this combinator the Thrush. Unfortunately we have a name collision as we already defined
// `T` as the church encoding of true, so we omit the single-letter version of this combinator. There is another 
// letter sometimes reserved for true, in which case we can use `T` for Thrush; the alternate true combinator name is
// coming up soon.

demo('POW 2 3 = 8', jsnum( POW(n2)(n3) ) === 8)
demo('POW 3 2 = 9', jsnum( POW(n3)(n2) ) === 9)
demo('POW 6 1 = 6', jsnum( POW(n6)(n1) ) === 6)
demo('POW 5 0 = 1', jsnum( POW(n5)(n0) ) === 1)

// ### Num -> Bool

// As stated earlier, there is no general function-equivalence algorithm (this lies at the heart of Church's research 
// efforts into "decidability"). But just as we did for booleans, we can develop a specific equality check for numbers.

// #### Zero Equality

// We start with zero. If our input is zero, we want to produce `T`. Otherwise, we want to produce `F`.
// In our function below, if the input is zero, we run the inner function zero times,
// which means we return the final argument (`T`). However, if the input is any number greater than zero,
// we run the inner function at least once; that inner function is designed to always produce `F`.

header('ISZERO := λn.n(λ_.F)T')
const ISZERO = num => num(_ => F)(T)

demo('ISZERO 0 = T', ISZERO(n0) === T)
demo('ISZERO 1 = F', ISZERO(n1) === F)
demo('ISZERO 2 = F', ISZERO(n2) === F)

// #### The Kestrel

// ISZERO used a nice trick to produce a constant. We'll abstract that out. This is the Kestrel combinator `K`,
// named for the German word "Konstante". The `K` combinator takes a value, and produces a function which ignores its input, 
// always returning the original value. So, `K0` is a function that always returns 0; (`K tweet`) is a 
// function which always returns tweet.

header('Kestrel combinator and IS0')

header('Kestrel := K := konst := λk_.k')
const konst = k => _ => k
const K = konst
const Kestrel = K

demo('K0 tweet = 0', K(n0)(tweet) === n0)
demo('K0 chirp = 0', K(n0)(chirp) === n0)
demo('K tweet chirp = tweet', K(tweet)(chirp) === tweet)

// With K, we can redefine our isZero function more concisely.

header('IS0 := λn.n(KF)T')
const IS0 = num => num(K(F))(T)

demo('IS0 0 = T', IS0(n0) === T)
demo('IS0 1 = F', IS0(n1) === F)
demo('IS0 2 = F', IS0(n2) === F)

// `K` should look familiar; it's "alpha-equivalent" to `T`. Alpha-equivalence means it is identical except 
// for variable names, which are arbitrary and don't affect the behavior: `λk_.k = λab.a`.

// #### The Kite

// We can also make `F` out of `K` and `I`. Try tracing through the logic and confirming that `KI = F`.
// This result is known as the Kite.

header('         K = T')
header('Kite := KI = F')
const Tru = K
const Fls = K(I)
const Kite = Fls

demo('K  tweet chirp = tweet', Tru(tweet)(chirp) === tweet)
demo('KI tweet chirp = chirp', Fls(tweet)(chirp) === chirp)
demo('De Morgan using K and KI', deMorgansLawDemo(K, K(I)))

// ### Interlude: Predecessor (So Far)

// We're still a way off from numeric equality. To get it working we'll need `succ`'s opposite, `pred` (predecessor).
// For a given num, `pred` gives you the number that came before, unless we're at 0, in which case it just gives you 0.
// It is possible to define predecessor using only the tools we've built thus far, but it's quite difficult to comprehend.
// Glance at it, but we'll be seeing a better version soon:

header('PREDECESSOR := λn.n (λg.IS0 (g 1) I (B SUCC g)) (K0) 0')
const PREDECESSOR = num => num(g => IS0(g(n1))(I)(B(SUCC)(g)))(K(n0))(n0)

demo('PREDECESSOR 0 = 0', jsnum( PREDECESSOR(n0) ) === 0)
demo('PREDECESSOR 1 = 0', jsnum( PREDECESSOR(n1) ) === 0)
demo('PREDECESSOR 2 = 1', jsnum( PREDECESSOR(n2) ) === 1)
demo('PREDECESSOR 3 = 2', jsnum( PREDECESSOR(n3) ) === 2)

// Idiots, Bluebirds, and Kestrels — oh my! The essence of this formulation for `PREDECESSOR` is a machine of sorts which,
// if skipped, yields `K0 0 = 0`; if run once, produces `I K0 0 = 0`; and if run n times,
// produces `(n - 1) succ (I K0 0) = n - 1`. However, there are other versions of predecessor, including one that is far
// clearer than this. To get there, we are going to have to take a small detour into functional data structures.

// ## Functional Data Structures: Pair

header('Pair: a Tiny Functional Data Structure')

// There are varying definitions for "data structure". In this context we will use it to mean a way of organizing information,
// plus an interface for accessing that information (some might argue that this is closer to the definition of an 
// Abstract Data Type). In the lambda calculus, we do not have objects, arrays, sets or what-have-you… only functions. 
// But we've already seen that functions capture values through *closure*, and are able to produce those values again later. 
// That's the essence of the K combinator, in fact.

// Here we define a more complex entity, the Church encoding for "pair". Smullyan named this combinator the Vireo.

header('Vireo := V := PAIR := λabf.fab')
const PAIR = a => b => f => f(a)(b)
const V = PAIR
const Vireo = V

// `PAIR` takes two arbitrary values, a and b, and returns a function ("the pair") closing over those values. 
// When the pair is fed a final argument f, f is applied to a and b. So our pair can "provide" a and b, in that order,
// to any binary function.

const examplePair = PAIR(tweet)(chirp)

demo('(PAIR tweet chirp) T = tweet', examplePair(T) === tweet)
demo('(PAIR tweet chirp) F = chirp', examplePair(F) === chirp)

// ### Opening the Closure

// As you can see, when a pair is fed the binary function `T` or `F`, it has the effect of extracting out one member of 
// the pair. To make this more expressive and English-y, we can define FST (first) and SND (second) functions 
// that perform this work for us:

header('FST := λp.pT; SND = λp.pF')
const FST = somePair => somePair(T)
const SND = somePair => somePair(F)

demo('FST (PAIR tweet chirp) = tweet', FST(examplePair) === tweet)
demo('SND (PAIR tweet chirp) = chirp', SND(examplePair) === chirp)

// ### Immutability

// There isn't any way to change the closed-over variables, but that's a good thing – immutability means that we never 
// accidentally mess up data someone else was relying on. We can generate new data instead.

header('SET_FST := λcp.PAIR c (SND p)')
const SET_FST = newFirst => oldP => PAIR(newFirst)(SND(oldP))

demo('FST (SET_FST chirp (PAIR tweet tweet)) = chirp', FST( SET_FST(chirp)(PAIR(tweet)(tweet)) ) === chirp)
demo('SND (SET_FST chirp (PAIR tweet tweet)) = tweet', SND( SET_FST(chirp)(PAIR(tweet)(tweet)) ) === tweet)

// It would help to have a shorthand for pairs. We will use <a, b> to stand in for `(pair a b)`.

header('SET_SND := λcp.PAIR (FST p) c')
const SET_SND = newSecond => oldP => PAIR(FST(oldP))(newSecond)

demo('FST (SET_SND chirp <tweet, tweet>) = tweet', FST( SET_SND(chirp)(PAIR(tweet)(tweet)) ) === tweet)
demo('SND (SET_SND chirp <tweet, tweet>) = chirp', SND( SET_SND(chirp)(PAIR(tweet)(tweet)) ) === chirp)

// ### Counting Up with Memory

// Back on track towards our cleaner `PRED`, we will define a special pair function Φ (aka PHI) which moves 
// the second element to the first, and increments the second element by 1. In shorthand, `Φ <a, b> = <b, b + 1>`.
// The use of this function will become apparent shortly.

header('PHI := Φ := λp.PAIR (SND p) (SUCC (SND p))')
const Φ = oldPair => PAIR(SND(oldPair))(SUCC(SND(oldPair)))
const PHI = Φ

const examplePairChirp0 = PAIR(chirp)(n0)
const examplePairTweet4 = PAIR(tweet)(n4)

demo('Φ <chirp, 0> = <0, 1>',
  jsnum( FST(Φ(examplePairChirp0)) ) === 0 &&
  jsnum( SND(Φ(examplePairChirp0)) ) === 1
)
demo('Φ <tweet, 4> = <4, 5>',
  jsnum( FST(Φ(examplePairTweet4)) ) === 4 &&
  jsnum( SND(Φ(examplePairTweet4)) ) === 5
)

// ## Back to Arithmetic

// ### A Cleaner Predecessor

// At long last, we can return to our predecessor function. With the help of Φ, it is wonderfully simple… well, 
// relatively speaking at least.

header('PRED := λn.FST (n Φ <0, 0>)')
const PRED = n => FST( n(Φ)(PAIR(n0)(n0)) )

// All we do is successive applications of Φ to a seed pair <0, 0>. After n applications, the pair is <n - 1, n>.
// Then we can pluck off the first value of the pair! In effect, we count up to n, but keep the predecessor around
// for easy reference.

// n | n Φ <0, 0> | first of result pair
// --|------------|---------------------
// 0 |     <0, 0> | 0
// 1 |     <0, 1> | 0
// 2 |     <1, 2> | 1
// 3 |     <2, 3> | 2

demo('PRED 0 = 0', jsnum( PRED(n0) ) === 0)
demo('PRED 1 = 0', jsnum( PRED(n1) ) === 0)
demo('PRED 2 = 1', jsnum( PRED(n2) ) === 1)
demo('PRED 3 = 2', jsnum( PRED(n3) ) === 2)

// ### Subtraction At Last

// Now that the epic `pred` exists, we can do subtraction… at least, down to 0.

header('SUB := λab.b PRED a')
const SUB = a => b => b(PRED)(a)

const n7 = ADD(n4)(n3)

demo('SUB 5 2 = 3', jsnum( SUB(n5)(n2) ) === 3)
demo('SUB 4 0 = 4', jsnum( SUB(n4)(n0) ) === 4)
demo('SUB 2 2 = 0', jsnum( SUB(n2)(n7) ) === 0)
demo('SUB 2 7 = 0', jsnum( SUB(n2)(n7) ) === 0)

// ### Number Comparisons

// This kind of limited subtraction enables less-than-or-equal-to.

header('LEQ := λab.IS0(SUB a b)')
const LEQ = a => b => IS0(SUB(a)(b))

demo('LEQ 3 2 = F', LEQ(n3)(n2) === F)
demo('LEQ 3 3 = T', LEQ(n3)(n3) === T)
demo('LEQ 3 4 = T', LEQ(n3)(n4) === T)

// Finally we can test for numeric equality. 🎉🎉🎉

header('eq := λab.AND (LEQ a b) (LEQ b a)')
const EQ = a => b => AND (LEQ(a)(b)) (LEQ(b)(a))

demo('EQ 4 6 = F', EQ(n4)(n5) === F)
demo('EQ 7 3 = F', EQ(n7)(n3) === F)
demo('EQ 5 5 = T', EQ(n5)(n5) === T)
demo('EQ (ADD 3 6) (POW 3 2) = T', EQ(ADD(n3)(n6))(POW(n3)(n2)) === T)

// ## More Composition

// Of course we can use composition to create other results. At first glance, it would seem like greater-than can be 
// the composition of `NOT` and `LEQ`. But this doesn't work because `LEQ` is a two-arg function, and compose only works 
// with unary functions. Thanks to the beautiful Blackbird combinator, however, we can create point-free compositions 
// where the rightmost function is binary.

header('Blackbird := B′ := BBB')
const B1 = compose(compose)(compose)
const Blackbird = B1

// If you find B1 confusing, the point-ful version might help: `B1 := λfgxy.f(g x y)`. 
// Also, why Smullyan chose "B1" instead of "B2", I can only guess.

header('GT := B1 NOT LEQ')
const GT = B1(NOT)(LEQ)

demo('GT 6 2 = T', GT(n6)(n2) === T)
demo('GT 4 4 = F', GT(n4)(n4) === F)
demo('GT 4 5 = F', GT(n4)(n5) === F)

// Another use of Blackbird: `neq := B1 not eq`.

// ## Final Notes

// There are church encodings and lambda techniques for lists, types, rationals, reals, and anything else that is 
// computable – plus the astonishing Y-combinator, which enables recursion in a syntax where functions are all anonymous.
// We also omitted the Starling, which can be combined with the Kestrel in various ways to produce *every other function.*
// For now, we will end with an actual real-world classic math problem, calculated entirely using lambda calculus – only 
// converted back to JS numbers at the end, purely for display purposes.

header('FIB := λn.n (λfab.f b (ADD a b)) K 0 1')
const FIB = n => n(f => a => b => f(b)(ADD(a)(b)))(K)(n0)(n1)

demo('FIB 0 = 0', jsnum( FIB(n0) ) === 0)
demo('FIB 1 = 1', jsnum( FIB(n1) ) === 1)
demo('FIB 2 = 1', jsnum( FIB(n2) ) === 1)
demo('FIB 3 = 2', jsnum( FIB(n3) ) === 2)
demo('FIB 4 = 3', jsnum( FIB(n4) ) === 3)
demo('FIB 5 = 5', jsnum( FIB(n5) ) === 5)
demo('FIB 6 = 8', jsnum( FIB(n6) ) === 8)

logErrsAndSetExitCode()