In the context of logic, and also in the context of type theory, I have been introduced to so called "calculi", that consist of derivation rules, and can be used to generate a language over a symbol set (i.e. a subset of possible strings of that set), such as the following calculus of simple types on lambda-terms (from Nederpelt & Geuvers, Type theory and formal proof), which generates all possible correct typing judgments on lambda-terms :
Another example is the calculus of terms in first-order logic (from Ebbinghaus, Flum, & Thomas, Mathematical Logic), which generates all syntactically valid terms :
On the other hand, in the context of computation theory, I've been introduced to "formal grammars", which also can be used to generate languages. Here is the definition from the article on wikipedia.
In the classic formalization of generative grammars first proposed by Noam Chomsky in the 1950s,4[5] a grammar $G$ consists of the following components:
A finite set $N$ of nonterminal symbols, that is disjoint with the strings formed from $G$.
A finite set $\Sigma$ of terminal symbols that is disjoint from $N$.
A finite set $P$ of production rules, each rule of the form
$${\displaystyle (\Sigma \cup N)^{*}N(\Sigma \cup N)^{*}\rightarrow (\Sigma \cup N)^{*}}$$
where ${*}$ is the Kleene star operator and $\cup$ denotes set union. That is, each production rule maps from one string of symbols to another, where the first string (the "head") contains an arbitrary number of symbols provided at least one of them is a nonterminal. In the case that the second string (the "body") consists solely of the empty string—i.e., that it contains no symbols at all—it may be denoted with a special notation (often $\Lambda$ , $e$ or $\epsilon$ ) in order to avoid confusion.
- A distinguished symbol $S\in N$ that is the start symbol, also called the sentence symbol.
A grammar is formally defined as the tuple $(N,\Sigma ,P,S)$. Such a formal grammar is often called a rewriting system or a phrase structure grammar in the literature.
I am trying to understand how these two are related.
On the one hand, they look like they are doing the same thing, and merely have quite different notation.
On the other hand, I cannot manage to translate the calculi for e.g. first-order logic terms straightforwardly into a formal grammar, because it seems the derivation rules T1 and T3 would have to be represented by countably infinite number of production rules in the corresponding grammar. So it doesn't seem like one derivation rule in a calculus corresponds to one production rule in a formal grammar. As an example, take rule T3 from the calculus of terms in first order logic: There is a family of rules for each $n$. In fact, since there are an infinite amount of variable symbols even rule T1 specifies an infinite family of rules. However, I notice that the definition of formal grammar, explicitly states that the number of rules are finite.
This makes me doubt whether I should conceptually even think of them as doing the same thing.
My question is: How are calculi and formal grammars related? Should I think of them as fundamentally the same thing, just with a different name and different notation, or are they the same? In particular, can we define for every calculus a formal grammar that is equivalent, and vice versa (despite my failed attempt to do so)?
