Software Abstraction Cheat Sheet

def factorial(n):
    result = 1
    for i in range(1, n + 1):
        result *= i
    return result

fact = Y (λf. λn. if (iszero n) 1 (mult n (f (pred n))))

where:
  Y    = λf.(λx.f(x x))(λx.f(x x))  -- fixed-point combinator
  mult = λm.λn.λf.m(n f)            -- Church numerals
  pred = λn.λf.λx.n(λg.λh.h(g f))(λu.x)(λu.u)

def and_gate(a, b):
    if a == True:
        if b == True:
            return True
        else:
            return False
    else:
        return False

TRUE  = λx.λy.x
FALSE = λx.λy.y
AND   = λp.λq.p q p

def increment_binary(bits):
    carry = 1
    result = []
    for bit in reversed(bits):
        if carry:
            if bit == '0':
                result.append('1')
                carry = 0
            else:
                result.append('0')
                carry = 1
        else:
            result.append(bit)
    if carry:
        result.append('1')
    return ''.join(reversed(result))

States: {qcarry, halt}
Alphabet: {0, 1, □}

Transitions (add 1 with carry):
  δ(qcarry, 0) = (halt,   1, L)  -- flip 0→1, done
  δ(qcarry, 1) = (qcarry, 0, L)  -- flip 1→0, carry
  δ(qcarry, □) = (halt,   1, L)  -- overflow: new 1

def balanced(s):
    count = 0
    for c in s:
        if c == '(': count += 1
        elif c == ')': count -= 1
        if count < 0: return False
    return count == 0

CFG:  S → SS | "(" S ")" | ε

PDA:
  read '(' → push
  read ')' → pop (reject if empty)
  accept if stack empty at end

def add(m, n):
    result = m
    for _ in range(n):
        result += 1
    return result

add(m, 0)    = m           -- base
add(m, S(n)) = S(add(m, n)) -- step

Formally: add = Pr[π₁, Cn[S, π₃]]

x = 5
while x > 0:
    x = x - 1
# x is now 0

⟦while b do c⟧ = fix(F)

F = λφ.λσ. if ⟦b⟧σ = true 
            then φ(⟦c⟧σ) 
            else σ

(2 + 3) * 4
= 5 * 4      # addition first
= 20         # then multiplication

⟨(2+3)*4, σ⟩ → ⟨5*4, σ⟩
             → ⟨20, σ⟩

Rule: ⟨n₁+n₂, σ⟩ → ⟨n, σ⟩

# Sum 1 to n
s = 0; i = 0
while i < n:
    i = i + 1
    s = s + i
# s = n(n+1)/2

{n ≥ 0}
{INV: s = i(i+1)/2 ∧ i ≤ n}
while i < n do body
{s = n(n+1)/2}

Node* n = malloc(sizeof(Node));
n->value = val;
n->next = NULL;
return n;

{emp}
  n := alloc(2);
{n ↦ _, _}
  [n] := val; [n+1] := NULL;
{n ↦ val, NULL}

def double(x: int) -> int:
    return x * 2

result = double(5)  # OK
# double("hi")  # Type error!

Γ ⊢ double : Int → Int
Γ ⊢ 5 : Int
────────────────────────
Γ ⊢ double(5) : Int

A → B     (function)
A × B     (pair/tuple)
A + B     (Either/union)
⊥         (Void/Never)

A ⟹ B    (implication)
A ∧ B     (conjunction)
A ∨ B     (disjunction)
⊥         (false)

"The mutex is never held
by two processes at once"

"Every request eventually
gets a response"

□(¬(holds₁ ∧ holds₂))
  [SAFETY]

□(request → ◇response)
  [LIVENESS]

x = 5      # x ∈ {5}
y = -3     # y ∈ {-3}
z = x * y  # z ∈ {-15}

x = +   # positive
y = -   # negative
z = + × - = -  # negative

class Stack:
    def __init__(self):
        self._data = []
    def push(self, x):
        self._data.append(x)
    def pop(self):
        return self._data.pop()

Stack[T]
  empty : Stack[T]
  push  : Stack[T] × T → Stack[T]
  pop   : Stack[T] → Stack[T] × T

pop(push(s, x)) = (s, x)

SELECT name, dept
FROM employees
WHERE salary > 50000

π_{name,dept}(
  σ_{salary>50000}(employees)
)