程序设计语言的形式语义

1 - Mathematical Background

2019-09-27 10:00 CST
2019-09-30 00:12 CST
CC BY-NC 4.0

Set

Different notations:

  • $\mathcal{P}(S)$: powerset

Example 1. $A \cup B = \bigcup \{A, B\}$.

Proof. $\Rightarrow: A \cup B \subseteq \bigcup \{A, B\}.$

$\forall x \in A \cup B$, we have $x \in A$ or $x \in B$. By definition, $x \in \bigcup \{A, B\}$.

$\Leftarrow: \bigcup \{A, B\} \subseteq A \cup B$.

$\forall x \in \bigcup \{A, B\}, \exists T \in \{A, B\}, x \in T.$ Therefore $x \in A$ or $x \in B$.

Relations

Cartesian product $A \times B = \{(x, y) \vert x \in A, y \in B\}$.

Projections over pairs: $\pi_0(x, y) = x, \pi_1(x, y) = y$.

$\rho$ is a relation from $A$ to $B$ if $\rho \subseteq A \times B$, or $\rho \in \mathcal{P}(A \times B)$.

We say $\rho$ relates $x$ and $y$ if $(x, y) \in \rho$, written as $x \rho y$.

$\rho$ is an identity relation if $\forall (x, y) \in \rho, x = y$.

Equivalence Relations:

  • Reflexivity: $Id_S \subseteq \rho$.
  • Symmetry: $\rho^{-1} = \rho$.
  • Transitivity: $\rho \circ \rho \subseteq \rho$.

Function

A relation $\rho$ is a function if, for all $x, y$ and $y'$, $(x, y) \in \rho$ and $(x, y') \in \rho$ imply $y = y'$.

Variation

Variation of a function at a single argument:

$$f\{ x \leadsto n\} = \lambda z. \begin{cases} fz, & z \neq x, \\ n, & z = x. \end{cases}$$

Note that $x$ does not have to be in $\text{dom}(f)$ (domain of $f$).

$$\text{dom}(f\{x \leadsto n\}) = \text{dom}(f) \cup \{x\},$$ $$\text{ran}(f\{x \leadsto n\}) = \text{ran}(f - \{(x, n') | (x, n') \in f\}) \cup \{n\}.$$

Note: $\text{ran}(f\{x \leadsto n\}) \neq \text{ran}(f) \setminus \{n'\} \cup \{n\}.$

Function Types

$A \rightarrow B$ denotes the set of all function from $A$ to $B$. $\rightarrow$ is right associative.

$$A \rightarrow B \rightarrow C = A \rightarrow (B \rightarrow C).$$

Suppose $f \in A \rightarrow B \rightarrow C$, $a \in A$ and $b \in B$, then $f a b = (f(a))b \in C$.

Note: $f a b \neq f(a, b)$. $fa$ is a function of $B \rightarrow C$. They can be transformed by currying.

Products

$(x_0, \dots, x_{n-1})$ is called a $n$-tuple. $\pi_i(x_0, \dots, x_{n-1}) = x_i$.

Tuples as Functions

We can view a pair as a function $$\lambda i \in \textbf{2}. \begin{cases} x, & i=0, \\ y, & i = 1. \end{cases}$$

where $\textbf{2} = \{0, 1\}.$ Then we can redifine Cartesian products as $$A \times B = \{f | \text{dom}(f) = \textbf{2}, f0 \in A, f1 \in B\}.$$

Similarly, we can view a $n$-tuple as a function $$\lambda i \in \textbf{n}. \begin{cases} x_0, & i=0, \\ \dots & \dots \ x_{n-1}, & i = n-1. \end{cases}$$

where $\textbf{n} = \{0, 1, \dots, n-1\}.$ Then we can redifine $$S_0 \times \cdots \times S_{n-1} = \{f | \text{dom}(f) = \textbf{n}, \forall i \in \textbf{n}, f i \in S_i\}.$$

Generalized Products

Define $\Pi \theta$

$$\Pi \theta = \{ f \vert \text{dom}(f) = \text{dom}(\theta), \forall i \in \text{dom}(\theta), fi \in \theta i\}.$$

Example: $\theta = \lambda i \in \textbf{2}.\textbf{B}.$, then $\theta$ is a function from $\{0, 1\}$ to $\{T, F\}$.

$$\Pi \theta = \left\{\{(0, T), (1, T)\}, \{(0, T), (1, F)\}, \{(0, F), (1, T)\}, \{(0, F), (1, F)\}\right\}.$$

Note that $\textbf{B} \times \textbf{B} = \{(T, T), (T, F), (F, T), (F, F)\}$ by definition. There is a map between $\textbf{B} \times \textbf{B}$ and $\Pi \theta$.

Example 2: $\Pi \emptyset = \{\emptyset\}$.

Example 3: If $\exists i \in \text{dom}(\theta)$, $\theta i = \emptyset$, then $\Pi \theta = \emptyset$.

Exponentiation

If $S$ is independent of $x$,

$$S^T = \prod\limits_{x \in T} S = \Pi (\lambda x \in T.S) = (T \rightarrow S)$$

$S^T$ is the set of all functions from $T$ to $S$.

The powerset of $S$, $\mathcal{P}(S) = 2^S = (S \rightarrow \textbf{2})$.

Sums (Disjoint Unions)

To define the disjoint union of $A$ and $B$, we need to index the elements according to which set they originated in.

$$A+B = \{(i, x) | (i=0 \wedge x \in A) \vee (i=1 \wedge x \in B)\}.$$

Injection operations ($\iota$, iota):

$$\iota_{A+B}^0 \in A \rightarrow (A+B)$$ $$\iota_{A+B}^1 \in A \rightarrow (A+B)$$

The disjoint union can be generalized to $n$ sets:

$$S_0 + \cdots + S_{n-1} = \{ (i, x) | i \in \textbf{n} \wedge x \in S_i \}.$$

Define $\Sigma \theta$ as

$$\Sigma \theta = \{(i, x) | i \in \text{dom}(\theta), x \in \theta i\}$$

Example 1: $\sum\limits_{i \in \textbf{n}} S(i) = \Sigma \left(\lambda i \in \textbf{n}.S(i)\right).$

Example 2. Let $\theta = \lambda i \in \textbf{2}.\textbf{B}$. Then $$\Sigma \theta = \{ (0, T), (0, F), (1, T), (1, F) \} = \textbf{2} \times \textbf{B}.$$

Example 3. $\Sigma \emptyset = \emptyset$.

Example 4. If $\forall i \in \text{dom}(\theta)$, $\theta i = \emptyset$, then $\Sigma \theta = \emptyset$.

Example 5. Let $\theta = \lambda i \in \textbf{2}. \begin{cases} \textbf{B}, & i = 0, \\ \emptyset, & i = 1. \end{cases}$, then $\Sigma \theta = \{(0, T), (0, F)\}.$

If $S$ is independent of $x$, then

$$\sum\limits_{x \in T} S = \Sigma (\lambda x \in T.S) = (T \times S).$$