Operation on relation – what is it called?

67 Views Asked by At

Given two binary relations $R_1 \subseteq X \times X$ and $R_2 \subseteq Y \times Y$, I can define the following binary relation on $X \times Y$: $$ R_1 \stackrel?\otimes R_2 := \{ ((x,y),(x,y')) \mid x \in X, y R_2y'\} \cup \{ ((x,y),(x',y)) \mid xR_1x', y \in Y\} $$

How is this operations on binary relations usually called?

For some intuition: Let $X$ and $Y$ be the set of expressions in the lambda calculus and both $R_1$ and $R_2$ be $\stackrel\beta\to$, the reduction of one redex anywhere in the term. Then we can use the operator above to calculate the one-step reductions of an application (assuming the application is not a redex on its own): $$ e_1 e_2 \stackrel\beta\to e_1' e_2' \iff (e_1, e_2) (\stackrel\beta\to \stackrel?\otimes \stackrel\beta\to) (e_1', e_2'). $$

1

There are 1 best solutions below

1
On BEST ANSWER

In graph-theoretic terms, this is the cartesian product of graphs.

It is not identical to what is usually called the "cartesian product of relations", though.