CSE 331: Math Conventions

This page consolidates all of our math conventions in CSE 331. These rules exist to remove ambiguity and reduce mistakes in your mathematical proofs. We ask that you follow these conventions on all relevant homeworks, and may deduct points for submissions that do not follow these conventions.

Our notation may not always reflect math conventions elsewhere, particularly in more advanced math (that often requires additional assumptions or has notational ambiguity). We ask that you stick to our notation within our class, and will note non-standard notation when possible.

This is a new resource! If you have any questions or suggestions, please let the course staff know. Thanks!

Changelog:

• 05/25:
  • moved "list functions" to new "allowed assumptions" category
  • added definitions for \(\textsf{equal}\) and \(\textsf{contains}\)
  • added allowed assumptions for \(\textsf{sum}\), \(\textsf{rev}\), and their composition
• 05/20:
  • new conventions: partially-applied math functions, representation invariants, abstraction functions
  • clarity improvements: clarify that loop invariants are documented as math or comments, explicitly clarify that equalities refer to prior lines implies that proofs by calculations should not operate on both sides of an equality, explicitly allow starting from either side of an assertion

Sets, Types, and Functions

Functions

• Functions should always have type signatures.
• Side conditions and pattern matching must be exclusive and exhaustive over the range of allowed inputs.
• Conversely, do not define functions (via either side conditions or pattern matching) over invalid inputs.
• If a (math) function returns undefined for a specific input, that input is invalid.
  • This property is transitive: for example, any input that triggers a recursive call that leads to a base case returning undefined is also invalid input.
  • Code implementations of these math functions should throw an explicit Error (note that this is different from inputs that are undefined, where we do not specify program behavior).
  • (for those curious, in mathematics this is describes a partial function; the aforementioned behavior is how Haskell treats partial functions)

Proofs

Proof by Calculation

• Equality and inequalities should only refer to the immediate prior line.
  • As a corollary, proofs by calculation should not "operate on both sides of an equality".
  • Proofs should only start from one side of an equality/inequality (an "expression") and have a chain of relations to the other side of that equality/inequality.
  • When proving an equality or inequality, it is sufficient to start from either "side" of the equality/inequality.
• Steps that are not arithmetic (e.g. applying the definition of a function) must include a short justification.

Proof by Cases

• Proof by cases must be exhaustive.

Structural Induction

• When proving something via structural induction, clearly include:
  • the claim (i.e. what is being proven)
  • the base case(s)
  • the inductive hypothesis
  • the inductive step(s)
  • the conclusion (i.e., that the claim holds)

Floyd Logic

Reasoning

• Forward and backwards reasoning steps (Hoare triples with non-zero code) should include no proofs. Reasoning steps should be straightforward. Proofs should only exist at Hoare triples with no code. The exceptions to this rule are:
  • reasoning that is just arithmetic (including changing equality/inequality bounds)
  • negating a boolean condition
  • splitting a non-\(\textsf{nil}\) list into its head and tail
• Other than lines of code that only assign to a constant variable, all lines of code should be annotated with an assertion.

Subscripts

• Do not use subscripts for variable mutation that is invertible. Only use subscripts for non-invertible mutation.
  • roughly speaking, by "invertible" we mean: can you "undo" the operation easily for all inputs?
  • examples of invertible mutation: addition, subtraction, and multiplication over \(\mathbb{N}\) or \(\mathbb{R}\) (when well-defined)
  • examples of non-invertible mutation: division over the \(\mathbb{N}\) or \(\mathbb{R}\), re-assigning a list value to its tail
  • (for those curious: here, we mean "invertible" as in "is there a bijection")

Loop Invariants

• Prefix loop invariant assertions (as math or comments) with "Inv: ".
• When proving correctness about code with loops, clearly include:
  • the loop invariant itself
  • a proof that the invariant holds initially
  • a proof that the loop body preserves the loop invariant
  • a proof that the post-condition is satisfied when the loop exits

Representation Invariants and Abstraction Functions

• Prefix abstraction functions (as math or comments) with "AF: ".
• Prefix representation invariant assertions (as math or comments) with "RI: ".
• When proving correctness about immutable data structures, clearly prove that:
  • after the constructor, both the abstraction function and representation invariant hold
  • for every other method, the postcondition is met for every input allowed by the precondition --- assuming that the abstraction function and representation invariant are true at the beginning of the method

