Function machines in sequence

Lens

MotivationH

Thirty degrees in Accra

Kofi lives in Accra, where the afternoon temperature is $30\,^\circ\mathrm{C}$ . His cousin Maya in Chicago uses the Fahrenheit scale, so Kofi converts with the rule his teacher gave him: multiply by $1.8$ , then add $32$ .

30 \xrightarrow{\ \times 1.8\ } 54 \xrightarrow{\ +32\ } 86.

So it is $86\,^\circ\mathrm{F}$ . Maya wants to check, so she converts back. She subtracts $32$ to get $54$ , then divides by $1.8$ to get $30$ . Perfect. But her friend Sam tries “divide by $1.8$ , then subtract $32$ ” and gets

86 \div 1.8 - 32 \approx 47.8 - 32 = 15.8.

Sam used exactly the right two undoing steps — just in the wrong order — and got the wrong answer. This lesson explains why, and what “doing one thing after another” really means for functions.

IntuitionH

Machines, tables and arrows

Think of a function as a machine: put an input in, and exactly one output comes out (see functions). Two machines can be placed in a row, so that whatever comes out of the first goes straight into the second. The whole row is a new machine.

The same chain can be shown with arrow diagrams. Here the first function sends each person to their home city, and the second sends each city to its continent. Following two arrows in a row sends each person to a continent.

Two functions in sequence. Following an arrow from a person to their home city, and then an arrow from the city to its continent, defines a new function from people to continents.

DefinitionsH

Definitions

Definition— applying f, then g

Let $f : A \to B$ and $g : B \to C$ be functions. Applying $f$ , then $g$ sends each $a \in A$ to

g\big(f(a)\big) \in C.

This defines a new function from $A$ to $C$ . Read $g(f(a))$ from the inside out: first work out $f(a)$ , then feed the result to $g$ .

The chain only makes sense if every output of $f$ is an allowed input of $g$ . If $g$ is only defined on some set $B'$ , the chain “ $f$ , then $g$ ” exists exactly when every value $f(a)$ lies in $B'$ .

Definition— identity function

For any set $A$ , the identity function $\mathrm{id}_A : A \to A$ is defined by $\mathrm{id}_A(a) = a$ . It returns every input unchanged — a machine that does nothing.

Definition— undoing and inverse functions

A function $g : B \to A$ undoes $f : A \to B$ if

g\big(f(a)\big) = a \quad \text{for every } a \in A.

If $g$ undoes $f$ and $f$ undoes $g$ , then $f$ and $g$ are inverse functions of each other, and we write $g = f^{-1}$ .

Note

In the next lesson, on composition, “ $f$ , then $g$ ” gets its own symbol, $g \circ f$ , read “ $g$ after $f$ ”. The order in the symbol matches the order in $g(f(a))$ : the function written nearest to $a$ acts first.

Worked examplesH

Worked examples

Example— Chaining tables

With the functions from the arrow diagram:

person	home city	continent
Amina	Kano	Africa
Bo	Chengdu	Asia
Carlos	Lima	South America
Dilnoza	Tashkent	Asia

The chain “home city, then continent” sends Amina to Africa, Bo and Dilnoza to Asia, and Carlos to South America. Notice that Bo and Dilnoza have different home cities but end up in the same continent: a chain can combine outputs that were separate after the first step.

Example— Chaining formulas — and the order matters

Let $f(x) = x + 3$ and $g(x) = 2x$ , both on the integers.

“ $f$ , then $g$ ”: $\;x \mapsto g(x + 3) = 2(x + 3) = 2x + 6$ .
“ $g$ , then $f$ ”: $\;x \mapsto f(2x) = 2x + 3$ .

These never agree: $2x + 6$ and $2x + 3$ always differ by $3$ . With a third step, “add $3$ , then double, then subtract $6$ ” sends $x$ to $2(x + 3) - 6 = 2x$ : the long chain is just doubling.

Example— A chain that cannot be formed

Let $f(x) = x - 2$ on the rational numbers $\Q$ , and let $g(x) = \tfrac{1}{x}$ , which is defined only for $x \neq 0$ . The chain “ $f$ , then $g$ ” would send $x$ to $\tfrac{1}{x - 2}$ — but at $x = 2$ the output of $f$ is $0$ , which $g$ does not accept. So the chain is a function on $\Q$ without $2$ , not on all of $\Q$ .

Example— Undoing

