Images of a set under a relation

Direct Image

R(A):={β€…β€Šy∈B:βˆƒ(x∈A::(x,y)∈R)β€…β€Š}R(A) := \{\; y \in B : \exists(x \in A :: (x,y) \in R) \; \}

Relationβ€…β€ŠXβ€…β€ŠYβ€…β€ŠR\textbf{Relation} \; X \; Y \; R

Includesβ€…β€ŠAβ€…β€ŠX\textbf{Includes} \; A \; X


Alloy provides syntax for the direct image. R(A)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 BKType\textbf{BKType}.

BKTypeβ€…β€ŠXβ€…β€ŠYβ€…β€ŠRβ€…β€ŠAβ€…β€Šy\textbf{BKType} \; X \; Y \; R \; A \; y

Relationβ€…β€ŠXβ€…β€ŠYβ€…β€ŠR\textbf{Relation} \; X \; Y \; R

AβŠ†XA \subseteq X

y∈Yy \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

SubDIβ€…β€ŠXβ€…β€ŠYβ€…β€ŠRβ€…β€ŠA:={β€…β€Šy∈Y:βˆ…βŠ‚AβŠ†Ryβ€…β€Š}\textbf{SubDI} \; X \; Y \; R \; A := \{\; y \in Y : \empty \subset A \subseteq Ry \; \}

Notation.

  1. SubDIβ€…β€ŠXβ€…β€ŠYβ€…β€ŠRβ€…β€ŠA\textbf{SubDI} \; X \; Y \; R \; A can be written SubDIβ€…β€ŠRβ€…β€ŠA\textbf{SubDI} \; R \; A when XX and YY are clear from the context.

  2. SubDIβ€…β€ŠRβ€…β€ŠA\textbf{SubDI} \; R \; A is written in symbols as R⊲(A)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

SupDIβ€…β€ŠXβ€…β€ŠYβ€…β€ŠRβ€…β€ŠA={β€…β€Šy∈Y:βˆ…βŠ‚RyβŠ†Aβ€…β€Š}\textbf{SupDI} \; X \; Y \; R \; A = \{\; y \in Y : \empty \subset Ry \subseteq A \; \}

Notation.

  1. SupDIβ€…β€ŠXβ€…β€ŠYβ€…β€ŠRβ€…β€ŠA\textbf{SupDI} \; X \; Y \; R \; A can be written SupDIβ€…β€ŠRβ€…β€ŠA\textbf{SupDI} \; R \; A when XX and YY are clear from the context.

  2. SupDIβ€…β€ŠRβ€…β€ŠA\textbf{SupDI} \; R \; A is written in symbols as R⊳(A)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

SqrIβ€…β€ŠXβ€…β€ŠYβ€…β€ŠRβ€…β€ŠA={β€…β€Šy∈Y:βˆ…βŠ‚A=Ryβ€…β€Š}\textbf{SqrI} \; X \; Y \; R \; A = \{\; y \in Y : \empty \subset A = Ry \; \}

Notation.

  1. SqrIβ€…β€ŠXβ€…β€ŠYβ€…β€ŠRβ€…β€ŠA\textbf{SqrI} \; X \; Y \; R \; A can be written SqrIβ€…β€ŠRβ€…β€ŠA\textbf{SqrI} \; R \; A when XX and YY are clear from the context.

  2. SqrIβ€…β€ŠRβ€…β€ŠA\textbf{SqrI} \; R \; A is written in symbols as Rβ‹„(A)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

SubDIβ€…β€ŠXβ€…β€ŠYβ€…β€ŠRβ€…β€ŠA:={β€…β€Šy∈Y:AβŠ†Ryβ€…β€Š}\textbf{SubDI} \; X \; Y \; R \; A := \{\; y \in Y : A \subseteq Ry \; \}

Notation.

  1. SubDIβ€…β€ŠXβ€…β€ŠYβ€…β€ŠRβ€…β€ŠA\textbf{SubDI} \; X \; Y \; R \; A can be written SubDIβ€…β€ŠRβ€…β€ŠA\textbf{SubDI} \; R \; A when XX and YY are clear from the context.

  2. SubDIβ€…β€ŠRβ€…β€ŠA\textbf{SubDI} \; R \; A is written in symbols as R⊲(A)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

SupDIβ€…β€ŠXβ€…β€ŠYβ€…β€ŠRβ€…β€ŠA={β€…β€Šy∈Y:AβŠ‡Ryβ€…β€Š}\textbf{SupDI} \; X \; Y \; R \; A = \{\; y \in Y : A \supseteq Ry \; \}

Notation.

  1. SupDIβ€…β€ŠXβ€…β€ŠYβ€…β€ŠRβ€…β€ŠA\textbf{SupDI} \; X \; Y \; R \; A can be written SupDIβ€…β€ŠRβ€…β€ŠA\textbf{SupDI} \; R \; A when XX and YY are clear from the context.

  2. SupDIβ€…β€ŠRβ€…β€ŠA\textbf{SupDI} \; R \; A is written in symbols as R⊳(A)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

SqrIβ€…β€ŠXβ€…β€ŠYβ€…β€ŠRβ€…β€ŠA={β€…β€Šy∈Y:A=Ryβ€…β€Š}\textbf{SqrI} \; X \; Y \; R \; A = \{\; y \in Y : A = Ry \; \}

Notation.

  1. SqrIβ€…β€ŠXβ€…β€ŠYβ€…β€ŠRβ€…β€ŠA\textbf{SqrI} \; X \; Y \; R \; A can be written SqrIβ€…β€ŠRβ€…β€ŠA\textbf{SqrI} \; R \; A when XX and YY are clear from the context.

  2. SqrIβ€…β€ŠRβ€…β€ŠA\textbf{SqrI} \; R \; A is written in symbols as Rβ‹„(A)R^{\diamond}(A)


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

Last updated