SKI boolsk logik

Kombinatorer er ikke et let koncept at forstå. Som programmør finder jeg det nyttigt at skrive noget kode, der beviser det koncept, jeg vil forstå. At lære ved at gøre det!

I dette indlæg implementerer jeg de tre grundlæggende kombinatorer fra SKI combinator calculus. Derefter tilføjer jeg boolske logik-operatorer og tester De Morgans love.

Jeg påstår ikke at være ekspert. Betragt dette indlæg blot som noter, jeg skrev for at forstå konceptet. Forhåbentlig kan disse noter hjælpe dem, der forsøger det samme.

Kombinator-fugle

I sin berømte bog "To Mock a Mockingbird and Other Logic Puzzles: Including an Amazing Adventure in Combinatory Logic" bruger Raymond Smullyan fugle som en metafor for kombinatorer:

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.

At gennemgå bogen kapitel for kapitel ligger uden for denne artikels rammer, men forhåbentlig gør jeg det delvist i kommende indlæg.

Uanset hvad: nogle fugle tager fugle ind og returnerer fugle ud — hvilken smuk analogi til funktioner! Kombinatorerne er funktioner, og vi giver dem fuglenavne.

Mød nu nok den simpleste kombinator nogensinde:

Idiot λa.a

Nogle kalder den Identity-fuglen. Trods dens enkelhed kan man se senere, at den faktisk kan være nyttig. Her er, hvordan vi definerer en Idiot i TypeScript:

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

Den tager en ting og returnerer den samme ting uden at ændre den:

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

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

Kestrel λab.a

Kestrel er også kendt som constant eller TRUE. Den tager simpelthen en værdi og returnerer derefter den værdi, uanset hvad man giver den bagefter:

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)

Starling (eller substitutions-operatoren) er mere kompliceret: "Den tager tre argumenter og returnerer derefter det første argument anvendt på det tredje, som derefter anvendes på resultatet af det andet argument anvendt på det tredje":

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

Vi kan bygge enhver kombinator (inklusive I) kun med K og 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

Lad os sige, at vi har et ordnet par af to værdier: true og false. Da Kestrel altid returnerer den første værdi, kan vi kalde den 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

På samme måde kan vi bygge en kombinator, der altid returnerer 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)
  })
})

Bemærk, hvordan vi i den anden test bruger KI i stedet for SK. I er faktisk ikke nødvendig, men kan bruges som syntaktisk sukker.

NOT = (SK)(K)

Nu bliver tingene komplicerede. Vi kan ikke stole på vores intuition og skriver tests. Her er 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)
  })
})

Definitionen af NOT er ikke helt den samme som på Wikipedia. Tjek svaret på mit spørgsmål på Stackoverflow for at se hvorfor.

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 Morgans love

Nu hvor vi har et boolsk logiksystem, lad os tjekke De Morgans love:

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)
  })
})

Repositoryet er her.