Programming with Algebra

Link to code

Introduction

Students often ask (in CIS352): “why learn Racket, a language with an arcane syntax that I might not use outside of this class?” It is a very reasonable question, and today we will answer it directly:

We use Racket because Racket is the language that lets us most rapidly experiment with and compute over term algebras.

Using algebra will allow us to reason rigorously about code, enabling us to (a) prove that certain fragments of code are equal but also (b) giving us a way of gaining intuition for what the code is doing as we evaluate the program. The essential purpose of algebra is to be able to perform equational reasoning: substituting equals by equals to iteratively establish the equality of increasingly-complex code via simple, easily-understood local conversions.

Computers are extremely complex, and the typical programmer’s mental model of the program’s execution probably involves (at least) some local variables, a stack, and memory (e.g., the heap). While this is not an unreasonable abstraction (although it is arguably a bit archaic for truly modern hardware), it relies on a lot of complexity which you (likely) do not fully understand. Our goal is to have you look at languages that are so simple, you can understand their execution completely, with absolutely zero semantic ambiguity. To do that, we will start by connecting back to our high school algebra classes.

We all intuitively understand:

f(x,y) = x^2 + cos(y/x)

In high-school algebra, we learn how to manipulate algebraic expressions, and in particular we know how to do substitution, e.g.:

f(z+k, z^2) = (z+k)^2 + cos((z^2)/(z+k))

High-school algebra then teaches us to “simplify” expressions into canonical forms. E.g., the “FOIL” rule, i.e., the identity:

(x + y)^2 = x^2 + 2xy + y^2

A significant amount of high-school algebra is about building our intuition for how to simplify these algebraic expressions into canonical forms.

Term Algebras

“Term algebras are finite trees.”

Definition: Term Algebra (not to be confused with high-school algebra, etc.)

Assume T is a signature: a set of constructors (names) along with associated arities. The term algebra over T is the set of terms which may be formed by applying constructors (respecting their associated arities) to other terms in the algebra. We may construe zero-arity constructors as the algebra’s “constants.”

