Composing Contracts, Part 3: What Is a Contract Worth?

Following “Composing Contracts” by Peyton Jones, Eber and Seward (ICFP 2000). Parts 1 and 2 built a language for describing financial contracts out of ten primitives. This post answers the only question anyone actually asks about a contract: what would I pay to own it?

This is the part of the paper where the design decisions get audited. Every “why is this a separate primitive?” from part 1 gets its answer here, and the answer is always the same shape: because it makes the valuation rule one line instead of five.

🔗Two layers, and why

The authors split valuation in two, and the analogy they reach for is a compiler:

An abstract valuation semantics translates a contract into a value process — a mathematical object — together with a handful of operations over processes. This is the machine-independent intermediate language.

A concrete implementation represents those processes somehow and computes with them. This is code generation, and it’s where you pick a financial model and a numerical method.

The payoff is the same as a compiler’s. You can optimise at the intermediate level, using algebraic identities, before ever touching the numerics. And you can swap the back end — lattice methods, Monte Carlo, PDEs — without disturbing the language or its semantics at all.

Readers of the algebra-driven design series will recognise this exactly: an obviously-correct abstract semantics first, a fast implementation second, with the semantics as the specification the implementation must satisfy. Same structure, arrived at twenty years earlier in a completely different domain.

Part 4 does the concrete layer. This post is the abstract one.

🔗Value processes

Here is the central definition, and it takes a moment.

A value process over type A is a partial function from time to a random variable of type A.

PR[A] = Date ⇀ RV[A]

Two levels of structure. At each moment in time, you don’t have a value — you have a distribution over values, because the future is uncertain. A value process is that distribution, indexed by time.

The intuitions the paper insists you internalise:

• The value process for an observable maps a time t to a random variable describing the possible values of that observable at t. “IBM stock price in USD” is a total function from time to a real-valued random variable.
• The value process for a contract, in currency k, maps a time t to a random variable describing the value, in k, of acquiring that contract at t.

That second one is the sentence to reread. The time argument of a contract’s value process is the acquisition date. Which is why part 1 spent so long on the acquisition date being distinct from the horizon.

And it’s why the function is partial: a contract has no value process beyond its horizon, because it cannot be acquired there. Observables are total; contracts are not.

The paper is upfront that these are, properly speaking, adapted stochastic processes given a filtration, and that the underlying theory is unlikely to be familiar to computer scientists — so it presents only the intuitions. I’ll do the same, and note that “process” and “variable” here mean nothing like what they mean to us.

🔗The semantics, in ten equations

Write E⟦c⟧ₖ for the value process of contract c in currency k. Here is the whole thing, paraphrased into Scala-ish notation.

give negates:

E⟦Give(c)⟧ₖ  =  −E⟦c⟧ₖ

Your counter-party’s gain is your loss. One operator.

and adds:

E⟦And(c1, c2)⟧ₖ  =  E⟦c1⟧ₖ + E⟦c2⟧ₖ     where both are defined
                 =  E⟦c1⟧ₖ              where only c1 is
                 =  E⟦c2⟧ₖ              where only c2 is

Three cases because the domains differ — beyond one horizon but not the other, you get the surviving one. Beyond both, undefined.

or takes the maximum:

E⟦Or(c1, c2)⟧ₖ  =  max(E⟦c1⟧ₖ, E⟦c2⟧ₖ)   where both are defined
                =  E⟦c1⟧ₖ / E⟦c2⟧ₖ       where only one is

You’ll choose the more valuable branch, so the compound is worth the max. And here’s the answer to a question I had in part 1 — why is a value process partial rather than total and zero past the horizon? Because of this equation. Past c1’s horizon you are forced into c2, and max(v, 0) ≠ v in general. Encoding “expired” as zero would silently give the holder a choice they don’t have.

That is a lovely piece of design justification. A representation decision made several pages earlier turns out to be forced by one equation.

scale multiplies:

E⟦Scale(o, c)⟧ₖ  =  V⟦o⟧ · E⟦c⟧ₖ

Pointwise multiplication by the observable’s own process. This looks suspicious — how can you scale pointwise when the scaling applies to future payments? The answer is in the definition: the value at t is the value of acquiring at t, so if that’s v, then the same contract with everything multiplied by x is worth v · x. The paper says plainly that the “sample at the moment of acquisition” rule from part 2 was chosen to make this equation simple. Design driven by the semantics, not the other way round.

zero is the constant zero process. truncate restricts the domain. thereafter behaves like the first process where that’s defined and the second elsewhere. All trivial, which is the point.

one is an exchange rate:

E⟦One(k2)⟧ₖ  =  exch ₖ(k2)

The value, in k, of one unit of k2.

get discounts:

E⟦Get(c)⟧ₖ  =  discᴴ⁽ᶜ⁾ₖ ( E⟦c⟧ₖ(H(c)) )

Acquire c at its horizon, so all that matters is the random variable at the horizon — E⟦c⟧ₖ(H(c)). What is that worth earlier? That needs a model of interest rates, which is what disc encapsulates: it maps a payout at a date into a process giving its value at earlier dates.

anytime takes a Snell envelope:

E⟦Anytime(c)⟧ₖ  =  snellᴴ⁽ᶜ⁾ₖ ( E⟦c⟧ₖ )

Mathematically the subtlest one, with a clean characterisation: snell(p) is the smallest process q such that q ≥ p (you can exercise now, so it’s at least as good as c) and q ≥ disc(q) at every time (you can always defer, so it’s at least as good as waiting).

Ten combinators, ten equations. That is the entire valuation semantics of every contract expressible in the language, and it fits on a page because part 1 refused to make zcb primitive.

