How to write a coequation

TL;DR

This paper reviews the diverse syntaxes for coequations in the literature, clarifying their definitions, uses, and relationships to promote their practical adoption in computer science.

Contribution

It categorizes four main syntaxes for coequations, providing a tutorial overview and clarifying their roles and interrelations.

Findings

Identified four types of coequation syntaxes

Clarified the purpose and differences of each syntax

Provided a unified perspective to facilitate practical use

Abstract

There is a large amount of literature on the topic of covarieties, coequations and coequational specifications, dating back to the early seventies. Nevertheless, coequations have not (yet) emerged as an everyday practical specification formalism for computer scientists. In this review paper, we argue that this is partly due to the multitude of syntaxes for writing down coequations, which seems to have led to some confusion about what coequations are and what they are for. By surveying the literature, we identify four types of syntaxes: coequations-as-corelations, coequations-as-predicates, coequations-as-equations, and coequations-as-modal-formulas. We present each of these in a tutorial fashion, relate them to each other, and discuss their respective uses.