 Of course, many other program constructors can be used. Among them, one worthy of mention is that for the  converse  of a given relation. Modalities for the converse of a relation have been used in, e.g.,  tense logic,  with the ‘past’ modalities (H and P, the universal and existential versions, respectively) interpreted semantically in terms of the converse of the relation used for interpreting the ‘future’ modalities (G and F, respectively).