“Subtract $3$ ” undoes “add $3$ ”, and “add $3$ ” undoes “subtract $3$ ”: they are inverses.
On $\Q$ , “halve” undoes “double”, and “double” undoes “halve”: $\tfrac{2x}{2} = x$ and $2 \cdot \tfrac{x}{2} = x$ .
On $\Z$ , “square” cannot be undone: $2^2 = 4$ and $(-2)^2 = 4$ , so a function undoing it would have to send $4$ back to both $2$ and $-2$ .

Example— Undoing the temperature conversion

“Celsius to Fahrenheit” is the chain “multiply by $\tfrac{9}{5}$ , then add $32$ ” (and $\tfrac{9}{5} = 1.8$ ). Its undoing steps are “divide by $\tfrac{9}{5}$ ” (that is, multiply by $\tfrac{5}{9}$ ) and “subtract $32$ ”, and they must be done in reverse order:

F \;\longmapsto\; \tfrac{5}{9}\,(F - 32).

At $F = 86$ this gives $\tfrac{5}{9} \cdot 54 = 30$ . Sam's order gives $\tfrac{5}{9} \cdot 86 - 32 = \tfrac{142}{9} \approx 15.8$ .

ProofH

The rules of chaining and undoing

Theorem— Theorem 1 (doing nothing changes nothing)

For every function $f : A \to B$ : “ $\mathrm{id}_A$ , then $f$ ” is $f$ , and “ $f$ , then $\mathrm{id}_B$ ” is $f$ .

Proof

Two functions are equal when they give the same output for every input. For each $a \in A$ : “ $\mathrm{id}_A$ , then $f$ ” gives $f(\mathrm{id}_A(a)) = f(a)$ , and “ $f$ , then $\mathrm{id}_B$ ” gives $\mathrm{id}_B(f(a)) = f(a)$ .

∎

Theorem— Theorem 2 (when can adding and multiplying be swapped?)

Let $a$ and $m$ be integers. “Add $a$ , then multiply by $m$ ” and “multiply by $m$ , then add $a$ ” are the same function on $\Z$ exactly when $a = 0$ or $m = 1$ .

Proof

The first chain sends $x$ to $m(x + a) = mx + ma$ ; the second sends $x$ to $mx + a$ .

If $a = 0$ , both are $x \mapsto mx$ . If $m = 1$ , both are $x \mapsto x + a$ . So in these cases the chains agree.

Conversely, suppose the chains agree for every $x$ . At $x = 0$ this says $ma = a$ , so $(m - 1)a = 0$ . A product of two integers is $0$ only if one of them is $0$ , so $m = 1$ or $a = 0$ .

∎

So for most choices the order matters — Kofi's “multiply by $1.8$ , then add $32$ ” is not the same as “add $32$ , then multiply by $1.8$ ”.

Theorem— Theorem 3 (socks and shoes)

Suppose $f : A \to B$ is undone by $f' : B \to A$ , and $g : B \to C$ is undone by $g' : C \to B$ . Then “ $f$ , then $g$ ” is undone by “ $g'$ , then $f'$ ”.

Proof

Take any $a \in A$ . Doing $f$ , then $g$ , then $g'$ , then $f'$ gives

f'\Big(g'\big(g(f(a))\big)\Big) = f'\big(f(a)\big) = a.

The first step uses that $g'$ undoes $g$ (applied to the input $f(a)$ ), and the second that $f'$ undoes $f$ .

∎

The proof shows why the order is forced: $g'$ can only cancel $g$ if it comes directly after it. In Sam's order, “divide by $1.8$ ” arrives while the $+32$ is still in the way.

Theorem— Theorem 4 (undoable functions keep inputs apart)

If some function $g$ undoes $f$ , then $f$ never sends two different inputs to the same output: whenever $f(a) = f(b)$ , we have $a = b$ .

Proof

Suppose $f(a) = f(b)$ . Apply $g$ to both sides: $g(f(a)) = g(f(b))$ . Since $g$ undoes $f$ , the left side is $a$ and the right side is $b$ . So $a = b$ .

∎

In the language of the functions lesson, a function that can be undone is injective. Squaring on $\Z$ is not injective ( $2^2 = (-2)^2$ ), so by Theorem 4 nothing can undo it. Conversely, an injective function on a non-empty set can always be undone: send each output back to the input it came from, and send everything that is never an output anywhere you like.

Note

Undoing is not quite the same as being an inverse. On $\Z$ , “halve and round down” undoes “double”, because $\tfrac{2x}{2} = x$ . But “double” does not undo “halve and round down”: $1$ is halved to $0$ , and doubling gives $0$ , not $1$ . In fact doubling has no inverse function $\Z \to \Z$ at all, because odd numbers are never outputs, so nothing could be sent back to them. On $\Q$ , doubling and halving are true inverses. A function has an inverse function exactly when it is a bijection — injective and surjective.

