If a Triple Graph Grammar rule counts as a Mathematical Proof

Question

I am intrigued by Triple Graph Grammars (TGG) as a potential for formal mathematical proof.

Triple Graph Grammars (TGGs) are a technique for defining the correspondence between two different types of models in a declarative way.

In some systems, proofs are simply trees of rules being applied to transform one syntax tree of terms into another. I don't really have a firm grasp of what that actually means in practice, but I think I understand the gist of it. As such, a proof is a transformation of a into b, so a correspondence between two different models. Some sort of isomorphism.

The diagrams below show (roughly) that there are links between source and target objects, defining how to transform them (bijection). I'm wondering if a TGG rule has enough information in it to allow it to be considered a valid proof of a transformation of isomorphism. That is, and I don't fully understand how to apply TGGs, you define a TGG between two forms of an object (or more generally, between two objects), and that definition is equivalent to a formal proof of the isomorphism between the two objects. Wondering if this is true or if it is close to true. If close / along the lines of the right direction, wondering what it would require to make it into a valid proof.

To summarize, the questions are:

1. If a TGG counts as a valid proof of transformation (maybe of isomorphism) from $A \to B$.
2. If a TGG counts as a valid proof of transformation from $B \to A$.
3. If not, what would be required to make it into a valid proof.

---

Some more notes are:

A triple graph $G =(G_S \overset{s_G}{\longleftarrow} G_C \overset{t_G}{\longrightarrow} G_T)$ consists of three graphs $G_S$, $G_C$, and $G_T$, called source, correspondence, and target graphs, together with two graph morphisms $s_G : G_C \to G_S$ and $t_G : G_C \to G_T$. A triple graph morphism $m = (m_S, m_C , m_T) : G \to H$ consists of three graph morphisms $m_S : G_S \to H_S$, $m_C : G_C \to H_C$ and $m_T : G_T \to H_T$ such that $m_S \circ s_G = s_H \circ m_C$ and $m_T \circ t_G = t_H \circ m_C$. A typed triple graph $G$ is typed over a triple graph $T_G$ by a triple graph morphism $type_G : G \to T_G$. [source]

A function transforming A into B doesn't keep track of the actual individual steps between transformation, so the information is lost. But the TGG does. The only way to "prove" that A can be transformed to B with a function is to actually apply the function and compare the outputs. But with a mapping defined in a TGG, the "proof" would be the mapping itself, so you don't have to actually perform the transformation (or it seems). So given A and B and R (rule) in TGG context, R is the proof, we don't have to try converting A $\to$ B.

An example of this would be the transform between a parse tree and an abstract syntax tree. The parse tree let's say is the actual individual tokens organized into a tree of symbols and words, where every object in the tree is the same type of object (let's say a "parse node" object). The AST though is a tree of custom objects like "function node" and "variable node". So you convert the parse tree to the AST. How to prove that AST came from the parse tree. A function requires recomputing the output, maybe a TGG rule means it's automatically proven as a "derivation" of the parse tree.

Given I have parse tree A and AST B in memory, I would like to be able to say "A becomes B" without having to recompute it. I would like to say "B came from A" as well, which seems possible because of the bidirectional mapping of TGGs.

---

Answer 1

A TGG defines (generates) a language of triples of graphs. This can be used for many things, including establishing a notion of correctness for forward and backward transformations. So if you have some transformation A -> B, you can check if it is correct by checking if there exists some A <-C->B that can be generated by the TGG.

Correct forward and backward transformations do not have to be bijections, although this could be enforced by analysing the TGG appropriately.

As a proof, one could use a TGG to generate proofs of consistency. So given some A and B, I can prove that A and B are consistent (and whatever produced B from A or A from B correct), by determining a rule application sequence that takes you from some start triple graph to some A<-C->B.

So for your concrete syntax tree and AST you could check for consistency without recomputing the trees. In practice, however, such a consistency checker can actually be slower than a recomputation (but is sometimes still better, e.g., if the computation was non-deterministic or required some form of decision making).