LARA

Products of Lattices

Lattice elements can be combined into finite or infinite-dimensional vectors, and the result is again a lattice.

Lemma: Let $(A_1,\le_1), \ldots, (A_n, \le_n)$ be partial orders. Define $(L,\le)$ by

\begin{equation*}
    A = \{ f.\  f : \{1,\ldots,n\} \to (A_1 \cup \ldots \cup A_n) \mbox{ where } \forall i. f(i) \in A_i \}
\end{equation*}

For $f,g\in A$ define

\begin{equation*}
    f \leq g   \iff   \forall i. f(i) \le_i g(i)
\end{equation*}

Then $(A,\le)$ is a partial order. We denote $(A,\le)$ by

\begin{equation*}
   \prod_{i=1}^n (L_i,\le_i)
\end{equation*}

Moreover, if for each $i$, $(A_i,\le_i)$ is a lattice, then $(A,\le)$ is also a lattice.

Note: for $n=2$ a function $f : \{1,2\} \to (L_1 \cup L_2)$ with $f(1) \in L_1$, $f(2) \in L_2$ is isomorphic to an ordered pair $(f(1),f(2))$. We denote the product by $(L_1,\le_1) \times (L_2,\le_2)$.

Example: Let $R=\{a,b,c,d\}$ denote set of values. Let $A_1 = A_2 = 2^R$. Let

\begin{equation*}
   s_1 \leq_1 s_2 \iff  s_1 \subseteq s_2
\end{equation*}

and let

\begin{equation*}
   t_1 \leq_2 t_2 \iff  t_1 \supseteq t_2
\end{equation*}

Then we can define the product $(A_1,\le_1)\times (A_2,\le_2)$. In this product, $(s_1,t_1) \le (s_2,t_2)$ iff: $s_1 \leq s_2$ and $t_1 \supseteq t_2$. The original partial orders were lattices, so the product is also a lattice. For example, we have

\begin{equation*}
    (\{a,b,c\},\{a,b,d\}) \sqcap (\{b,c,d\},\{c,d\}) = (\{b,c\}, \{a,b,c,d\})
\end{equation*}

Collecting Semantics as example of products, fixpoints.