How exactly is "normal-ordering an operator" defined? (In this question, I'm only talking about the second-quantization version of normal ordering, not the CFT version.)
Most sources (e.g. Wikipedia) very quickly define normal-ordering as "reordering all the ladder operators so that all of the creation operators are to the left of all of the annihilation operators." This definition is extremely vague, and I want to make sure I understand the actual definition.
If I understand correctly, people use the phrase "normal-order an operator" to mean two inequivalent things. Sometimes they mean "use the (anti)commutation relations to rewrite the operator so that it is normal-ordered (without changing the operator itself)." Under this (unambiguous) definition, we have that the normal-ordered form of the operator $a a^\dagger$ is $a^\dagger a + 1$. We can use this definition to put any operator into canonical form (up to a sign, in the fermionic case. We can fix this sign ambiguity by specifying a canonical ordering of the single-site Hilbert spaces.)
But sometimes the verb "normal-order" is used in a different way, which can actually change the operator. I believe that this definition is the one usually represented by surrounding the operator with colons. If I understand correctly, this procedure is defined as "use the (anti)commutation relations $\left[ a_i, a_j \right]_\pm = \left[ a_i^\dagger, a_j^\dagger \right]_\pm = 0$ to move all the creation operators to the left of all the annihilation operators, while ignoring the $\left[ a_i, a_j^\dagger \right]_\pm = \delta_{ij}$ (anti)commutation relation and pretending that its RHS were zero."
This procedure obviously seems a bit arbitrary and unmotivated. Moreover, it doesn't seem entirely well-defined.  It's fine for products of ladder operators, but the problem is that under this definition, normal-ordering does not distribute over addition:
$$ {:} a^\dagger a{:} \ =\ a^\dagger a\ =\ a a^\dagger - 1\ $$
but
$${:} a a^\dagger{:}  -1\ = a^\dagger a - 1.$$
It's therefore not clear how to define normal-ordering for a general operator, i.e. a general linear combination of products of ladder operators. And of course, whether or not an operator is a nontrivial sum of products of ladder operators depends on how you write it; we can equivalently write the same operator as $a^\dagger a$ (only one summand) or as $a a^\dagger - 1$ (multiple summands).
From this, I conclude that (under the second definition) "normal-ordering an operator" is actually an abuse of terminology; we can only meaningfully normal-order certain particular expressions for some operators. Is this correct? If not, how does one define the normal-ordering of a linear combination of products of ladder operators?
 A: *

*The main point is that the normal ordering procedure $:~:$ does not take operators to operators, but symbols/functions to operators. This important point resolves various paradoxes created by abuse of language.


*That is, if $a$ and $a^{\ast}$ denotes the symbols/functions corresponding to the operators $\hat{a}$ and $\hat{a}^{\dagger}$, respectively, then the normal order satisfies
$$:aa^{\ast}:~=~:a^{\ast}a:~=~\hat{a}^{\dagger}\hat{a},$$ and so forth.


*For a full explanation, see e.g. this Phys.SE post and links therein.
A: In quantum mechanics with finitely many degrees of freedom, normal ordering always means applying the commutation rules to move creators to the left of annihilators, resulting in a unique final expression equal to the original one in the operator sense.
In quantum field theory (i.e., quantum mechanics with infinitely many degrees of freedom) proceeding this way usually is impossible as it leads to ill-defined coefficients. Therefore, in quantum field theory, normal ordering always means
permuting creators to the left of annihilators without any consideration of commutation rules (i.e., on the classical expression). However the sign is changed when permuting two fermionic operators. In this way otherwise ill-defined expressions make sense at least as quadratic forms. In spacetime dimension $>2$, further renormalization is needed to turn the expressions into true operators.
A: An axiomatic definition of normal order can be found in the book "Solitons: Differential Equations, Symmetries and Infinite Dimensional Algebra" by T. Miwa, M. Jimbo and E. Date at page 44-46. This is the best definition I have found so far and goes as follow for products of bosonic operators. Call $\mathcal{A}$ the set of linear combinations of formal finite products of bosonic operators $b_i,\,b_i^\dagger$.  The normal order ${:} a {:}$ of $a \in\mathcal{A}$ is a notation defined inductively  by the properties


*

*Linearity, $${:} z_1a_1+z_2a_2 {:}= z_1{:} a_1 {:} + z_2 {:} a_2 {:}\quad \text{for} \quad z_1,\,z_2\in \mathbb{C}\quad \text{and}\quad a_1,\,a_2 \in \mathcal{A}$$

*${:} 1 {:} = 1$, with $1$ the identity operator in $\mathcal{A}$

*within the dots all the operators $b_i,\,b_i^\dagger$ commute among themselves

*the annihilation operators can be taken out of the columns on the right $${:}a b_i{:} = {:} a{:}\,b_i$$

*the creation operators can be taken out of the columns on the left $${:}b_i^\dagger a{:} = b_i^\dagger\,{:} a{:}$$


The definition for fermionic operators is the same with the only difference that the fermionic operators anticommute among themselves (Property 3). It is important to stress that usually annihilation operators are those operators that annihilate a specified vacuum state, therefore the normal ordering depends on the choice of the vacuum.
The normal order is a notation and not a function that acts on operators (i.e. a superoperator). This means that, whereas $b_ib_i^\dagger$ and $b_i^\dagger b_i +1$ are the same operators according to the canonical commutations relations, they are represented as different elements of $\mathcal{A}$ which is the set of linear combinations of strings of symbols generated by $b_i,b_i^\dagger$. In mathematical terms the normal order is a function defined on the elements of of the free algebra generated by $b_i,b_i^\dagger$, but is not a well defined function on the CCR-algebra (Canonical Commutation Relations algebra). The wrong step that leads to the paradoxical result
$$b_ib_i^\dagger = b_i^\dagger b_i +1 \Rightarrow {:}b_ib_i^\dagger {:} = {:}b_i^\dagger b_i +1{:} = {:}b_i^\dagger b_i{:} + 1  = {:}b_ib_i^\dagger{:} + 1 \Rightarrow 0 = 1$$
is actually the first equality since $b_ib_i^\dagger \neq b_i^\dagger b_i +1$ in $\mathcal{A}$. In another post it was suggested that the normal product is undefined when acting on linear combinations. However this would seriously limit the usefulness of the normal order. For example it is common to take the normal order of infinite series such as exponentials. The definition as a function acting on the free algebra $\mathcal{A}$ is in fact the one employed in practice. 
This is a good example of how being mathematically rigor should not be regarded as a nuisance in the physics community, but rather as an important tool to avoid misunderstanding and confusion. 
A: I think the wisdom comment of Sidney Coleman is useful. (see his lecture 4.5 for more details).
My paraphrase:
"Normal order product" is not something you product operators first and then "normalize" the product. It is a new type of product that you always put annihilation operators in the right of the creation operators. Similar to the cross-product: You don't "cross" the product to do a cross-product, right?
The motivation we introduced such a kind of product is to get rid of unnecessary (at least we don't care about them in the terms of QFT) infinities after commutating operators.
