# Data Synchronization: A Complete Theoretical Solution for Filesystems
## 3 Definitions
### Internal Filesystem Commands  
The synchronizer operates using a specially designed and highly symmetrical set of _internal filesystem commands_. They each modify the filesystem at a single node only, and contain additional information usually not thought of as part of a command which allows them to be inverted, and makes them amenable to algebraic manipulation. Inventing such a command set was one of the main contributions of [18]. The commands basically implement creating and deleting files and directories. Modifying a part of a file only is not available as a command; whenever a file is modified, the new content must be supplied in its entirety. Still, commands issued by a real-life user or system can be easily transformed into the internal commands; for example, the _move_ or _rename_ operation can be modeled as a sequence of a _delete_ and a _create_. The set of the internal commands is denoted by \(\Omega\), and each command \(\sigma\in\Omega\) has three components, written as \(\sigma=\langle n,x,y\rangle\), as follows:  
* \(n\in\mathbb{N}\) is the node on which the command acts,
* \(x\) is the content at node \(n\) before the command is executed (precondition), and
* \(y\) is the content at node \(n\) after the command was executed. Thus \(rndir(n)\) corresponds to the internal command \(\langle n,\mathbb{D},\mathbb{O}\rangle\), which replaces the directory value at \(n\) by the empty value. The command \(\langle n,\mathbb{O},\mathbb{D}\rangle\) creates a directory at \(n\), but only if the node \(n\) has no content, i.e., there is no directory or file at \(n\) (a usual requirement for \(mklir(n)\)). For files \(\mathfrak{f}_{1}\) and \(\mathfrak{f}_{2}\in\mathbb{F}\) the command \(\langle n,\mathfrak{f}_{1},\mathfrak{f}_{2}\rangle\) replaces \(\mathfrak{f}_{1}\) stored at node \(n\) by the new content \(\mathfrak{f}_{2}\). This latter command can be considered to be an equivalent of \(edit(n,\mathfrak{f}_{1},\mathfrak{f}_{2})\). Applying \(\sigma\in\Omega\) to a filesystem \(\Phi\) is written as the left action \(\sigma\Phi\). The command \(\sigma=\langle n,x,y\rangle\) is _applicable_ to \(\Phi\) if  
* \(\Phi\) contains \(x\) at the node \(n\), that is, \(\Phi(n)=x\), and
* after changing the content at \(n\) to \(y\) the filesystem still has the tree property. If \(\sigma\) is not applicable to \(\Phi\) then we say that \(\sigma\)_breaks_ the filesystem, and write \(\sigma\Phi=\bot\). If \(\sigma\) does not break \(\Phi\), then \(\sigma\Phi\) is the filesystem where every node has the same value as in \(\Phi\) except for the node \(n\) where the new content is \(y\). Command sequences are applied from left to right, thus \((\sigma\alpha)\Phi=\alpha(\sigma\Phi)\). The composition of sequences \(\alpha\) and \(\beta\) is written as \(\alpha\beta\); occasionally we write it as \(\alpha\circ\beta\) to emphasize that \(\beta\) is to be executed after \(\alpha\). A sequence breaks \(\Phi\) if one of its commands is not applicable. More formally, \(\sigma\alpha\) breaks \(\Phi\) if either \(\sigma\) breaks \(\Phi\), or \(\alpha\) breaks \(\sigma\Phi\). Two additional commands will be used, which are denoted by \(\epsilon\) and \(\lambda\), respectively. In practice they do not occur, and cannot be elements of command sequences, but are useful in algebraic derivations. The command \(\epsilon\) breaks every filesystem, while \(\lambda\) acts as identity: \(\epsilon\Phi=\bot\) and \(\lambda\Phi=\Phi\) for every filesystem \(\Phi\). The command sequences \(\alpha\) and \(\beta\) are _semantically equivalent_, written as \(\alpha\equiv\beta\) if they have the same effect on all filesystems: \(\alpha\Phi=\beta\Phi\) for all \(\Phi\). We write \(\alpha\sqsubseteq\beta\) to denote that \(\beta\)_semantically extends_\(\alpha\), that is, \(\alpha\Phi=\beta\Phi\) for all filesystems that \(\alpha\) does not break. Clearly, \(\alpha\equiv\beta\) if and only if both \(\alpha\sqsubseteq\beta\) and \(\beta\sqsubseteq\alpha\).