I have the need to define a multi-component object type for which I provide numerous definitions throughout the text. However, in most of these definitions, I only need to refer to one or two of the components constituting the object type. Therefore, I am looking for a widely used notation that allows to quickly refer to only a single component of the object type without having to introduce the entire object.
I have identified four possible notations for defining multi-component objects. which I do introduce below using the object type transition system as an example. The first notation is the classical one where the object type is defined as a tuple. The drawback of this definition is that anytime that I want to express properties on the object type I need to re-introduce the entire tuple. The other three notations (2-4) avoid this issue, but I am not sure whether they are widely used and accepted.
Here are a few options
A transition system $TS$ is a tuple $(S,\Sigma,\delta, s_0)$ where
- $S$ is a set of states
- $\Sigma$ is a set of Actions
- $\delta \subseteq S \times \Sigma \times S$ is the state transition relation
- $s_0 \in S$ is the initial state
Usage example
A transition systems $TS = (S,\Sigma,\delta, q_0)$ is finite if $S$ is finite
A transition system $TS$ is consists of
- a set of states $S(TS)$
- a set of actions $\Sigma(TS)$
- a transittion relation $\delta(TS) \subseteq S(TS) \times \Sigma(TS) \times S(TS)$
- the initial state $s_0(TS) \in S(TS)$
Usage example
A transition systems $TS$ is finite if $S(TS)$ is finite
A transition system $TS$ is consists of
- a set of state $S^{TS}$
- a set of action $\Sigma^{TS}$
- the transition relation $\delta^{TS} \subseteq S^{TS} \times \Sigma^{TS} \times S^{TS}$
- the initial state $s_0^{TS} \in S^{TS}$
Usage example
A transition systems $TS$ is finite if $S^{TS}$ is finite
A transition system $TS$ is consists of
- a set of states $TS.S$
- a set of actions $TS.\Sigma$
- a transittion relation $TS.\delta \subseteq TS.S \times TS.\Sigma \times TS.S$
- the initial state $TS.s_0 \in TS.S$
Usage example
A transition systems $TS$ is finite if $TS.S$ is finite