Pattern Matching: From Rule Induction to Functional Programming

The Connection

Rule induction in discrete maths and pattern matching in functional programming (OCaml, Haskell) are deeply connected. Both deal with inductively defined structures and recursive processing.

---

Recap: Inductive Definitions

A set defined inductively specifies:

• Axioms: base elements
• Rules: ways to construct new elements from existing ones

Example: Arithmetic Expressions

$E ::= \text{Num}(n) \mid \text{Add}(E, E) \mid \text{Mul}(E, E)$

The set of expressions includes:

• $\text{Num}(5)$
• $\text{Add}(\text{Num}(3), \text{Num}(7))$
• $\text{Mul}(\text{Add}(\text{Num}(1), \text{Num}(2)), \text{Num}(3))$

---

Abstract Syntax Trees

Concrete Syntax

The textual representation: 1 + 2 * 3

Abstract Syntax Tree (AST)

The tree structure:

      Add
     /   \
  Num(1)  Mul
         /   \
      Num(2) Num(3)

OCaml Data Type

The BNF grammar translates directly to an algebraic data type:

type expr =
  | Num of int
  | Add of expr * expr
  | Mul of expr * expr

Each constructor corresponds to a rule in the inductive definition.

---

Rule Induction Recap

The Principle

To prove a property $P(e)$ holds for all expressions $e$:

1. Base case (axioms): Prove $P(\text{Num}(n))$ for all $n$
2. Inductive step (rules): Assuming $P(e_1)$ and $P(e_2)$, prove $P(\text{Add}(e_1, e_2))$ and $P(\text{Mul}(e_1, e_2))$

Example: All Expressions Have Non-negative Size

Define $\text{size}(e)$ as the number of constructors:

$\text{size}(\text{Num}(n)) = 1$ $\text{size}(\text{Add}(e_1, e_2)) = 1 + \text{size}(e_1) + \text{size}(e_2)$ $\text{size}(\text{Mul}(e_1, e_2)) = 1 + \text{size}(e_1) + \text{size}(e_2)$

By rule induction: $\text{size}(e) \geq 1$ for all $e$.

---

Pattern Matching in OCaml

The Core Idea

A match expression examines the structure of data and:

1. Identifies which constructor was used
2. Extracts (binds) the sub-components to variables

Evaluating Expressions

let rec eval (e : expr) : int =
  match e with
  | Num n -> n
  | Add (e1, e2) -> eval e1 + eval e2
  | Mul (e1, e2) -> eval e1 * eval e2

Correspondence to Rule Induction

Pattern match branch	Rule induction step
`	Num n -> …`
`	Add (e1, e2) -> …`
`	Mul (e1, e2) -> …`

The recursive calls eval e1 and eval e2 apply the function to the sub-expressions, exactly as rule induction applies the hypothesis to premises.

---

Variable Binding

The Mechanism

When pattern matching encounters:

| Add (e1, e2) -> ...

and the input is Add (Num 3, Num 7):

1. The constructor Add matches
2. e1 is bound to Num 3
3. e2 is bound to Num 7
4. The right-hand side executes with these bindings

---

Exhaustiveness Checking

The Compiler’s Job

The OCaml compiler checks that a match covers ALL constructors.

let rec eval (e : expr) : int =
  match e with
  | Num n -> n
  | Add (e1, e2) -> eval e1 + eval e2
(* Warning: this pattern-matching is not exhaustive. *)

The compiler warns that Mul is missing.

Why This Works

Because the data type was inductively defined with a fixed set of constructors, the compiler knows exactly what patterns are possible.

Mathematical Connection

Exhaustiveness checking is the compiler verifying that your proof covers all axioms and rules!

---

Structural Recursion

Definition

A function is structurally recursive if:

• Each recursive call is on a proper sub-structure of the input
• There is a base case for each axiom

This guarantees termination.

Example: Size Function

let rec size (e : expr) : int =
  match e with
  | Num _ -> 1
  | Add (e1, e2) -> 1 + size e1 + size e2
  | Mul (e1, e2) -> 1 + size e1 + size e2

The recursion follows the tree structure:

• Base case: Num _ has size 1
• Recursive calls on e1 and e2 are on smaller sub-trees

Termination

Since the AST has finite depth, structural recursion always terminates.

---

Example: Pretty Printing

Convert an AST back to a string:

let rec pretty (e : expr) : string =
  match e with
  | Num n -> string_of_int n
  | Add (e1, e2) -> 
      "(" ^ pretty e1 ^ " + " ^ pretty e2 ^ ")"
  | Mul (e1, e2) ->
      "(" ^ pretty e1 ^ " * " ^ pretty e2 ^ ")"

Pattern: recurse on sub-expressions, combine results.

---

Example: Optimisation

Simplify expressions (constant folding):

let rec simplify (e : expr) : expr =
  match e with
  | Num n -> Num n
  | Add (e1, e2) ->
      (match simplify e1, simplify e2 with
       | Num 0, e -> e          (* 0 + e = e *)
       | e, Num 0 -> e          (* e + 0 = e *)
       | Num n1, Num n2 -> Num (n1 + n2)  (* fold *)
       | e1', e2' -> Add (e1', e2'))
  | Mul (e1, e2) ->
      (match simplify e1, simplify e2 with
       | Num 0, _ -> Num 0
       | _, Num 0 -> Num 0
       | Num 1, e -> e
       | e, Num 1 -> e
       | Num n1, Num n2 -> Num (n1 * n2)
       | e1', e2' -> Mul (e1', e2'))

---

Lists: Another Inductive Structure

Definition

$\text{List}(A) ::= \text{Nil} \mid \text{Cons}(A, \text{List}(A))$

OCaml Type

type 'a list =
  | []
  | (::) of 'a * 'a list

Pattern Matching

let rec length (lst : 'a list) : int =
  match lst with
  | [] -> 0
  | _ :: xs -> 1 + length xs

Base case: empty list. Inductive step: head + tail.

---

Summary

Discrete Maths	Functional Programming
Inductive definition	Algebraic data type
Axiom	Constructor (e.g., Num)
Rule	Constructor with arguments (e.g., Add)
Rule induction proof	Recursive function
Base case	Base case pattern
Inductive hypothesis	Recursive call
Variable in rule	Pattern variable
Exhaustive cases?	Exhaustiveness check

Pattern matching is executable rule induction: the compiler verifies your proof structure, and the machine executes the computation.

---

Tripos Questions

2021 P1 Q4: Explain how pattern matching in functional programming relates to proof by rule induction.

Paper 1 FOCS: Implement a recursive function to compute the depth of an expression tree.