Syntax and Semantics of μG

The syntax and denotational semantics of $\mu \mathcal{G}$ were published in our FORTE 2023 article¹ The operational semantics will be added here after being published in a future article.

Syntax of $\mu \mathcal{G}$

We start by recalling the abstract syntax of $\mu \mathcal{G}$

Syntax of $\mu \mathcal{G}$

Given a set $\mathcal{X}=\{X,Y,Z,\dots \}$ of variable symbols and a set $\mathcal{S}$ of function symbols, $\mu \mathcal{G}$ expressions can be composed with the following abstract syntax:

$$\begin{array}{rl}\mathcal{N}::=& \psi \mid {⊲}_{\sigma }^{\phi }\mid {⊳}_{\sigma }^{\phi }\mid {\mathcal{N}}_1;{\mathcal{N}}_2\mid {\mathcal{N}}_1||{\mathcal{N}}_2\mid X\mid f({\mathcal{N}}_1,{\mathcal{N}}_2,\dots ,{\mathcal{N}}_k)\mid \\ & \mathtt{\text{let }}X={\mathcal{N}}_1\mathtt{\text{ in }}{\mathcal{N}}_2\mid \mathtt{\text{def }}f(\tilde{X})\{{\mathcal{N}}_1\}\mathtt{\text{ in }}{\mathcal{N}}_2\mid \\ & \mathtt{\text{if }}{\mathcal{N}}_1\mathtt{\text{ then }}{\mathcal{N}}_2\mathtt{\text{ else }}{\mathcal{N}}_3\mid \mathtt{\text{fix }}X={\mathcal{N}}_1\mathtt{\text{ in }}{\mathcal{N}}_2\end{array}$$

with $\phi ,\sigma ,\psi ,f\in \mathcal{S}$ and $X\in \mathcal{X}$ .

Given a graph $\mathtt{G}$ and an (optional) edge-labeling $\xi$, the meaning of a $\mu \mathcal{G}$ expression is a graph neural network, a function between node-labeling functions.

One of the basic $\mu \mathcal{G}$ terms is the function application $\psi$. This represents the application of a given function (referenced by $\psi$) to the input node-labeling function.

Moreover, the pre-image operator ${⊲}_{\sigma }^{\phi }$ and the post-image operator ${⊳}_{\sigma }^{\phi }$ are used to compute the labeling of a node in terms of the labels of its predecessors and successors, respectively.

Basic terms are composed by sequential composition ${\mathcal{N}}_1;{\mathcal{N}}_2$ and parallel composition ${\mathcal{N}}_1||{\mathcal{N}}_2$.

Local variables $X$ and functions $f(\tilde{X})$ can be defined using let and def.

The choice operator $\mathtt{\text{if }}{\mathcal{N}}_1\mathtt{\text{ then }}{\mathcal{N}}_2\mathtt{\text{ else }}{\mathcal{N}}_3$ allows to run different GNNs according to the result of a guard GNN.

Finally, the fixed point operator $\mathtt{\text{fix }}X={\mathcal{N}}_1\mathtt{\text{ in }}{\mathcal{N}}_2$ is used to program recursive behavior.

Typing of $\mu \mathcal{G}$

We say that a $\mu \mathcal{G}$ expression is well-formed whenever it can be typed with the rules of the following table. These rules guarantee that any well-formed $\mu \mathcal{G}$ expression can be interpreted as a GNN.

Denotational semantics of $\mu \mathcal{G}$

We are now ready to discuss the denotational semantics of $\mu \mathcal{G}$. In the following definition, $\eta$ denotes a node-labeling function, $O_{\mathtt{G}}(v)$ and $I_{\mathtt{G}}(v)$ are the outgoing and incoming edges of node $v$, and by $(\eta ,\xi )(E)$ we denote the multi-set of tuples $(\eta (u),\xi ((u,v))),\eta (v))$ for each $(u,v)\in E$.

Denotational semantics of $\mu \mathcal{G}$

