algebra.rkt

#lang racket

;; CIS352 -- The Algebra of Programming
;; Spring 2026 -- Kristopher Micinski

;; 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* using 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 (equal? n1 0)
;; - 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?, and 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 3
;; 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 z 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))]))

;; 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
'todo-write-proof-in-comments

;; 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?
;; 
;; Pictorally, 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)
;; 
;; Pictorally, 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 (foldr-2)
;; and the induction hypothesis. 
;; 
;; We will see this later on, when we look at using Lean.

;; 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 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 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 fold*r*) 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.