For example, take C = {'0 with arity 0, '1 with arity 0, '+ with arity 2}

Terms include: 0, 1, 0 + 1, 1 + (0 + 1), (0 + 0) + 1, etc…

We wrote examples in infix style to be intuitive. Pedantically, we might write:

0(), 1(), +(0(),1()), +(1(),+(0(),1()))

Without loss of generality, we will represent all function calls in prefix form. By doing this, we see a central advantage of using Racket for the course: Racket’s lists enable us to trivially represent term algebras.

You can think of term algebras as “raw, uninterpreted terms.”

(Rhetorical) Question: Why are they so closely related to Racket?

Answer: Racket makes term algebras immediately visible:

  1. Constructors: cons / '()
  2. Functions defined via case analysis: match
  3. Recursion mirrors the inductive structure of terms

QuickAnswer

Now, let’s have you write this up in Racket: Write a type predicate, add-expr?, which characterizes the set of expressions over the constants 1/0 and the two-argument +:

(define (add-expr? e)
  (match e
    [0 'todo]               ;; 0 is an add-expr?
    [1 'todo]               ;; 1 is an add-expr?
    ;; Hint: possible to use a predicate pattern: ,(? p? e0)
    [`(+ ,e0 ,e1) 'todo]    ;; (+ e0 e1) is an add-expr? if e0 / e1 are add-expr?s
    [_ #f]))

Now, given an expression, e, we may write a Racket function that evaluates the expression e down to a number. In fact, if we construe add-expr? to define a programming language, then we are writing our first interpreter. We will use recursion and matching to build our interpreter, following a common style we will learn about later. We will not focus extensively on interpreters in today’s class, but we will use algebraic data types to define the abstract syntax of programming languages frequently.

;; (add-expr->number '(+ 1 (+ 0 (+ 1 0)))) => 2
(define (add-expr->number e)
  (match e
    [0 'todo]
    [1 'todo]
    [`(+ ,e0 ,e1) 'todo]))

Given any signature T (a set of constructors and associated arities), it is possible to write a type predicate using match.

Example:

Let the algebra bool? be formed by the following constructors:

  • true – of arity 0
  • false – of arity 0
  • and – of arity 2
  • or – of arity 2
(define (bool? e)
  (match e
    ['true #t]
    ['false #t]
    [`(and ,(? bool? e0) ,(? bool? e1)) #t]
    [`(or ,(? bool? e0) ,(? bool? e1))  #t]
    [_ #f]))

QuickAnswer

Define a function that converts a bool? to a Racket boolean? (i.e., just #t/#f).

(define (bool?->racket b)
  'todo)

The natural numbers, as a term algebra

We now define the natural numbers as a term algebra whose signature is 0 with arity 0 and S (successor) with arity 1:

(define (nat? n)
  (match n
    ['0 #t]
    [`(S ,(? nat? n)) #t]
    [_ #f]))

(define zero '0)
(define three '(S (S (S 0))))

Convert a Racket natural to a number:

(define (nat->num n)
  (match n
    ['0 0]
    [`(S ,n+) (add1 (nat->num n+))]))

Assume n0 satisfies nat?, write nat-even?:

(define (nat-even? n)
  (match n
    ['0 #t]
    [`(S 0) #f]
    [`(S (S ,n)) (nat-even? n)]))

QuickAnswer

Don’t use nat->num or nat-even?:

(define (nat-odd? n)
  'todo)

QuickAnswer

Assume n0 and n1 are both nat?. Now, define (<= n0 n1).

Basic approach: use recursion over n0 / n1:

  • Match n0, if n0 is 0 then return #t
  • If n0 not 0, then what do you do…?

DON’T use nat->num (which makes this easier):

(define (nat-lte n0 n1)
  'todo)

Quasiquoting and Recursive Functions on Algebras

Last lecture (and this lecture), we learned about quasipatterns, which allow us to match list-like patterns. We can use quasiquoting to produce lists which “drop in” or “splice in” other expressions.

For example:

(let ([x 20])
  `(,x x ,(+ x 1))) ;; notice, `, *NOT* '

This expression produces a list of three elements:

  1. 20, because x was unquoted (i.e., evaluated, to be dropped in)
    • The comma unquotes, it says: “evaluate the next expression you read and then drop it in.”
  2. x, because x was under a quasiquote and not unquoted
    • Unless you unquote, ` acts like '
  3. 21, because ,(+ x 1) says: evaluate (+ x 1), then take its result and drop it in here.

If we use quote ' instead of quasiquote `, we will just get the literal expression, and no unquoting is possible:

(let ([x 20]) '(,x x ,(+ x 1))) ;; produces literally '(,x x ,(+ x 1))

We will start to use quasiquotes pervasively to produce algebraic data. For example, we will now define the (add-two n) function.

;; Assume n satisfies nat?
(define (add-two n) `(S (S ,n)))

(add-two '(S (S (S 0)))) ;; '(S (S (S (S (S 0)))))

Assume n0, n1 both nat. Define n0 + n1. Algebraically, we say:

(plus 0 k) = k
(plus (S n) k) = (S (plus n k))

Your result must satisfy nat?, and forall n0, n1 which satisfy nat?, we must have that:

(nat->num (plus n0 n1)) = (+ (nat->num n0) (nat->num n1))

(define (plus n0 n1)
  (match n0
    ['0 n1]
    [`(S ,n) `(S ,(plus n n1))]))

QuickAnswer

Idea: recursion on n0

(times 0 k) = 0
(times (S n) k) = k + (times n k)

Remember:

(nat->num (times n0 n1)) = (* (nat->num n0) (nat->num n1))

(define (times n0 n1)
  'todo)

QuickAnswer

Now, we use recursion on nat? to define the factorial function:

(fac 0) => 1
(fac (S n)) => (S n) * (fac n)

Remember, we must produce a nat?:

(define (factorial n)
  'todo)

;; (factorial '(S (S (S (S 0)))))
;;   => '(S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S 0))))))))))))))))))))))))
;; (nat->num (factorial '(S (S (S (S 0)))))) => 24

Equality and Canonical Terms (Advanced)

It is important to understand that the term algebra is a set of “raw” terms, which are not equated in any way. For example, although we may be tempted to think that `(+ 1 0) and `(+ 0 1) should represent the same term (because they both evaluate to 1 in Racket), they are distinct terms from the perspective of the term algebra add-expr?. Specifically…

(equal? '(+ 1 0) '(+ 0 1)) ;; #f

Definition: Quotient Algebra

In many settings, it will be desirable to define equations over terms. These equations effectively partition the term algebra into equivalence classes. For example, for the algebra add-expr?, we might also consider the following equations:

(+ x y) = (+ y x)    (plus-comm)
(+ 0 x) = x          (plus-id-0)

From these two rules, we may prove that: (+ x 0) = x

  • (+ x 0) = (+ 0 x) (applying plus-comm)
  • (+ 0 x) = x (applying plus-id-0)

Recall that = is reflexive, antisymmetric, and transitive.

When we take a term algebra and add an equivalence relation, we get a quotient algebra. It is an esoteric-sounding name, but it involves a key distinction:

  • The term algebra is just a raw set of terms, all of which are just finite trees.
  • A quotient algebra refines this, equating some of the terms to each other, effectively partitioning the space.

For example, while…

(equal? '(+ 0 (+ 1 1)) '(+ 1 (+ 0 1))) ;; #f

…in Racket, the quotient algebra formed by the two equations above would disagree, instead saying that all of the following are equal:

(+ 0 (+ 1 1)) = (+ 1 (+ 0 1)) = (+ 1 1)

IMPORTANT: Specific proofs around quotient algebras are a more advanced topic, and you will not need to deeply understand them for the course. However, it is important to be able to understand the difference between “structural equality” (i.e., equal?) and “application-specific” equality.

In general, it is not possible to decide whether two arbitrary quotient algebra terms are equal or not. The “word problem for equational theories” says that it is impossible, in general, to decide the equivalence of two terms t0 and t1, under the set of equations E.

While we cannot decide the equivalence of arbitrary algebraic formulas, almost all of our day-to-day programming is done in a setting where equality is trivially decidable: for example, deciding the equality of numbers is easy.

;; Compare two add-expr?s for equality
;; Assume: n0 / n1 satisfy add-expr?
(define (add-expr-equal? n0 n1)
  (define (add-expr->num e)
    (match e
      [0 0]
      [1 1]
      [`(+ ,e0 ,e1) (+ (add-expr->num e0) (add-expr->num e1))]))
  (equal? (add-expr->num n0) (add-expr->num n1)))

This section was more advanced–let’s switch back to using algebra to do programming.

Folding over lists (foldr)

We are now ready to use some of the algebra we have developed in this lecture to develop a very special function, foldr, which is defined via the following equations:

(fold-1)   (foldr f z '()) = z
(fold-2)   (foldr f z (cons hd tl)) = (f hd (foldr f z tl))

(foldr f z l) “folds” the function f across the list l with the initial value (“zero”) z. By “fold” f across the list, I actually mean “iterate” or “accumulate.” It will make more sense once we see an example:

;; (foldr + 0 '(1 2 3)) => 6
;; (foldr + 3 '(1 2 3)) => 9
;; (foldr * 1 '(2 3 4)) => 24

Fold’s second argument is a “folder” or “updater” function, which takes two inputs:

  • The next element in the list being inspected.
  • The current “accumulator” value.

In the case of foldr (fold right), the folder / updater function is applied from right to left, and the initial accumulator value is z (the second argument, “zero”–a sensible default value).

(define (foldr f z l)
  (match l
    ['() z]
    [`(,hd ,tl ...) (f hd (foldr f z tl))]))

Equational reasoning example

Let’s use equational reasoning to show that (foldr + 0 '(1 2 3)) = 6:

(foldr + 0 '(1 2 3)) = (foldr + 0 (cons 1 (cons 2 (cons 3 '()))))
                     = (+ 1 (foldr + 0 (cons 2 (cons 3 '())))) (via fold-2)
                     = (+ 1 (+ 2 (foldr + 0 (cons 3 '()))))    (via fold-2)
                     = (+ 1 (+ 2 (+ 3 (foldr + 0 '()))))       (via fold-2)
                     = (+ 1 (+ 2 (+ 3 0)))                     (via fold-1)
                     = (+ 1 (+ 2 3))
                     = (+ 1 5)
                     = 6

QuickAnswer

Using the standard rules of arithmetic for *, +, etc., and also the two rules:

(fold-1)   (foldr f z '()) = z
(fold-2)   (foldr f z (cons hd tl)) = (f hd (foldr f z tl))

Rigorously prove–via a series of equalities (annotate fold-1/2 when appropriate)–the following:

(foldr * 1 '(2 3 4)) = 24

The identity: l = (foldr cons '() l)

As a more advanced example of how we might use algebra for programming, I want to pose the following equality:

forall l. l = (foldr cons '() l)

Why is this the case intuitively?

Pictorially, here is what (foldr f z l) is doing:

(cons x0 (cons x1 (cons x2 ... (cons xn-1 '()) ...)))
  |       |        |           |          | '() maps to z
  v       v        v           v          v
( f   x0 ( f   x1 ( f   x2 ... (f    xn-1  z) ) ) )

Notice how the fold transforms the list, effectively replacing each cons with a call to f, and the empty list '() by the zero (initial value) z.

Now, back to our original claim: forall l. l = (foldr cons '() l)

Pictorially, this is true because…

  (cons x0 (cons x1 (cons x2 ... (cons xn-1 '()) ...)))
    |       |        |           |          |
    v       v        v           v          v
  (cons x0 (cons x1 (cons x2 ... (cons xn-1 '()) ...)))

ADVANCED (optional): However, this picture is not a rigorous proof. To make a rigorous proof, we would do induction over the list l, establishing an inductive hypothesis that for all sublists xs of (cons x xs), xs = (foldr cons '() xs), and we would prove that (cons x xs) = (foldr cons '() (cons x xs)) by using (fold-2) and the induction hypothesis.

We will see this later on, when we look at using Lean.

The power of fold

It is easy to miss the power of this idea, or see it as abstract pedantic nonsense. In fact, foldr characterizes an extremely common class of functions that process lists by accumulating a result, walking over the list in some order (right to left, as in foldr, or left to right as in foldl).

Foldr gives us a general-purpose way to transform lists by walking over each element one at a time and firing a two-argument “updater” function, which takes (a) the next value in the list, and (b) the current accumulator value (which defaults to “zero”, foldr’s third argument).

For example, we can define the function (filter f l) via foldr:

(define (filter f l)
  (foldr (lambda (next-elt acc) (if (f next-elt) (cons next-elt acc) acc))
         '()
         l))

QuickAnswer

Use foldr to add all even numbers in the list l:

;; (add-evens '(0 1 2 3 4 5)) => 6
(define (add-evens l)
  (foldr (lambda (x acc) 'todo)
         0
         l))

Fold in other languages

Fold is a pervasive construct, popular across many languages. For example:

Rust:

let sum = vec![1, 2, 3, 4].iter().fold(0, |acc, x| acc + x);

Python:

sum = reduce(lambda acc, x: acc + x, [1, 2, 3, 4], 0)

JavaScript:

const sum = [1, 2, 3, 4].reduce((acc, x) => acc + x, 0);

C++:

std::vector<int> v = {1, 2, 3, 4};
int sum = std::accumulate(v.begin(), v.end(), 0);

SQL:

SELECT SUM(x)
FROM (VALUES (1), (2), (3), (4)) AS t(x)

Fold is so popular because it represents the following imperative construct:

acc = 0
for (elt in list.reverse) { acc = f(elt,acc); }

In practice, almost any function over lists can be written using fold.

Also, fold forms the basis for MapReduce, a popular distributed / parallel computing framework: https://www.ibm.com/think/topics/mapreduce

QuickAnswer

What is the result of…

(foldr (lambda (x acc) (+ acc (- x))) 0 '(10 10 10))

Optional: Using algebra for proving correctness of code

We will prove: for all l, (filter (lambda (x) #t) l) = l

Proof:

First, we show that:

(lambda (next-elt acc) (if ((lambda (x) #t) next-elt) (cons next-elt acc) acc))
=
cons

Proving this equality is actually a bit tricky, because we have not talked about lambdas, but notice that (lambda (x) #t) will always return true, and thus the guard is always true. Thus–because the guard is always true–the function is really equal to…

(lambda (next-elt acc) (cons next-elt acc))

This is almost cons, and it is in fact equal to cons, in the sense that the above lambda does the same things to the same arguments (i.e., the function is extensionally equal). We will see that they are related via a concept named η-expansion in the λ-calculus.

Summary

Key concepts from this lecture:

  • A “term algebra” is an infinite set of terms (all individually finite), each of which is formed via the application of constructors according to some signature T (constructors and their arities).

  • Racket’s lists (“S-expressions”) naturally represent term algebras in prefix form, and it is easy to express term algebras via Racket type predicates using pattern matching.

  • Term algebras are all finite trees, and thus syntactic equality is dictated by structural equality (i.e., equal? in Racket!).

  • It is sometimes desirable to extend term algebras with a set of equations. These equations partition the term algebra into equivalence classes, and form a quotient algebra–however, deciding equality of terms in an arbitrary quotient algebra is not possible (undecidable) in general via any algorithm. Instead, we must manually demonstrate a “proof,” via a chain of reasoning steps.

  • Algebra gives us a very powerful tool to reason about equality of programs by transitive term rewriting–each equality in the chain follows from some equation in the system.

  • Folding over lists is a fundamental looping construct, which allows us to “fold” an “updater” or “folder” function across a list, walking over it from right to left (hence foldr) and starting with some initial accumulator zero.

  • Folds can be used for a wide range of list-processing tasks, we will begin to use them more frequently throughout class.