Bandler and Kohout Products of Relations

There are multiple ways to compose relations

Sub Product

$\textbf{SubPrd} \; X \; Y \; Z \;R \; S := \{ \; x,z : xR \subseteq Sz \; \}$

---

$\textbf{Relation} \; X \; Y \; R$

$\textbf{Relation} \; Y \; Z \; S$

---

Notation.

1. $\textbf{SubPrd} \; X \; Y \; Z \; R \; S$ can be written $\textbf{SubPrd} \; R \; S$ when $X$, $Y$ and $Z$ are clear from the context.

2. $\textbf{SubPrd} \; R \; S$ can be written in symbols as $R \vartriangleleft S$.

---

fun SubPrd (X,Y,Z: set univ, R: X->Y, S: Y->Z) : X->Z {
  { x: X, z: Z | x.R in S.z }
}

Super Product

$\textbf{SupPrd} \; X \; Y \; Z \; R \; S := \{ \; x,z : xR \supseteq Sz \; \}$

---

$\textbf{Relation} \; X \; Y \; R$

$\textbf{Relation} \; Y \; Z \; S$

---

Notation.

1. $\textbf{SupPrd} \; X \; Y \; Z \; R \; S$ can be written $\textbf{SupPrd} \; R \; S$ when $X$, $Y$ and $Z$ are clear from the context.

2. $\textbf{SupPrd} \; R \; S$ can be written in symbols as $R \vartriangleright S$.

---

fun SupPrd (X,Y,Z: set univ, R: X->Y, S: Y->Z) : X->Z {
  { x: X, z: Z | S.z in x.R }
}

Square Product

$\textbf{SqrPrd} \; X \; Y \; Z \; R \; S := \{ \; x,z : xR = Sz \; \}$

---

$\textbf{Relation} \; X \; Y \; R$

$\textbf{Relation} \; Y \; Z \; S$

---

Notation.

1. $\textbf{SqrPrd} \; X \; Y \; Z \; R \; S$ can be written $\textbf{SqrPrd} \; R \; S$ when $X$, $Y$ and $Z$ are clear from the context.

2. $\textbf{SqrPrd} \; R \; S$ can be written in symbols as $R \diamond S$.

---

fun SqrPrd(X,Y,Z: set univ, R: X->Y, S: Y->Z) : X->Z {
  { x: X, z: Z | x.R = S.z }
}