How to Write a Long Formula

Leslie Lamport December 25, 1993 Minor correction: January 18, 1994

\begin{matrix}c \\ ◯ \end{matrix}Digital Equipment Corporation 1993

This work may not be copied or reproduced in whole or in part for any commercial purpose. Permission to copy in whole or in part without payment of fee is granted for nonprofit educational and research purposes provided that all such whole or partial copies include the following: a notice that such copying is by permission of the Systems Research Center of Digital Equipment Corporation in Palo Alto, California; an acknowledgment of the authors and individual contributors to the work; and all applicable portions of the copyright notice. Copying, reproducing, or republishing for any other purpose shall require a license with payment of fee to the Systems Research Center. All rights reserved.

Author’s Abstract

Standard mathematical notation works well for short formulas, but not for the longer ones often written by computer scientists. Notations are proposed to make one or two-page formulas easier to read and reason about.

Introduction

Mathematicians seldom write formulas longer than a dozen or so lines. Computer scientists often write much longer formulas. For example, an invariant of a concurrent algorithm can occupy more than a page, and the specification of a real system can be a formula dozens or even hundreds of pages long. Standard mathematical notation works well for short formulas, but not for long ones. I propose a few simple notations for writing formulas of up to a couple of pages. These notations can make formulas much easier to read and reason about.

Formulas significantly longer than two pages require hierarchical structuring. Methods for structuring long programs can be used to structure long formulas. Programs of less than a dozen or so pages can be adequately structured with procedures; longer programs require some method of grouping procedures into modules. The definition is the mathematical analog of the procedure. Definitions suffice for structuring formulas of up to about a dozen pages. For longer formulas, some form of module structure is also needed.

Any formula can be written with a hierarchy of definitions, each only a few lines long. However, just as programs become hard to read if broken into too many procedures, formulas are hard to read if broken into definitions that are too small. In my experience, the best way to structure a long formula is in terms of individual formulas of up to a page or two.

Writing Formulas

Consider the following definition, written with standard mathematical conventions. (The examples come from the invariant of an unpublished correctness proof for a cache coherence algorithm; the reader is not expected to understand them.)

memQLoc(a) ≡ \begin{cases}“None” & if Locs = ∅ \\ max(Locs) & otherwise \end{cases}
where Locs ≡ \begin{cases}i ∈ \{0 … |memQ| − 1\} : \\ (memQ[i].req.type = “Write”) \\ ∧ (memQ[i].req.adr = a) \} \end{cases}

This definition is easy to read because it is short. However, suppose that “None” and max(Locs) were replaced by much longer expressions. We would then see that the “where” construct is bad because it forces us to read the entire definition of memQLoc(a) before we learn what Locs is. A structure that scales better to large formulas is

let Locs ≡ \begin{cases}i ∈ \{0 … |memQ| − 1\} : \\ (memQ[i].req.type = “Write”) \\ ∧ (memQ[i].req.adr = a) \} \end{cases}

in memQLoc(a) ≡ \begin{cases}“None” & if Locs = ∅ \\ max(Locs) & otherwise \end{cases}

Suppose once again that “None” were replaced by a long expression e, perhaps crossing onto the next page. The typographic difficulties posed by the resulting large left brace are daunting. Simply removing the brace still leaves us with the problem of where to put the condition Locs = ∅. If it goes after e, we have to read several lines before discovering the structure of the definition. If it goes at the end of the first line, we read the Locs = ∅ in the middle of reading e. A better notation is the if/then/else construct used in programming languages.

let Locs ≡ \begin{cases}i ∈ \{0 … |memQ| − 1\} : \\ (memQ[i].req.type = “Write”) \\ ∧ (memQ[i].req.adr = a) \} \end{cases}

in memQLoc(a) ≡ if Locs = ∅ then “None” else max(Locs)

The if/then/else makes the structure immediately clear, even for long formulas. The obvious analog of the case construct of programming languages works for definitions with more than two alternatives. The customary closing end (or fi) is unnecessary, because we can use parentheses and indentation to delimit the scope of an if or case.

The original version of the definition had an important feature that has been lost in these transformations: we could see at once that it was a definition of memQLoc(a). One further change recovers this feature.

memQLoc(a) ≡ let Locs ≡ \begin{cases}i ∈ \{0 … |memQ| − 1\} : \\ (memQ[i].req.type = “Write”) \\ ∧ (memQ[i].req.adr = a) \} \end{cases} in if Locs = ∅ then “None” else max(Locs)

The basic problem with the “if … otherwise” construct is shared by all infix operators: we discover the high-level structure only after reading to the end of the first argument. Consider the following formula.

(∀ c ∈ CacheAddress : cache[p, c] ∈ ([[adr : Address, val : Value]] ∪ {“Invalid”})) ∧ ((request[p] ∈ Request)

∨ ((request[p] = “Ready”) ∧ (state[p] = “Idle”))) ∧ (response[p] ∈ Value)

We have to read to the end of the second line, and count parentheses, before learning that the formula is a conjunction. One possible solution is prefix notation, writing ∧(A, B, C) instead of A ∧ B ∧ C.

∧ (∀ c ∈ CacheAddress :

cache[p, c] ∈ ([[adr : Address, val : Value]] ∪ {“Invalid”}), ∨ (request[p] ∈ Request,

∧ (request[p] = “Ready”, state[p] = “Idle”)),

response[p] ∈ Value)

This formula is easy to read only because of the way it is indented. If one needs indentation anyway, why not use it to eliminate the parentheses and commas required by a prefix notation? We write the formula A_{1}∧A_{2}∧…∧A_{n} as the aligned list

