# Mathematical Preliminaries
## 2.1 Sets, Relations, and Functions
### 2.1.1
$\{ 1, 2, 3 \}$
$\{ x \in S | \ldots \}$
$\emptyset$ 空集合
$S \setminus T$ 差集合
$|S|$ 集合のサイズ
$\mathcal{P}(S)$ $S$のべき集合
### 2.1.2
$\mathbb{N}$ 自然数の集合、0を含む
$\mathbb{N}$ と1対1に対応する集合のことを可算集合と呼ぶ
### 2.1.3
$S \times T = \{(s, t) |~s \in S,~t \in T \}$
$R\subseteq S_1 \times S_2 \times \dots \times S_n$
$(s_1, \dots, s_n)\in R$のとき、「$s_1$から$s_n$は$R$によって関係付けられている」と言う
### 2.1.4
$P \subseteq S$ のときは $P$ は $S$ における述語といい、$s \in P$ のとき $P$ は $s$ について真であるという。
$P: S \rightarrow \{ \text{true}, \text{false} \}$ とみなす事もできる
($P(s) = (s \in P かどうか)$ とすればよい)
### 2.1.5
$R \subseteq S \times T$ のときは $R$ を二項関係とよび、$(s, t) \in R$ のことを $s R t$ と書く。
### 2.1.6
$\Gamma \vdash \mathtt{s}:T$ は型付け規則だが、このような形で三項関係$(\Gamma, \mathtt{s}, T)$が成り立つという意味で使うことがある
### 2.1.7
集合 $S$ と $T$ の上の二項関係 $R$ に対し、 $dom(R) = \{ s \in S ~|~ ^\exists t \in T ~~ (s, t) \in R \}$
$\mathit{range}(R) = \{ t \in T ~|~ ^\exists s \in S ~~ (s, t) \in R \}$
とする
### 2.1.8
集合 $S$ と $T$ 上の二項関係 $R$ は、以下を満たすときに partial function と呼ばれる:
$\forall s \in S, (s, t_1) \in R かつ (s, t_2) \in R \implies t_1 = t_2$
(任意のsに対して、対応する t が高々1つしか存在しない)
さらに $R$ が $dom(R) = S$ を満たすときは total (全域) function と呼ばれる
### 2.1.9
$S$から$T$へのPartial function $R$ に対して、
$s \in dom(R)$ のとき $R$ は $s$ に対して定義されているという。
$s \not\in dom(R)$のとき、$R$ は $s$に対して定義されていないという。
$f$ が $x$ に対して未定義のとき、$f(x) ~=~ \uparrow$ と書く。
$f$ が $x$ に対して定義されているとき、 $f(x)\downarrow$ と書く。
$f$ が入力 $x$ に対して失敗を返すとき、 $f(x) ~=~ \mathit{fail}$ と書く。
### 2.1.10
$R$ が $S$ 上の二項関係で、$P$ が $S$ 上の述語であるとき、以下が満たされる時に $R$ は $P$ を保存するという:
$s R s' \wedge P(s) \implies P(s')$
## 2.2 Ordered Sets (順序集合)
### 2.2.1
集合 $S$ 上の二項関係 $R$ について、
$\forall s \in S$ に対し $s R s$ が成り立つ時、 「$R$ は反射的である」と言う。
$S$ 中の全ての $s$ と $t$ に対して、
$s R t \implies t R s$ が成り立つとき、「$R$ は対称的である」と言う。
$s R t \wedge t R u \implies s R u$ が成り立つとき、 「$R$ は推移的である」と言う。
$s R t \wedge t R s \implies s = t$ が成り立つとき、「$R$ は反対称的である」と言う。
### 2.2.2
集合$S$上の関係$R$が反射的で、かつ推移的である時、$R$を$S$上の前順序(まえじゅんじょ)と呼ぶ。
*(一般的には「ぜんじゅんじょ」と読むはずだが、全順序と区別するためにこの会では「まえじゅんじょ」と読むことにする)*
前順序は$\leq$や$\sqsubseteq$で表す。
$(s \leq t) \wedge (s \not= t)$ のことを $s \lt t$ と書く。
反対称律を満たす前順序のことを半順序という。
半順序で、$\forall s, t \in S$ に対し $s \leq t \vee t \leq s$ が成り立つものを全順序という。
### 2.2.3
$\leq$が集合$S$上の半順序関係で、$s, t \in S$とする。
以下の条件を満たす要素$j \in S$は結び(あるいは最小上界)である
1. $s \leq j \wedge t \leq j$
2. $\forall k \in S\ ((s \leq k \wedge t \leq k) \implies j \leq k)$
同様に、上記に登場するすべての $\leq$ の両辺を入れ替えたものを交わり(あるいは最大下界)と呼ぶ。
[参考: 順序集合 と 束](https://www.hongo.wide.ad.jp/~jo2lxq/dm/lecture/03.pdf)
### 2.2.4
反射的で、推移的で、対称的な関係のことを同値関係と呼ぶ。
### 2.2.5
$R$を集合$S$上の二項関係とする。反射閉包$R$は$R$を含む最も小さい反射関係$R'$である。
(ここで「最も小さい」とは、もし$R''$が他の反射的関係で$R$に含まれるペアを含んでいるものであったら、$R'\subseteq R''$であることである。)
同様に、$R$の推移閉包とは、$R$を含む最も小さい推移的関係のことである。$R^+$と書かれる。
$R$の反射推移閉包とは、$R$を含む最も小さい反射的で推移的な関係である。$R^*$と書かれる。
(例)
$S=\{A, B, C\}$
$R=\{(A, B), (B, C)\}$
$R'=\{(A, B), (B, C), (A, A), (B, B), (C, C)\}$
$R^+=\{(A, B), (B, C), (C, A)\}$
$s = A$
$sRs \equiv (s, s) \in R$
$(A, A)$
### 2.2.6
$S$ 上の関係 $R$ が与えられたとする。このとき、関係 $R'$ を以下のように定義する:
$R' = R \cup \{(s, s) ~|~ s \in S \}$
$R'$ が $R$ の反射的閉包であることを示せ。
---
定義より $R \subseteq R'$で、$R'$は反射的である
$R'$ が最小であることを言えれば良い。
$R''$ が $R$ を含む反射的な関係であるとする。このとき、 $R' \subseteq R''$ であることを示そう。
すなわち、 $(s, t) \in R' \implies (s,t) \in R''$ を示せば良い。
$(s, t) \in R' = R \cup \{(s,s) ~|~ s \in S\}$ とする。
- $(s, t) \in R$ のとき
- 仮定から $(s, t) \in R \subseteq R''$ すなわち $(s, t) \in R''$
- $(s, t) \in \{(s,s) ~|~ s \in S\}$ のとき
- このときは $s = t$ 。$R''$ は反射的だったので $(s, t) = (s, s) \in R''$
### 2.2.7
関係$R$の推移的閉包のより構成的な定義がある。
はじめに、以下のペアの集合の列を定義する。
- $R_0 = R$
- $R_{i+1} = R_i \cup \{(s, u) ~|~ ^\exists t, (s, t) \in R_i \wedge (t, u) \in R_i\}$
すなわち、$R_i$に含まれる全てのペアから推移的に得られるペアを全て$R_i$に加えることで$R_{i+1}$を構成する。
最後に、全ての $R_i$ の和集合として関係$R^+$を定義する:
$$R^+ = \bigcup_{i}{R_i}$$
このとき、 $R^+$ が $R$ の推移的閉包であることを示せ。
(例)
$S = \{a, b, c, d, e\}$
$R_0 = R = \{(a, b), (b, c), (c, d), (d, e)\}$
$R_1 = \{(a, b), (b, c), (c, d), (d, e), (a,c), (b,d),(c,e) \}$
$R_2 = \{(a, b), (b, c), (c, d), (d, e), (a,c), (b,d),(c,e),(a,d), (b,e), (a,e) \}$
(補足)
$$R^+ = \bigcup_{i \in \mathbb{N}} R_i$$
というのは、
$x \in R^+ \iff ^\exists i \in \mathbb{N}, \ x \in R_i$ ということである。
---
まず $R^+$ が推移的であることを示さなければならない。すなわち
$(s, t) \in R^+ \wedge (t, u) \in R^+ \implies (s, u) \in R^+$ を示そう。
$(s, t) \in R^+ \wedge (t, u) \in R^+$ とする。このとき、
$^\exists i \ (s, t) \in R_{i}$ および $^\exists j \ (t, u) \in R_{j}$ が成り立つ。この $i$ と $j$ に対し、 $k = \max(i, j) + 1$ とすれば $(s, u) \in R_k$ である。
($a \leq b \implies R_a \subseteq R_b$ なので、 $(s, t) \in R_i \subseteq R_{\max(i, j)}$ であり $(t,u) \in R_j \subseteq R_{\max(i, j)}$ である。よって $(s, u) \in R_{\max(i, j)+1} = R_k$ となる)
次に、 $R \subseteq R'' \wedge (R'' が推移的) \implies R^+ \subseteq R''$ であることを示せばよい。
$R \subseteq R'' \wedge (R'' が推移的)$ であるとする。このとき $R^+ \subseteq R''$ であることを示したい。そのために、
$\forall i \in \mathbb{N} \ R_i \subseteq R''$ を、$i$ に関する帰納法で示そう。
まず $R_0 = R \subseteq R''$ である。
次に、$R_i \subseteq R'' \implies R_{i+1} \subseteq R''$ であることを示す。
$R_i \subseteq R''$ のとき、 $\forall (s, u) \in R_{i+1} = R_i \cup \{(s, u) ~|~ ^\exists t, (s, t) \in R_i \wedge (t, u) \in R_i\}$ に対し、
- $(s, u) \in R_i$ のとき
- 帰納法の仮定から、$(s, u) \in R_i \subseteq R''$
- $(s, u) \in \{(s, u) ~|~ ^\exists t, (s, t) \in R_i \wedge (t, u) \in R_i\}$ のとき
- ある $t$ が存在して $(s, t) \in R_i \subseteq R''$ かつ $(t,u) \in R_i \subseteq R''$ となる
- $R''$ は推移的なので、 $(s,t) \in R''$ 及び $(t, u) \in R''$ から $(s, u) \in R''$ が成り立つ。
### 2.2.8
$R$ を集合 $S$ における二項関係、 $P$ を $R$ によって保存される、集合 $S$ における述語と仮定する。
$P$ が $R^*$ でも保存されることを示せ。
---
(2.2.5 $R^*$ は $R$ の反射推移閉包)
(2.1.10 より、「$P$ が$R$によって保存される」とは $(s,t)\in R \wedge P(s) \implies P(t)$ ということである)
まず $R^* = R'^+$ であることを示す。
$R'^+$ が $R$ の反射推移閉包であることを示せば良い。
- $R \subseteq R' = R_0 \subseteq R'^+$ より $R \subseteq R'^+$
- $R'^+$ が反射的であることは、 $R'=R \cup \{(s,s) ~|~ s \in S\}$ 及び $R' \subseteq R'^+$ から分かる。
- $R'^+$ が推移的であることは定義より明らか。
- 最小性を示す。
- $Q$ が $R$ を含み、反射的で推移的であるとする。このとき $R'^+ \subseteq Q$ であることを示せば良い。
- $R_i$ の $i$ に対する帰納法で、 $R_i \subseteq Q$ であることを示す。
- $R' = R_0 \subseteq Q$ は、$Q$ が反射的であることから、$R'$の最小性により従う。
- $R_i \subseteq Q$ だったとき、 $R_{i+1} \subseteq Q$ となることは 2.2.7 と同様の議論から従う。
以上から、 $R'^+$ が$R$の反射推移閉包であることが言えた。
$P$ が $R^* = R'^+$ で保存されることを示そう。
そのために、$R_i$ が $P$ を保存することを $i$ に関する帰納法で示す。
- $i=0$ のとき
- $R_0 = R' = R \cup \{(s,s) ~|~ s \in S\}$ なので、以下の2通りになる:
- $(s,t) \in R$ のとき
- 問題の仮定より、$P(s)$ であれば $P(t)$ が成り立つ。
- $(s,t) \in \{(s,s) ~|~ s \in S\}$ のとき
- このときは $s = t$ なので、$P(s)$ ならば $P(t)$ が成り立つ。
- $R_i$ が $P$ を保存するとき
- $R_{i+1} = R_i \cup \{(s, u) ~|~ ^\exists t, (s, t) \in R_i \wedge (t, u) \in R_i\}$ であった。従って以下の2通りになる:
- $(s,t) \in R_i$ のとき
- $R_i$ は $P$ を保存するので、 $P(s)$ ならば $P(t)$ が成り立つ。
- $(s,t) \in \{(s, u) ~|~ ^\exists t, (s, t) \in R_i \wedge (t, u) \in R_i\}$ のとき
- $^\exists r \in S$ によって $(s, r) \in R_i \wedge (r, t) \in R_i$ となる
- $R_i$ は $P$ を保存し、$(s,r) \in R_i$ なので、$P(s)$ ならば $P(r)$ が成り立つ。
- $R_i$ は $P$ を保存し、$(r,t) \in R_i$ なので、 $P(r)$ ならば $P(t)$ が成り立つ。
- 上記2つより、 $P(s)$ ならば $P(t)$ が成り立つ。
以上から、$\forall i \in \mathbb{N}$ に対して $R_i$ は $P$ を保存する。
従って、$R'^+=R^*$ は $P$ を保存する。
### 2.2.9
$S$ 上に前順序 $\leq$ があったとする。**降下列**とは、$s_1, s_2, s_3,...$ という$S$ の元の列であり、全ての $i$ に対して $s_{i+1} \lt s_i$ となっているもののことである。
(列は有限列でも無限列でも構わない)
### 2.2.10
$S$上になんらかの前順序$\leq$があったとする。これが無限の降下列を持たないとき、この$\leq$を **well founded (整礎)** と言う。
例えば自然数の集合における通常の順序は well founded である。
しかしながら整数の集合における通常の順序は well founded ではない。
(参考: https://ja.wikipedia.org/wiki/%E6%95%B4%E7%A4%8E%E9%96%A2%E4%BF%82)
## 2.3 Sequences
### 2.3.1
Sequence はその要素をカンマ区切りで並べることで書かれる。
カンマは列の最初に要素を加える "cons" としても、列の最後に要素を加えるものとしても、列を結合する "append" としても使われる。
(参考: cons means "constructs memory objects" https://en.wikipedia.org/wiki/Cons)
例えば a が 3,2,1 という列で、 b が 5,6 という列だったとき、
- 0,a は 0,3,2,1 という列を表す
- a,0 は 3,2,1,0 という列を表す
- b,a は 5,6,3,2,1 という列を表す
(この記法は、「列の列」というものが登場しない限りは混乱を招かない)
1 から n までの数の列を 1..n と書く。
$|a|$ は $a$ の長さを表す。
空の列は・または空白で表す。
ある列が別の列の並べ替え(permutation)であるというのは、順番が違うかもしれないが同じ要素を含むということである。
## 2.4 Induction
### 2.4.1 公理: 自然数における通常の帰納法の原則
$P$を自然数における述語と仮定する。このとき:
$P(0)$ かつ
$\forall i \ (P(i) \implies P(i+1))$ のとき
$\forall n \ P(n)$ が成り立つ
### 2.4.2 公理: 自然数における完全帰納法の原則
$P$を自然数における述語とする。このとき:
$\forall n \ ((\forall i < n \ P(i)) \implies P(n))$
が成り立てば、
$\forall n \ P(n)$ が成り立つ
### 2.4.3 定義:
自然数の対に対する**辞書式順序**は次のように定義される
$(m, n) \leq (m', n') \iff (m < m' \vee (m = m' \wedge n \leq n'))$
例えば
$(1, 2) \leq (3, 1)$
$(2, 3) \leq (2, 4)$
### 2.4.4 公理: 辞書順帰納法の原則
$P$ が自然数の対における述語であると仮定する。
$\forall (m, n) \ ((\forall (m', n') < (m, n) \ P(m', n')) \implies P(m, n))$
が成り立つとき、
$\forall (m, n) \ P(m, n)$
## 2.5 Background Reading
関さんおすすめ本:https://www.amazon.co.jp/%E9%9B%86%E5%90%88%E3%83%BB%E4%BD%8D%E7%9B%B8%E5%85%A5%E9%96%80-%E6%9D%BE%E5%9D%82-%E5%92%8C%E5%A4%AB/dp/4000054244
3章: https://hackmd.io/Ob2QAK2HQs2pEDBZT4Eyyg