On the semantic equivalence of language syntax formalisms (Q2202012)

There are various approaches to describing the syntax of a language [\textit{E. Visser}, Syntax definition for language prototyping. Amsterdam: Univ. Amsterdam (1997; Zbl 0900.68290)]. Formal grammar [\textit{N. Chomsky}, Three models for the description of language. IRE Trans. Inf. Theory 2, No. 3, 113-124 (1956; Zbl 0156.25401)], [\textit{J. Earley}, Commun. ACM 13, 94--102 (1970; Zbl 0185.43401)], [\textit{D. E. Knuth,} Semantics of context-free languages. Math. Syst. Theory 2, 127-145 (1968; Zbl 0169.01401)] is widely used to design the syntax of programming languages [\textit{M. L. Scott}, Programming language pragmatics. Oxford: Morgan Kaufmann/ Elsevier (1999; Zbl 1005.68031)]. The methods of context-free parsing are especially effective [\textit{L. J. Valiant}, J. Comput. Syst. Sci. 10, 308--315 (1975; Zbl 0312.68042); \textit{L. Lee}, J. ACM 49, No. 1, 1--15 (2002; Zbl 1323.68332)]. Algebraic signatures provide an algebraic approach for syntax specification used in universal algebra [\textit{P. M. Cohn}, Universal algebra. Dordrecht-Boston-London: D. Reidel Publishing Company (1981; Zbl 0461.08001)] and model theory [\textit{C. C. Chang} and \textit{H. J. Keisler}, Model theory. Amsterdam etc.: North-Holland (1990; Zbl 0697.03022)]. The paper under review is devoted to the comparison of three syntax formalisms: context-free grammars (\(Grm\)), many-sorted signatures (\(Sig\)), and order-sorted signatures (\(Sig^{\leq}\)). These syntactic formalisms are treated as categories, as justified in Propositions 1, 4 and 5. Translations of descriptions from one formalism to another are considered functors. \[ \Delta: Grm \to Sig, \nabla: Sig \to Grm, \vee: Sig\to Sig^{\leq}, \Lambda: Sig^{\leq}\to Sig \] This capability is established using Propositions 10, 11, 14, 15. It was proved that the functor \(\nabla\) is left adjoint to \(\Delta\) (Theorem 1). Moreover, these categories are equivalent (Corollary 2). The functor \(\mathrm V\) is left adjoint to \(\Lambda\) (Theorem 2). Propositions 16 and 17 show that these categories are equivalent. Any of these functors preserves classes of semantics, in the sense that if \(Alg ({\mathscr X})\) denotes the class of semantics of an object \({\mathscr X}\), and \(\Upsilon\) is a functor, then \(Alg (\Upsilon {\mathscr X})\) is equivalent to \(Alg ({\mathscr X})\). This is proved in Theorems 3, 4, 5. (Functors \(Alg: Grm\to Cat^{op}\), \(Alg: Sig\to Cat^{op}\), \(Alg: Sig^{\leq}\to Cat^{op}\) are constructed using Propositions 4, 7, 8.) Similar questions were studied by \textit{J. A. Goguen} et al. [J. Assoc. Comput. Mach. 24, 68--95 (1977; Zbl 0359.68018); Theor. Comput. Sci. 105, No. 2, 217--273 (1992; Zbl 0778.68056)], but their results are special cases of the results of this paper.