SKI boolean logic

Combinators are not an easy concept to grok. As a programmer, I find it helpful to write code that demonstrates the concept I am trying to understand. For me, the best way to learn is by doing.

In this post, I implement the three basic combinators of the SKI combinator calculus. Then, I add boolean logic operators and test De Morgan's laws.

I'm not an expert. These are simply notes I wrote while trying to grasp the concept, and I hope they help others doing the same.

Combinator Birds

In his famous book "To Mock a Mockingbird and Other Logic Puzzles: Including an Amazing Adventure in Combinatory Logic", Raymond Smullyan uses birds as a metaphor of combinators:

A certain enchanted forest is inhabited by talking birds. Given any birds A and B, if you call out the name of B to A, then A will respond by calling out the name of some bird to you; this bird we designate by AB. Thus AB is the bird named by A upon hearing the name of B. Instead of constantly using the cumbersome phrase "A's response to hearing the name of B," we shall more simply say: "A's response to B." Thus AB is A's response to B. In general, A's response to B is not necessarily the same as B's response to A-in symbols, AB is not necessarily the same bird as BA. Also, given three birds A, B, and C, the bird A(BC) is not necessarily the same as the bird (AB)C. The bird A(BC) is A's response to the bird BC, whereas the bird (AB)C is the response of the bird AB to the bird C. The use of parentheses is thus necessary to avoid ambiguity; if I just wrote ABC, you could not possibly know whether I meant the bird A(BC) or the bird (AB)C.

I won't go through the book chapter by chapter here, but I hope to cover parts of it in future posts.

Some birds take other birds as input and return birds as output. It's a lovely analogy for functions. The combinators are functions, and we give them bird names.

Let's start with perhaps the simplest combinator:

Idiot λa.a

Some call it the Identity bird. Despite its simplicity, we'll see later that it can be useful. Here is how we define an Idiot in TypeScript:

export type Idiot = <T>(a: T) => T
export const I: Idiot = a => a

It takes a value and returns it unchanged:

