t_uda/tex/2010/京名合宿レジュメ
をテンプレートにして作成
[
トップ
] [
新規
|
一覧
|
検索
|
最終更新
|
ヘルプ
|
ログイン
]
開始行:
[[t_uda/tex]]
* 京大名大合同合宿 [#n71cc5bc]
[[H.22年度 京大名大合同合宿>http://www.geocities.jp/meida...
* 「Curry-Howard対応」レジュメ [#pc58d72b]
私は「Curry-Howard対応」というタイトルで 50 分の発表をし...
-PDF版
#ref(t_uda/kyomei_h22_resume.pdf)
-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 追記:]
この文書は京大名大合同合宿において、宇田が発表し...
そもそも、前提知識を一切仮定せずに 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 \i...
\end{enumerate}
\end{definition}
\begin{remark}
$ P \land Q $ は"$P$ かつ $Q$"と解釈できる。
ここでは扱わないが、必要に応じて"$P$ または $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 ...
これは不都合なので、カッコ付きで定義しておいて改めて...
\end{remark}
\begin{definition}[推論規則]\label{推論規則}
$ \NJ|_{\land,\imply} $ の推論規則を次の図式で定める:
\begin{enumerate}\setlength{\itemsep}{5pt}\setlength...
\item \fbox{
\infer[(Axiom)]{P \vdash P}{}
}
\item \fbox{
\infer[(\land I)]{\Gamma, \Sigma \vdash P \l...
\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 \...
\Gamma, P, \Sigma \vdash Q
}
} \fbox{
\infer[(\imply I')]{\Gamma, P, \Sigma \vdash...
\Gamma, P, \Sigma \vdash Q
}
}
\item \fbox{
\infer[(\imply E)]{\Gamma, \Sigma \vdash Q}{
\Gamma \vdash P \imply Q & \Sigma \v...
}
}
\end{enumerate}
ここで、$P,Q$ は論理式、$\Gamma$ や $\Sigma$ は適当...
\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$ に至る証明図が存在する時...
\item 論理式 $P$ が $\NJ$ において証明可能とは、...
\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...
図式 \fbox{ \infer{Q}{P} } は、(適当な仮定の下で)...
\end{remark}
\begin{example}[$ P \imply Q \imply R \vdash_{\NJ} P \la...
\ \\
\fbox{
\infer{ P \imply Q \imply R \vdash P \land Q \im...
\infer{ P \imply Q \imply R, P \land Q \vdas...
\infer{ P \imply Q \imply R, P \land Q \...
\infer{ P \imply Q \imply R, P \land...
&
\infer{ P \imply Q \imply R, P \land...
\infer{ P \imply Q \imply R, P \...
}
} &
\infer{ P \imply Q \imply R, P \land Q \...
\infer{ P \imply Q \imply R, P \land...
}
}
}
}
\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...
\end{enumerate}
\end{definition}
\begin{remark}
1において、型変数の代わりに有限個の原始型(型定数)...
2についてはそれぞれ、$ U \to V $ は $U$ から $V$ へ...
型は集合のことと考えれば分かりやすいが、必ずしも集合...
\end{remark}
\begin{definition}[型付き $\lambda$ 項]\label{λ項}
\begin{enumerate}\setlength{\itemsep}{-5pt}
\item 型 $U$ に対し、型 $U$ に属する変数 $ x^U, ...
\item 型 $U$ の $\lambda$ 項 $M$ と型 $V$ の $\l...
\item 型 $ U \times V $ の $\lambda$ 項 $M$ に対...
\item 型 $U$ の変数 $x^U$ と型 $V$ の $\lambda$ ...
\item 型 $ U \to V $ の $\lambda$ 項 $M$ と型 $U...
\end{enumerate}
\end{definition}
\begin{notation}
混乱のない限り、次のように略記して良い:
\begin{enumerate}\setlength{\itemsep}{-5pt}
\item $ (\lambda{x}.(\lambda{y}.M)) = \lambda{x}...
\item $ ((MN)L) = (MNL) = MNL $
\end{enumerate}
また本稿では必要に応じて、 $\lambda$ 項 $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]$ で置き...
得ることを、束縛変数の置き換えと呼ぶ。
この時、繰り返し $P$ の束縛変数を置き換えて $Q$ が得...
$Q$ は $P$ から $\alpha$ 変換で得られると言い、$ P =...
\end{definition}
\begin{proposition}[$\alpha$ 同値]
$=_\alpha$ は同値関係である。
\end{proposition}
以降、 $\lambda$ 項は $\alpha$ 同値を除いて同一視するこ...
\section{Curry-Howard 対応}
\setcounter{theorem}{-1}
論理式の定義 \ref{論理式} と型の定義 \ref{型} 及び、$\N...
\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}) := $...
\infer{ \pair{M}{N} : U \times V }{
D(M) & D(N)
}
}
\item $ M :: U \times V $ に対し、$ D(\pi^1{M}) ...
\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) ...
\infer{ \lambda{x}.M : U \to V }{ D(M) }
}
\item $ M :: U \to V, N::U $ に対し、$ D(MN) := ...
\infer{ MN : V }{
D(M) & D(N)
}
}
\end{enumerate}
\end{definition}
\begin{theorem}[Curry-Howard 対応1]
任意の $\lambda$ 項 $M::V$ に対して、$\NJ$ 証明図 $P...
$M$ の自由変数全体 $ FV(M) = \{ x_1::U_1, \cdots, x_...
証明図 $P$ は $ U_1, \cdots, U_n $ から $V$ に至る証...
\end{theorem}
\begin{proof}
$D(M)$ の $ \times, \to $ をそれぞれ $ \land, \imply...
図の中の全ての $\lambda$ 項の部分 $N:$ を $ U_1, \cd...
得られる図を $\Phi(M)$ とすればよい。
但しここで、 $ U_1, \cdots, U_n $ は $N$ が持つ $n$ ...
\end{proof}
\begin{theorem}[Curry-Howard 対応2]
任意の $\NJ$ の証明図 $P$ に対して、型付き $\lambda$...
$\Psi$ は $\Phi$ の逆対応になる。
\end{theorem}
\begin{fact}[Curry-Howard の同型性]
Curry-Howard 対応には次のような性質がある:
\begin{itemize}\setlength{\itemsep}{-5pt}
\item 正規証明図と正規 $\lambda$ 項が 1 対 1 に...
\item さらに、証明図の正規化手続きと、$\lambda$ ...
\end{itemize}
\end{fact}
\begin{thebibliography}{99}
\bibitem{proofs_and_types} ``Proofs and Types'' / J....
\bibitem{asigara} ``情報科学における論理'' / 小野 寛...
\end{thebibliography}
\end{document}
終了行:
[[t_uda/tex]]
* 京大名大合同合宿 [#n71cc5bc]
[[H.22年度 京大名大合同合宿>http://www.geocities.jp/meida...
* 「Curry-Howard対応」レジュメ [#pc58d72b]
私は「Curry-Howard対応」というタイトルで 50 分の発表をし...
-PDF版
#ref(t_uda/kyomei_h22_resume.pdf)
-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 追記:]
この文書は京大名大合同合宿において、宇田が発表し...
そもそも、前提知識を一切仮定せずに 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 \i...
\end{enumerate}
\end{definition}
\begin{remark}
$ P \land Q $ は"$P$ かつ $Q$"と解釈できる。
ここでは扱わないが、必要に応じて"$P$ または $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 ...
これは不都合なので、カッコ付きで定義しておいて改めて...
\end{remark}
\begin{definition}[推論規則]\label{推論規則}
$ \NJ|_{\land,\imply} $ の推論規則を次の図式で定める:
\begin{enumerate}\setlength{\itemsep}{5pt}\setlength...
\item \fbox{
\infer[(Axiom)]{P \vdash P}{}
}
\item \fbox{
\infer[(\land I)]{\Gamma, \Sigma \vdash P \l...
\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 \...
\Gamma, P, \Sigma \vdash Q
}
} \fbox{
\infer[(\imply I')]{\Gamma, P, \Sigma \vdash...
\Gamma, P, \Sigma \vdash Q
}
}
\item \fbox{
\infer[(\imply E)]{\Gamma, \Sigma \vdash Q}{
\Gamma \vdash P \imply Q & \Sigma \v...
}
}
\end{enumerate}
ここで、$P,Q$ は論理式、$\Gamma$ や $\Sigma$ は適当...
\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$ に至る証明図が存在する時...
\item 論理式 $P$ が $\NJ$ において証明可能とは、...
\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...
図式 \fbox{ \infer{Q}{P} } は、(適当な仮定の下で)...
\end{remark}
\begin{example}[$ P \imply Q \imply R \vdash_{\NJ} P \la...
\ \\
\fbox{
\infer{ P \imply Q \imply R \vdash P \land Q \im...
\infer{ P \imply Q \imply R, P \land Q \vdas...
\infer{ P \imply Q \imply R, P \land Q \...
\infer{ P \imply Q \imply R, P \land...
&
\infer{ P \imply Q \imply R, P \land...
\infer{ P \imply Q \imply R, P \...
}
} &
\infer{ P \imply Q \imply R, P \land Q \...
\infer{ P \imply Q \imply R, P \land...
}
}
}
}
\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...
\end{enumerate}
\end{definition}
\begin{remark}
1において、型変数の代わりに有限個の原始型(型定数)...
2についてはそれぞれ、$ U \to V $ は $U$ から $V$ へ...
型は集合のことと考えれば分かりやすいが、必ずしも集合...
\end{remark}
\begin{definition}[型付き $\lambda$ 項]\label{λ項}
\begin{enumerate}\setlength{\itemsep}{-5pt}
\item 型 $U$ に対し、型 $U$ に属する変数 $ x^U, ...
\item 型 $U$ の $\lambda$ 項 $M$ と型 $V$ の $\l...
\item 型 $ U \times V $ の $\lambda$ 項 $M$ に対...
\item 型 $U$ の変数 $x^U$ と型 $V$ の $\lambda$ ...
\item 型 $ U \to V $ の $\lambda$ 項 $M$ と型 $U...
\end{enumerate}
\end{definition}
\begin{notation}
混乱のない限り、次のように略記して良い:
\begin{enumerate}\setlength{\itemsep}{-5pt}
\item $ (\lambda{x}.(\lambda{y}.M)) = \lambda{x}...
\item $ ((MN)L) = (MNL) = MNL $
\end{enumerate}
また本稿では必要に応じて、 $\lambda$ 項 $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]$ で置き...
得ることを、束縛変数の置き換えと呼ぶ。
この時、繰り返し $P$ の束縛変数を置き換えて $Q$ が得...
$Q$ は $P$ から $\alpha$ 変換で得られると言い、$ P =...
\end{definition}
\begin{proposition}[$\alpha$ 同値]
$=_\alpha$ は同値関係である。
\end{proposition}
以降、 $\lambda$ 項は $\alpha$ 同値を除いて同一視するこ...
\section{Curry-Howard 対応}
\setcounter{theorem}{-1}
論理式の定義 \ref{論理式} と型の定義 \ref{型} 及び、$\N...
\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}) := $...
\infer{ \pair{M}{N} : U \times V }{
D(M) & D(N)
}
}
\item $ M :: U \times V $ に対し、$ D(\pi^1{M}) ...
\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) ...
\infer{ \lambda{x}.M : U \to V }{ D(M) }
}
\item $ M :: U \to V, N::U $ に対し、$ D(MN) := ...
\infer{ MN : V }{
D(M) & D(N)
}
}
\end{enumerate}
\end{definition}
\begin{theorem}[Curry-Howard 対応1]
任意の $\lambda$ 項 $M::V$ に対して、$\NJ$ 証明図 $P...
$M$ の自由変数全体 $ FV(M) = \{ x_1::U_1, \cdots, x_...
証明図 $P$ は $ U_1, \cdots, U_n $ から $V$ に至る証...
\end{theorem}
\begin{proof}
$D(M)$ の $ \times, \to $ をそれぞれ $ \land, \imply...
図の中の全ての $\lambda$ 項の部分 $N:$ を $ U_1, \cd...
得られる図を $\Phi(M)$ とすればよい。
但しここで、 $ U_1, \cdots, U_n $ は $N$ が持つ $n$ ...
\end{proof}
\begin{theorem}[Curry-Howard 対応2]
任意の $\NJ$ の証明図 $P$ に対して、型付き $\lambda$...
$\Psi$ は $\Phi$ の逆対応になる。
\end{theorem}
\begin{fact}[Curry-Howard の同型性]
Curry-Howard 対応には次のような性質がある:
\begin{itemize}\setlength{\itemsep}{-5pt}
\item 正規証明図と正規 $\lambda$ 項が 1 対 1 に...
\item さらに、証明図の正規化手続きと、$\lambda$ ...
\end{itemize}
\end{fact}
\begin{thebibliography}{99}
\bibitem{proofs_and_types} ``Proofs and Types'' / J....
\bibitem{asigara} ``情報科学における論理'' / 小野 寛...
\end{thebibliography}
\end{document}
ページ名: