Difference between revisions of "Notation"

From Internet Computer Wiki
Jump to: navigation, search
 
(10 intermediate revisions by 2 users not shown)
Line 1: Line 1:
== Notation ==
+
The following is the notation used within the descriptions of the [[IC state manager|state manager]] and the [[IC message routing layer|message routing]] layer.
  
* <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>
 
* 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.
+
* <math>\cdot</math> is used to denote an arbitrary value that some variable takes. For example, when quantifying over a set of tuples of the form <math>(x, y)</math>, <math>(x, \cdot)</math> can be used to express an arbitrary value that <math>y</math> may take 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. <math>|X|</math> is used 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. <math>X[i]</math> is used 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>.
+
* The concatenation of two ordered sequences is defined <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
+
* It is common to work with partial maps <math>M: X \mapsto Y</math>, which can be written 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>. Note that partial maps can be nested, i.e., the set <math>Y</math> could again be a partial map
 +
* Square brackets are used to index into a partial map, for example <math>M[x] = y</math> if <math>(x \mapsto y) \in M</math>
 +
* When working with nested partial maps, such as <math>M: X \mapsto (Y \mapsto Z)</math>, for example, they are ususally written as a single map <math>M: (X \times Y) \mapsto Z</math>, i.e., <math>\{ ((x_1, y_1) \mapsto z_1), …​ ((x_m, y_n) \mapsto z_{mn}) \}</math>.
 +
* Let <math>X</math> be a set. Define <math>\min(X) := \{ i | i \in X \land \nexists j \in X : j < i \}</math> and <math>\max(X) :=
 +
\{ i | i \in X \land \nexists j \in X : j > i \}</math>. Note that a set can contain multiple incomparable elements in which case <math>|\min(X)|</math> or <math>|\max(X)|</math> could be greater than 1.
 +
* For partial maps <math>M : X \mapsto Y</math>, define the function <math>\text{dom}(M) := \{ i | (i ↦ ·) \in M \}</math>.
 +
* The map merge operator is defined as <math>A \cup B</math> on partial maps <math>A: X \mapsto Y</math> and <math>B: X \mapsto Y</math> as <math>(x \mapsto y) \in A \cup B</math> iff <math>(x \mapsto y) \in A \lor (x \mapsto y) \in B</math>. The operation fails if the domains of A and B are not disjoint.
 +
* The <math>\text{merge}(S)</math> operator, which, for a set of partial maps <code>S : Set<X ↦ Y></code> is defined as <math>\text{merge}(\{ M_1, …​, M_n \}) := M_1 ∪ …​ ∪ M_n</math>.
 +
* When working with sets of types with multiple fields, e.g., set <math>S = \{ t_1, …​, t_n \}</math> of type <code>Set<T></code> where <math>T</math> has a field <math>A</math> of type <math>T_A</math>, <math>S.A</math> is used to denote the set <math>\{ t_1.A, …​, t_n.A \}</math> of type <code>Set<T_A></code>.
 +
* The same can be done for nested partial maps where the innermost partial map is a type with multiple fields. For example, for a map <math>M : X \mapsto Y \mapsto T</math>, <math>M.A</math> is used to denote the map <math>\{ (x \mapsto y \mapsto a) | (x \mapsto y \mapsto t) \in M \land a = t.A \}</math> of type <math>X ↦ Y ↦ T_A</math>.
 +
* Sometimes there is a need to drop the property of (nested) partial maps that each key maps to a unique value in which case the same notation is used, but replace the <math>\mapsto</math> with a <math>\times</math> in the type definition, i.e., use sets of key-value tuples of type <code>Set((X × …​ × Y) × V)</code> tuples. The same notational conventions are used as defined for partial maps above.
 +
* <code>FAIL IF: p</code> is sometimes used for some predicate <code>p</code> before function definitions in pseudocode. The semantic of this is that whenever p evaluates to false the actual implementation should fail, while the implementation given in the specification does not fail.
 +