\begin{aligned}∧ & A_{1} \\ ∧ & A_{2} \\ & … \\ ∧ & A_{n} \end{aligned}

and write disjunctions similarly. We can then use indentation to eliminate parentheses, writing the formula above as

∧ ∀ c ∈ CacheAddress : cache[p, c] ∈ ([[adr : Address, val : Value]] ∪ {“Invalid”})

∧ ∨ request[p] ∈ Request ∨ ∧ request[p] = “Ready” ∧ state[p] = “Idle”

∧ response[p] ∈ Value

We continue to use ∧ and ∨ as infix operators in subformulas. For example, the second conjunct of this formula can also be written

∧ ∨ request[p] ∈ Request ∨ (request[p] = “Ready”) ∧ (state[p] = “Idle”)

The list convention for conjunction and disjunction can be used for other associative operators, including addition and multiplication. However, it does not work for the nonassociative boolean operator ⇒ (implies). I have not found a good general method of writing A ⇒ B when A and B are long formulas. When A and B are conjunctions or disjunctions, the format

∧ A_{1}

…

∧ A_{m}

⇒ \begin{aligned}∧ & B_{1} \\ & … \\ ∧ & B_{n} \end{aligned}

works fairly well if A_{1} ∧ … ∧ A_{m} is only a few lines long.

Writing conjunctions and disjunctions as lists lets us take full advantage of indentation to eliminate parentheses. Indentation has meaning; shifting an expression to the left or right changes the way a formula is parsed. It is not hard to devise precise rules for parsing these two-dimensional formulas. However, there is some question about what formulas should be allowed. For example, should it be legal to write (A_{1} ∨ A_{2}) ∧ B as follows?

\begin{matrix}∨ A_{1} \\ ∨ A_{2} \end{matrix} ; ∧ B

Answers to these questions will evolve as people use the notation.

Numbering Parts of Formulas

We don’t just write formulas, we also reason about them. Reasoning about a large formula requires a convenient way of referring to its components. With the list convention, we can name individual conjuncts and disjuncts by numbering them. The ith conjunct or disjunct of a formula named F is called F.i. A universally quantified formula can be viewed as a conjunction, where the yth conjunct of ∀ x : Q is Q[y/x], the formula obtained by substituting y for x in Q. If F is the name of the formula ∀ x : Q, then we take F (y) to be the name of the formula Q[y/x]. A similar convention applies to existential quantification.

Figure 1 illustrates the use of these structuring and naming conventions in a real example—the definition of an invariant I for a cache coherence algorithm. For simplicity, only the outermost three levels of con-

I ≡ let cacheLocs(p, a) ≡ \{c ∈ CacheAddress : ∧ cache[p, c] ≠ “Invalid” ∧ cache[p, c].adr = a  \} inCache(p, a) ≡ cacheLocs(p, a) ≠ ∅ memQLoc(a) ≡ let Locs ≡ \{i ∈ \{0 … |memQ| − 1\} : ∧ memQ[i].req.type = “Write” ∧ memQ[i].req.adr = a  \} in if Locs = ∅ then “None” else max(Locs) memVal(a) ≡ if memQLoc(a) = “None” then mainMemory[a] else memQ[memQLoc(a)].req.val in 1.∧ ∀ p ∈ Process : 1.∧ ∀ a ∈ Address : 1.∧ #cacheLocs(p, a) ≤ 1 2.∧ inCache(p, a) ⇒ (cacheVal(p, a) = memVal(a)) 3.∧ mainMemory[a] ∈ Value 2.∧ ∀ c ∈ CacheAddress : cache[p, c] ∈ ([[adr : Address, val : Value]] ∪ \{“Invalid”\}) 3.∧ a.∨ request[p] ∈ Request b.∨ ∧ request[p] = “Ready” ∧ state[p] = “Idle” 4.∧ response[p] ∈ Value 5.∧ 1.∧ state[p] ∈ \begin{cases}“RdCache”, “MemWait”, \\ “BusWait”, “WrDone”, “Idle”\} \end{cases} 2.∧ (state[p] = “RdCache”) ⇒ ∧ request[p].type = “Read” ∧ inCache(p, request[p].adr) 3.∧ (state[p] = “MemWait”) ⇒ ∧ ¬inCache(p, request[p].adr) ∧ #\{i ∈ \{0 … |memQ| − 1\} : ∧ p = memQ[i].proc ∧ memQ[i].req.type = “Read”\} = 1 4.∧ (state[p] = “BusWait”) ∧ (request[p].type = “Read”) ⇒ ¬inCache(p, request[p].adr) 5.∧ (state[p] = “WrDone”) ⇒ (request[p].type = “Write”) 2.∧ memQ ∈ SequenceOf ([[proc : Process, req : Request]]) 3.∧ ∀ i ∈ \{0 … |memQ| − 1\} : memQ[i].req.type = “Read” ⇒ 1.∧ state[memQ[i].proc] = “MemWait” 2.∧ request[memQ[i].proc] = memQ[i].req

Figure 1: An invariant of a cache coherence algorithm. juncts and disjuncts are labeled. (I like to label conjuncts with numbers and disjuncts with letters.) The naming convention implies that I.2 is the formula memQ ∈ SequenceOf (…), and I.1(q).3.a is the formula request[q] ∈ Request.

Conclusion

The notations introduced here will be unfamiliar to most readers, and unfamiliar notation usually seems unnatural. I have used the notations for several years, and I now find them indispensable. I urge the reader to rewrite formula I of Figure 1 in conventional notation and compare it with the original. Having to keep track of six or seven levels of parentheses reveals the advantage of using indentation to eliminate parentheses.