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 :

enter image description here

enter image description here

Another example is the calculus of terms in first-order logic (from Ebbinghaus, Flum, & Thomas, Mathematical Logic), which generates all syntactically valid terms :

enter image description here

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)?


2 Answers 2


A useful explanation is in Richard Kaye, The Mathematics of Logic (Cambridge U.P., 2007), Chapter 3 : Formal systems:

[a formal systems is] a kind of mathematical game with strings of symbols and precise rules.

Rules are of two basic kind :

  • rules of formation : how to generate well formed (i.e.admissible) strings

  • rules of transformation : how to produce new (well formed) strings from existing ones.

Thus, the grammar of a formal language is made of rules of formation; they can be formalized (as in your example regarding the "calculus of terms") as a calculus i.e. as a set of rules for producing syntactically correct terms from an initial empty set of them.

The inference rules of a logical calculus are rules of transformation, like e.g. the rules of Natural Deduction calculus, that produce the set of all tautologies from an initial empty set of them.

  • $\begingroup$ Is there really a syntactic difference between rules of formation and rules of transformation? Can't I formalize rules of formation as rules of transformation but with an empty initial set of strings? $\endgroup$
    – user56834
    Dec 23, 2019 at 15:55
  • $\begingroup$ @user56834 - as you can see from your example above, there is no formal difference : rules for terms formation are formalized as *transformation rules in the term calculus. The only difference is that in a proof system you need formation/transformation rules to produce terms and formulas and transformation rules to prove theorems from axioms. $\endgroup$ Dec 23, 2019 at 16:25
  • $\begingroup$ So you implicitly say wellformedness includes validity, not just syntax in the everyday meaning of the word? $\endgroup$
    – Hibou57
    May 5, 2020 at 15:04

There are various formal notions of inductive definitions such that usual calculi and grammars are special cases of them. Inductive types in type theories are usually sufficiently general, e.g. as implemented in Coq. Coq's inductive types are fairly complicated to formally specify, but we can also consider W-types, which are much simpler but somewhat less convenient to actually use. In category theory, essentially algebraic theories are a fairly general notion of inductive definition.

All of the above precisely specify what a derivation rule is, and in each case it is possible to devise collections of rules which describe calculi or grammars. In the case of formal grammars, a language of a grammar would be defined as an inductive predicate over lists of symbols, generated by finite rule application to the start symbol. In the case of calculi, we would have inductively defined sets of syntax trees together with typing and well-formedness relations, which are also inductively defined from rules.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .