論理と計算のしくみ

1 集合と関係

章末問題の解答全部にあるわけじゃないんやね

2 命題論理と述語論理

命題論理（propositional logic）

排中律や背理法のような命題を単位とする推論を形式化した論理
内部構造までには立ち入らない

命題（proposition）

正しいか間違っているかのどちらかになる（はず）の主張
真偽値（truth value）
- 真（true）[$\top$]または偽（false）[$\bot$]のこと
  - Trueの$\top$ と考えるとわかりやすい
- 正しい命題では真、間違った命題では偽となる
  - 命題を$P$として、正しい命題は$P=\top$、間違った命題は$P=\bot$となる
（命題論理の意味論では）真偽値の等しい命題は互いに等しいと扱う

論理記号（logical symbol）

簡単な命題から複雑な命題を作るための接続詞的なもの
連言（conjunction）
- $P \land Q$ （$P$かつ$Q$）
- どちらの命題も真であるとき、かつそのときに限り真
- 可換則、結合則、分配則が成り立つ
選言（disjunction）
- $P \lor Q$ （$P$または$Q$）
- どちらかの命題が真であるときに、かつそのときに限り真
- 連言より結合力が弱い
- 可換則、結合則、分配則が成り立つ
否定（negation）
- $\neg P$ （$P$でない）
- 命題が間違っているとき、かつそのときに限り真
- ド・モルガン則（de Morgan’s law）
  - $\neg (P \land Q) = \neg P \lor \neg Q$
  - $\neg (P \lor Q) = \neg P \land \neg Q$
含意（implication）
- $P \supset Q$ （$P$ならば$Q$）
  - $Q$は$P$の結論であることを表す
- もし$P$が真なら$Q$、それ以外なら真
  - if P then Q else True と考える
- $P \supset Q = \neg P \lor Q$が成り立つ
- 連言、選言より結合力が弱い
- 右結合である
同値命題（equivalence）
- $P \leftrightarrow Q$ （$P$ならば$Q$であり、$Q$ならば$P$である）
- $P$と$Q$がともに真、もしくは偽のとき、かつそのときに限り真
- $P \leftrightarrow Q = (P \supset Q) \land (Q \supset P)$が成り立つ
- 含意より結合力が弱い
排他的選言（exclusive disjunction）
- $P \oplus Q$
- 同値命題の否定
- $P$が真で$Q$が偽、もしくは$P$が偽で$Q$が真のとき、かつそのときに限り真
- $P \oplus Q = (P \land \neg Q) \lor (\neg P \land Q)$が成り立つ

構文論（syntax）

命題論理の論理式がどのように構成されるか
命題記号（propositional symbol）
- 命題を表す記号
- 原子論理式（atomic formula）とも言う
論理式（formula）・命題論理式（propositional formula）
- 命題記号、真偽値、論理記号を組み合わせて作られる命題
- 論理式のBNF記法的表現
```
$$
A ::= \top | \bot | P | \neg A | A \land A | A \lor A | A \supset A
$$
```
- 木構造である
- 帰納的に定義される（inductive definition）
構文論においては異なる木構造を持つ論理式は異なると扱う
- $P \land Q$と$Q \land P$は異なる
- $\neg P \land Q$と$(\neg P) \land Q$は括弧のスタイルが異なるだけなので同じ
  - 木構造としては同じなのでね
構文的に等しい論理式を$\equiv$と表す

意味論（semantics）

命題論理の論理式がどのように解釈されるか
解釈（interpretation）
- 命題記号に真偽値を対応させる関数
  - $I$を解釈とすると、$I \in \mathbb{B}^\mathbb{P}$、すなわち$I:\mathbb{P} \rarr \mathbb{B}$である
$\llbracket A \rrbracket_I$によって解釈$I$の元での論理式$A$を表す
恒真（valid）・トートロジ（tautology）
- 任意の解釈のもとで、$\llbracket A \rrbracket _I = \top$が成り立つこと
  - 常に真
- $\models A$と書く
- 排中律（excluded middle）
  - $P$または$P$ではないことを表す
    - $P \lor \neg P$
    - $\neg \neg P \supset P$
      - 二重否定の除去と呼ばれる
  - トートロジである
- 論理式がトートロジであるかは決定可能
  - 1つの論理式に現れる命題記号は有限個なので
  - 与えられた吉敷がトートロジであるかどうかを多項式時間で判定するアルゴリズムが存在する
充足可能（satisfiable）
- ある解釈$I$のもとで$\llbracket A \rrbracket _I = \top$が成り立つこと
- 成り立たない場合充足不能（unsatisfiable）である
同値（equivalent）・論理同値（logically equivalent）
- 任意の解釈$I$のもとで$\llbracket A \rrbracket _I = \llbracket B \rrbracket _I$が成り立つこと
- 命題論理では$A \leftrightarrow B$がトートロジであるとき、かつそのときに限り同値となる

コンパクト性（compactness）

論理式の集合に対して、任意の有限部分集合が個別に充足可能ならば、集合全体を同時に充足する解釈が存在する
無矛盾（consistent）
- 論理式の集合において、属する任意の有限部分集合が充足可能であること
極大無矛盾（maximally consistent）
- 無矛盾な集合の有限部分集合と、それらに属さない任意の論理式の集合との和集合が矛盾すること
  - つまり、無矛盾な論理式の集合に対して、新たな論理式を加えると矛盾する
- $\Gamma$が極大無矛盾であるとき、$A\in\Gamma$ならば$\neg A\notin\Gamma$であり、$\neg A\notin\Gamma$であれば$A\in\Gamma$である
ツォルンの補題（Zorn’s lemma）
- 半順序集合における任意の全順序部分集合には極大の要素が存在する

演繹体系（deduction system）

定理（theorem）と呼ばれる論理式を導く形式体系
- 定理とは証明可能な論理式に他ならない！！
公理（axiom）と呼ばれる論理式から始めて、推論規則（inference rule）を有限回適用して得られる論理式を証明可能（provable）であるという
シーケント計算（sequent calculus）
- シーケント（sequent）
```
$$
A_1,...,A_mとB_1,...,B_nを論理式の並びとしたとき、\\
A_1,...,A_m \rarr B_1,...,B_n
$$
```
  - 矢式、連鎖、式ということもある
  - $A_1,…,A_m$を前提部（antecedent）といい$B_1,…,B_n$を結論部（succeedent）という
    - からの並びでも良い
- $A_1,…,A_m \rarr B_1,…,B_n$というシーケントに対し、$A_1 \land … \land A_m \supset B_1 \lor … \lor B_n$という論理式を対応させる
  - $m=0$の場合は前提部が$\top$、$n=0$の場合は結論部が$\bot$であると考える
- すでにトートロジと判明しているシーケントから新たなトートロジであるシーケントを得る規則を推論規則とよび、以下のような形をしている
```
$$
\frac{前提_1...前提_n}{結論}(規則の名前)
$$
```
  - 前提（premise）と結論（conclusion）はシーケントである
    - すべての前提がトートロジであるとき、結論もトートロジとなる
- 初期シーケント（initial sequent）
  - 命題記号のみから成るシーケント$P_1,…,P_m \rarr Q_1,…,Q_n$で、前提部と結論部の両方に同じ命題記号が現れるようなもの
    - ある$i$と$j$があって、$P_i$と$Q_j$が同じ命題記号であるようなもの
      - もし前提が真であれば共通の命題記号が結論にもあるので真
      - もし前提が偽であれば$\supset$が真となるので真
        →トートロジである
- 推論規則
  - $\Gamma$や$\Delta$は論理式の有限の並びを表す
    - $\Gamma’$や$\Delta’$は前提のそれぞれの論理式を入れ換えたもの
      $$ \frac{\Gamma \rarr \Delta}{\Gamma’ \rarr \Delta’}(並べ換え) $$
      $$ \frac{A, \Gamma \rarr \Delta}{\Gamma \rarr \Delta, \neg A}(\neg 右) $$
      $$ \frac{\Gamma \rarr \Delta, A}{\neg A, \Gamma \rarr \Delta}(\neg 左) $$
      $$ \frac{\Gamma \rarr \Delta, A ~~ \Gamma \rarr \Delta, B}{\Gamma \rarr \Delta, A \land B}(\land 右) $$
      $$ \frac{A,B,\Gamma \rarr \Delta}{A \land B, \Gamma \rarr \Delta}(\land 左) $$
  $$ \frac{\Gamma \rarr \Delta, A,B}{\Gamma \rarr \Delta,A \lor B}(\lor 右) $$
  $$ \frac{A, \Gamma \rarr \Delta ~~ B, \Gamma \rarr \Delta}{A \lor B, \Gamma \rarr \Delta}(\lor 左) $$
  $$ \frac{A,\Gamma \rarr \Delta, B}{\Gamma \rarr \Delta, A \supset B}(\supset 右) $$
  $$ \frac{\Gamma \rarr \Delta, A ~~ B, \Gamma \rarr \Delta}{A \supset B, \Gamma \rarr \Delta}(\supset 左) $$
- 証明図（proof figure）・証明木（proof tree）・証明（proof）
  - シーケントが、その上にあるシーケントを前提とする推論規則の結論になっているもの
- 証明可能（provable）
  - 初期シーケントから始めて推論規則を有限回適用して得られるシーケント
- ワングのアルゴリズム（Wang’s algorithm）
  - 論理式を分解し、帰納的に真かどうかを調べることによってシーケントがトートロジかどうかを判定するアルゴリズム
  - 手順
    - $\Gamma \rarr \Delta$というシーケントに対し、まずこれが論理記号を含むかどうかを調べる
      - 論理記号が含まれない場合、共通の命題記号があるか調べる
        共通の命題記号があればトートロジである
        共通の命題記号がなければトートロジではない
      - 論理記号が含まれる場合、$\Gamma$中の論理式を並べ換え$B \lor C, \Gamma’$という形にできたならば、$B,\Gamma’ \rarr \Delta$と$C,\Gamma’ \rarr \Delta$の両方がトートロジかどうかを、このアルゴリムを帰納的に適用することにより調べる
        どちらもトートロジであればトートロジである
        どちらかがトートロジでなければトートロジではない
  - 証明の構築に失敗した際には、そのシーケントを偽にする解釈を求めることができる
    - 偽になる選択肢がある場合、それがどういうパターンなのか分かる

一階述語論理（predicate logic）

述語論理（predicate logic）
- 命題の内部構造も形式化した論理

構文論

述語（predicate）
- 不特定な対象（変数など）に関する主張
- 変数$x$に関する述語を$P(x)$と表す
  - $P$は述語記号（predicate symbol）である
- アリティ（arity）
  - 述語記号の引数の数
項（term）
- 関数記号と定数記号と個体変数から作られる式
- 関数記号（function symbol）
  - 関数を表す記号
- 定数記号（constant symbol）
  - 定数を表す
  - アリティが0の関数と考えることができる
- 一階の変数（first-order variable）・個体変数（individual variable）
  - 数などのものを表す変数
  - 領域（universe）
    - 個体変数の動き得る範囲の集合
- 二階の変数（second-order variable）
  - ものの集合やものからものへの関数を表す変数
- 閉じた（closed）項
  - 変数を含まない項
原子論理式（atomic formula）
- 述語記号と項から作られる式
  - $Q(f(x,c),g(f(c,d)))$など
述語論理式（predicate formula）
- 原子論理式と論理記号から作られる式
- 論理記号
  - 命題論理の記号も使用できる
  - 量化記号（quantifier）
    - 全称記号（universal quantifier）
      - $\forall x$
        すべての$x$に対して
        存在記号に可換である
        $\forall x A := \neg \exists x \neg A$
    - 存在記号（existential quantifier）
      - $\exists x$
        ある$x$が存在して
        全称記号に可換である
        $\exists x A := \neg \forall x \neg A$
一階述語論理（first-order predicate logic）
- 変数に一階の変数のみを用いた述語論理
束縛変数（bound variable）
- 量化記号の後ろに書かれ、別の変数で置き換えても命題の意味が変わらないような変数
  - $\forall x P(x)$における$x$など
- スコープが定まっており、量化記号が有効な範囲でのみ束縛される
- $\alpha$変換（$\alpha$-conversion）
  - 束縛変数の名前を変えること
- $\alpha$同値（$\alpha$-equivalent）
  - $\alpha$変換した結果同じになる論理式
自由変数（free variable）
- 束縛変数でない変数

意味論

構造（structure）
- 述語記号と定数記号を含む関数記号の解釈
- 述語論理における解釈では、変数が動き得る範囲となる領域があるため
- 構造$I$にによる関数記号$f$の解釈を$I(f)$と書く
  - 関数$f$に対して構造を持たせる
領域（universe）
- 変数が取りうる値の集合
  - $U_I$は構造$I$における領域
付値（valuation）
- 1つの構造$I$が定義されたとき、それぞれの変数に領域$U_I$の要素を対応させる関数
  - 変数から値への写像
- 付値$J$によってある変数$x$に対して値を割り当てることを$J(x)$と書く
- $J[u/x]$を変数$x$に値$u$を割り当てた新しい付値とする
  - $J(x)=2$、$J(y)=10$の場合、$J9/x=9$となり、$J9/x=10$である
構造と付値によって項$t$の解釈$\llbracket t \rrbracket _{I,J} \in U$を帰納的に定義できる
- $\llbracket x \rrbracket _{I,J} = J(x)$
- $\llbracket f(t_1,…,t_n) \rrbracket _{I,J} = I(f)(\llbracket t_1 \rrbracket _{I,J},…,\llbracket t_n \rrbracket _{I,J})$
  - 上記により、論理式$A$の解釈$\llbracket A \rrbracket _{I,J} \in \mathbb{B}$を帰納的に定義できる
恒真（valid）
- 論理式$A$が任意の構造$I$と任意の付値$J$のもとで$\llbracket A \rrbracket _{I,J} = \top$となる場合
  - $\vDash A$と書く
充足可能（satisfiable）
- 論理式$A$がある構造$I$とある付値$J$で真となる場合
  - $I$と$J$は$A$を充足するという
充足不能（unsatisfiable）
- 充足可能でない場合
  - どのような構造と付値でも論理式を真とできない
    - $\neg A$が恒真であるということ
同値（equivalent）・論理同値（logically equivalent）
- 論理式$A$と$B$について、任意の構造$I$と任意の付値$J$において$\llbracket A \rrbracket _{I,J} = \llbracket B \rrbracket _{I,J}$が成り立つこと
モデル（model）
- $\forall A$が真となるような構造$I$

エルブランの定理

$\forall x A $という形の閉じた論理式が充足不能なら、その有限個の具体例$A[t_1],…,A[t_n]$が命題論理において充足不能となること
- $A $は$\forall$も$\exists$も含まない
述語論理における充足不能性を命題論理における充足不能性に還元できる
スコーレム関数（Skolem constant）
- 閉じた論理式$\forall x \exists y A[x,y]$が充足可能である場合、$f$を$A[x,y]$に現れない新しい関数記号とすると、$\forall x A[x, f(x)]$も充足可能となる
  - $\forall x \exists y A[x,y]$が真となる場合、それに対応する構造$I$が存在するので、真となる構造$I$の中の$y$の値に対しての付値となるような関数を$f$の解釈とすれば良い
  - 逆説的に、$\forall x A[x, f(x)]$が充足可能なら、$\forall x \exists y A[x, y]$も充足可能である
    - $f$の返り値を$y$とすればよい
  - 上記のような性質を持つ関数記号$f$をスコーレム関数という
- 一般に、$\forall x_1 … \forall x_n \exists y A[x_1,…,x_n,y]$という形の閉じた論理式が充足可能であるかどうかを調べるには、$\forall x_1 … \forall x_n A[x_1,…,x_n,f(x_1,…,x_n)]$が充足可能であるか調べれば良い
  - $n=0$の場合、$\exists y A[y]=A[c]$の充足可能性を調べれば良い
    - $c$はスコーレム定数（Skolem constant）と呼ばれる
冠頭形（prenex form）
- $\forall$や$\exists$が論理式の先頭に集まっている状態
- すべての論理式は同値な冠頭形変形できる
  - 変換規則（$B$は$x$を自由変数として含まないと仮定）
    - $\forall x A \land B$→$\forall x . A \land B$
    - $\forall x A \lor B$→$\forall x . A \lor B$
    - $\neg \forall x A $→$\exists x \neg A $
    - $\exists x A \land B$→$\exists x . A \land B$
    - $\exists x A \lor B$→$\exists x . A \lor B$
    - $\neg \exists x A $→$\forall x \neg A $
スコーレム化（Skolemization）
- 任意の閉じた論理式をスコーレム関数の導入を繰り返すことで、$\forall$と$\exists$を含まないような形に変換すること
  - つまり論理式から$\exists$を消して、スコーレム関数に置換すること
エルブラン領域（Herbrand universe）
- $\forall x_1 … \forall x_n A[x_1,…,x_n]$に含まれる定数記号と関数記号の全体を$\mathbb{F}$としたときに、$\mathbb{F}$の中の定数記号と関数記号から作られる閉じた項の全体をエルブラン領域$\mathbb{H}$とする
  - $\mathbb{F}$に定数記号が1つも属していないときは適当な定数記号を1つ加える
- つまり、自由変数を除いた記号を用いて作れる閉じた項の集合となる
  - $\forall x \forall y ( P(x) \land Q(x, f(x, c)) )$において
    - $\mathbb{F} = {c, f}$
    - $\mathbb{H} = {c,f(c,c), f(f(c,c),c),f(c,f(c,c)),f(f(c,c),f(c,c)),…}$
エルブラン構造（Herbrand structure）
- エルブラン領域をその領域とする構造
- 次の条件を満たす構造$I_H$
  - $U_{I_H} = \mathbb{H}$
  - 定数記号$c$は$c$自身に解釈する
    - $c$として$c$$f(c,c)$とかで解釈しないということ
    - $I_H(c) = c \in \mathbb{H}$
  - アリティ$n$の関数記号$f$に対して$I_H(f)$は、$\mathbb{H}$の要素である閉じた項$t_1,…,t_n$に$\mathbb{H}$の要素である閉じた項$f(t_1,…,t_n)$を対応させる
    - $t_1,…,t_n \in \mathbb{H}$に対して、$I_H(f)(t_1,…,t_n) = f(t_1,…,t_n) \in \mathbb{H}$
      - $f(c)$や$f(c, f(c,c),…)$みたいな解釈になるよってこと
- エルブラン構造により、任意の閉じた項$t$は$\mathbb{H}$の要素である$t$自身によって解釈される
  - $\llbracket t \rrbracket _{I_H} = t$が成り立つ
    - 述語記号の解釈はエルブラン構造によって異なっても良い
      - アリティ$n$の述語記号$P$に対して、$I_H(P)$は$\mathbb{H}^n \rarr \mathbb{B}$に属する関数であれば良い
- エルブラン充足可能（Herbrand-satisfiable）
  - 論理式を真に解釈するエルブラン構造（及び付値）が存在する場合
    - 論理式の集合$\Gamma$がエルブラン充足可能であるとは、$\Gamma$に属する任意の論理式を真に解釈するエルブラン構造（及び付値）が存在するということ
  - 存在しない場合はエルブラン充足不能となる
エルブラン基底（Herbrand base）
- $\forall x_1…\forall x_n A[x_1,…,x_n]$において、$A[x_1,…,x_n]$の中に含まれる述語記号の全体を$\mathbb{P}$とし、$\mathbb{P}$の中の述語記号と$\mathbb{F}$の中の定数記号と関数記号から作られる閉じた原子論理式の全体を、元の論理式のエルブラン基底$\mathbb{Q}$という
  - $\forall x \forall y ( P(x) \land Q(x, f(x, c)) )$において
    - $\mathbb{P}={P,Q}$
    - $\mathbb{Q}={P(c),P(f(c,c)),Q(c,c),Q(f(c,c),c),…}$
$\Gamma$が命題論理式の集合として充足可能であるならば、$\forall x_1 … \forall x_n A[x_1, …, x_n]$はエルブラン充足可能、従って述語論理式においても充足可能である
エルブランの定理（Herbrand’s theorem）
- $\forall x_1 … \forall x_n A[x_1,…,x_n]$が充足不能ならば、閉じた項$t_{ij} \in \mathbb{H} ~ (1 \leq i \leq m, 1 \leq j \leq n)$が存在して、${ A[t_{1_1}, …, t_{1_n}], …, A[t_{m_1}, …, t_{m_n}] }$が命題論理において充足不能になる
- 逆説的に、閉じた項$t_{ij} \in \mathbb{H} ~ (1 \leq i \leq m, 1 \leq j \leq n)$が存在して、${ A[t_{1_1}, …, t_{1_n}], …, A[t_{m_1}, …, t_{m_n}] }$が命題論理において充足不能ならば、$\forall x_1 … \forall x_n A[x_1,…,x_n]$は充足不能である

述語論理式のシーケント計算

推論規則

$$
\frac{\Gamma \rarr \Delta, A[a]}{\Gamma \rarr \Delta, \forall x A[x]}(\forall 右)
$$

$$
\frac{A[t],\Gamma \rarr \Delta}{\forall x A[x], \Gamma \rarr \Delta}(\forall 左)
$$

$$
\frac{\Gamma \rarr \Delta, A[t]}{\Gamma \rarr \Delta, \exists x A[x]}(\exists 右)
$$

$$
\frac{A[a],\Gamma \rarr \Delta}{\exists x A[x], \Gamma \rarr \Delta}(\exists 左)
$$

$$
\frac{\Gamma \rarr \Delta, A, A}{\Gamma \rarr \Delta, A}(重ね合わせ右)
$$

$$
\frac{A,A,\Gamma \rarr \Delta}{A,\Gamma \rarr \Delta}(重ね合わせ左)
$$

$$
\frac{\Gamma \rarr \Delta, A ~~ A, \Gamma \rarr \Delta}{\Gamma \rarr \Delta}(カット)
$$

$$
\frac{\Gamma \rarr \Delta}{\Gamma \rarr \Delta, A}(水増し右)
$$

$$
\frac{\Gamma \rarr \Delta}{A, \Gamma \rarr \Delta}(水増し左)
$$

等号付き一階述語論理（first-order predicate logic with equality）
- 等号を特別視した述語論理
- $I(=)(x,y)=\top ~~ iff ~~ x=y$
  - 等号$=$を常に領域の2つの要素の間の等しさとして解釈する

3 要素論理と直観主義論理

クリプキ構造
- 命題様相論理を解釈するための構造
- $S = \langle W, R, V \rangle$
  - $W$
    - 可能世界の集合
  - $R$
    - 到達可能関係
    - $W$が可能な世界の集合なので、到達可能である関係は、それらの中にある
      - $R \subseteq W \times W$
  - $V$
    - 各世界における命題記号の解釈を与える関数
      - $V : W \times {P_0, P_1, P_2, … } \rarr \mathbb{B}$
      - 世界$w \in W$と命題記号$P$に対して$V(w,P) \in \mathbb{B}$が成り立つ

4 計算可能性

帰納的関数

原始帰納的関数（primitive recursive）
- 以下の規則を有限回適用して定義できる自然数上の関数
  - 定数$0$は0引数の関数として原始帰納的である
  - $S(x)=x+1$と定義される関数$S$は原始帰納的である
    - $S$は後者関数（successor function）である
  - $f(x_1,…,x_n) = x_i$と定義される関数$f$は原子帰納的である
    - このような関数を射影（projection）という
  - $f$と$g_i$が原始帰納的であるとき
```
  $$
  h(x_1,...,x_n) = f(g_1(x_1,...,x_n),...,g_m(x_1,...,x_n))
  $$

  と定義される関数$h$は原始帰納的である
```
    - 合成（composition）である
  - $f$と$g$が原始帰納的であるとき
```
  $$
  h(0,x_1,...,x_n)=f(x_1,...,x_n) \\
  h(S(x),x_1,...,x_n)=g(x,h(x,x_1,...,x_n),x_1,...,x_n)
  $$

  と定義される関数$h$は原始帰納的である
```
    - 原始帰納法（primitive recursion）
部分帰納的関数（partial recursive function）
- ある関数に対して、引数を部分適用したような関数を返す
  - $f(x,y)=0$であるとき、そのようなy$y$$y_0$ としたとき、$h(x)=g(y_0)$
    - ない場合は$h(x)=\bot$
帰納関数とチューリングマシンの計算能力は等価

5 λ計算

λ計算

λ計算（lambda-calculus）
- 真理値や自然数、条件分岐はすべて関数として表現できるので、関数のみを対象とすれば良いという観点から定義された体系
  - 真理値
    - $true(x) = \lambda(y)x$
    - $false(x) = \lambda(y)y$
  - if P then x else y
    - $(P(x))(y)$
  - 自然数$n$
    - チャーチの数字として表現
      - $\lambda (f) \lambda (x) f(f(…f(x)…))$
        $f$の出現する個数が$n$
λ項（lambda-term）
- $M ::= x | (M~N) | \lambda x . M$
  - $(M~N)$は関数適用（function application）を表す
  - $\lambda x . M$はλ抽象（lambda-abstraction）を表す
    - $((\lambda x . x \times x)~10) = 100$みたいに使う
    - $M$中で$x$が使用されている場合、束縛されている（bound）という
代入（substitution）
- $((\lambda x . 2 ^ x)\ 10)$における$x$について、これを適用する項（$10$）で置き換えること
  - $M [x:=N]$と書く
    - 上の例では$\lambda x . 2^x [x := 10]$となる
$\alpha$変換（alpha-convention）
- 束縛変数を別の名前の変数に置き換える操作
- $\lambda y . xy$というラムダ項に$x:=\lambda z . zy$を代入する場合、単純な代入だと$\lambda y . (\lambda z . zy)y$となり、本来なら両者の$y$は異なるにも関わらず、束縛されてしまっている
- ラムダ項の意味を変えずに変数の表記のみを変更することで、この問題を回避する
  - $\lambda y’ . (\lambda z . zy)y'$
  - 変数規約（variable convention）
    - λ計算で扱うλ項は、$\alpha$同値であるλ項を適切に選んでくることにより、1つのλ項の中ではもちろん、各λ項の間でも束縛変数の名前は相違なることとする
    - 束縛変数の名前は自由変数の名前とも異なっているとする