Formal mathematicsF

Chains and undoing in Lean

In Lean we write the chain “ $f$ , then $g$ ” as andThen f g. Lean only allows it when the output type of f is the input type of g, so the rule “every output must be an allowed input” is checked automatically.

andThenLean 4Formally verified

/-- "Do `f`, then `g`": the function that sends `a` to `g (f a)`. It can only be formed when the
outputs of `f` (of type `β`) are inputs that `g` accepts. -/
def andThen {α β γ : Type} (f : α → β) (g : β → γ) : α → γ := fun a => g (f a)

Axioms used: No axiomsformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

Lean's own library writes the same function as g ∘ f; the two agree by definition:

and_then_eq_compLean 4Proved here from basic factsFormally verified

/-- Our `andThen f g` is the function Lean's library writes `g ∘ f`, read "`g` after `f`".
They agree by definition, so `rfl` proves it. -/
theorem and_then_eq_comp {α β γ : Type} (f : α → β) (g : β → γ) : andThen f g = g ∘ f := rfl

Axioms used: No axiomsformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

Computing chains, and seeing that the order matters:

add_then_doubleLean 4Proved here from basic factsFormally verified

/-- "Add 3, then double" sends `x` to `2(x + 3) = 2x + 6`. -/
theorem add_then_double (x : Int) : andThen (fun n => n + 3) (fun n => 2 * n) x = 2 * x + 6 := by
  show 2 * (x + 3) = 2 * x + 6
  omega

Axioms used: propext, Quot.soundformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

double_then_addLean 4Proved here from basic factsFormally verified

/-- "Double, then add 3" sends `x` to `2x + 3`. -/
theorem double_then_add (x : Int) : andThen (fun n => 2 * n) (fun n => n + 3) x = 2 * x + 3 := by
  show 2 * x + 3 = 2 * x + 3
  rfl

Axioms used: No axiomsformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

order_mattersLean 4Proved here from basic factsFormally verified

/-- **Order matters**: "add 3, then double" and "double, then add 3" are different functions.
One input is enough to tell them apart: at `0` they give `6` and `3`. -/
theorem order_matters :
    andThen (fun n : Int => n + 3) (fun n => 2 * n) ≠ andThen (fun n : Int => 2 * n) (fun n => n + 3) := by
  intro h
  have h0 := congrFun h 0
  rw [add_then_double, double_then_add] at h0
  omega

Axioms used: propext, Quot.soundformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

add_mul_swap_iffLean 4Proved here from basic factsFormally verified

/-- **When can "add `a`" and "multiply by `m`" be swapped?** "Add `a`, then multiply by `m`" gives
`m(x + a) = mx + ma`, while "multiply by `m`, then add `a`" gives `mx + a`. They agree for every
`x` exactly when `ma = a`, that is, when `a = 0` or `m = 1`. -/
theorem add_mul_swap_iff (a m : Int) :
    (∀ x, andThen (fun n => n + a) (fun n => m * n) x = andThen (fun n => m * n) (fun n => n + a) x)
      ↔ a = 0 ∨ m = 1 := by
  constructor
  · intro h
    -- At `x = 0` the two chains give `m · a` and `a`.
    have h0 : m * (0 + a) = m * 0 + a := h 0
    have hma : (m - 1) * a = 0 := by
      rw [Int.sub_mul, Int.one_mul]
      rw [Int.zero_add, Int.mul_zero, Int.zero_add] at h0
      omega
    cases Int.mul_eq_zero.mp hma with
    | inl hm => exact Or.inr (by omega)
    | inr ha => exact Or.inl ha
  · intro h x
    show m * (x + a) = m * x + a
    cases h with
    | inl ha => rw [ha, Int.add_zero, Int.add_zero]
    | inr hm => rw [hm, Int.one_mul, Int.one_mul]

Axioms used: propext, Quot.soundformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

The identity laws are true “by definition”: Lean accepts rfl, which means both sides compute to literally the same function.

id_and_thenLean 4Proved here from basic factsFormally verified

/-- Doing nothing first changes nothing: "identity, then `f`" is `f`. -/
theorem id_and_then {α β : Type} (f : α → β) : andThen id f = f := rfl

Axioms used: No axiomsformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

and_then_idLean 4Proved here from basic factsFormally verified

/-- Doing nothing afterwards changes nothing: "`f`, then identity" is `f`. -/
theorem and_then_id {α β : Type} (f : α → β) : andThen f id = f := rfl