describe('Idiot', () => {
  const x = 'whatever';

  test('Ix = x', () => {
    expect(I(x)).toBe(x);
  });
);

Kestrel λab.a

Kestrel is also known as constant or TRUE. It takes a value and returns it regardless of what you pass next:

export type Kestrel = <T0, T1>(a: T0) => (b: T1) => T0
export const K: Kestrel = a => b => a

describe("Kestrel", () => {
  test("Kxy = x", () => {
    const x = "x"
    const y = "y"

    const actual = K(x)(y)

    expect(actual).toBe(x)
  })
})

Starling λabc.ac(bc)

The Starling, or substitution operator, is more complicated. It takes three arguments and returns a(c)(b(c)): the first argument applied to the third, then applied to the result of the second argument applied to the third.

export type Starling = <TC>(
  a: (c: TC) => any
) => (b: (c: TC) => any) => (c: TC) => any

export const S: Starling = a => b => c => a(c)(b(c))

describe("Starling", () => {
  test("Sxyz = xz(yz)", () => {
    const x = _ => I
    const y = a => a() * 2
    const z = () => 3

    const xz = x(z)
    const yz = y(z)

    const actual = S(x)(y)(z)

    expect(actual).toBe(xz(yz))
    expect(actual).toBe(6)
  })
})

Ix = SSKKx = SK(KK)x = x

We can build any combinator (including I) just with K and S:

describe("Idiot", () => {
  test("Ix = SSKKx = x", () => {
    expect(S(S)(K)(K)(x)).toBe(I(x))
  })

  test("Ix = SK(KK)x = x", () => {
    const sk = S(K)
    const kk = K(K)
    expect(sk(kk)(x)).toBe(I(x))
  })
})

TRUE = K

Suppose we have an ordered pair of two values: true and false. Since Kestrel always returns the first value, we can call it TRUE:

export const TRUE = K

const t = () => true
const f = () => false

describe("TRUE = K", () => {
  test("Ktf = (TRUE)tf = t", () => {
    const actual = TRUE(t)(f)()
    expect(actual).toBe(K(t)(f)())
    expect(actual).toBe(true)
  })
})

FALSE = SK = KI

Similarly, we can build a combinator that always returns FALSE:

export const FALSE = S(K)

describe("FALSE = SK", () => {
  test("SKxy = y", () => {
    expect(FALSE(t)(f)()).toBe(false)
  })

  test("KItf = (FALSE)tf = f", () => {
    const actual = K(I)(t)(f)()
    expect(actual).toBe(FALSE(t)(f)())
    expect(actual).toBe(false)
  })
})

Notice that the second test uses KI instead of SK. I is not necessary, but we can use it as syntactic sugar.

NOT = (SK)(K)

Things get more complicated here, so let's rely on tests rather than intuition. Here is NOT:

export const NOT = b => b(S(K))(K)

describe("NOT = (SK)(K)", () => {
  test("NOT = (SK)(K)", () => {
    const sk = S(K)
    expect(TRUE(sk(K))(t)(f)()).toBe(false)
    expect(TRUE(sk(K))(f)(t)()).toBe(true)
  })

  test("NOT(TRUE) = FALSE", () => {
    expect(NOT(TRUE)(t)(f)()).toBe(false)
    expect(NOT(TRUE)(f)(t)()).toBe(true)
  })

  test("NOT(FALSE) = TRUE", () => {
    expect(NOT(FALSE)(t)(f)()).toBe(true)
    expect(NOT(FALSE)(f)(t)()).toBe(false)
  })

  test("TRUE(FALSE)(TRUE) = FALSE", () => {
    expect(TRUE(FALSE)(TRUE)(t)(f)()).toBe(false)
  })

  test("FALSE(FALSE)(TRUE) = TRUE", () => {
    expect(FALSE(FALSE)(TRUE)(t)(f)()).toBe(true)
  })
})

This definition of NOT is not exactly the same as the one on Wikipedia. The answer to my question on Stack Overflow explains why.

OR = TRUE

export const OR = TRUE

describe("OR = T = K", () => {
  test("(T)OR(T) = T(T)(T) = T", () => {
    expect(TRUE(OR)(TRUE)(t)(f)()).toBe(true)
  })

  test("(T)OR(F) = T(T)(F) = T", () => {
    expect(TRUE(OR)(FALSE)(t)(f)()).toBe(true)
  })

  test("(F)OR(T) = F(T)(T) = T", () => {
    expect(FALSE(OR)(TRUE)(t)(f)()).toBe(true)
  })

  test("(F)OR(F) = F(T)(F) = F", () => {
    expect(FALSE(OR)(FALSE)(t)(f)()).toBe(false)
  })
})

AND = FALSE

export const AND = FALSE

describe("AND = F = SK", () => {
  test("(T)(T)AND = T(T)(F) = T", () => {
    expect(TRUE(TRUE)(AND)(t)(f)()).toBe(true)
  })
  test("(T)(F)AND = T(F)(F) = F", () => {
    expect(TRUE(FALSE)(AND)(t)(f)()).toBe(false)
  })
  test("(F)(T)AND = F(T)(F) = F", () => {
    expect(FALSE(TRUE)(AND)(t)(f)()).toBe(false)
  })
  test("(F)(F)AND = F(F)(F) = F", () => {
    expect(FALSE(FALSE)(AND)(t)(f)()).toBe(false)
  })
})

De Morgan's laws

With a Boolean logic system in place, we can check De Morgan's laws:

describe("De Morgan's Laws", () => {
  const or = (a, b) => a(OR)(b)
  const and = (a, b) => a(b)(AND)
  const not = a => NOT(a)

  test("¬(a ∨ b) ⇔ (¬a) ∧ (¬b)", () => {
    expect(!(true || true)).toBe(false)
    expect(!true && !true).toBe(false)
    expect(not(or(TRUE, TRUE))(t)(f)()).toBe(false)
    expect(and(not(TRUE), not(TRUE))(t)(f)()).toBe(false)

    expect(!(true || false)).toBe(false)
    expect(!true && !false).toBe(false)
    expect(not(or(TRUE, FALSE))(t)(f)()).toBe(false)
    expect(and(not(TRUE), not(FALSE))(t)(f)()).toBe(false)

    expect(!(false || false)).toBe(true)
    expect(!false && !false).toBe(true)
    expect(not(or(FALSE, FALSE))(t)(f)()).toBe(true)
    expect(and(not(FALSE), not(FALSE))(t)(f)()).toBe(true)

    expect(!(false || true)).toBe(false)
    expect(!false && !true).toBe(false)
    expect(not(or(FALSE, TRUE))(t)(f)()).toBe(false)
    expect(and(not(FALSE), not(TRUE))(t)(f)()).toBe(false)
  })

  test("¬(a ∧ b) ⇔ (¬a) ∨ (¬b)", () => {
    expect(!(true && true)).toBe(false)
    expect(!true || !true).toBe(false)
    expect(not(and(TRUE, TRUE))(t)(f)()).toBe(false)
    expect(or(not(TRUE), not(TRUE))(t)(f)()).toBe(false)

    expect(!(true && false)).toBe(true)
    expect(!true || !false).toBe(true)
    expect(not(and(TRUE, FALSE))(t)(f)()).toBe(true)
    expect(or(not(TRUE), not(FALSE))(t)(f)()).toBe(true)

    expect(!(false && false)).toBe(true)
    expect(!false || !false).toBe(true)
    expect(not(and(FALSE, FALSE))(t)(f)()).toBe(true)
    expect(or(not(FALSE), not(FALSE))(t)(f)()).toBe(true)

    expect(!(false && false)).toBe(true)
    expect(!false || !false).toBe(true)
    expect(not(and(FALSE, FALSE))(t)(f)()).toBe(true)
    expect(or(not(FALSE), not(FALSE))(t)(f)()).toBe(true)

    expect(!(false && true)).toBe(true)
    expect(!false || !true).toBe(true)
    expect(not(and(FALSE, TRUE))(t)(f)()).toBe(true)
    expect(or(not(FALSE), not(TRUE))(t)(f)()).toBe(true)
  })
})

The source code is on GitHub.