![[PukiWiki]](image/pukiwiki.png "[PukiWiki]")
H.22年度 京大名大合同合宿は京大生と名大生が主催して、全国の大学生達が集まりそれぞれが学ぶ数学や物理の発表を行う勉強合宿です。私（t_uda ）は本年度初参加です。
私は「Curry-Howard対応」というタイトルで 50 分の発表をしました。そのレジュメを TeX で書いたのでここに置いておきます。
\documentclass{jarticle}
\usepackage{amssymb}
\usepackage{theorem}
\usepackage{proof}
\title{Curry-Howard 対応}
\author{Tomoki UDA}
\date{\today}
\theoremstyle{break}
\newtheorem{theorem}{Th}[section]
\newtheorem{corollary}{Cor}[theorem]
\newtheorem{definition}[theorem]{Def}
\newtheorem{proposition}[theorem]{Prop}
\newtheorem{lemma}[theorem]{Lem}
\newtheorem{example}{Ex.}
\newtheorem{proof}{＜proof＞}
\newtheorem{remark}{Remark}
\newtheorem{notation}{Notation}
\newtheorem{fact}{Fact.}
\renewcommand{\theproof}{}
\renewcommand{\theremark}{}
\renewcommand{\thenotation}{}
\renewcommand{\thefact}{}
\def\imply{\Rightarrow}
\def\empty{\O}
\def\NJ{\mathrm{NJ}}
\newcommand{\pair}[2]{ \langle #1, #2 \rangle }
\setcounter{section}{-1}
\begin{document}
\maketitle
\begin{description}
\item[2011-03-12 追記:]
この文書は京大名大合同合宿において、宇田が発表した「Curry-Howard 対応」のレジュメです。
そもそも、前提知識を一切仮定せずに 50 分の講義時間内にこの内容を理解してもらうこと自体
かなり無謀だったのですが、それを無理矢理 2 時間分の内容に圧縮したのがこのレジュメです
（つまり実際の発表ではほとんど飛ばしています）。
内容は十分精査して厳密に書いているつもりですが、それでも誤魔化し切れていない
「誤り」がいくつもあります。特に、計算機科学分野に不慣れな人にも分かりやすいようにと
思って説明や定義を我流にアレンジしてしまっている節が多々あります
（例えば、図や項の等価性などはかなり誤魔化しています）。
このレジュメを読む際はその点に留意した上で読んで頂き、更に詳しい内容が知りたい場合は
参考文献の方を参照して頂くようお願いいたします。
\end{description}
\section{自然演繹}
\setcounter{theorem}{-1}
\begin{definition}[論理式]\label{論理式}
\begin{enumerate}\setlength{\itemsep}{-5pt}
\item 命題変数 $ p,q,r,\cdots $ は論理式である。
\item 論理式 $P,Q$ に対し、 $ (P \land Q), (P \imply Q) $ も論理式である。
\end{enumerate}
\end{definition}
\begin{remark}
$ P \land Q $ は"$P$ かつ $Q$"と解釈できる。
ここでは扱わないが、必要に応じて"$P$ または $Q$"を意味する $P \lor Q$ や
全称量化子 $\forall$ なども定義される。
\end{remark}
\begin{notation}
$\land$ の方が $\imply$ より結合が強いと約束して、冗長なカッコは省略してよい。また、
$ (P \imply (Q \imply R)) $ は $ P \imply Q \imply R $ と略す。
\end{notation}
\begin{remark}
定義に冗長な $ (カッコ) $を含めておくことで、結合の強さの曖昧さなく定義できる。
もしカッコがない場合、$ P \land Q \imply R $ は論理式であるが、それが
$ (P \land Q) \imply R $ なのか $ P \land (Q \imply R) $ なのかは分からない。
これは不都合なので、カッコ付きで定義しておいて改めて冗長な書き方をしなくても良いように記法を定めるのである。
\end{remark}
\begin{definition}[推論規則]\label{推論規則}
$ \NJ|_{\land,\imply} $ の推論規則を次の図式で定める:
\begin{enumerate}\setlength{\itemsep}{5pt}\setlength{\parskip}{5pt}
\item \fbox{
\infer[(Axiom)]{P \vdash P}{}
}
\item \fbox{
\infer[(\land I)]{\Gamma, \Sigma \vdash P \land Q}{
\Gamma \vdash P & \Sigma \vdash Q
}
}
\item \fbox{
\infer[(\land E1)]{\Gamma \vdash P}{
\Gamma \vdash P \land Q
}
} \fbox{
\infer[(\land E2)]{\Gamma \vdash Q}{
\Gamma \vdash P \land Q
}
}
\item \fbox{
\infer[(\imply I)]{\Gamma, \Sigma \vdash P \imply Q}{
\Gamma, P, \Sigma \vdash Q
}
} \fbox{
\infer[(\imply I')]{\Gamma, P, \Sigma \vdash P \imply Q}{
\Gamma, P, \Sigma \vdash Q
}
}
\item \fbox{
\infer[(\imply E)]{\Gamma, \Sigma \vdash Q}{
\Gamma \vdash P \imply Q & \Sigma \vdash P
}
}
\end{enumerate}
ここで、$P,Q$ は論理式、$\Gamma$ や $\Sigma$ は適当な論理式の列（順序対） $ P_1, P_2, \cdots, P_n $ を表す。
\end{definition}
本稿では以降、 $\NJ$ と言えば単に $ \NJ|_{\land,\imply} $ のことを表す。
\begin{definition}[証明図, 証明可能]
\begin{enumerate}\setlength{\itemsep}{-5pt}
\item 推論規則を組み合わせて得られる図式が \fbox{
\infer{ \Gamma \vdash P }{\vdots}
} という形の時、この図を $\Gamma$ から $P$ に至る証明図と言う。
\item $\Gamma$ から $P$ に至る証明図が存在する時、 $ \Gamma \vdash_{\NJ} P $ と書く。
\item 論理式 $P$ が $\NJ$ において証明可能とは、 $ \empty \vdash_{\NJ} P $
\end{enumerate}
\end{definition}
\begin{notation}
$ \Gamma \vdash_{\NJ} P $ は簡単に $ \Gamma \vdash P $ と書くことが多い。
\end{notation}
\begin{remark}
$ P_1, P_2, \cdots, P_n \vdash Q $ は、「 $ P_1, P_2, \cdots, P_n $ を仮定した時 $Q$ が成り立つ」ことと解釈できる。
図式 \fbox{ \infer{Q}{P} } は、（適当な仮定の下で）論理式 $P$ から論理式 $Q$ が推論されることと解釈できる。
\end{remark}
\begin{example}[$ P \imply Q \imply R \vdash_{\NJ} P \land Q \imply R $]
\ \\
\fbox{
\infer{ P \imply Q \imply R \vdash P \land Q \imply R }{
\infer{ P \imply Q \imply R, P \land Q \vdash R }{
\infer{ P \imply Q \imply R, P \land Q \vdash Q \imply R } {
\infer{ P \imply Q \imply R, P \land Q \vdash P \imply Q \imply R } {}
&
\infer{ P \imply Q \imply R, P \land Q \vdash P } {
\infer{ P \imply Q \imply R, P \land Q \vdash P \land Q }{}
}
} &
\infer{ P \imply Q \imply R, P \land Q \vdash Q }{
\infer{ P \imply Q \imply R, P \land Q \vdash P \land Q }{}
}
}
}
}
\end{example}
\section{型付きλ計算}
\setcounter{theorem}{-1}
\begin{definition}[型]\label{型}
\begin{enumerate}\setlength{\itemsep}{-5pt}
\item 型変数 $ a, b, c, \cdots $ は型である。
\item 型 $ U, V $ に対し、$ (U \to V), (U \times V) $ も型である。
\end{enumerate}
\end{definition}
\begin{remark}
1において、型変数の代わりに有限個の原始型（型定数）だけを考える場合もある（例えば、自然数全体の集合 $\mathbf{N} = \{0, 1, 2, \cdots\} $ など）。
2についてはそれぞれ、$ U \to V $ は $U$ から $V$ への写像型、$ U \times V $ は $U$ と $V$ の直積型と解釈できる。
型は集合のことと考えれば分かりやすいが、必ずしも集合とは限らない。抽象的な型がどのように用意されているかは文脈による。
\end{remark}
\begin{definition}[型付き $\lambda$ 項]\label{λ項}
\begin{enumerate}\setlength{\itemsep}{-5pt}
\item 型 $U$ に対し、型 $U$ に属する変数 $ x^U, y^U, z^U, \cdots $ は型 $U$ の $\lambda$ 項である。
\item 型 $U$ の $\lambda$ 項 $M$ と型 $V$ の $\lambda$ 項 $N$ に対し、$ \pair{M}{N} $ は型 $ U \times V $ の $\lambda$ 項である。
\item 型 $ U \times V $ の $\lambda$ 項 $M$ に対し、$ \pi^1{M} $ は型 $U$ の $\lambda$ 項、$ \pi^2{M} $ は型 $V$ の $\lambda$ 項である。
\item 型 $U$ の変数 $x^U$ と型 $V$ の $\lambda$ 項 $M$ に対し、 $( \lambda{x^U}.M )$ は型 $ U \to V $ の $\lambda$ 項である。
\item 型 $ U \to V $ の $\lambda$ 項 $M$ と型 $U$ の $\lambda$ 項 $N$ に対し、$(MN)$ は型 $V$ の $\lambda$ 項である。
\end{enumerate}
\end{definition}
\begin{notation}
混乱のない限り、次のように略記して良い:
\begin{enumerate}\setlength{\itemsep}{-5pt}
\item $ (\lambda{x}.(\lambda{y}.M)) = \lambda{x}.\lambda{y}.M = \lambda{xy}.M $
\item $ ((MN)L) = (MNL) = MNL $
\end{enumerate}
また本稿では必要に応じて、 $\lambda$ 項 $M$ が型 $U$ であることを便宜的に $M::U$ と略すことにする。
\end{notation}
\begin{remark}
型変数 $a$ と型に属する変数 $x^U$ とは全く違うものである。
\end{remark}
\begin{remark}
$\lambda$ 項 $ \lambda{x}.M $ は、対応 $ x \mapsto M $ が表す関数と解釈できる。
また $\lambda$ 項 $MN$ は、関数値 $M(N)$ と解釈できる。
このように考えると、型付き $\lambda$ 項は計算の形式化と思える。
従って当然 $ (\lambda{x}.fx)M $ の"計算結果"は $fM$ であることが期待されるが、
$\lambda$ 項に対する変換規則は一切与えていないので、
$ (\lambda{x}.fx)M $ に $\lambda$ 項としての記号列以上の意味はない。
その意味で、 $\lambda$ 項自体は計算の"手続き"の形式化である。
計算の"結果"を得るためには $\beta$ 変換について考察する必要があるが、ここでは扱わない。
\end{remark}
\begin{definition}[$\alpha$ 変換]
$\lambda$ 項 $P$ が部分項 $\lambda{x}.M$ を持つ時、
部分項 $\lambda{x}.M$ を $\lambda{y}.M[y/x]$ で置き換えて別の $\lambda$ 項 $P'$ を
得ることを、束縛変数の置き換えと呼ぶ。
この時、繰り返し $P$ の束縛変数を置き換えて $Q$ が得られるならば、
$Q$ は $P$ から $\alpha$ 変換で得られると言い、$ P =_\alpha Q $ と書く。
\end{definition}
\begin{proposition}[$\alpha$ 同値]
$=_\alpha$ は同値関係である。
\end{proposition}
以降、 $\lambda$ 項は $\alpha$ 同値を除いて同一視することとする。
\section{Curry-Howard 対応}
\setcounter{theorem}{-1}
論理式の定義 \ref{論理式} と型の定義 \ref{型} 及び、$\NJ$ の推論規則の定義 \ref{推論規則} と型付き $\lambda$ 項の定義 \ref{λ項} が非常に似通っていることに注目しよう。
\begin{lemma}
論理式と型は1対1対応する。
\end{lemma}
\begin{proof}
同じ記号であらわされる命題変数と型変数を対応させればよい。
\end{proof}
以降、特に断らなくても論理式と型は同一視する。
\begin{definition}[ $\lambda$ 項の図表示]
$\lambda$ 項 $M$ の図表示 $D(M)$ を、次で定める:
\begin{enumerate}\setlength{\itemsep}{-5pt}
\item $x::U$ に対し $D(x) := $ \fbox{
$x:U$
}
\item $M::U, N::V$ に対し、$ D(\pair{M}{N}) := $ \fbox{
\infer{ \pair{M}{N} : U \times V }{
D(M) & D(N)
}
}
\item $ M :: U \times V $ に対し、$ D(\pi^1{M}) := $ \fbox{
\infer{ \pi^1{M} : U }{ D(M) }
}, $ D(\pi^2{M}) := $ \fbox{
\infer{ \pi^2{M} : V }{ D(M) }
}
\item $ x::U, M::V $ に対し、 $ D(\lambda{x}.M) := $ \fbox{
\infer{ \lambda{x}.M : U \to V }{ D(M) }
}
\item $ M :: U \to V, N::U $ に対し、$ D(MN) := $ \fbox{
\infer{ MN : V }{
D(M) & D(N)
}
}
\end{enumerate}
\end{definition}
\begin{theorem}[Curry-Howard 対応1]
任意の $\lambda$ 項 $M::V$ に対して、$\NJ$ 証明図 $P = \Phi(M)$ が対応して、次を満たす:
$M$ の自由変数全体 $ FV(M) = \{ x_1::U_1, \cdots, x_n::U_n \} $ とすると、
証明図 $P$ は $ U_1, \cdots, U_n $ から $V$ に至る証明図。
\end{theorem}
\begin{proof}
$D(M)$ の $ \times, \to $ をそれぞれ $ \land, \imply $ に置き換えて、
図の中の全ての $\lambda$ 項の部分 $N:$ を $ U_1, \cdots, U_n \vdash_{\NJ} $ に置き換えて
得られる図を $\Phi(M)$ とすればよい。
但しここで、 $ U_1, \cdots, U_n $ は $N$ が持つ $n$ 個の自由変数の型で定める。
\end{proof}
\begin{theorem}[Curry-Howard 対応2]
任意の $\NJ$ の証明図 $P$ に対して、型付き $\lambda$ 項 $M = \Psi(P)$ が対応して、
$\Psi$ は $\Phi$ の逆対応になる。
\end{theorem}
\begin{fact}[Curry-Howard の同型性]
Curry-Howard 対応には次のような性質がある:
\begin{itemize}\setlength{\itemsep}{-5pt}
\item 正規証明図と正規 $\lambda$ 項が 1 対 1 に対応する。
\item さらに、証明図の正規化手続きと、$\lambda$ 項の（弱）正規化手続きも 1 対 1 に対応する。
\end{itemize}
\end{fact}
\begin{thebibliography}{99}
\bibitem{proofs_and_types} ``Proofs and Types'' / J.-Y.Girard, Y.Lafont and P.Taylor / Cambridge Univ. Press, 1989
\bibitem{asigara} ``情報科学における論理'' / 小野 寛晰 / 日本評論社, 1994
\end{thebibliography}
\end{document}
