It is not completely clear to me how Return[] works.

The documentation says:

Return[expr] returns the value expr from a function.

But in Mathematica it is not clear where are the boundaries of a "function" defined using patterns and Set(Delayed). The system simply applies replacement rules until there's nothing to change anymore.

Consider these examples:

In[1]:= a := (Module[{}, Return[0]; 1]; 2)

In[2]:= a
Out[2]= 0

It is not completely clear to me why Return breaks out from a, and not from Module or one of the CompoundExpression.

The following doesn't work, and simply returns the Return expression. It reminds me a bit of how Unevaluated is handled.

In[3]:= (Module[{}, Return[0]; 1]; 2)
Out[3]= Return[0]

If we add another layer of definitions, the effect of Return will stop there:

In[4]:= b := (a; 3)
Out[4]= 3

Why do these three inputs give different results? What is the general rule for deciding where Return breaks out to precisely?

The answer lies somewhere in fully understanding the evaluation process.

Would someone care to elucidate this point, perhaps with pointers to the parts of the documentation which make this clear?

It is not completely clear to me how Return[] works.

The documentation says:

Return[expr] returns the value expr from a function.

But in Mathematica it is not clear where are the boundaries of a "function" defined using patterns and Set(Delayed). The system simply applies replacement rules until there's nothing to change anymore.

Consider these examples:

a := (Module[{}, Return[0]; 1]; 2)     
a
(* 0 *)

It is not completely clear to me why Return breaks out from a, and not from Module or one of the CompoundExpression.

The following doesn't work, and simply returns the Return expression. It reminds me a bit of how Unevaluated is handled.

(Module[{}, Return[0]; 1]; 2)
(* Return[0] *)

If we add another layer of definitions, the effect of Return will stop there:

b := (a; 3)
(* 3 *)

Why do these three inputs give different results? What is the general rule for deciding where Return breaks out to precisely?

The answer lies somewhere in fully understanding the evaluation process.

Would someone care to elucidate this point, perhaps with pointers to the parts of the documentation which make this clear?