Alphabetised Relational Calculus

The core of the UTP is the alphabetised relational calculus which acts as a lingua franca for denotational semantics of programming and modelling languages. The relational calculus combines typical predicate calculus operators, such as Boolean connectives, with binary relation algebra operators such as sequential composition and if-then-else conditional. The main type for relations is $(\alpha,\beta)\,urel$, where $\alpha$ and $\beta$ are the input and output alphabet types, respectively. This is synonymous with the alphabetised predicate $(\alpha \times \beta)\,upred$, that is the alphabet is a produce type. There is also $\alpha\,hrel$ when a homogeneous relation is required. Conditions can be expressed using predicate operators.

The main operators of the mechansied relational calculus and their types are give below.

• Sequential composition: P ;; Q, for P :: (α, β) urel and Q :: (β, γ) rel
• Conditional (infix if-then-else): P ◃ b ▹ Q, for P, Q :: (α,β) rel and b :: α upred
• Assignment: ⟨σ⟩ :: α hrel, for σ :: α ⇒ α
• Identity (skip): II :: α hrel
• Universal relation: true :: (α,β) rel
• Empty relation: false :: (α,β) rel
• Weakest fixed-point: μX∙ F(X), for F :: (α, β) rel ⇒ (α, β) rel