An explicit algorithm for the Higman Embedding Theorem

We propose an algorithm which for any recursive group $G$, given by its effectively enumerable generators and recursively enumerable relations, outputs an explicit embedding of $G$ into a finitely presented group directly written by its generators and defining relations. This is the explicit analogue of the remarkable Higman Embedding Theorem stating that a finitely generated group $G$ is embeddable into a finitely presented group if and only if $G$ is recursive. The constructed finitely presented group can even be chosen to be $2$-generator. This algorithm has already been applied, for example, to the additive group of rational numbers $\mathbb Q$, which clearly is recursive. The question on explicit embedding of $\mathbb Q$ into a finitely presented group was mentioned in the literature by Johnson, de la Harpe, Bridson and others. The suggested method can be used to solve the problem of embeddings for some other recursive groups, also. The embedding algorithm is built using conventional free constructions, including free products with amalgamation, HNN-extensions, and also their modifications, such as the auxiliary $*$-constructions. We also analyze the steps of original Higman embedding to clearly indicate which of its parts are not explicit.