F1 · Algebra
The substitution model
Evaluating an expression is nothing more than replacing equals with equals until a value is left. The catch is that the move is only sound when a function is pure.
F1.01 settled that a function returns exactly one output, so f(a) is a single definite value. This module turns that into a way of computing — and a way of reasoning. We step through an evaluation by substitution, find the property that makes substitution valid, and name the kind of function that guarantees it.
Equals for equals
The oldest rule in algebra is that equals may be swapped for equals. If x = 3, then anywhere x appears you may write 3 instead, and the meaning is unchanged. Carry that rule far enough and it becomes a method of evaluation: to find the value of an expression, replace each name and each call with what it equals, one step at a time, until nothing is left to replace.
This is the same rewriting you met as β-reduction in F0.1, now wearing ordinary clothes. Bind an input and step through the expression below; each line is one substitution.
Substitution · evaluate one step at a time
Algebra
A name equals a fixed value, so it can be replaced by that value wherever it appears.
Elixir
x = 3 binds x to an immutable value; from then on the name is the value.
Evaluation is reduction by substitution. Nothing changes underneath you, so a half-finished expression always means the same thing as the one before it.
Referential transparency
Substitution rests on a quiet assumption: that an expression always stands for the same value. When that holds, the expression is referentially transparent — you can replace it with its value, or its value with it, and the program behaves identically.
It does not always hold. A call that returns a fresh result each time cannot be replaced by any single
value. Compare a function that always answers the same against one that reads and advances a counter, and
evaluate next() + next() for each.
Substitute, or not · two definitions of next()
Algebra
If an expression always denotes the same value, it and the value are interchangeable.
Elixir
A pure call is interchangeable with its result; one reading a process, the clock, or :rand is not.
Referential transparency is the licence to substitute. Where it holds, equational reasoning is exact; where it fails, replacing a call can change the answer.
Purity
A function earns referential transparency by being pure, which is two conditions at once. Its result must depend only on its arguments — not on the clock, a random source, or any state that can change between calls. And it must have no side effect — it returns a value and does nothing else observable. Meet both and the function can always be replaced by its result; miss either and it cannot.
- pure
- output determined only by the arguments, with no observable effect.
- side effect
- anything beyond returning a value: writing output, changing state, reading the clock.
- transparent
- replaceable by its value without changing what the program does.
Is it pure? · check both conditions
Algebra
A function is a fixed mapping — same input, same output, and nothing more.
Elixir
Keep effects at the edges; let the core be pure functions that compute and return.
Purity is the price of substitution and the discipline that pays it. The functions you can reason about are the ones that only compute.
What this lands
Substitution gave evaluation a single mechanism — replace equals with equals — and purity gave it a guarantee. Together they are referential transparency, and the payoff runs through the whole course: a pure call can be reordered, computed once and reused, or run in parallel, because its value never depends on when or where it runs. F1.03 uses it to chain functions into composition; F2 makes purity a working style; and the BEAM of F0.2 keeps effects isolated so the pure core stays clean.
Next: F1.03 — Composition, f∘g — chaining mappings, associativity, and the pipe. Until it lands, the rest of F1 · Algebra is listed on the chapter page.