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