Allowed Assumptions

After introduced in lecture (and unless otherwise disallowed by the problem), you may assume all of the following subsections without proof. However, facts still must be cited (when relevant).

List Functions

Unless otherwise disallowed by the problem, you may assume that the following functions have been defined for you and are correct (for all parametrized lists \(\textsf{List}\langle T \rangle\)):

For types that can be summed (e.g. \(\mathbb{Z}\) or \(\mathbb{R}\)), a \(\textsf{sum}\) function can be defined, e.g. over the integers:

Facts About List Functions

After they have been discussed in lecture and unless otherwise disallowed by the problem, you may assume that the following facts hold for any lists \(L\), \(R\), and \(S\). They should still be cited (when relevant); the parenthetical names for the facts are suggested names for each fact.

For lists \(L\), \(R\) with individual elements that support addition (e.g. \(\mathbb{Z}\) or \(\mathbb{R}\)), we also have:

The proofs for these are analogous to the in-class proofs for \(\textsf{len}\).

Notation Conventions

The following describes notation we will use in the class. You may freely use any of these on homeworks or the exam without definition.

For a longer treatment, we suggest looking at James & Kevin's notes on math notation.

Core Set Notation

• \(x \in S\) or \(x : S\): \(x\) is an element of set \(S\)
• \(x \notin S\): \(x\) is not an element of set \(S\)

Basic Sets and Types

We assume that the following sets exist:

Note: our notation for boolean as \(\mathbb{B}\) is semi-standard, and \(\mathbb{S}\) and \(\mathbb{S}^*\) for characters and strings is non-standard.

Compound Types

Note: these all describe types. This syntax should appear in places that describe types (e.g. function signatures).

Defining Functions

We define functions in two pieces:

1. a function's "type signature", which consists of:
   • its name
   • the types of its parameter(s)
   • its return type
2. a function's "body", which can be defined with side conditions or pattern matching.

Functions with multiple arguments should use a comma to separate each argument (instead of a tuple). For example, the following defines addition over \(\mathbb{N}\):

Note that names for parameters are only used in the function definition, not the type signature.

Lists (as Inductive Types)

We define the parametrized \(\textsf{List}\langle T \rangle\) inductive data type as:

where \(T\) can be any type (e.g. \(\mathbb{N}\) or \(\mathbb{Z}\)).

In Homework 4, we allow \(\textsf{List}\) to represent \(\textsf{List}\langle \mathbb{Z} \rangle\), but ask that you use the parametrized list from HW5-onwards.

You may abbreviate (unless otherwise disallowed in the spec):

• \(\textsf{cons}\) as \(::\), e.g. \(1 :: 2 :: 3 :: \textsf{nil}\) as \(\textsf{cons}(1, \textsf{cons}(2, \textsf{cons}(3, \textsf{nil})))\)
• \(\textsf{concat}\) as \(\mathbin{+\mkern-10mu+}\), which is defined in the List Functions section

Assertions

Floyd logic assertions should be defined in-line within code using \(\{\{\) and \(\}\}\). Each assertion should refer to the line of code immediately after the braces.

As {{ and }} are not valid TypeScript, they should instead be written as comments in code (this is often removed from lecture examples for brevity).

/**
 * @param n an integer with n >= 1
 * @returns an integer m with m >= 10
 */
const f = (n: bigint): bigint => {
  // {{ n >= 1 }}
  n = n + 3n;
  // {{ n2 >= 10 }}
  return n * n;
};

Multiple assertions should be separated with the literal words "\(\textsf{and}\)" and "\(\textsf{or}\)" when appropriate. If mixing the two, use parentheses to make the order of operations explicit.

// Returns an integer m with m > n
const g = (n: bigint): bigint => {
  // {{ }}
  let m;
  if (n >= 0n) {
    m = 2n * n + 1n;
  } else {
    m = 0n;
  }
  // {{ (n >= 0 and m = 2n + 1) or (n < 0 and m = 0) }}
  // {{ m > n }}
  return m;
}