# formal languages – Name for a function on formulae that does not break the structure of given formula I have two logics `L1` and `L2` and a mapping `f: Formulas_L1 -> Formulas_L2`, and want to argue that the mapping is “nice”, in the sense that it is structure-preserving. But I do not know the right name for this concept.

Formulas of the logics are generated by grammar, and thus the two languages form two term algebras. The mapping satisfies `f = g . h`, where `h : Formulas_L1 -> Formulas_L2'` is structure-preserving, in the sense that it is an injective homomorphism between the two term algebras,
and the language of `L2'` is a sublanguage of the language of `L2` (Therefore, `Formulas_L2' subset Formulas_L2`). The function `g : Formulas_L2' -> Formulas_L2`, however, is not a homomorphism: it just wraps the given formula in a nonterminal which is not present in the grammar of `L2'`. However, it `g` still does not break the structure of the given formula; intuitively, it just wraps it in some container. Maybe ‘functor’ from category theory is a related concept? An example of that function would be: `g(t) = one_plus t`.

What is the right term/name for the sense in which `g` does not break the structure of given formula? How can I argue that `Formulas_L2`, thanks to `g . h`, extend the syntax of `Formulas_L1`; i.e., that `g . h` is an embedding of the syntax of `L1` into the syntax of `L2`? Posted on