🔗The model primitives

The equations above lean on three operations that a financial model must supply, and it’s worth being clear that this is where all the actual finance lives:

trait Model:
  def exch(k1: Currency, k2: Currency): PR[Double]
  def disc(k: Currency, t: Date, rv: RV[Double]): PR[Double]
  def snell(k: Currency, t: Date, p: PR[Double]): PR[Double]

Everything else — K, lift, lift2, time — is generic and model-independent.

And these primitives satisfy laws. Not conventions: laws, of the kind that follow from no arbitrage — the assumption that no risk-free money-making opportunity exists, because if one did, everyone would take it and it would vanish.

exch ₖ(k)                       =  K(1)
exch ₖ₂(k₁) · exch ₖ₃(k₂)        =  exch ₖ₃(k₁)
disc ᵗₖ(v)(t)                   =  v
disc ᵗₖ(v₁ + v₂)                =  disc ᵗₖ(v₁) + disc ᵗₖ(v₂)

A currency converts to itself at unity; converting via an intermediate currency gives the same answer as converting directly; discounting is the identity at its own horizon; and discounting distributes over addition.

That last one is used right-to-left as an optimisation: rather than discount two random variables separately and add the resulting trees, add the variables — a single column — and discount once. The paper notes that this is exactly what an optimising compiler does with algebraic identities, and it is.

But here’s the trap the paper flags, and I’d have fallen straight into it:

disc ᵗₖ(max(v₁, v₂))  ≠  max(disc ᵗₖ(v₁), disc ᵗₖ(v₂))

That looks fine. It would be fine if v₁ and v₂ were numbers and disc were multiplication by a factor. They’re random variables, and it’s false. Discounting and maximising don’t commute, which is the mathematical shadow of a real fact: the option to choose later is worth more than choosing now.

🔗Proving things about contracts

Now the part that makes this a programming-languages paper rather than a finance paper. Two plausible-looking equations:

Get(Get(c))            == Get(c)
Give(c1 or c2)         == Give(c1) or Give(c2)

One is true and one is false. Which, and how would you know? By comparing their valuation semantics — the abstract semantics is the reference model for what it means for two contracts to be the same. That’s observational equality again, in a third domain.

The first is true. H(Get(c)) = H(c), so both discounts run to the same horizon; apply the get rule twice, then disc ᵗₖ(v)(t) = v collapses the inner one. Five lines of substitution.

The second is false, and its core is a one-line observation:

−max(a, b)  ≠  max(−a, −b)

Negating swaps max and min. And the real-world reading is immediate and slightly chilling: on the left, Give(c1 or c2), the counter-party chooses, and they will choose what’s worst for you. On the right, Give(c1) or Give(c2), you choose. Those are different contracts and they are worth different amounts. If your system silently rewrote one into the other, you would be systematically mispricing every deal with an embedded choice — in your favour on paper, against you in reality.

Some laws hold only conditionally:

Scale(o, c1 or c2)  ==  Scale(o, c1) or Scale(o, c2)     only if o ≥ 0

Multiplying by a negative number also swaps max and min. And “o ≥ 0” means the observable is non-negative at all times — an ordering on observables, not on numbers. The paper develops an ordering on contracts too: c1 ≥ c2, pronounced “c1 dominates c2”, meaning it’s at least as good to acquire at every time within c2’s horizon.

The authors close the section by noting that from a programming-languages standpoint all of this is routine, including the proofs — but that it is most unusual to find formal proofs in the finance industry at this level of abstraction. Having named and tamed the difficult primitives, you can prove identities about contracts without understanding much about random variables at all. Which is exactly what a good abstraction is for.

🔗Why this is my favourite part of the paper

Look back at what the ten equations bought.

Every “why separate?” from part 1 is now answered. scale, get, truncate and one are separate primitives because each maps to one mathematical operation — multiply, discount, restrict, exchange. A primitive zcb would have needed a rule bundling all four, and no identity like Get(Get(c)) = Get(c) would have been visible at all.

The semantics is compositional, which is the property the paper puts in its abstract: the value of a compound contract is obtained by combining the values of its sub-contracts. Nothing needs global analysis.

The laws are optimisations. disc(v₁ + v₂) = disc(v₁) + disc(v₂), read backwards, turns two tree traversals into one. A “contract compiler” can rewrite at the process level before computing anything numerical.

And the laws are also safety. Give(c1 or c2) ≠ Give(c1) or Give(c2) is a rewrite that looks obviously valid, is not, and would cost real money. The semantics is what tells you which of your intuitions to trust.

We can now say precisely what a contract is worth. We cannot yet compute it — disc, exch and snell are still abstract, and a value process is still a mathematical object rather than a data structure.

Next: Part 4 — Lattices, laziness, and the sharing problem, in which processes become LazyLists, the Ho–Lee model becomes twenty lines, and we hit the open problem the paper ends on.

---

🔗Sources

• Peyton Jones, Simon, Jean-Marc Eber & Julian Seward. Composing Contracts: An Adventure in Financial Engineering. ICFP 2000. The two-layer architecture, the value-process definition, the compositional semantics for all ten combinators, the model primitives and their no-arbitrage laws, the Get(Get(c)) = Get(c) proof, the refutation of the give/or distribution, and the observation that disc does not commute with max are all theirs.
• Ho, Thomas & Sang-Bin Lee. Term structure movements and pricing interest rate contingent claims. Journal of Finance, 1986 — the model part 4 uses.
• Maguire, Sandy. Algebra-Driven Design. 2020 — for the abstract-semantics-then-fast- implementation method this paper anticipates.

The Scala 3 framing and the reading of the give/or refutation as a mispricing hazard are mine.