\documentclass[a4paper, 12pt]{jarticle}

%%% amslatex %%%
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
%%% figure %%%
\usepackage{graphicx}
%%% array %%%
\usepackage{array}

%%% equation (section number. equation number)
\numberwithin{equation}{section}

%%% parameters %%%
%\setlength{\oddsidemargin}{31pt}
%\setlength{\topmargin}{31pt}
%\setlength{\textwidth}{389pt}
%\setlength{\textheight}{623pt}

%%% upright font in theorem environment %%%
\theoremstyle{definition}
\newtheorem{teigi}{定義}[section]

\newtheorem{hodai}{補題}[section]
\newtheorem{meidai}[hodai]{命題}
\newtheorem{teiri}[hodai]{定理}

\newtheorem{chuui}[hodai]{注意}

\newtheorem{kisoku}{規則}

%%% example environment %%%
\newtheorem{rei}{例}[section]



%%% proof environment %%%
\renewcommand{\proofname}{証明}
\renewcommand{\qed}{//}


%%% new command: place member center in tabular %%%
\newcommand{\Gcenter}[2]{
	\dimen0=\ht\strutbox%
	\advance\dimen0\dp\strutbox%
	\multiply\dimen0 by#1%
	\divide\dimen0 by2%
	\advance\dimen0 by-.5\normalbaselineskip
	\raisebox{-\dimen0}[0pt][0pt]{#2}}%

%%% titlepage %%%
\title{CSP 輪読会}
\author{杵渕 朋彦}
\date{}

\begin{document}

\section{復習}

\subsection{イントロダクション}
process というものが event の連鎖で書ける.

\subsection{絵図}
process は event を矢印でつないだもので書ける.

たいていは上から下へ流れる木構造になるけど,
recursive な定義があった場合は上に戻る.

\subsection{規則}
「process が等しい」という命題を厳密に定義するために規則を定めて,
その規則「のみ」を使って等しいということを示す.

数学, 特に代数系で使われる定義の手法.
この本の各章は「イメージの説明」→「規則で表現」→「Lisp もどきで実装」という流れになっている.

\section{今回の話}
\subsection{Implementation of processes, プロセスの実装}
P.18 の {\it interact} から.

最終行に括弧が足りない.
\begin{align*}
interact(A, P(car(k))), cdr(k)))
\end{align*}


\begin{align*}
interact(A, P, k) =\ 
& cons(menu(A, P),\ \text{if}\ car(k) = ``END \ \text{then}\\
& \qquad \text{;; if the END inputed, terminate an interaction.}\\
& \qquad NIL\\
& \text{else if}\ P(car(k)) = ``BLEEP \ \text{then}\\
& \qquad \qquad \text{;; if the inputed command is not yet implemented,}\\
& \qquad \qquad \text{;; just ``beep'' and do not change.}\\
& \qquad \qquad cons(``BLEEP,\ interact(A, P, cdr(k)))\\
& \qquad \text{else}\\
& \qquad \qquad \text{;; otherwise, accept the inputed command}\\
& \qquad \qquad \text{;; and make the specified transition.}\\
& \qquad \qquad interact(A, P(car(k)), cdr(k)))
\end{align*}

\begin{rei}
「プログラムのメニューを選んで入力していく」というアナロジー
\begin{itemize}
\item P: 入力を受け付け, 次の入力待ちの状態に遷移するプロセス. ところどころ実装してない.
\item A: P の入力一覧.
\item k: Keyboard Input.
\end{itemize}
\end{rei}

(ここから後は「LISP の実装系によってコードの書き方が様々になるよね」ということが書いてあるだけ.)

\subsection{Traces, トレース}


\begin{teigi}
\label{teigi:trace}
トレースとはプロセスが動作した記録. 厳密には以下で定義される.
\begin{enumerate}
\item $\langle \rangle$ は trace. (空 trace)
\item $x$ を event とするとき, $\langle x \rangle$ は trace.
\item $s = \langle s_0, s_1, s_2,\dots, s_n \rangle, t = \langle t_0, t_1, t_2,\dots, t_m \rangle$ を trace とするとき,\\
 $\langle s_0, s_1, s_2,\dots, s_n, t_0, t_1, t_2,\dots, t_m \rangle$ も trace. これを $s^\frown t$ と書く.
\end{enumerate}
\end{teigi}


\subsection{Operations on traces, トレース演算}

\subsubsection{Catenation, 結合}
定義 \ref{teigi:trace} で出てきた ${}^\frown$ のこと.

\begin{kisoku}[identity element, 単位元]
\label{kisoku:trace_identity}
$s^\frown\langle\rangle = \langle\rangle^\frown s = s$
\end{kisoku}

\begin{kisoku}[associative law, 結合則]
\label{kisoku:trace_assoc}
$s^\frown(t^\frown u) = (s^\frown t)^\frown u$
\end{kisoku}

ちなみに上の規則 \ref{kisoku:trace_identity}, \ref{kisoku:trace_assoc} を満たすものをモノイド (monoid) と呼ぶ.

\begin{kisoku}[left cancellation, 左簡約]
\label{kisoku:trace_left_cancel}
$s^\frown t = s^\frown u \Leftrightarrow t = u$
\end{kisoku}
\begin{kisoku}[right cancellation, 右簡約]
\label{kisoku:trace_right_cancel}
$s^\frown t = u^\frown t \Leftrightarrow s = u$
\end{kisoku}
\begin{kisoku}
$s^\frown t = \langle\rangle \Leftrightarrow s = \langle\rangle \wedge t = \langle\rangle$
\end{kisoku}

ちなみにここまでの 5 つの規則は公理である.

\begin{teigi}
trace → trace 型の関数 $f$ が {\it strict} であるとは,
\begin{align*}
f(\langle\rangle) = \langle\rangle
\end{align*}
を満たすということ.
\end{teigi}

\begin{teigi}
trace → trace 型の関数 $f$ が {\it distributive} であるとは,
\begin{align*}
f(s^\frown t) = f(s)^\frown f(t)
\end{align*}
を満たすということ.
\end{teigi}

規則 \ref{kisoku:trace_left_cancel}, \ref{kisoku:trace_right_cancel} から, distributive ならば strict であることが分かる.
数学では distributive な関数を (monoid 上の) homomorphism (準同型写像) と呼ぶ.

\begin{teigi}
結合演算を乗算に見立ててべき乗を定義する.
\begin{kisoku}
$t^0 = \langle \rangle$
\end{kisoku}
\begin{kisoku}
$t^{n + 1} = t^\frown t^n$
\end{kisoku}
\end{teigi}

これから帰納法で以下が示せる.

\begin{kisoku}
$t^{n + 1} = t^{n\frown} t$
\end{kisoku}
\begin{kisoku}
$(s^\frown t)^{n + 1} = s^\frown (t^\frown s)^{n\frown} t$
\end{kisoku}

\subsubsection{Restriction, 絞り込み}
\setcounter{kisoku}{0}

\begin{teigi}
定義 \ref{teigi:trace} と同じ形式で記述する.
\begin{kisoku}
$\langle\rangle \uparrow A = \langle\rangle$
\end{kisoku}
\begin{kisoku}
$
\langle x \rangle \uparrow A = 
\begin{cases}
\langle\rangle & \text{if}\ x \in A\\
\langle x \rangle & \text{otherwise}
\end{cases}
$
\end{kisoku}
\begin{kisoku}
$(s^\frown t) \uparrow A = (s \uparrow A)^\frown (t \uparrow A)$
\end{kisoku}
\end{teigi}

\setcounter{kisoku}{4}

この定義から以下が示せる.
\begin{kisoku}
$s \uparrow \{\} = \langle\rangle$
\end{kisoku}
\begin{kisoku}
$(s \uparrow A) \uparrow B = s \uparrow (A \cap B)$
\end{kisoku}

\subsubsection{Head and tail, 頭と尾}

要は Lisp の car と cdr. なので以下(ry

\subsubsection{Star, 星?}

正規表現で出てくる asterisk と同じ意味.


\begin{teigi}
\setcounter{kisoku}{0}
\begin{kisoku}
$\langle\rangle \in A^*$
\end{kisoku}
\begin{kisoku}
$\langle x \rangle \in A^* \iff x \in A$
\end{kisoku}
\begin{kisoku}
$(s^\frown t) \in A^* \iff s \in A^* \wedge \ t \in A^*$
\end{kisoku}
\end{teigi}

\subsubsection{Ordering, 順序付け}
\begin{teigi}
trace には順序が入れられる.
trace の集合は「順序付きモノイド」で右演算が順序を保つ.
\begin{align*}
s \leq t \equiv \exists u\ \text{s.t.}\ s^\frown u = t
\end{align*}
\end{teigi}

\subsubsection{Length, 長さ}
そのまんまの意味.


\end{document}
