Boolsk logik med SKI

Kombinatorer er ikke ligefrem nemme at forstå. Som programmør har jeg mest gavn af at skrive kode, der viser det begreb, jeg prøver at få greb om. Jeg lærer bedst ved selv at arbejde med det.

I dette indlæg implementerer jeg de tre grundlæggende kombinatorer i SKI-kombinatorlogikken. Derefter tilføjer jeg boolske operatorer og afprøver De Morgans love.

Jeg er ikke ekspert. Det er blot noter fra mit eget forsøg på at forstå emnet, og jeg håber, at de kan hjælpe andre, der prøver at forstå det samme.

Kombinatorfugle

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 metafor for kombinatorer:

I en fortryllet skov bor der talende fugle. Hvis du har to vilkårlige fugle A og B og råber B's navn til A, svarer A ved at råbe navnet på en anden fugl til dig. Denne fugl kalder vi AB. AB er altså den fugl, som A nævner efter at have hørt B's navn. I stedet for hele tiden at bruge den besværlige formulering "A's svar på at høre B's navn" siger vi mere enkelt: "A's svar på B". AB er dermed A's svar på B. A's svar på B er ikke nødvendigvis det samme som B's svar på A. Med symboler betyder det, at AB ikke nødvendigvis er den samme fugl som BA. Hvis vi har tre fugle A, B og C, er fuglen A(BC) heller ikke nødvendigvis den samme som fuglen (AB)C. Fuglen A(BC) er A's svar på fuglen BC, mens fuglen (AB)C er fuglen AB's svar på fuglen C. Parenteserne er derfor nødvendige for at undgå tvetydighed. Hvis jeg blot skrev ABC, kunne du ikke vide, om jeg mente fuglen A(BC) eller fuglen (AB)C.

Jeg gennemgår ikke bogen kapitel for kapitel her, men jeg håber at vende tilbage til dele af den i senere indlæg.

Nogle fugle tager andre fugle som input og returnerer fugle som output. Det er en fin analogi til funktioner. Kombinatorerne er funktioner, og vi giver dem fuglenavne.

Lad os begynde med den måske enkleste kombinator:

Idiot λa.a

Nogle kalder den Identity-fuglen. Selv om den er enkel, får vi senere brug for den. Sådan definerer vi en Idiot i TypeScript:

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

Den tager en værdi og returnerer den uændret:

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

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

Kestrel λab.a

Kestrel kaldes også constant eller TRUE. Den tager en værdi og returnerer den igen, uanset hvad man sender ind 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, også kaldet substitutionsoperatoren, er mere kompliceret. Den tager tre argumenter og returnerer a(c)(b(c)). Først anvender den a på c og b på c. Derefter anvender den resultatet af a(c) på resultatet af b(c):

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, udelukkende 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

Antag, at vi har et ordnet par med 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, at den anden test bruger KI i stedet for SK. I er ikke nødvendig, men kan bruges som syntaktisk sukker.

NOT = (SK)(K)

Her bliver det mere kompliceret, så lad os stole på testene frem for intuitionen. 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)
  })
})

Denne definition af NOT adskiller sig lidt fra den, der står på Wikipedia. Svaret på mit spørgsmål på Stack Overflow forklarer 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

Med det boolske logiksystem kan vi efterprøve 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)
  })
})

Kildekoden ligger på GitHub.