* A function <math>H: X \rightarrow Y</math> is collision resistant, if—​for practical purposes—​it it will never happen that one comes up with two values <math>x, x' \in X</math> so that <math>x \neq x'</math> and <math>H(x) = H(x')</math>.

Latest revision as of 09:47, 27 February 2023

The following is the notation used within the descriptions of the state manager and the message routing layer.

  • [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]
  • [math]\displaystyle{ \cdot }[/math] is used to denote an arbitrary value that some variable takes. For example, when quantifying over a set of tuples of the form [math]\displaystyle{ (x, y) }[/math], [math]\displaystyle{ (x, \cdot) }[/math] can be used to express an arbitrary value that [math]\displaystyle{ y }[/math] may take in each of the tuples.
  • Let [math]\displaystyle{ X }[/math] be a set or a sequence. [math]\displaystyle{ |X| }[/math] is used to denote the size/length of the set/sequence.
  • Let [math]\displaystyle{ X }[/math] be a sequence. [math]\displaystyle{ X[i] }[/math] is used 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].
  • The concatenation of two ordered sequences is defined [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].
  • It is common to work with partial maps [math]\displaystyle{ M: X \mapsto Y }[/math], which can be written 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]. Note that partial maps can be nested, i.e., the set [math]\displaystyle{ Y }[/math] could again be a partial map
  • Square brackets are used to index into a partial map, for example [math]\displaystyle{ M[x] = y }[/math] if [math]\displaystyle{ (x \mapsto y) \in M }[/math]
  • When working with nested partial maps, such as [math]\displaystyle{ M: X \mapsto (Y \mapsto Z) }[/math], for example, they are ususally written as a single map [math]\displaystyle{ M: (X \times Y) \mapsto Z }[/math], i.e., [math]\displaystyle{ \{ ((x_1, y_1) \mapsto z_1), …​ ((x_m, y_n) \mapsto z_{mn}) \} }[/math].
  • Let [math]\displaystyle{ X }[/math] be a set. Define [math]\displaystyle{ \min(X) := \{ i | i \in X \land \nexists j \in X : j \lt i \} }[/math] and [math]\displaystyle{ \max(X) := \{ i | i \in X \land \nexists j \in X : j \gt i \} }[/math]. Note that a set can contain multiple incomparable elements in which case [math]\displaystyle{ |\min(X)| }[/math] or [math]\displaystyle{ |\max(X)| }[/math] could be greater than 1.
  • For partial maps [math]\displaystyle{ M : X \mapsto Y }[/math], define the function [math]\displaystyle{ \text{dom}(M) := \{ i | (i ↦ ·) \in M \} }[/math].
  • The map merge operator is defined as [math]\displaystyle{ A \cup B }[/math] on partial maps [math]\displaystyle{ A: X \mapsto Y }[/math] and [math]\displaystyle{ B: X \mapsto Y }[/math] as [math]\displaystyle{ (x \mapsto y) \in A \cup B }[/math] iff [math]\displaystyle{ (x \mapsto y) \in A \lor (x \mapsto y) \in B }[/math]. The operation fails if the domains of A and B are not disjoint.
  • The [math]\displaystyle{ \text{merge}(S) }[/math] operator, which, for a set of partial maps S : Set<X ↦ Y> is defined as [math]\displaystyle{ \text{merge}(\{ M_1, …​, M_n \}) := M_1 ∪ …​ ∪ M_n }[/math].
  • When working with sets of types with multiple fields, e.g., set [math]\displaystyle{ S = \{ t_1, …​, t_n \} }[/math] of type Set<T> where [math]\displaystyle{ T }[/math] has a field [math]\displaystyle{ A }[/math] of type [math]\displaystyle{ T_A }[/math], [math]\displaystyle{ S.A }[/math] is used to denote the set [math]\displaystyle{ \{ t_1.A, …​, t_n.A \} }[/math] of type Set<T_A>.
  • The same can be done for nested partial maps where the innermost partial map is a type with multiple fields. For example, for a map [math]\displaystyle{ M : X \mapsto Y \mapsto T }[/math], [math]\displaystyle{ M.A }[/math] is used to denote the map [math]\displaystyle{ \{ (x \mapsto y \mapsto a) | (x \mapsto y \mapsto t) \in M \land a = t.A \} }[/math] of type [math]\displaystyle{ X ↦ Y ↦ T_A }[/math].
  • Sometimes there is a need to drop the property of (nested) partial maps that each key maps to a unique value in which case the same notation is used, but replace the [math]\displaystyle{ \mapsto }[/math] with a [math]\displaystyle{ \times }[/math] in the type definition, i.e., use sets of key-value tuples of type Set((X × …​ × Y) × V) tuples. The same notational conventions are used as defined for partial maps above.
  • FAIL IF: p is sometimes used for some predicate p before function definitions in pseudocode. The semantic of this is that whenever p evaluates to false the actual implementation should fail, while the implementation given in the specification does not fail.
  • A function [math]\displaystyle{ H: X \rightarrow Y }[/math] is collision resistant, if—​for practical purposes—​it it will never happen that one comes up with two values [math]\displaystyle{ x, x' \in X }[/math] so that [math]\displaystyle{ x \neq x' }[/math] and [math]\displaystyle{ H(x) = H(x') }[/math].