use a commutative diagram to complete another one

[amblafont]

As an example, consider the associativity monadic law:

    SSS -- Sμ --> SS
    |             | 
 Sμ |     (1)     | μ
    |             | 
    v             v 
    SS  --  μ --> S

Suppose I am selecting a branch TTT -- Tμᵀ --> TT -- μᵀ --> T. I would like to be able to use diagram (1) to create the other branch TTT -- μᵀT --> TT -- μᵀ --> T.

This requires three steps:

1. Turning the two branches of diagram (1) into patterns, e.g., for the top branch, ?S?S?S -- ?S?μ --> ?S?S -- ?μ --> ?S
2. Unifying the top branch pattern with the selected branch TTT -- Tμᵀ --> TT -- μᵀ --> T to get ?S := T and ?μ := μᵀ
3. Apply the metavariable substitution to the bottom branch of (1).

Step 1 could be done manually by the user by introducing question marks explicitly in Diagram (1). Later, the editor may try guessing the patterns. For example, the set of metavariables could be guessed by looking for substrings shared by multiple labels in the diagram.

Step 2 involves unification up to associativity (since character concatenation is associative). There is some litterature on this algorithmic problem to be investigated.