t_uda/tex/2013/春セミナー「Scottの逆極限構成」
をテンプレートにして作成
[
トップ
] [
新規
|
一覧
|
検索
|
最終更新
|
ヘルプ
|
ログイン
]
開始行:
[[t_uda/tex]]
* Scott の逆極限構成〜計算機科学と圏論〜 @ 春セミナー201...
2013-03-27 (Wed.) の私 [[t_uda]] の発表で必要な前提知識な...
- S2S春セミナー2013
-- [[events/sss2013]]
- PDF版
#ref(sss2013-scott.pdf)
- TeXソースファイル
#ref(sss2013-scott.tex)
\documentclass[a4j,twocolumn]{jsarticle}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{braket}
\usepackage{theorem}
\usepackage{proof}
\usepackage{comment}
\usepackage[dvips]{graphicx}
\usepackage{kmathmacro}
\title{S2S春セミナー2013 \newline 「Scott の逆極限構成--...
\makeatletter
\author{Tomoki UDA (@t\_uda)}
\makeatother
\date{2013-03-27 Wed.}
\theoremstyle{break}
\newtheorem{theorem}{Th}[section]
\newtheorem{corollary}{Cor}[theorem]
\newtheorem{definition}[theorem]{Def}
\newtheorem{proposition}[theorem]{Prop}
\newtheorem{scheme}[theorem]{Scheme}
\newtheorem{lemma}[theorem]{Lem}
\newtheorem{example}{E.g.}
\newtheorem{proof}{<proof>}
\newtheorem{remark}{Remark}
\newtheorem{notation}{Notation}
\newtheorem{fact}{Fact.}
\renewcommand{\theproof}{}
\renewcommand{\theremark}{}
\renewcommand{\thenotation}{}
\renewcommand{\thefact}{}
\def\iso{ \cong }
\renewcommand{\C}{ \mathcal{C} }
\newcommand{\D}{ \mathcal{D} }
\newcommand{\Succ}{ \mathop{\mathrm{Succ}} }
\renewcommand{\succ}{ \mathop{\mathrm{succ}} }
\newcommand{\List}{ \mathop{\mathrm{List}} }
\newcommand{\Int}{ \mathord{\mathrm{Int}} }
\renewcommand{\Set}{ \mathord{\mathrm{\mathbf{Set}}} }
\newcommand{\CPO}{ \mathord{\mathrm{\mathbf{CPO}}} }
\newcommand{\embed}[1]{ #1^\mathrm{E} }
\newcommand{\CPOE}{ \embed{\CPO} }
\setcounter{section}{-1}
\begin{document}
\maketitle
\begin{abstract}
In this lecture, we consider fixpoint equations $X \iso...
a set function $F$. For example, the set of natural num...
the recursive equation $\N = \set{0} \cup \set{n+1 | n ...
which can be easily derived from the recursive definiti...
On the other hand, $\lambda$-terms also have the recurs...
which looks like $\Lambda \iso V + [\Lambda \to \Lambda...
in fact, any set $X$ does not satisfies $X \iso A \cup ...
Thus, set-theoretically, we cannot easily find a mathem...
which represents $\lambda$-terms. Our goal is to constr...
to this equation in categorical settings.
\begin{description}
\item[Keywords] 再帰方程式(recursive equation)、再帰的...
圏(category)、関手(functor)、$F$-代数(algebra)、不動...
始対象(initial object)、$\omega$-鎖(chain)、
余極限(colimit)、逆極限(limit or inverse limit)、逆極...
\end{description}
\end{abstract}
\begin{description}
\item[圏(category)]{
$\C$, $\D$, $\dots$
}
\item[対象(object)]{
$A$, $B$, $\dots$ \\
$A \in \C$
}
\item[射(morphism, arrow)]{
$f$, $g$, $h$, $\dots$ \\
$\map f from A to B ;$ in $\C$ \\
$\map g from A to B ;$ \\
$h \in \C(A, B)$
}
\item[関手(functor)]{
$\map F from \C to \D ;$
}
\end{description}
\section{Preliminaries}
この講義では、「圏論もしくは(関数型)プログラミング言語...
圏論の基本的な用語が分かるならば、講義の内容は難しくない...
講義を理解しやすいように、圏論の用語とこの講義のモチベー...
なお厳密な説明はしないので、詳しい定義は参考文献を見るこ...
\subsection{圏の基本的な用語}
講義では、圏を計算機科学的な視点で捉えるため、圏論の用語...
\begin{tabular}{ll}
対象 & 型 \\
& (型のついた集合)\\
射 & 副作用のない関数・プログラム \\
& (入力と出力の型が定められた写像)\\
圏 & プログラムの集まり \\
& (型と関数の集まり)\\
関手 & 型から別の型を作る対応
\end{tabular}
\begin{example}
例えば、$\Set$ は集合を対象、写像を射とする圏である。
整数型 $\Int$ は、整数全体の集合だと思えば、$\Set$ の対...
関数 $\mapmapsto \succ from \Int to \Int ; n to {n+1} ;$...
集合 $A$ に対して、$A$ の有限列全体の集合を $\List A$ と...
$\map \List from \Set to \Set ;$ は $\Set$ の間の関手に...
また、関数 $\map f from A to B ;$ に対し、新しい関数
$\mapmapsto \List f from \List A to \List B ; (x_i) to (...
を対応させることができる。(註: 関数型言語では $\List f$...
$\mathop{\mathrm{map}} f$ と書くことが多い。)
この時、任意の$\map f from A to B ;$ と $\map g from B t...
定義から明らかに $\List (g \comp f) = \List g \comp \Lis...
(実は、このように合成に関して分配則が成り立つ対応 $F$ ...
\end{example}
\subsection{半順序集合}
$\sqsubseteq$ を集合 $P$ 上の二項関係とする。この時、$(P...
二項関係 $\sqsubseteq$ が反射律、対称律、推移律を満たす...
この順序について増大列 $p_0 \sqsubseteq p_1 \sqsubseteq ...
$p \in P$ がこの増大列の上界であるとは、任意の $p_i$ に...
上界の中で最小のものが存在すれば、それを上限といい $\sqc...
実は、半順序集合 $(P, \sqsubseteq)$ はそれ自体を圏と見な...
つまり、この圏は、$P$ の元を対象として、$p \sqsubseteq q...
この圏の射と見なすのである。この意味において、圏は半順序...
後の第3節では、増大列や上界、上限を圏の上で一般化した概...
\begin{example}
計算機科学的な半順序集合の捉え方についても話そう。$P$ を...
この時、半順序 $\sqsubseteq$ を上手く定めて、$p \sqsubse...
プログラム $p$ よりも $q$ の方がより多くの情報を計算する...
この解釈の下で、(非自明な)増大列はプログラムの反復回数...
上限は反復回数を可能な限り増やした理想的なプログラムと思...
例えば、素数の集合を入力として取り、新しい素数を計算し付...
$p$ とすると、$p$ を反復適用することでより多くの情報が得...
無限回反復する理想的なプログラムは全ての素数を計算する(...
もちろん、素数全てを書き出すプログラムは現実には存在しな...
有限回の反復で打ち切れば現実的にもプログラムは作れるであ...
このように、上限への増大列は、理想的なプログラムを近似す...
\end{example}
\subsection{始対象}
任意の集合 $A \in \Set$ に対して、空集合 $\emptyset$ は ...
一般の圏 $\C$ において、任意の対象 $A \in \C$ への写像が...
対象 $0 \in \C$ がある時、これを始対象 (initial object) ...
どうせ $A$ への射が一つしかないのだから、これのためにわ...
記号を用意してやるのはシャクである。そのため、この射を $...
\begin{example}
半順序集合 $(P, \sqsubseteq)$ の場合の例を挙げよう。$P$ ...
これはつまり、任意の $p \in P$ に対して $0 \sqsubseteq p...
$0$ は圏として見た $P$ の始対象である。このように、始対...
\end{example}
前提知識についての軽い(?)説明はここまでにしよう。以下...
\section{Introduction}
\section{$F$-algebras and fixpoints}
\section{$\omega$-chains and limits}
\section{$\CPO$}
講義の内容は主に ~\cite{basic_cat_benjamin} を基にした。...
コンパクトにまとめられているので、興味があれば参照された...
\nocite{*}
\bibliographystyle{plain}
\bibliography{reference}
\end{document}
- 参考文献
#ref(reference.bib)
@book{
basic_cat_benjamin,
author = "Benjamin C. Pierce",
title = "Basic Category Theory for Computer Scientists",
publisher = "The MIT Press",
year = "1991"
}
@book{
alg_p_benjamin,
author = "Richard Bird and Oege de Moor",
title = "Algebra of Programming",
publisher = "Prentice Hall",
year = "1997"
}
@book{
tapl_benjamin,
author = "Benjamin C. Pierce",
title = "Types and Programming Languages",
publisher = "The MIT Press",
year = "2002"
}
@book{
topl_reynolds,
author = "John C. Reynolds",
title = "Theories of Programming Languages",
publisher = "Cambridge University Press",
year = "2009"
}
- keno さんの数学用マクロ集 [[kmathmacro>https://bitbucke...
-- commit-id: d79fb16d737996900239456bcf1021d5f4332a7c 時...
-- 圏論マクロおくれ
終了行:
[[t_uda/tex]]
* Scott の逆極限構成〜計算機科学と圏論〜 @ 春セミナー201...
2013-03-27 (Wed.) の私 [[t_uda]] の発表で必要な前提知識な...
- S2S春セミナー2013
-- [[events/sss2013]]
- PDF版
#ref(sss2013-scott.pdf)
- TeXソースファイル
#ref(sss2013-scott.tex)
\documentclass[a4j,twocolumn]{jsarticle}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{braket}
\usepackage{theorem}
\usepackage{proof}
\usepackage{comment}
\usepackage[dvips]{graphicx}
\usepackage{kmathmacro}
\title{S2S春セミナー2013 \newline 「Scott の逆極限構成--...
\makeatletter
\author{Tomoki UDA (@t\_uda)}
\makeatother
\date{2013-03-27 Wed.}
\theoremstyle{break}
\newtheorem{theorem}{Th}[section]
\newtheorem{corollary}{Cor}[theorem]
\newtheorem{definition}[theorem]{Def}
\newtheorem{proposition}[theorem]{Prop}
\newtheorem{scheme}[theorem]{Scheme}
\newtheorem{lemma}[theorem]{Lem}
\newtheorem{example}{E.g.}
\newtheorem{proof}{<proof>}
\newtheorem{remark}{Remark}
\newtheorem{notation}{Notation}
\newtheorem{fact}{Fact.}
\renewcommand{\theproof}{}
\renewcommand{\theremark}{}
\renewcommand{\thenotation}{}
\renewcommand{\thefact}{}
\def\iso{ \cong }
\renewcommand{\C}{ \mathcal{C} }
\newcommand{\D}{ \mathcal{D} }
\newcommand{\Succ}{ \mathop{\mathrm{Succ}} }
\renewcommand{\succ}{ \mathop{\mathrm{succ}} }
\newcommand{\List}{ \mathop{\mathrm{List}} }
\newcommand{\Int}{ \mathord{\mathrm{Int}} }
\renewcommand{\Set}{ \mathord{\mathrm{\mathbf{Set}}} }
\newcommand{\CPO}{ \mathord{\mathrm{\mathbf{CPO}}} }
\newcommand{\embed}[1]{ #1^\mathrm{E} }
\newcommand{\CPOE}{ \embed{\CPO} }
\setcounter{section}{-1}
\begin{document}
\maketitle
\begin{abstract}
In this lecture, we consider fixpoint equations $X \iso...
a set function $F$. For example, the set of natural num...
the recursive equation $\N = \set{0} \cup \set{n+1 | n ...
which can be easily derived from the recursive definiti...
On the other hand, $\lambda$-terms also have the recurs...
which looks like $\Lambda \iso V + [\Lambda \to \Lambda...
in fact, any set $X$ does not satisfies $X \iso A \cup ...
Thus, set-theoretically, we cannot easily find a mathem...
which represents $\lambda$-terms. Our goal is to constr...
to this equation in categorical settings.
\begin{description}
\item[Keywords] 再帰方程式(recursive equation)、再帰的...
圏(category)、関手(functor)、$F$-代数(algebra)、不動...
始対象(initial object)、$\omega$-鎖(chain)、
余極限(colimit)、逆極限(limit or inverse limit)、逆極...
\end{description}
\end{abstract}
\begin{description}
\item[圏(category)]{
$\C$, $\D$, $\dots$
}
\item[対象(object)]{
$A$, $B$, $\dots$ \\
$A \in \C$
}
\item[射(morphism, arrow)]{
$f$, $g$, $h$, $\dots$ \\
$\map f from A to B ;$ in $\C$ \\
$\map g from A to B ;$ \\
$h \in \C(A, B)$
}
\item[関手(functor)]{
$\map F from \C to \D ;$
}
\end{description}
\section{Preliminaries}
この講義では、「圏論もしくは(関数型)プログラミング言語...
圏論の基本的な用語が分かるならば、講義の内容は難しくない...
講義を理解しやすいように、圏論の用語とこの講義のモチベー...
なお厳密な説明はしないので、詳しい定義は参考文献を見るこ...
\subsection{圏の基本的な用語}
講義では、圏を計算機科学的な視点で捉えるため、圏論の用語...
\begin{tabular}{ll}
対象 & 型 \\
& (型のついた集合)\\
射 & 副作用のない関数・プログラム \\
& (入力と出力の型が定められた写像)\\
圏 & プログラムの集まり \\
& (型と関数の集まり)\\
関手 & 型から別の型を作る対応
\end{tabular}
\begin{example}
例えば、$\Set$ は集合を対象、写像を射とする圏である。
整数型 $\Int$ は、整数全体の集合だと思えば、$\Set$ の対...
関数 $\mapmapsto \succ from \Int to \Int ; n to {n+1} ;$...
集合 $A$ に対して、$A$ の有限列全体の集合を $\List A$ と...
$\map \List from \Set to \Set ;$ は $\Set$ の間の関手に...
また、関数 $\map f from A to B ;$ に対し、新しい関数
$\mapmapsto \List f from \List A to \List B ; (x_i) to (...
を対応させることができる。(註: 関数型言語では $\List f$...
$\mathop{\mathrm{map}} f$ と書くことが多い。)
この時、任意の$\map f from A to B ;$ と $\map g from B t...
定義から明らかに $\List (g \comp f) = \List g \comp \Lis...
(実は、このように合成に関して分配則が成り立つ対応 $F$ ...
\end{example}
\subsection{半順序集合}
$\sqsubseteq$ を集合 $P$ 上の二項関係とする。この時、$(P...
二項関係 $\sqsubseteq$ が反射律、対称律、推移律を満たす...
この順序について増大列 $p_0 \sqsubseteq p_1 \sqsubseteq ...
$p \in P$ がこの増大列の上界であるとは、任意の $p_i$ に...
上界の中で最小のものが存在すれば、それを上限といい $\sqc...
実は、半順序集合 $(P, \sqsubseteq)$ はそれ自体を圏と見な...
つまり、この圏は、$P$ の元を対象として、$p \sqsubseteq q...
この圏の射と見なすのである。この意味において、圏は半順序...
後の第3節では、増大列や上界、上限を圏の上で一般化した概...
\begin{example}
計算機科学的な半順序集合の捉え方についても話そう。$P$ を...
この時、半順序 $\sqsubseteq$ を上手く定めて、$p \sqsubse...
プログラム $p$ よりも $q$ の方がより多くの情報を計算する...
この解釈の下で、(非自明な)増大列はプログラムの反復回数...
上限は反復回数を可能な限り増やした理想的なプログラムと思...
例えば、素数の集合を入力として取り、新しい素数を計算し付...
$p$ とすると、$p$ を反復適用することでより多くの情報が得...
無限回反復する理想的なプログラムは全ての素数を計算する(...
もちろん、素数全てを書き出すプログラムは現実には存在しな...
有限回の反復で打ち切れば現実的にもプログラムは作れるであ...
このように、上限への増大列は、理想的なプログラムを近似す...
\end{example}
\subsection{始対象}
任意の集合 $A \in \Set$ に対して、空集合 $\emptyset$ は ...
一般の圏 $\C$ において、任意の対象 $A \in \C$ への写像が...
対象 $0 \in \C$ がある時、これを始対象 (initial object) ...
どうせ $A$ への射が一つしかないのだから、これのためにわ...
記号を用意してやるのはシャクである。そのため、この射を $...
\begin{example}
半順序集合 $(P, \sqsubseteq)$ の場合の例を挙げよう。$P$ ...
これはつまり、任意の $p \in P$ に対して $0 \sqsubseteq p...
$0$ は圏として見た $P$ の始対象である。このように、始対...
\end{example}
前提知識についての軽い(?)説明はここまでにしよう。以下...
\section{Introduction}
\section{$F$-algebras and fixpoints}
\section{$\omega$-chains and limits}
\section{$\CPO$}
講義の内容は主に ~\cite{basic_cat_benjamin} を基にした。...
コンパクトにまとめられているので、興味があれば参照された...
\nocite{*}
\bibliographystyle{plain}
\bibliography{reference}
\end{document}
- 参考文献
#ref(reference.bib)
@book{
basic_cat_benjamin,
author = "Benjamin C. Pierce",
title = "Basic Category Theory for Computer Scientists",
publisher = "The MIT Press",
year = "1991"
}
@book{
alg_p_benjamin,
author = "Richard Bird and Oege de Moor",
title = "Algebra of Programming",
publisher = "Prentice Hall",
year = "1997"
}
@book{
tapl_benjamin,
author = "Benjamin C. Pierce",
title = "Types and Programming Languages",
publisher = "The MIT Press",
year = "2002"
}
@book{
topl_reynolds,
author = "John C. Reynolds",
title = "Theories of Programming Languages",
publisher = "Cambridge University Press",
year = "2009"
}
- keno さんの数学用マクロ集 [[kmathmacro>https://bitbucke...
-- commit-id: d79fb16d737996900239456bcf1021d5f4332a7c 時...
-- 圏論マクロおくれ
ページ名: