New constructs for synchronization termed synchronization expressions (SEs) have been developed as high-level language constructs for parallel programming languages. We introduce a new family of languages named synchronization languages which we use to give a precise semantic description for SEs. Under this description, relations such as equivalence and inclusion between SEs can be easily understood and tested. In practice, it also provides us with a systematic way for the implementation as well as the simplification of SEs in parallel programming languages. We also show that each synchronization language is closed under the following rewriting rules: (1) a/sub s/b/sub s//spl rarr/b/sub s/a/sub s/, (2) a/sub t/b/sub t//spl rarr/b/sub t/a/sub t/, (3) a/sub s/b/sub t//spl rarr/b/sub t/a/sub s/, (4) a/sub t/a/sub s/b/sub t/b/sub s//spl rarr/b/sub t/b/sub s/a/sub t/a/sub s/ and also h(a/sub t/a/sub s/b/sub t/b/sub s/)/spl rarr/h(b/sub t/b/sub s/a/sub t/a/sub s/) for any morphism h that satisfies certain conditions which will be specified in the paper. We show that this property can be used to reduce the number of states of a finite automaton that describes a synchronization language.