- $\alpha$同値（alpha-equivalent）
  - λ項が式として同型であること
  - どのように$\alpha$変数してもλ項は同値である

簡約

より簡単な式に置き換えること
- $1+1$を$2$に置き換えるなど
簡約を繰り返し、値を求めることが計算と言っても過言ではない

$\beta$簡約（beta-reduction）

関数適用において、適用される項を関数の変数に代入する事によって簡約する
- $(\lambda x . M)~N \rarr M[x:=N]$
$\beta$正規（beta-normal form）
- これ以上$\beta$簡約できない形
チャーチ-ロッサーの定理
- ある$M$が2種類に$\beta$簡約できる場合、それらは更に同じ形に$\beta$簡約できる
  - $\beta$簡約の正規形は最終的に一意に定まる
標準簡約列（standard reduction sequence）
- 一番左の項から簡約していったときにできる簡約列

評価戦略（evaluation strategy）

どのように簡約するかについての戦略
名前呼び評価戦略（call-by-name evaluation strategy）
- 基本的には最外最左簡約だが、項の内部$M$は監訳しない
  - (lambda (x)(+ x (* 2 4)) において、(lambda (x)(+ x 8) とはならない
    - x が(+ 1 1) だとしても、まず代入し、値が必要になったタイミングで簡約する
値呼び評価戦略（call-by-value evaluation strategy）
- $M~N$において、$M$を簡約した後$N$を簡約する
  - 関数部と引数部の両方を簡約した後、引数を変数に代入して関数の計算に取り掛かる

$\eta$簡約（eta-reduction）

$\lambda x . Mx$は引数を関数$M$で適用する
- これは関数$M$と同様の働きである
このような動作を$M$で置換することを$\eta$簡約という

型付きλ計算

型（type）

各変数における変数の動く範囲の集合を表す式

単純型付きλ計算

BNFを用いて以下のように定義できる
$$ A ::= \alpha | A \rarr B | A \times B | A + B $$
- $A,B,C$などは型を表す
- $\alpha, \beta, \gamma$などは基本型（basic type）を表す
  - 基本的な集合に対応する型であり、あらかじめ定まっている
- $A \rarr B$は関数型（function type）である
  - $\rarr$は右に結合する
- $A \times B$は直積型（product type）である
  - 集合$A$と集合$B$の直積を表す
    - $A$の要素と$B$の要素との組の全体
  - $\times$は左に結合する
- $A + B$は直和型（sum type）である
  - 集合$A$と集合$B$の直和を表す
  - $+$は左に結合する
型付け
- 変数$x^A$の型は$A$である
- $M$の型が$B$ならば、$\lambda x^A . M$の型は$A \rarr B$である
- $M$の型が$A \rarr B$で、$N$の型が$A$ならば、$M~N$の型は$B$である
- 直積型＜$(M, N)$を$M$と$N$の対を表すλ項とし、$\pi_1(L)$を対$L$の第一成分、$\pi_2(L)$を対$L$の第二成分を表すλ項とする＞
  - $M$の型が$A$であり、$N$の型が$B$であるならば、$(M,N)$の型は$A \times B$である
  - $L$の型が$A \times B$であるならば、$\pi_1(L)$の型は$A$である
  - $L$の型が$A \times B$であるならば、$\pi_2(L)$の型は$B$である

$\beta$簡約と型付け

サブジェクト・リダクション定理（subject reduction theorem）
- $\beta$簡約前に$A$という型により正しく型付けされている場合、簡約後も$A$によって正しく型付けされていることが成り立つ

正規化可能性

型付きλ計算では、強い正規化可能性（strong normalizability）が成り立つ！
- 弱い正規化可能性
  - 正しく型付けされたλ項$M$に対して、$\beta$正規形に至る$\beta$簡約列$M \rarr_\beta M_1 \rarr_\beta M_2 \rarr_\beta … \rarr_\beta M_n (M_nは \beta 正規形)$が存在するとき、$M$は弱い正規化可能である
    - うまく簡約すれば$\beta$正規形に到達することができる
      - ミスれば簡約できない
- 強い正規化可能性
  - 正しく型付けされたλ項$M$に対して、$M$から始まる無限$\beta$簡約列$M \rarr_\beta M_1 \rarr_\beta M_2 \rarr_\beta …$が存在しない
    - どのように簡約しようが必ず簡約が止まる

暗黙的型付け

λ項と型付けの機構を分離した型付けスタイル
型判断（type judgement）
- $f~x$に対して、$f$ $f$$A \rarr B$、$x$の型は$A$という情報を与えることにより、$f~x$の型が$B$であると決まる
  - $\textcircled{\scriptsize 1} \vdash \textcircled{\scriptsize 2} : \textcircled{\scriptsize 3}$と書く
    - 「自由変数に関する型の情報として$\textcircled{\scriptsize 1}$が与えられたとき、λ項の$\textcircled{\scriptsize 2}$の型は$\textcircled{\scriptsize 3}$に決まる」という三項関係
- 型判断を導く証明木を型付け導出木（typing derivation tree）と呼ぶ
型割り当て（type assignment）・型環境（type environment）
- $\textcircled{\scriptsize 1}$のこと
- 変数と型の対の有限集合${x_1:A_1,…,x_m:A_n}$となる
  - $x_1,…,x_n$は相違なるものとする
  - $x_1:A_1,…,x_m:A_n \vdash M : A$と書ける
型付け規則
$$ \frac{1 \le i \le n}{x_1:A_1,…,x_n:A_n \vdash x_i:A_i}ImpVar $$
$$ \frac{\Gamma \vdash M:A \rarr B ~~ \Gamma \vdash N:A}{\Gamma \vdash M~N : B}ImpApp $$
$$ \frac{{x:A} \cup \Gamma \vdash M:B}{\Gamma \vdash \lambda x . M : A \rarr B}ImpLam $$

型推論

型検査（type checking）
- 型判断の成否を調査する行為
型推論（type inference）
- どのような型を持つのか調べること
自然演繹（natural deduction）
- 型付きλ計算と同一視できる演繹体系
- 証明図
  - 0個以上の仮定と1個の結論を持つ図
  - 論理式を節点とし、推論規則（inference rule）を枝とする木である
- $I$を導入則、$E$を除去則とする
カリー・ハワードの対応（Curry-Howard correspondence）
- 型付きλ計算と直観主義論理が対応するというもの
- λ項の構造と証明の構造が対応付けられる
- λ項における変数$x^A$は、論理式$A$の仮定に相当する
  - 変数$x^A$の型は$A$である
    - 論理式$A$を仮定とする証明$A$は、論理式$A$を証明しているという推論規則に対応する
    - $A \supset A$
  - $M$の型が$B$ならば、$\lambda x^A . M$の型は$A \rarr B$である
    - 論理式$A$を仮定して論理式$B$を導ける場合、仮定を外し含意として良いという推論規則に対応する
    - $[A]^l \rarr B$であれば、$A \supset B$
- λ抽象が推論規則$\supset I$に対応する
- λ抽象における変数の束縛が仮定のディスチャージ（除去）に対応する
多相型（polymorphic type）
- 幾通りもの（単純）型を表現する式
  - 恒等関数$\lambda x . x$に対しては$\forall \alpha . \alpha \rarr \alpha$が対応する

多相λ計算（polymorphic lambda-calculus）

多相型を導入した型付きλ計算
BNFを用いて以下のように定義できる
$$ A ::= \alpha | A \rarr B | \forall \alpha . A $$
- $\alpha$は型変数を表す
- $\forall \alpha .$は一階述語論理の$\forall x .$や$\exists x.$、二階論理の$\forall X .$と同様に、型変数の束縛を行う
  - 束縛されていない型変数の出現を自由であると言う
- 直積型や直和型は$\rarr$と$\forall$で表現できるので含めない
多相λ計算のλ項は以下のように定義される
$$ M ::= | x^A | \lambda x^A.M | (M~N) | \Lambda \alpha . M | (M~A) $$
- $\Lambda \alpha . M$はλ項$M$を型変数$\alpha$に関して抽象化したものであり、型抽象（type abstraction）と呼ぶ
- $(M~A)$は型抽象されたλ項$M$に対して、型$A$を適用したものであり、型適用（type application）と呼ぶ
推論規則（λ計算の規則に加えて）
- 導入則
  - $M$の型が$A$であり、$M$に出現する各自由変数において型変数$\alpha$が自由に出現しないならば、$\Lambda \alpha . M$の型は$\forall \alpha . A$である
    - $\forall$右の規則である$\alpha$が$\Gamma$と$\Delta$に自由に現れない変数であるに対応する
- 除去則
  - $M$の型が$\forall \alpha . A$であるならば、$M~B$の型は$A[\alpha := B]$である
簡約
- 型抽象と型適用に関する簡約が定義されている
  - $(\Lambda \alpha . M)A \rarr_A M[\alpha := A]$
データ型の表現
- 真偽値
  - 型なしλ計算における真偽値に対応する関数はいずれも型$\alpha \rarr \alpha \rarr \alpha$を持つため以下のようになる
  - 真偽を以下のように定義すれば、それらは共に型Bool となる
    - $true = \Lambda \alpha . \lambda x^\alpha . \lambda y^\alpha . x^\alpha$
    - $false = \Lambda \alpha . \lambda x^\alpha . \lambda y^\alpha . y^\alpha$
  - 条件式は、λ項$M$、$N$の型を共に$A$とし、$L$を型Bool のλ項とすれば、以下のように定義できる
    - if L then M else N = $L~A~M~N$
      - true, falseに具体的な型$A$が適用され、それらが返る
- 直積型
  - $A \times B = \forall \alpha . (A \rarr B \rarr \alpha) \rarr \alpha$
  - 型$A$のλ項$M$、型$B$のλ項$N$の対
    - $(M, N) = \Lambda \alpha . \lambda f^{A \rarr B \rarr \alpha} . fMN$
  - 取得関数
    - 対は型引数を取るので、取得したい方の具体的な型を渡して、そこから実際の値を取得するような関数を渡して取るイメージ
    - $first = \lambda p^{\forall \alpha . (A \rarr B \rarr \alpha) \rarr \alpha} . pA(\lambda x^A . \lambda y^B . x)$
    - $second = \lambda p^{\forall \alpha . (A \rarr B \rarr \alpha) \rarr \alpha} . pB(\lambda x^A . \lambda y^B . y)$
- 自然数
  - 型なしλ計算と同様チャーチの数字に基づいて表現
    - チャーチの数字は$(A \rarr A) \rarr A \rarr A$という型を付けられる
  - 自然数の型
    - $Nat = \forall \alpha . (\alpha \rarr \alpha) \rarr \alpha \rarr \alpha$
  - λ項として
    - $\Lambda \alpha . \lambda f^{\alpha \rarr \alpha} . \lambda x^\alpha . f(f(…(fx)…))$
  - 零
    - $\overline{0} = \Lambda \alpha . \lambda f^{\alpha \rarr \alpha} . \lambda x^\alpha . x$
  - 後者関数
    - $\overline{S} = \lambda m^{Nat} . \Lambda \alpha . \lambda f^{\alpha \rarr \alpha} . \lambda x^\alpha . f(m \alpha f x)$
      - $Nat$の型引数に$\alpha$を適用してできた型を、$f$に適用して$f^{\alpha \rarr \alpha}$を元の$fx$に繋げられるようにしている
- 繰り返し演算子（iteration operator）
  - 与えられた自然数の回数分関数を繰り返し適用する
  - $iter = \lambda f^{A \rarr A} . \lambda x^A . \lambda n^{Nat} . n A f x$
    - $\lambda n^{Nat}$に型$A$と$f$を渡すことで、$n$個分の$f$が返るため、それによって$n$回$f$を適用するという感じになる
多相λ計算で表現できる関数の集合は原始帰納的関数全体の集合より真に大きい

依存型（dependent type）

項をパラメタとする型
- $A$の$n$個の直積を表す型$A^n$など
依存関数型（dependent function type）・$\Pi$型
- $\Pi_n : Nat . A^n$とする
  - この型を持つ項$M$を関数として、型$Nat$の項$\overline{3}$に適用することができる
    - 項$M\overline{3}$の型は$A^3$、すなわち$A \times A \times A$となる
  - $\Pi_n : Nat . A$は$Nat \rarr A$と同じものとなる
依存直積型（dependent product type）・$\Sigma$型
- 双対的に$\Sigma_n : Nat.A^n$という型がある
  - 「ある$n$が存在していて、$A^n$という型」を表す
  - 項$M$がこの型を持つとすると、$Nat$の項とその項（$n$とする）に依存して決まる型$A^n$の項とを得ることができる
    - 第一成分の項に第二成分の項の型が依存するような対であると考えられる
  - $\Sigma_n : Nat . A$は$Nat \times A$と同じものとなる

多相型・依存型におけるカリー・ハワードの対応

多相型
- 命題$\forall \alpha . A$の証明$\Lambda \alpha . M$から、任意の型$B$に対して、$A[x:=B]$という命題の証明を得ることができる
  - 型変数$\alpha$は二階の変数（アリティ0）に対応し、$\forall \alpha$は二階の変数に対する全称$\forall X$に対応する
    - 直観主義二階命題論理に対応する
依存型
- $\Pi_x : A . P(x)$は、項の変数による型の抽象を可能とするものである
  - 命題を光により抽象すると考えれば、一階の変数$x$に対する全称の$\forall x$に対応すると考えられる
    - 依存型を持つ型付きλ計算は、直感主義一階述語論理に対応する
    - 依存型を持つ多相λ計算は、直観主義二階述語論理に対応する

1 集合と関係#

2 命題論理と述語論理#

命題論理（propositional logic）#

命題（proposition）#

論理記号（logical symbol）#

構文論（syntax）#

意味論（semantics）#

コンパクト性（compactness）#

演繹体系（deduction system）#

一階述語論理（predicate logic）#

構文論#

意味論#

エルブランの定理#

3 要素論理と直観主義論理#

4 計算可能性#

帰納的関数#

5 λ計算#

λ計算#

簡約#

$\beta$簡約（beta-reduction）#

評価戦略（evaluation strategy）#

$\eta$簡約（eta-reduction）#

型付きλ計算#

型（type）#

単純型付きλ計算#

$\beta$簡約と型付け#

正規化可能性#

暗黙的型付け#

型推論#

多相λ計算（polymorphic lambda-calculus）#

依存型（dependent type）#

多相型・依存型におけるカリー・ハワードの対応#

1 集合と関係

2 命題論理と述語論理

命題論理（propositional logic）

命題（proposition）

論理記号（logical symbol）

構文論（syntax）

意味論（semantics）

コンパクト性（compactness）

演繹体系（deduction system）

一階述語論理（predicate logic）

構文論

意味論

エルブランの定理

3 要素論理と直観主義論理

4 計算可能性

帰納的関数

5 λ計算

λ計算

簡約

$\beta$簡約（beta-reduction）

評価戦略（evaluation strategy）

$\eta$簡約（eta-reduction）

型付きλ計算

型（type）

単純型付きλ計算

$\beta$簡約と型付け

正規化可能性

暗黙的型付け

型推論

多相λ計算（polymorphic lambda-calculus）

依存型（dependent type）

多相型・依存型におけるカリー・ハワードの対応