Techniques for proving NP-completeness I've been reading Garey-Johnson book Computers and Intractability and I am focusin on Section 3.2, Techniques for proving NP-completeness. In these definitions and explanations nothing is formally defined. I was wondering, how would someone define those techniques formally?
The techniques mentioned are restriction, local replacement, and component design. Here are some relevant excerpts:

Proof by restriction is the simplest, and perhaps the most frequently applicable, of our three proof types. An NP-completeness proof by restriction for a given problem $\Pi \in \mathrm{NP}$ consists of simply showing that $\Pi$ contains a known NP-complete problem $\Pi'$ as a special case.
In proofs by local replacement, the transformations are sufficiently nontrivial to warrant spelling out in the standard proof format, but they still tend to be relatively uncomplicated. All we do is pick some aspect of the known NP-complete problem instance to make up a collection of basic units, and we obtain the corresponding instance of the target problem by replacing each basic unit, in a uniform way, with a different structure. The transformation from SAT to 3SAT is of this type.
Our last type of proof, and the one that tends to be the most complicated, is component design. The NP-completeness proofs for 3-DIMENSIONAL MATCHING, VERTEX COVER, and HAMILTONIAN CIRCUIT are typical examples of this type of proof. The basic idea is to use the constituents of the target problem instance to design certain &quot;components&quot; that can be combined to &quot;realize&quot; instances of the known NP-complete problem.

What exactly are those &quot;basic units&quot; and &quot;components&quot;?
I was trying to find some literature about those strict and formal definitions, but couldn't find any.
For restriction, can it be defined as a bijection from instance of one problem to another?
A basic misconception about mathematics is that it is a purely formal game. Promulgated by the formalist school, we are taught that all that matters in mathematics are formal proofs. Yet in practice, completely formal proofs almost never get written; and mathematical thought has a strong informal component. In order to get further in mathematics, you need to understand mathematical concepts intuitively rather than just formally. A formal proof might be the end result, but the thought process is more liberal.

Furthermore, mathematicians are interested in things beyond definitions, theorems and proofs: key insights are sometimes more interesting than the proof itself or the result being proved. The philosophy behind the proof uncovers a deep truth which reaches much beyond the proof itself.

Such is the case here. Garey and Johnson are explaining how they conceive of NP-completeness proofs. They describe three basic types:


Proofs by special case: If a special case of a problem is NP-hard, then so is the original problem. For example, if 3-coloring is NP-hard, then the $k$-coloring problem (with $k$ a parameter) is also NP-hard. This can in principle be modeled formally by using very weak reductions &mdash; in this case, to reduce 3-coloring to $k$-coloring, it might suffice to use an $\mathsf{NC^0}$-reduction.  In contrast to what you write, this is certainly not a bijection, since when $k &gt; 3$, the correspondence is less direct.
Proofs by gadget reduction: These are proofs in which each "basic unit" of the original instance is replaced by a "gadget" in the new instance. For example, when reducing SAT to 3SAT, we replace a clause $\ell_1 \lor \cdots \lor \ell_n$ by the clauses $\ell_1 \lor \ell_2 \lor x_2$, $\lnot x_2 \lor \ell_3 \lor x_3$, ..., $\lnot x_{n-2} \lor \ell_{n-1} \lor \ell_n$.  Basic unit is a completely informal concept. It doesn't have a formal definition. It is supposed to help you conceptualize this kind of proof. Garey and Johnson give several examples, which might help you in constructing similar NP-hardness proofs.
Proofs by indirect gadget reduction: These are proofs in which several "components" of the original instance are replaced by several kinds of gadgets. For example, when reducing from SAT, we might have different gadgets representing variables and clauses, which are connected together in an appropriate way.  Once again, component is a completely informal concept. The difference between direct gadget reduction and indirect gadget reduction is significant in our mind, but cannot necessarily be described formally.


This description is useful since it covers many NP-hardness proofs, and even other hardness proofs such as PSPACE-hardness. Understanding these techniques is helpful for coming up with new hardness proofs. However, in no way is this case distinction supposed to be formal. It is just a mental aid.