Given a graph $\mathtt{G}$, an edge-labeling function $\xi$, and an environment $\rho$ that comprises a variable evaluation function ${\rho }_v:\mathcal{X}\to {\mathrm{\Phi }}_{\mathtt{G},\xi }$ and a function evaluation function ${\rho }_f:\mathcal{S}\to (({\mathrm{\Phi }}_{\mathtt{G},\xi }\times \dots \times {\mathrm{\Phi }}_{\mathtt{G},\xi })\to {\mathrm{\Phi }}_{\mathtt{G},\xi })$ we define the semantic interpretation function $⟦\cdot {⟧}_{\rho }^{\mathtt{G},\xi }:\mathcal{N}\to {\mathrm{\Phi }}_{\mathtt{G},\xi }$ on $\mu \mathcal{G}$ formulas $\mathcal{N}$ by induction in the following way:

For any $\psi ,\phi ,\sigma ,f\in \mathcal{S}$ and any $X\in \mathcal{X}$. The functions $cond$ and $g$ are defined as follows:

$$cond(t,f_1,f_2)(\eta )=\{\begin{array}{ll}{f}_1(\eta )& \text{if }t(\eta )=\lambda v.\mathtt{True}\\ f_2(\eta )& \text{otherwise}\end{array}$$

$$g(\mathrm{\Phi })(\eta )=\{\begin{array}{ll}\mathrm{\Phi }(\eta )& \text{if }\mathrm{\Phi }(\eta )=⟦{\mathcal{N}}_2{⟧}_{\rho [X\leftarrow \mathrm{\Phi }]}^{\mathtt{G},\xi }(\eta )\\ g(⟦{\mathcal{N}}_2{⟧}_{\rho [X\leftarrow \mathrm{\Phi }]}^{\mathtt{G},\xi })(\eta )& \text{otherwise}\end{array}$$

Function application

The function symbols ${\psi }_1,{\psi }_2,\dots \in \mathcal{S}$ are evaluated as the graph neural networks $⟦{\psi }_1{⟧}_{\rho }^{\mathtt{G},\xi },⟦{\psi }_2{⟧}_{\rho }^{\mathtt{G},\xi },\dots$ that map a node-labeling function $\eta$ to a new node-labeling function by applying a function on both local and global node information. The local information consists of applying $\eta$ to the input node, while the global information is the multiset of the labels of all the nodes in the graph. The graph neural network we obtain applies a possibly trainable function $f_{\psi }$ to these two pieces of information. Two particular cases arise if $f_{\psi }$ decides to ignore either of the two inputs. If $f_{\psi }$ ignores the global information, the GNN returns a node-labeling function ${\eta }_l$, a purely local transformation of the node labels. On the other hand, if $f_{\psi }$ ignores the local information, the GNN returns a node-labeling function ${\eta }_g$ that assigns to each node a label that summarizes the entire graph, emulating what in the GNN literature is known as a global pooling operator.

Pre-image and Post-Image

The pre-image symbol $⊲$ and the post-image symbol $⊳$, together with function symbols $\phi \in \mathcal{S}$ and $\sigma \in \mathcal{S}$ are evaluated as the graph neural networks $⟦{⊲}_{\sigma }^{\phi }{⟧}_{\rho }^{\mathtt{G},\xi }$ and $⟦{⊳}_{\sigma }^{\phi }{⟧}_{\rho }^{\mathtt{G},\xi }$ for any $\sigma ,\phi \in \mathcal{S}$. In the case of the pre-image, for any symbol $\phi \in \mathcal{S}$ the corresponding function $f_{\phi }$ generates a message from a tuple $(\eta (u),\xi ((u,v)),\eta (v))$, and this is repeated for each $(u,v)\in I_{\mathtt{G}}(v)$. Then for any symbol $\sigma \in \mathcal{S}$ the corresponding function $f_{\sigma }$ generates a new label for a node $v$ from the multiset of messages obtained from $f_{\phi }$ and the current label $\eta (v)$. The functions $f_{\phi }$ and $f_{\sigma }$ may be trainable. The case of the post-image is analogous, with the difference that $f_{\phi }$ is applied to tuples $(\eta (v),\xi ((v,u)),\eta (u))$ for each $(v,u)\in O_{\mathtt{G}}(v)$ instead.

Sequential composition

An expression of the form ${\mathcal{N}}_1;{\mathcal{N}}_2$ for $\mu \mathcal{G}$ formulas ${\mathcal{N}}_1,{\mathcal{N}}_2$ is evaluated as the graph neural network $⟦{\mathcal{N}}_1;{\mathcal{N}}_2{⟧}_{\rho }^{\mathtt{G},\xi }$ that maps a node-labeling function $\eta$ to a new node-labeling function obtained from the function composition of $⟦{\mathcal{N}}_2{⟧}_{\rho }^{\mathtt{G},\xi }$ and $⟦{\mathcal{N}}_1{⟧}_{\rho }^{\mathtt{G},\xi }$.

Parallel composition

An expression of the form ${\mathcal{N}}_1||{\mathcal{N}}_2$ for $\mu \mathcal{G}$ formulas ${\mathcal{N}}_1,{\mathcal{N}}_2$ is evaluated as the graph neural network $⟦{\mathcal{N}}_1||{\mathcal{N}}_2{⟧}_{\rho }^{\mathtt{G},\xi }$ that maps a node-labelling function $\eta$ to a new node-labelling function that maps a node $v$ to the tuple $⟨⟦{\mathcal{N}}_1{⟧}_{\rho }^{\mathtt{G},\xi }(\eta )(v),⟦{\mathcal{N}}_2{⟧}_{\rho }^{\mathtt{G},\xi }(\eta )(v)⟩$. Moreover, combining this operator with the basic function symbols ${\psi }_1,{\psi }_2,\dots \in \mathcal{S}$ allows the execution of $k$-ary operations on the node-labelling functions: a $k$-ary function application $f_{o{p}_k}({\mathcal{N}}_1,\dots ,{\mathcal{N}}_k)$ is expressible as the $\mu \mathcal{G}$ expression $((\dots ({\mathcal{N}}_1||{\mathcal{N}}_2)||\dots )||{\mathcal{N}}_k);o{p}_k$.

Choice

The choice operator $\mathtt{\text{if }}{\mathcal{N}}_1\mathtt{\text{ then }}{\mathcal{N}}_2\mathtt{\text{ else }}{\mathcal{N}}_3$ for $\mu \mathcal{G}$ formulas ${\mathcal{N}}_1,{\mathcal{N}}_2,{\mathcal{N}}_3$ is evaluated as the graph neural network $⟦{\mathcal{N}}_2{⟧}_{\rho }^{\mathtt{G},\xi }$ if ${\eta }^{\prime }=⟦{\mathcal{N}}_1{⟧}_{\rho }^{\mathtt{G},\xi }(\eta )$ is a node-labelling function such that $\mathrm{\forall }v\in \mathtt{G},{\eta }^{\prime }(v)=\mathtt{True}$. Otherwise it is evaluated as the graph neural network $⟦{\mathcal{N}}_3{⟧}_{\rho }^{\mathtt{G},\xi }$.

Fixed points

The fixed point operator is evaluated as the graph neural network that is obtained by applying $⟦{\mathcal{N}}_1{⟧}_{\rho }^{\mathtt{G},\xi }$ to the least fixed point of the functional $\mathcal{F}$ associated to $g$. Formally, it is $⨆\{{\mathcal{F}}^n\mid n\ge 0\}(⟦{\mathcal{N}}_1{⟧}_{\rho }^{\mathtt{G},\xi })$ where

$$\begin{array}{rl}& {\mathcal{F}}^0=\lambda \mathrm{\Phi }.\lambda \eta .\mathrm{\perp }\\ & {\mathcal{F}}^{n+1}=\mathcal{F}({\mathcal{F}}^n)\end{array}$$

---

1. Matteo Belenchia, Flavio Corradini, Michela Quadrini, and Michele Loreti. 2023. Implementing a CTL Model Checker with μG, a Language for Programming Graph Neural Networks. In Formal Techniques for Distributed Objects, Components, and Systems: 43^rd IFIP WG 6.1 International Conference, FORTE 2023, Held as Part of the 18^th International Federated Conference on Distributed Computing Techniques, DisCoTec 2023, Lisbon, Portugal, June 19–23, 2023, Proceedings. Springer-Verlag, Berlin, Heidelberg, 37–54. https://doi.org/10.1007/978-3-031-35355-0_4 ↩