binji's comments

document/execution/instructions.rst

@@ -844,11 +844,11 @@ Control Instructions
 
 2. Assert: due to :ref:`validation <valid-call_indirect>`, :math:`F.\MODULE.\TABLES[0]` exists.
 
-3. Let :math:`a` be the :ref:`table address <syntax-tableaddr>` :math:`F.\MODULE.\TABLES[0]`.
+3. Let :math:`\X{ta}` be the :ref:`table address <syntax-tableaddr>` :math:`F.\MODULE.\TABLES[0]`.
 
-4. Assert: due to :ref:`validation <valid-call_indirect>`, :math:`S.\TABLES[a]` exists.
+4. Assert: due to :ref:`validation <valid-call_indirect>`, :math:`S.\TABLES[\X{ta}]` exists.
 
-5. Let :math:`\X{tab}` be the :ref:`table instance <syntax-tableinst>` :math:`S.\TABLES[a]`.
+5. Let :math:`\X{tab}` be the :ref:`table instance <syntax-tableinst>` :math:`S.\TABLES[\X{ta}]`.
 
 6. Assert: due to :ref:`validation <valid-call_indirect>`, :math:`F.\MODULE.\TYPES[x]` exists.
 

document/execution/numerics.rst

@@ -18,7 +18,7 @@ Auxiliary Operations
 .. math::
    \begin{array}{lll@{\qquad}l}
    \bytes_N(i) &=& \epsilon & (N = 0 \wedge i = 0) \\
-   \bytes_N(i) &=& b~\bytes_{N-8}(j) & (N \geq 8 \wedge i = 8\cdot j + b) \\
+   \bytes_N(i) &=& b~\bytes_{N-8}(j) & (N \geq 8 \wedge i = 2^8\cdot j + b) \\
    ~ \\
    \bytes_{\K{i}N}(i) &=& \bytes_N(i) \\
    \bytes_{\K{f}N}(b^N) &=& \F{reverse}(b^N) \\

document/execution/runtime.rst

@@ -15,7 +15,7 @@ Values
 WebAssembly computations manipulate *values* of the four basic :ref:`value types <syntax-valtype>`: :ref:`integers <syntax-int>` and :ref:`floating-point data <syntax-float>` of 32 or 64 bit width each, respectively.
 
 In most places of the semantics, values of different types can occur.
-In order to avoid ambiguities, values are therefor represented with an abstract syntax that makes their type explicit.
+In order to avoid ambiguities, values are therefore represented with an abstract syntax that makes their type explicit.
 It is convenient to reuse the same notation as for the |CONST| :ref:`instructions <syntax-const>` producing them:
 
 .. math::

document/syntax/conventions.rst

@@ -42,7 +42,7 @@ The following conventions are adopted in defining grammar rules for abstract syn
 Auxiliary Notation
 ~~~~~~~~~~~~~~~~~~
 
-When dealing with syntactic constructs the following notation is also used:
+When dealing with syntactic constructs the following notations and conventions are also used:
 
 * :math:`\epsilon` denotes the empty sequence.
 
@@ -52,26 +52,35 @@ When dealing with syntactic constructs the following notation is also used:
 
 * :math:`s[i:n]` denotes the sub-sequence of length :math:`n` a sequence :math:`s` that consists of its :math:`i`-th to :math:`(i+n-1)`-the element.
 
-* :math:`s~\mbox{with}~[i] = x` denotes the same sequence as :math:`s`,
-  except that the :math:`i`-the element is replaced with :math:`x`.
+* :math:`s \with [i] = A` denotes the same sequence as :math:`s`,
+  except that the :math:`i`-the element is replaced with :math:`A`.
 
-* :math:`s~\mbox{with}~[i:n] = x^n` denotes the same sequence as :math:`s`,
-  except that the sub-sequence :math:`s[i:n]` is replaced with :math:`x^n`.
+* :math:`s \with [i:n] = A^n` denotes the same sequence as :math:`s`,
+  except that the sub-sequence :math:`s[i:n]` is replaced with :math:`A^n`.
 
-Productions of the following form are interpreted as *records* that map a fixed set of fields :math:`\K{field}_i` to values :math:`x_i`, respectively:
+* :math:`x^n`, where :math:`x` is a non-terminal symbol, is treated as a meta variable ranging over respective sequences of :math:`x` (similarly for :math:`x^\ast`, :math:`x^+`, :math:`x^?`).
+
+* When given a sequence :math:`x^n`,
+  then the ocurrences of :math:`x` in a sequence written :math:`(A_1~x~A_2)^n` are assumed to be in pointwise correspondence with :math:`x^n`
+  (similarly for :math:`x^\ast`, :math:`x^+`, :math:`x^?`).
+  This implicitly expresses a form of mapping syntactic constructions over a sequence.
+
+Productions of the following form are interpreted as *records* that map a fixed set of fields :math:`\K{field}_i` to values :math:`A_i`, respectively:
 
 .. math::
-   \X{r} ~::=~ \{ \K{field}_1~x_1, \K{field}_2~x_2, \dots \}
+   \X{r} ~::=~ \{ \K{field}_1~A_1, \K{field}_2~A_2, \dots \}
 
 The following notation is adopted for manipulating such records:
 
 * :math:`r.\K{field}` denotes the :math:`\K{field}` component of :math:`r`.
 
-* :math:`r~\mbox{with}~\K{field} = x` denotes the same record as :math:`r`,
-  except that the :math:`\K{field}` component is replaced with :math:`x`.
+* :math:`r \with \K{field} = A` denotes the same record as :math:`r`,
+  except that the :math:`\K{field}` component is replaced with :math:`A`.
 
 The update notation for sequences and records generalizes recursively to nested components accessed by "paths" :math:`\X{pth} ::= ([\dots] \;| \;.\K{field})^+`:
 
-* :math:`s~\mbox{with}~[i]\,\X{pth} = x` is short for :math:`s~\mbox{with}~[i] = (s[i]~\mbox{with}~\X{pth} = x)`.
+* :math:`s \with [i]\,\X{pth} = A` is short for :math:`s \with [i] = (s[i] \with \X{pth} = A)`.
+
+* :math:`r \with \K{field}\,\X{pth} = A` is short for :math:`r \with \K{field} = (r.\K{field} \with \X{pth} = A)`.
 
-* :math:`r~\mbox{with}~\K{field}\,\X{pth} = x` is short for :math:`r~\mbox{with}~\K{field} = (r.\K{field}~\mbox{with}~\X{pth} = x)`.
+where :math:`r \with .\K{field} = A` is shortened to :math:`r \with \K{field} = A`.