Axioms used: No axiomsformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

Undoing, and some examples on $\Z$ and $\Q$ (core Lean's Rat is the rational numbers):

UndoesLean 4Formally verified

/-- `g` **undoes** `f` if doing `f` and then `g` always gives back the input: `g (f a) = a`. -/
def Undoes {α β : Type} (g : β → α) (f : α → β) : Prop := ∀ a, g (f a) = a

Axioms used: No axiomsformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

sub_undoes_addLean 4Proved here from basic factsFormally verified

/-- "Subtract 3" undoes "add 3" … -/
theorem sub_undoes_add : Undoes (fun x : Int => x - 3) (fun x => x + 3) := by
  intro a
  show a + 3 - 3 = a
  omega

Axioms used: propext, Quot.soundformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

add_undoes_subLean 4Proved here from basic factsFormally verified

/-- … and "add 3" undoes "subtract 3". Each undoes the other: they are **inverse** functions. -/
theorem add_undoes_sub : Undoes (fun x : Int => x + 3) (fun x => x - 3) := by
  intro a
  show a - 3 + 3 = a
  omega

Axioms used: propext, Quot.soundformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

halve_undoes_doubleLean 4Proved here from basic factsFormally verified

/-- On the rational numbers, "halve" undoes "double" and "double" undoes "halve": `x ↦ 2x` and
`x ↦ x / 2` are inverse functions of `ℚ`. -/
theorem halve_undoes_double :
    Undoes (fun x : Rat => x / 2) (fun x => 2 * x) ∧ Undoes (fun x : Rat => 2 * x) (fun x => x / 2) := by
  constructor
  · intro a
    show 2 * a / 2 = a
    grind
  · intro a
    show 2 * (a / 2) = a
    grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

int_halve_undoes_doubleLean 4Applies a library theoremFormally verified

/-- On the integers, halving *with rounding down* (Lean's `y / 2`) still undoes doubling:
`(2x) / 2 = x`. This applies core Lean's `Int.mul_ediv_cancel_left`. -/
theorem int_halve_undoes_double : Undoes (fun y : Int => y / 2) (fun x => 2 * x) :=
  fun x => Int.mul_ediv_cancel_left x (by decide)

Axioms used: propextformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

int_double_not_undoes_halveLean 4Proved here from basic factsFormally verified

/-- … but on the integers doubling does **not** undo halving: `1` is halved (rounding down) to
`0`, and doubling `0` gives `0`, not `1`. So `x ↦ 2x` has no inverse function `ℤ → ℤ`: odd
numbers are never outputs, so nothing can be sent back to them. -/
theorem int_double_not_undoes_halve : ¬ Undoes (fun x : Int => 2 * x) (fun y => y / 2) := by
  intro h
  have h1 : 2 * (1 / 2 : Int) = 1 := h 1
  exact absurd h1 (by decide)

Axioms used: No axiomsformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

undo_chainLean 4Proved here from basic factsFormally verified

/-- **Socks and shoes.** If `f'` undoes `f` and `g'` undoes `g`, then "`f`, then `g`" is undone by
"`g'`, then `f'`": undo the **last** step **first**. The calculation:
`f' (g' (g (f a))) = f' (f a) = a`. -/
theorem undo_chain {α β γ : Type} {f : α → β} {g : β → γ} {f' : β → α} {g' : γ → β}
    (hf : Undoes f' f) (hg : Undoes g' g) : Undoes (andThen g' f') (andThen f g) := by
  intro a
  calc andThen g' f' (andThen f g a) = f' (g' (g (f a))) := rfl
    _ = f' (f a) := by rw [hg (f a)]
    _ = a := hf a

Axioms used: No axiomsformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

toFahrenheitLean 4Formally verified

/-- Celsius to Fahrenheit: multiply by `9/5`, then add `32`. -/
def toFahrenheit : Rat → Rat := andThen (fun c => 9 / 5 * c) (fun x => x + 32)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

toCelsiusLean 4Formally verified

/-- Fahrenheit to Celsius: subtract `32`, then multiply by `5/9` — the undoing steps, in reverse
order. -/
def toCelsius : Rat → Rat := andThen (fun f => f - 32) (fun x => 5 / 9 * x)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

thirty_degreesLean 4Proved here from basic factsFormally verified

/-- A warm day: `30 °C` is `86 °F`, and converting back gives `30 °C` again. Lean checks the
fraction arithmetic exactly (`decide +kernel` evaluates both sides). -/
theorem thirty_degrees : toFahrenheit 30 = 86 ∧ toCelsius 86 = 30 := by
  decide +kernel

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

to_celsius_undoesLean 4Proved here from basic factsFormally verified

/-- `toCelsius` undoes `toFahrenheit` for **every** temperature. This is the socks-and-shoes rule
`undo_chain` applied to the two steps: `× 5/9` undoes `× 9/5`, and `− 32` undoes `+ 32`. -/
theorem to_celsius_undoes : Undoes toCelsius toFahrenheit := by
  apply undo_chain
  · intro c
    show 5 / 9 * (9 / 5 * c) = c
    grind
  · intro x
    show x + 32 - 32 = x
    grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

wrong_order_failsLean 4Proved here from basic factsFormally verified

/-- Undoing the steps in the **wrong** order fails: "multiply by `5/9`, then subtract `32`" does
not undo `toFahrenheit`. At `0 °C`: `toFahrenheit 0 = 32`, and `5/9 · 32 − 32 = −128/9 ≠ 0`. -/
theorem wrong_order_fails :
    ¬ Undoes (andThen (fun x : Rat => 5 / 9 * x) (fun x => x - 32)) toFahrenheit := by
  intro h
  have h0 := h 0
  revert h0
  decide +kernel

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

Finally, Theorem 4 and its consequence for squaring:

injective_of_undoesLean 4Proved here from basic factsFormally verified

/-- If `f` can be undone, then different inputs always give different outputs: from
`f a = f b`, apply the undoing function `g` to both sides to get `a = g (f a) = g (f b) = b`. -/
theorem injective_of_undoes {α β : Type} {f : α → β} {g : β → α} (h : Undoes g f) (a b : α)
    (hab : f a = f b) : a = b :=
  calc a = g (f a) := (h a).symm
    _ = g (f b) := by rw [hab]
    _ = b := h b

Axioms used: No axiomsformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

Core Lean's library already knows Theorem 4, under the names Function.LeftInverse (for “undoes”) and Function.Injective; this version just applies it:

injective_of_undoes_libraryLean 4Applies a library theoremFormally verified

/-- The same fact from core Lean's library, where "`g` undoes `f`" is called
`Function.LeftInverse g f` (it is defined exactly like our `Undoes g f`) and "never sends two
inputs to the same output" is `Function.Injective f`. This applies
`Function.LeftInverse.injective`. -/
theorem injective_of_undoes_library {α β : Type} {f : α → β} {g : β → α} (h : Undoes g f) :
    Function.Injective f :=
  Function.LeftInverse.injective h

Axioms used: No axiomsformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

square_cannot_be_undoneLean 4Proved here from basic factsFormally verified

/-- **Squaring on ℤ cannot be undone**: `2² = (−2)² = 4`, so an undoing function would have to
send `4` back to both `2` and `−2`. -/
theorem square_cannot_be_undone : ¬ ∃ g : Int → Int, Undoes g (fun x => x * x) := by
  intro ⟨g, hg⟩
  have h : (2 : Int) = -2 := injective_of_undoes hg 2 (-2) (by decide)
  exact absurd h (by decide)

Axioms used: No axiomsformal/Lumenary/ChainingFunctions.leanTry it in the Lean web editor

What is formalised: every theorem of the proof section and every example above, using core Lean only. The small arithmetic steps are finished by tactics: omega for whole-number arithmetic, grind for rearranging fractions, and decide +kernel, which makes Lean's trusted kernel evaluate exact fraction arithmetic such as $\tfrac{9}{5} \cdot 30 + 32 = 86$ . Mathlib, Lean's large mathematical library, builds on the same names: it proves, for instance, that a function has an inverse exactly when it is a bijection (Function.bijective_iff_has_inverse).

ComputationC

Chaining tables by computer

Chaining tables, and undoing chains in the right orderPythonExact computationExhaustive finite checkComputationally tested

"""Chaining functions given by tables, and undoing chains in the right order.

Functions on finite sets are stored as Python dictionaries, so "f, then g"
is computed by looking up g[f[a]]. The experiment chains two tables, then
runs through all 27 functions from {0, 1, 2} to itself: it checks the
identity laws, finds which functions can be undone (exactly the 6 that never
send two inputs to the same output), and tests the "socks and shoes" rule
for undoing a chain on every pair of them - and how often undoing in the
WRONG order happens to work. Last, it converts temperatures exactly with
fractions. Exact, exhaustive-finite evidence.
"""

from fractions import Fraction
from itertools import product

def then(f, g):
    """The table of 'f, then g': a -> g[f[a]]. Every output of f must be an
    input of g, otherwise the chain is not defined."""
    missing = [b for b in f.values() if b not in g]
    if missing:
        raise ValueError(f"outputs {missing} are not inputs of the second table")
    return {a: g[f[a]] for a in f}

def identity(elements):
    """The identity function on a finite set, as a table."""
    return {a: a for a in elements}

def undoes(g, f):
    """True when g undoes f: g[f[a]] == a for every input a of f."""
    return all(f[a] in g and g[f[a]] == a for a in f)

def all_functions(elements):
    """Every function from the finite set to itself (n**n of them)."""
    elements = list(elements)
    for outputs in product(elements, repeat=len(elements)):
        yield dict(zip(elements, outputs))

def undoing_function(f, elements):
    """A function g on `elements` that undoes f, or None if there is none."""
    for g in all_functions(elements):
        if undoes(g, f):
            return g
    return None

def to_fahrenheit(c):
    """Multiply by 9/5, then add 32."""
    return Fraction(9, 5) * c + 32

def to_celsius(f):
    """Subtract 32, then multiply by 5/9: the undo steps in reverse order."""
    return Fraction(5, 9) * (f - 32)

def wrong_undo(f):
    """Multiply by 5/9, then subtract 32: the undo steps in the wrong order."""
    return Fraction(5, 9) * f - 32

HOME_CITY = {"Amina": "Kano", "Bo": "Chengdu", "Carlos": "Lima",
             "Dilnoza": "Tashkent", "Emma": "Oslo"}
CONTINENT = {"Kano": "Africa", "Chengdu": "Asia", "Lima": "South America",
             "Tashkent": "Asia", "Oslo": "Europe", "Perth": "Oceania"}

def main():
    print("1. Two tables in sequence: home city, then continent")
    for person, place in then(HOME_CITY, CONTINENT).items():
        print(f"   {person:<8} -> {HOME_CITY[person]:<9} -> {place}")
    print()
    elems = [0, 1, 2]
    funcs = list(all_functions(elems))
    ident = identity(elems)
    ok = all(then(ident, f) == f and then(f, ident) == f for f in funcs)
    print(f"2. All {len(funcs)} functions from {{0, 1, 2}} to itself")
    print("   identity, then f == f == f, then identity, for all f:", ok)
    pairs = sum(then(f, g) == then(g, f) for f in funcs for g in funcs)
    print(f"   pairs (f, g) where the order does not matter: {pairs} of 729")
    undo = [(f, undoing_function(f, elems)) for f in funcs]
    undo = [(f, u) for f, u in undo if u is not None]
    print(f"   functions that can be undone: {len(undo)}")
    right, wrong, swap = 0, set(), set()
    for (i, (f, uf)), (j, (g, ug)) in product(enumerate(undo), repeat=2):
        right += undoes(then(ug, uf), then(f, g))
        if undoes(then(uf, ug), then(f, g)):
            wrong.add((i, j))
        if then(f, g) == then(g, f):
            swap.add((i, j))
    total = len(undo) ** 2
    print(f"   'f, then g' undone by 'undo g, then undo f': {right} of {total}")
    print(f"   undone by 'undo f, then undo g' (wrong order): {len(wrong)} of {total}")
    print(f"   ... and those {len(wrong)} are exactly the pairs where f and g")
    print(f"   can be swapped: {wrong == swap}")
    print()
    print("3. Temperatures, with exact fractions")
    f = to_fahrenheit(30)
    print(f"   30 C -> {f} F -> back: {to_celsius(f)} C (right order)")
    print(f"   wrong order gives {wrong_undo(f)} C, about {float(wrong_undo(f)):.1f}")
    print()
    print("Epistemic status: exact and exhaustive for the 27 functions on a")
    print("3-element set. The lesson proves the socks-and-shoes rule for all")
    print("functions. That the wrong order works exactly when f and g can be")
    print("swapped is checked here for 36 pairs only; exercise: prove it.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Three things to notice. First, the order of a chain matters for most pairs: only $141$ of the $729$ pairs $(f, g)$ give the same function in both orders. Second, exactly $6$ functions can be undone — the ones that never send two inputs to the same output, as Theorem 4 predicts. Third, undoing in the right order works for all $36$ pairs (Theorem 3), while undoing in the wrong order works for exactly the $18$ pairs whose order can be swapped. The computation shows that pattern for this small set; one of the exercises asks you to prove it.

Explore

Explore: composition machines

Choose two machines and feed in a number. The widget runs them in both orders, so you can see at once whether the order matters. The “Arrow chains” tab shows chains of tables between small sets, as in our arrow diagram.

Composition machines

Feed a number through two machines. Does the order matter?

First machine fThen machine gInput x = 3

g ∘ ff first, then g

Add 1

x ↦ x + 1

→ 4

Double

x ↦ 2x

→ 8

f ∘ gg first, then f

Double

x ↦ 2x

→ 6

Add 1

x ↦ x + 1

→ 7

Different results: 8 versus 7. The order of composition matters.

Things to try:

Find a pair of machines whose order does not matter. (Does every pair involving “Do nothing” work? Why — which theorem is that?)
“Square” and “Opposite”: does the order matter? Try a negative input.
Find a machine that undoes itself: doing it twice gives back your input.
“Add 1” then “Subtract 3”: which single machine would do the same as this chain?

Exercises

1. Function machines in sequence

Warm-upHuman

Let $f(x) = 3x - 1$ and $g(x) = x^2$ . Apply $f$ , then $g$ , to the input $2$ . What is the output?

2. Function machines in sequence

CoreHuman

Let $f : \{1, 2, 3, 4\} \to \{a, b, c\}$ be given by $f(1) = a$ , $f(2) = c$ , $f(3) = a$ , $f(4) = b$ , and $g : \{a, b, c\} \to \{x, y\}$ by $g(a) = y$ , $g(b) = x$ , $g(c) = y$ . Which inputs does “ $f$ , then $g$ ” send to $y$ ? List them.

3. Function machines in sequence

CoreHuman

Which of these chains is defined for every integer input $x$ ? (Here $\sqrt{x}$ accepts only inputs $x \ge 0$ , and $\tfrac{1}{x}$ only inputs $x \neq 0$ .)

Choose one

“square, then take the square root”“subtract

1

, then take the reciprocal

\tfrac{1}{x}

”“add

1

, then take the square root”“square and change the sign (

x \mapsto -x^2

), then take the square root”

4. Function machines in sequence

CoreHuman

A function is the chain “multiply by $4$ , then subtract $7$ ”. Which chain undoes it?

Choose one

add

7

, then divide by

4

divide by

4

, then add

7

subtract

7

, then divide by

4

add

7

, then multiply by

4

5. Function machines in sequence

StretchHuman

From Bhāskara II's Līlāvatī (1150): a number is multiplied by $3$ ; then three quarters of the result is added to it; the sum is divided by $7$ ; a third of the quotient is subtracted from it; the result is multiplied by itself; $52$ is subtracted; the square root is taken; $8$ is added; and the result is divided by $10$ . The answer is $2$ . What was the number?

6. Function machines in sequence

CoreHuman

Which of these functions from $\Z$ to $\Z$ can be undone by some function from $\Z$ to $\Z$ ? Choose all that apply.

Choose all that apply

x \mapsto x + 10

x \mapsto 3x

x \mapsto x^2

x \mapsto |x|

(the distance from

0

)

x \mapsto -x

7. Function machines in sequence

CoreHuman

For which integer $a$ do “add $a$ , then multiply by $5$ ” and “multiply by $5$ , then add $a$ ” give the same output for every integer input?

8. Function machines in sequence

StretchHuman

Let $f$ and $g$ be functions from a set to itself with inverse functions $f^{-1}$ and $g^{-1}$ . Undoing “ $f$ , then $g$ ” in the wrong order means applying $f^{-1}$ , then $g^{-1}$ , so each input $a$ goes to $g^{-1}\big(f^{-1}(g(f(a)))\big)$ . When does this give back $a$ for every input?

Choose one

Exactly when

g(f(a)) = f(g(a))

for every

a

— that is, when the order of

f

and

g

does not matterOnly when

f = g

Only when

f

g

is the identityNever

9. Function machines in sequence

CoreFormal

In the Lean section, Undoes g f means $g(f(a)) = a$ for every $a$ . Which Lean statement says “squaring on $\Z$ cannot be undone”?

Choose one

¬ ∃ g : Int → Int, Undoes g (fun x => x * x)∃ g : Int → Int, ¬ Undoes g (fun x => x * x)¬ ∃ g : Int → Int, Undoes (fun x => x * x) g∀ g : Int → Int, Undoes g (fun x => x * x)

10. Function machines in sequence

StretchComputational

A function on a finite set can be stored as a dictionary, such as {1: 'a', 2: 'b'}. Write invert(table) that returns a dictionary undoing table — sending each output back to its input — or None if two inputs share an output (so the function cannot be undone).

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

Writing “first $f$ , then $g$ ” as $f(g(x))$ . In $f(g(x))$ you must work out $g(x)$ first, so $g$ acts first. “First $f$ , then $g$ ” is $g(f(x))$ : the function nearest to $x$ is the one that acts first.

Misconception

“Every function can be undone.” Squaring on $\Z$ sends $2$ and $-2$ to the same output, $4$ , so no function can send $4$ back to the right place (Theorem 4). The same goes for any function that sends two inputs to one output, such as “round to the nearest ten”.

Misconception

“To undo a chain, undo each step in the same order.” Undo the last step first: socks, then shoes, is undone by shoes off, then socks off. “Multiply by $1.8$ , then add $32$ ” is undone by “subtract $32$ , then divide by $1.8$ ”.

Misconception

Ignoring whether outputs are allowed inputs. “Subtract $2$ , then take the reciprocal” breaks at $x = 2$ , because $\tfrac{1}{0}$ is not defined. Before chaining, check that every output of the first function is an input the second one accepts.

Misconception

“If two chains agree for one input, they are the same function.” “Add $3$ , then double” and “double, then add $6$ ” agree everywhere, but “add $1$ , then square” and “square, then add $1$ ” agree only at $x = 0$ . Functions are equal only when they agree for every input.

ViewpointsH

Other ways of seeing

Algebra— Undoing in reverse, everywhere

The functions from a set to itself that can be undone in both directions — the bijections — can be chained, every one has an inverse, and the identity does nothing. A collection of reversible transformations like this is a group, and Theorem 3 becomes the rule: the inverse of “ $f$ , then $g$ ” is “ $g^{-1}$ , then $f^{-1}$ ”. Anyone who solves a Rubik's cube uses it: to undo the moves $R$ , then $U$ , you do $U$ backwards and then $R$ backwards. The same reversal appears with matrices, where $(AB)^{-1} = B^{-1}A^{-1}$ , and in solving equations: to solve $2(x + 3) = 20$ , undo “add $3$ , then double” by halving first and subtracting $3$ second.

Geometry— Moves of a square

Rotations and reflections of a square are functions from the plane to itself, and they can be chained. Turning a square a quarter turn anticlockwise and then reflecting it in its vertical axis gives a different result from reflecting first and then turning — the corner that ends up at the top right is different. But two rotations about the centre can always be swapped. Which moves can be swapped with which is the beginning of the study of symmetry (see symmetry and transformations).

Computation— Pipelines and the undo button

Programs are built from chained functions: read the data, then clean it, then sort it, then display it. A text editor's undo button keeps a stack of the actions you have performed and undoes the most recent one first — socks and shoes again. Computer scientists call this “last in, first out”.

Category-theoretic connectionH

A glimpse of structure

Picture each set as a dot and each function as an arrow between dots. Chaining is following arrows head to tail, and it is only allowed when one arrow ends where the next begins. Every dot has a “do nothing” arrow, and Theorem 1 says that following it changes nothing. In the next lesson you will also see that it never matters how you group a long chain. Dots and arrows with exactly these features form a category, and sets with functions are the first example. The Arrows that compose trail lets you build chains in a small category of your own.

Wonder Trails

Wonder Trail

Wonder Trail · Optional · never gradedArrows that composeWhat do functions between sets, maps between groups and continuous maps between shapes have in common? What if we studied only the arrows?Follow the trail

History & global context

History and global context

Working backwards through a chain of operations is an old technique. Āryabhaṭa's Āryabhaṭīya (499 CE) states the method of inversion: multipliers become divisors and divisors multipliers, additions become subtractions and subtractions additions, working from the end.
Bhāskara II's Līlāvatī (1150) contains a famous problem: a number is multiplied by $3$ , increased by three quarters of the product, divided by $7$ , decreased by a third of the result, multiplied by itself, decreased by $52$ ; then its square root is taken, $8$ is added and the result divided by $10$ , giving $2$ . What was the number? Undoing the steps from the last to the first gives the answer, $28$ (try it in the exercises).
The word function was used by Gottfried Wilhelm Leibniz in the 1690s, and Leonhard Euler introduced the notation $f(x)$ in 1734. The modern idea of a function as any rule that gives exactly one output for each input is usually credited to Peter Gustav Lejeune Dirichlet (1837).

Thirty degrees in Accra

Machines, tables and arrows

Definitions

Worked examples

The rules of chaining and undoing

Chains and undoing in Lean

Chaining tables by computer

Explore: composition machines

Exercises

Common misconceptions

Other ways of seeing

A glimpse of structure

Wonder Trail

History and global context

Further reading