Difference between revisions of "Notation"

Revision as of 09:23, 3 November 2022

Notation

[math]\displaystyle{ v : τ }[/math] means value [math]\displaystyle{ v }[/math] has type [math]\displaystyle{ τ }[/math].
[math]\displaystyle{ X = a }[/math] means that a type or a value [math]\displaystyle{ X }[/math] is an alias for [math]\displaystyle{ a }[/math].
[math]\displaystyle{ X := \text{[something]} }[/math] means that [math]\displaystyle{ X }[/math] is defined to be [math]\displaystyle{ \text{[something]} }[/math]
A percent sign % preceded only by spaces starts a line comment % [comment]
We use [math]\displaystyle{ \cdot }[/math] to denote that we do not care about the value some variable takes. For example, when quantifying over a set of tuples of the form [math]\displaystyle{ (x, y) }[/math] we may use a [math]\displaystyle{ (x, \cdot) }[/math] to express that we do not care about the value [math]\displaystyle{ y }[/math] takes in each of the tuples.
Let [math]\displaystyle{ X }[/math] be a set or a sequence. We use [math]\displaystyle{ |X| }[/math] to denote the size/length of the set/sequence.
Let [math]\displaystyle{ X }[/math] be a sequence. We use [math]\displaystyle{ X[i] }[/math] to access the element in [math]\displaystyle{ X }[/math] at index [math]\displaystyle{ i }[/math] and [math]\displaystyle{ X[u…v] }[/math] to refer to a slice of the sequence starting at index [math]\displaystyle{ u }[/math] and ending at index [math]\displaystyle{ v }[/math]. For example, for a sequence [math]\displaystyle{ X := (a, b, c, d) }[/math], the [math]\displaystyle{ slice X[2…3] = (b, c) }[/math].
We define the concatenation of two ordered sequences [math]\displaystyle{ a := (x_1, …, x_m) }[/math] and [math]\displaystyle{ b := (y_1, …, y_n) }[/math] as [math]\displaystyle{ (x_1, …, x_m, y_1, …, y_n) }[/math].
We often work with partial maps [math]\displaystyle{ M: X \mapsto Y }[/math], which we write as [math]\displaystyle{ \{ (x_1 \mapsto y_1), \dots, (x_n \mapsto y_n) \} }[/math], where [math]\displaystyle{ \forall~ i, 1 \leq i \leq n : x_i \in X \land y_i \in Y }[/math] and [math]\displaystyle{ \nexists~ i, j, 1 \leq i, j \leq n: x_i = x_j \land i \neq j }[/math]. We note that partial maps can be nested, i.e., the set [math]\displaystyle{ Y }[/math] could again be a partial map
We use square brackets to index into a partial map, for example [math]\displaystyle{ M[x] = y }[/math] if [math]\displaystyle{ (x \mapsto y) \in M }[/math]

@@ Line 1: / Line 1: @@
 == Notation ==
-* <code>v : τ</code> means value <code>v</code> has type <code>τ</code>.
+* <math>v : τ</math> means value <math>v</math> has type <math>τ</math>.
-* <code>X = a</code> means that a type or a value <code>X</code> is an alias for <code>a</code>.
+* <math>X = a</math> means that a type or a value <math>X</math> is an alias for <math>a</math>.
-* <code>X := [something]</code> means that <code>X</code> is defined to be <code>[something]</code>
+* <math>X := \text{[something]}</math> means that <math>X</math> is defined to be <math>\text{[something]}</math>
 * A percent sign <code>%</code> preceded only by spaces starts a line comment <code>% [comment]</code>
-* We use <code>·</code> to denote that we do not care about the value some variable takes. For example, when quantifying over a set of tuples of the form <math>(x, y)</math> we may use a <math>(x, \cdot)</math> to express that we do not care about the value <math>y</math> takes in each of the tuples.
+* We use <math>\cdot</math> to denote that we do not care about the value some variable takes. For example, when quantifying over a set of tuples of the form <math>(x, y)</math> we may use a <math>(x, \cdot)</math> to express that we do not care about the value <math>y</math> takes in each of the tuples.
-* Let <code>X</code> be a set or a sequence. We use <code>|X|</code> to denote the size/length of the set/sequence.
+* Let <math>X</math> be a set or a sequence. We use <math>|X|</math> to denote the size/length of the set/sequence.
-* Let <code>X</code> be a sequence. We use <code>X[i]</code> to access the element in <code>X</code> at index <code>i</code> and <code>X[u…v]</code> to refer to a slice of the sequence starting at index <code>u</code> and ending at index <code>v</code>. For example, for a sequence <code>X := (a, b, c, d)</code>, the <code>slice X[2…3] = (b, c)</code>.
+* Let <math>X</math> be a sequence. We use <math>X[i]</math> to access the element in <math>X</math> at index <math>i</math> and <math>X[u…v]</math> to refer to a slice of the sequence starting at index <math>u</math> and ending at index <math>v</math>. For example, for a sequence <math>X := (a, b, c, d)</math>, the <math>slice X[2…3] = (b, c)</math>.
 * We define the concatenation of two ordered sequences <math>a := (x_1, …, x_m)</math> and <math>b := (y_1, …, y_n)</math> as <math>(x_1, …, x_m, y_1, …, y_n)</math>.
 * We often work with partial maps <math>M: X \mapsto Y</math>, which we write as <math>\{ (x_1 \mapsto y_1), \dots, (x_n \mapsto y_n) \}</math>, where <math>\forall~ i, 1 \leq i \leq n : x_i \in X \land y_i \in Y</math> and <math>\nexists~ i, j, 1 \leq i, j \leq n: x_i = x_j \land i \neq j</math>. We note that partial maps can be nested, i.e., the set <math>Y</math> could again be a partial map
+* We use square brackets to index into a partial map, for example <math>M[x] = y</math> if <math>(x \mapsto y) \in M</math>