Relations

A relation is a triplet (A,B,R) where A and B are sets and R⊆A×B. A function from A to B is a relation (A,B,f) where

(x1,y),(x2,y)∈f ⇒ x1=x2 and x∈A ⇒ ∃y∈B: (x,y)∈f.

Some definitions:

\ remove brackets of object at top of stack

: unfence zst> drop ;

: domain \ (A,B,R) -- A
  unfence zdrop zdrop ;

: codomain \ (A,B,R) -- B
  unfence zdrop znip ;

: rel \ (A,B,R) -- R
  unfence znip znip ;

The set of all elements in the codomain that is related to some element in the domain:

\ y∈image(R) ⇔ ∃x:(x,y)∈R

: image \ R -- s
  { foreach ?do unfence zst> zst> drop loop } ;

The set of all elements in the domain that is related to some element in the codomain:

\ x∈coimage(R) ⇔ ∃y:(x,y)∈R

: coimage \ R -- s
  { foreach ?do unfence zst> drop zst> loop } ;

The image of a relation restricted to a subset s of the domain:

: subimage \ R s -- s'
  zst yst setmove
  { foreach
  ?do unfence zst> zst> yst zst setcopy smember 0=
     if drop then
  loop } yst setdrop ;

The coimage of a relation restricted to a subset s of the codomain:

: subcoimage \ R s -- s'
  zst yst setmove
  { foreach
  ?do unfence zst> zst> yst zst setcopy swap smember 0=
     if drop then
  loop } yst setdrop ;

Test if a relation (A,B,R) is a function:

: func? \ -- flag | (A,B,R) --
  unfence znip
  zst yst setmove true
  begin zst@
  while zsplit zst> yst zst setcopy >zst zfence
     subimage cardinality 1 = 0=
     if 0= zdrop yst setdrop exit then
  repeat zdrop yst setdrop ;

Evaluate f(x):

: eval \ x -- y | f --
  >zst zfence subimage unfence zst> ;

Making a ordered pair or triplet of the top bundles:

: pair \ s1 s2 -- (s1,s2)
  zswap zst@ 2 - zswap zst@ 2 - + 1- >zst ;

: triplet \ s1 s2 s3 -- (s1,s2,s3)
  zrot zst@ 2 - zrot zst@ 2 - zrot zst@ 2 - + + 1- >zst ;

The composition of two relations (A,B,R) and (B,C,S) is the relation (A,C,SR) defined by

(a,c)∈SR ⇔ ∃b∈B:(a,b)∈R & (b,c)∈S.

: composition \ (A,B,R) (B,C,S) -- (A,C,SR)
  0 >xst                                \ empty set on xst-stack
  unfence zrot zdrop zrot unfence       \ C S A B R
  zst yst setmove zdrop zswap           \ C A S
  zst yst setmove                       \ R S in yst
  zswap zover zover cartprod            \ A C A×C
  begin zst@                            \ while elements in top set
  while zsplit infence
     yzcopy1 zover zsplit znip subcoimage
     zst xst setmove
     yzcopy2 zover zsplit zdrop unfence subimage
     xst zst setmove intersection zst@ zdrop
     if unfence unfence zst> unfence >zst -5 >zst zfence
        xst zst setmove zetmerge zst xst setmove
     else zdrop
     then
  repeat zdrop yst setdrop yst setdrop
  xst zst setmove triplet ;