Images of a set under a relation

Direct Image

$R(A) := \{\; y \in B : \exists(x \in A :: (x,y) \in R) \; \}$

---

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

$\textbf{Includes} \; A \; X$

---

Alloy provides syntax for the direct image. $R(A)$ is written in Alloy as A.R

Images according to De Baets and Kerre

Typing

All images have the same basic type requirements, the details of which I will place in a predicate called $\textbf{BKType}$.

$\textbf{BKType} \; X \; Y \; R \; A \; y$

---

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

$A \subseteq X$

$y \in Y$

---

pred BKType(X,Y: set univ, R: univ->univ, A: set univ, y: univ) {
  R in X->Y
  A in X
  y in Y
}

Furthermore, I have chosen to extract the range of each set comprehension to its own (characteristic) predicate.

Sub-direct Image

$\textbf{SubDI} \; X \; Y \; R \; A := \{\; y \in Y : \empty \subset A \subseteq Ry \; \}$

---

Notation.

1. $\textbf{SubDI} \; X \; Y \; R \; A$ can be written $\textbf{SubDI} \; R \; A$ when $X$ and $Y$ are clear from the context.

2. $\textbf{SubDI} \; R \; A$ is written in symbols as $R^{\vartriangleleft}(A)$

---

fun SubDI(X,Y: set univ, R: univ->univ, A: set univ) : set univ {
  { y: Y | SubDI[X,Y,R,A,y] }
}

pred SubDI(X,Y: set univ, R: univ->univ, A: set univ, y: univ) {
  BKType[X,Y,R,A,y]

  some A
  A in R.y
}

Super-direct Image

$\textbf{SupDI} \; X \; Y \; R \; A = \{\; y \in Y : \empty \subset Ry \subseteq A \; \}$

---

Notation.

1. $\textbf{SupDI} \; X \; Y \; R \; A$ can be written $\textbf{SupDI} \; R \; A$ when $X$ and $Y$ are clear from the context.

2. $\textbf{SupDI} \; R \; A$ is written in symbols as $R^{\vartriangleright}(A)$

---

fun SupDI(X,Y: set univ, R: univ->univ, A: set univ) : set univ {
  { y: Y | SupDI[X,Y,R,A,y] }
}

pred SupDI(X,Y: set univ, R: univ->univ, A: set univ, y: univ) {
  BKType[X,Y,R,A,y]

  some R.y
  R.y in A
}

Square Image

$\textbf{SqrI} \; X \; Y \; R \; A = \{\; y \in Y : \empty \subset A = Ry \; \}$

---

Notation.

1. $\textbf{SqrI} \; X \; Y \; R \; A$ can be written $\textbf{SqrI} \; R \; A$ when $X$ and $Y$ are clear from the context.

2. $\textbf{SqrI} \; R \; A$ is written in symbols as $R^{\diamond}(A)$

---

fun SqrI(X,Y: set univ, R: univ->univ, A: set univ) : set univ {
  { y: Y | SqrI[X,Y,R,A,y] }
}

pred SqrI(X,Y: set univ, R: univ->univ, A: set univ, y: univ) {
  BKType[X,Y,R,A,y]

  some A
  A = R.y
}

Images according to Bandler and Kohout

Sub-direct Image

$\textbf{SubDI} \; X \; Y \; R \; A := \{\; y \in Y : A \subseteq Ry \; \}$

---

Notation.

1. $\textbf{SubDI} \; X \; Y \; R \; A$ can be written $\textbf{SubDI} \; R \; A$ when $X$ and $Y$ are clear from the context.

2. $\textbf{SubDI} \; R \; A$ is written in symbols as $R^{\vartriangleleft}(A)$

---

fun SubDI(X,Y: set univ, R: X->Y, A: set X) : set univ {
  { y: Y | A in R.y }
}

Super-direct Image

$\textbf{SupDI} \; X \; Y \; R \; A = \{\; y \in Y : A \supseteq Ry \; \}$

---

Notation.

1. $\textbf{SupDI} \; X \; Y \; R \; A$ can be written $\textbf{SupDI} \; R \; A$ when $X$ and $Y$ are clear from the context.

2. $\textbf{SupDI} \; R \; A$ is written in symbols as $R^{\vartriangleright}(A)$

---

fun SupDI(X,Y: set univ, R: X->Y, A: set X) : set univ {
  { y: Y | R.y in A }
}

Square Image

$\textbf{SqrI} \; X \; Y \; R \; A = \{\; y \in Y : A = Ry \; \}$

---

Notation.

1. $\textbf{SqrI} \; X \; Y \; R \; A$ can be written $\textbf{SqrI} \; R \; A$ when $X$ and $Y$ are clear from the context.

2. $\textbf{SqrI} \; R \; A$ is written in symbols as $R^{\diamond}(A)$

---

fun SqrI(X,Y: set univ, R: X->Y, A: set X) : set univ {
  { y: Y | A = R.y }
}