Differences between the formal grammar, formation rules and automaton for a formal language 
*

*Added: A formal grammar is a set of formation rules for strings in a formal language. Formation rules are rules for
describing which strings of symbols formed from the alphabet of a
formal language are syntactically valid within the language. I
wonder what differences are between formal grammar and formation
rules?

*Formation rules are rules for describing which strings of
symbols formed from the alphabet of a formal language are
syntactically valid within the language. 
An automaton recognizes a formal language, i.e. it can tell whether
a string belongs to the language.
So I think formation rules and automatons are doing the same thing?
What differences are between them?
Thanks and regards!
 A: No, the automaton and the formation rules are not doing the same thing.  The formation rules use what gets called metavariables.  Note that the examples for formation rules given use Greek letters instead of Latin alphabet letters.  The automaton, or mechanical reader when determining if some string does or does not adhere to the formation rules deals with object language variables, not metavariables (as far as I know the automaton can come as a human, so long as that person strictly adheres to the rules given).  The formation rules tell us in general what sorts of statements qualify as formulas (wff/statement form).  The automaton takes a particular string(s), and determines if that string(s) is (are) a wff.  The formation rules define what qualifies as a formula in principle.  The automaton basically recognizes strings as formulas.
To perhaps clarify things here, say we use "x" and "y" for metavariables, and only "a" and "b" for object language variables with the following formation rules:


*

*If "x" is a formula, then "xN" is a formula.

*If "x" and "y" are formulas, then "xyC" is a formula.

*"a" and "b" are both formulas.


From this given a string like abaabCCCCN, the automaton can determine if that string is or is not a formula.  This works out, because the formation rules basically inform the automaton to always move from the shortest string(s) to longer strings.  If no path from the shortest string(s) to the longest string L exists such that L ends up as a formula, then L is not a formula (there also exist algorithms, at least in Polish and reverse Polish notation, to check if a string is or is not a formula).  In particular, the automaton will return abaabCCCCN as a formula more-or-less as follows with the explanations:


*

*All instances of "a" and "b" are formulas by rule 3.

*Since a, and b are both formulas, abC is a formula.  Here "a" has taken the place of "x", and "b" the place of "y" in rule 2.

*Since a, and abC are both formulas, aabCC is a formula by rule 2.

*Since b, and aabCC are both formulas, baabCCC is a formula by rule 2.

*Since a, and baabCCC are both formulas, abaabCCCC is a formula by rule 2.

*Since abaabCCCC is a formula, abaabCCCCN is a formula by rule 1.


In other words, since we have this sequence of formulas,
(a, b, abC, aabCC, baabCCC, abaabCCCC, abaabCCCCN) 
abaabCCCCN is a formula.  
On the other hand if we considered the string abCaN, rule 2, along with the precondition that formulas only happen from the shortest string to longer strings in incremental steps, informs us that were it the case that abCaN was a formula, then abCa would be a formula.  Though abC and "a" are both formulas, all formulas other than "a" and "b", end with C or N.  So, abCa is not a formula, and thus neither is abCaN.
Here, we've functioned as the automaton and used the formation rules to figure out that abaabCCCCN is a formula and that abCaN is not a formula in a language with rules 1., 2., and 3 (I don't know how a non-human computer here would reason here especially in the case of determining that a string is not a formula, but the above, I think, should suffice for us).  On the other hand, the formation rules, cannot use themselves or the automaton.
I hope this helps.
