Wednesday, December 18, 2013

ノルウェーの司法: 修復的司法と応報的司法の対比

ツイッターでノルウェーの監獄が快適すぎると写真付きで話題になっている。元ネタは TIME 誌のこの特集記事のようだ: Inside the World's Most Humane Prison
2011 年ウトヤとオスロで計 77 人を殺害したテロリスト、Anders Breivik が収監されると見られている刑務所を取材している。正直私の自宅よりよっぽど快適そうなので移り住みたい。TL でも「APLAS (という学会) に参加したらノルウェーの監獄並の施設に寝泊まりできますよ!」とか言われたい放題だ。

何でそんな事になってるのかと思って (TIME の記事では「社会復帰を促すため」の一言しか書いてない)、ノルウェーの司法制度について調べた所、the Atlantic のこんな記事を見つけた。A Different Justice: Why Anders Breivik Only Got 21 Years for Killing 77 People
ノルウェーは修復的司法なので応報的司法のアメリカ(日本も)とは根本的に考え方が違うという解説記事。結構衝撃的な意識の違いだ。記事の内容はここに要約しておくが、出来れば原文を読んだほうが良いと思う。

Breivik 裁判では被害者や遺族が、死んだ被害者の夢などを陳述した。Breivik の前で、死んだ77人全員分、一人一人(というか一家族ごと)に十分な時間が与えられて嘆きを遺族同士共有しあう機会が与えられたのだそうだ。裁判の一環として。これは証拠や、量刑を重くせよという情緒的圧力として行われたのではなく、感情を吐露する場を与えることによる被害者のケアのためであり、また加害者に己の罪を意識させるためでもあるという。(勿論裁判では証拠の精査なども行う。)刑務所の整った環境も修復的司法の一環で、受刑者が自分の罪と向き合う痛みへ向けた準備の手助けなのだそうだ。Atlantic の記事によれば、端的に言えば (日米などの) 応報的司法では「因果応報」という抽象的な正義を満たす事を目的にしており加害者は受動的に罰を受ける立場なのに対し、ノルウェーの修復的司法では加害者は積極的に罪と向き合い被害者や社会に対して可能な限りの償いを立場なのだと。また修復的司法では加害者は「罰せられるべき悪」ではなく「修復されるべき壊れた個人」であり、刑も「罰」ではなく「強制治療」なのだという事だそうだ。記事によればこのシステムは犯罪率を下げ、犯罪者収容のコストも下げ(!)、再犯率も下げるのだという。

※「こんな至れり尽くせりしといてコストが下がるわけないだろう!」とかいう人がいるかも知れないので念の為言っておくと、受刑者一人あたりのコストが上がってもその結果再犯率が下がり、重犯罪に走る前に軽犯罪だけで更生する人が増えるなら全体のコストは下がる。

いかにも北欧らしい進歩的で合理的なシステムだ。遺族感情が気になるところだけど、報道を見る限り割と判決に満足してるらしい。ただし遺族感情に関する統計的なデータは出ていない。死刑廃止とかもこういう修復的司法の潮流の一部なんだろう。

※ Breivik に言い渡された 21 年の刑期はノルウェーでは最長。ただし Breivik に限っては修復的司法の目指す積極的な修復行為を行わない (平たく言うと反省してないし、しない) ので事実上死ぬまで刑期が延長され続ける見込み。修復的行為に至るまで、いつまででも強制的に療養させるぞという事か。

この記事を見て、日本の司法制度についても色々言われている事についてちょっと見方が変わった。その最たるものは死刑存廃議論だ。日本の死刑廃止論ではどうも冤罪の可能性がどうだとか、死刑自体の犯罪抑止効果がどうだとか、遺族感情のためには殺すしかない、いやそれは野蛮で不毛だとか、死刑そのものしか見てない議論の声が非常に大きい。しかしノルウェーのシステムを見る限り、死刑廃止はむしろもっと大きく包括的な司法制度改革に根ざしているようだ。つまり
  •  罰するのではなく、罪と向き合わせる (苦しめるのではなく、後悔させる)
  •  因果応報ではなく、感情や関係の修復を目指す
という目的の転換を経て、その一環として「じゃあ死刑は要らないや」となっているのであって、単に死刑だけが何か特に野蛮だから止めとこうという話ではないという事だ。なるほど、これは確かに近現代の「次」の社会のあり方として良さそうではある。

しかし、修復的司法を今すぐ日本に導入しても (日本の重大犯罪の) 被害者や遺族は納得しないだろうと思う。私もきっといまいち納得できないだろう。目には目を、の正義観が意識の底まで刷り込まれているから。悪いことをした奴には損をしてもらわないと気がすまない。こうした処罰感情はきっと説得によって動かされることは殆ど無いだろうと思う。こういう根深い感情は、それを抱いている人達が世代交代で死に絶えることによって変革されるものだからだ。でも、被害者のケアとしての裁判中の陳述機会を与えたりとかいうのは割とすぐ受け入れられる可能性がある。そうした修復的司法の手法を少しづつ導入することを目指したら、次の世代ぐらいには意識が変わって死刑廃止論はもっと受け入れられやすくなってるのかも知れない。

追記: 勿論、既にそういう方向性で死刑廃止論とかを含めた司法改革を求めている人はいるんだろうけど、それがもっと一般的になったほうが建設的なんじゃないかという話。

Saturday, December 14, 2013

ガチ勢になるための圏論勉強会 第二回 まとめ

ガチ勢になるための圏論勉強会第二回で読んだ、A.Pitts の Relational Properties of Domains の定理 3.3 の証明のまとめ。これが有名な "inverse limit construction" なのだろう。多分。定理の背景は論文か第一回のまとめ参照。


定理 3.3: 局所連続な関手 $F : \mathbf{Cpo}^\text{op}_\bot \times \mathbf{Cpo}_\bot \rightarrow \mathbf{Cpo}_\bot$ は常に最小不変性、つまり $i : F(D,D) \cong D$ で $\operatorname{fix}(\lambda f.\ i\circ F(f,f) \circ i^{-1}) = \operatorname{id}$ となるような $i$, $D$ を持つ。

証明:
まず\begin{align*}
f^\circ\circ f &= \operatorname{id} \\
f \circ f^\circ &\sqsubseteq \operatorname{id}
\end{align*}となるような $f^\circ$ が存在する時、$f$ は埋め込みであると言い、$f^\circ$ はそれに対応する射影と呼ぶ。$f$ が決まると、それに対応する $f^\circ$ は高々一つしか無い。論文では証明されていないが、勉強会では次のように証明した。仮に射影の条件を満たす別の関数 $g$があったとする。
\begin{align*}
g\circ f &= \operatorname{id} \\
f \circ g &\sqsubseteq \operatorname{id}
\end{align*}すると
\begin{align*}
f^\circ &= g \circ f \circ f^\circ & \ \ (\because g \circ f = \operatorname{id}) \\
&\sqsubseteq g & \ \ (\because f\circ f^\circ \sqsubseteq \operatorname{id})
\end{align*}で、
\begin{align*}
g &= f^\circ \circ f \circ g & \ \ (\because f^\circ \circ f = \operatorname{id}) \\
&\sqsubseteq f^\circ & \ \ (\because f\circ g \sqsubseteq \operatorname{id})
\end{align*}なので $g = f^\circ$ となり、$f$ に対応する射影は無二であることが分かる。関数合成が単調である事の証明は省く。[注1] 論文では書かれていないが、逆に射影が決まると埋め込みが (最大) 一つに決まる。証明は同様。

この埋め込み←→射影の対応を使って次のような双方向の鎖を作る。[注2]
\begin{equation}\label{eq:chain}
D_0 \underset{\underset{i_0^\circ}{\leftharpoondown}}{\overset{i_0}{\rightharpoonup}} D_1 \underset{\underset{i_1^\circ}{\leftharpoondown}}{\overset{i_1}{\rightharpoonup}} D_2 \underset{\underset{i_2^\circ}{\leftharpoondown}}{\overset{i_2}{\rightharpoonup}} \cdots
\end{equation}where
\begin{align*}
D_0 &= \varnothing_\bot \\
D_{n+1} &= F(D_n, D_n) \\
i_0 &= \bot_{\varnothing_\bot \rightarrow D_1} \\
i_{n+1} &= F(i_n^\circ, i_n)
\end{align*}この鎖の極限 (直観的に言えば鎖を無限に右に辿って行き着く対象) が、定理の主張している $D$ になる。この鎖の構成は (反変と共変、二種類の引数に対応する為 $-^\circ$ を駆使していることを除けば) 単純に $F$ を $\bot$ な対象と $\bot$ な射に繰り返し適用しているだけなので、その極限が不動点になるというのはそれほど不思議な事ではない。

この事を厳密に論証するには $D$ を天下り的に与えてそれが圏論的な極限になっていることを示す (Pitts は余極限としているが、どちらでも論証できる)。その上で元の鎖を $F$ で写した新たな鎖
\[
F\,(D_0,D_0) \underset{\underset{F\,(i_0, i_0^\circ)}{\leftharpoondown}}{\overset{F\,(i_0^\circ,i_0)}{\rightharpoonup}}
F\,(D_1,D_1) \underset{\underset{F\,(i_1, i_1^\circ)}{\leftharpoondown}}{\overset{F\,(i_1^\circ,i_1)}{\rightharpoonup}}
F\,(D_2,D_2) \underset{\underset{F\,(i_2, i_2^\circ)}{\leftharpoondown}}{\overset{F\,(i_2^\circ,i_2)}{\rightharpoonup}}
\cdots
\]を考える。これは、元の鎖の定義を見れば分かるように単に $\eqref{eq:chain}$ から $D_0$ を省いて得られる
\begin{equation}
D_1 \underset{\underset{i_1^\circ}{\leftharpoondown}}{\overset{i_1}{\rightharpoonup}} D_2 \underset{\underset{i_2^\circ}{\leftharpoondown}}{\overset{i_2}{\rightharpoonup}} \cdots \label{eq:chain2}
\end{equation}と同じなので、元の鎖と同じ極限を持つはずである (up to iso)。この同一性を立証する同型射が $i$ になる。

まず天下り的に
\[
D = \left\{x \in D_n : \forall n.\ x_n = i_n^\circ\,x_{n+1}  \right\}
\]とする。直観的には例えば無限リスト [1..] の表示はそれの有限な近似の列 $(\bot, (1:\bot), (1:1:\bot), \ldots) \in D$ と同一視するという事らしい。コーシー列で実数を構成するのに似ている。$D_n$ の鎖では右に行くほど $F$ の適用回数が増える (= より深いデータ構造が定義される) ので、より深くまで定義された近似値が拾ってこれる。$x_n = i_n^\circ\,x_{n+1}$ という制約は例えば $(\bot, (1:\bot), (2:3:\bot), (1:5:3\bot))$ のように互いに近似関係にないデータをそれぞれの $D_n$ から拾ってくるのを禁止している。

\begin{gather*}\pi_n  : D \rightarrow D_n \\
\pi_n\,(x_0, x_1, \ldots, x_n, \ldots) = x_n
\end{gather*}という射影は次のような埋め込みと対応する (i.e. $j_n^\circ = \pi_n$)。
\begin{gather*}
j_n : D_n \rightarrow D \\
j_n\,x_n =  (\ldots, i^\circ_{n-2}\,(i^\circ_{n-1}\,x_n), i^\circ_{n-1}\,x_n, x_n, i_n\,x_n, i_{n+1}\,(i_n\,x_n), \ldots)
\end{gather*} $j_n$ は $(x_0,x_1, \ldots, x_n, \ldots)$ から $x_n$ だけ与えられたら、「$x_n$ より左は $i_k^\circ$ で要素を復元し、$x_n$ 右は $i_k$ で復元する」という手法でできるだけ元の列を復元する。$D$ の定義より左に行く時の復元は完璧な復元だが、右に行く時の復元は元のデータより ($\sqsubseteq$ で) 小さい。つまり $j_n$ は元の列を $n$ 個目まで完璧に復元するので、上限を取ると完全な逆関数になることが予想される。この予想は、下の補題の後に実際に証明する。

$D$ が $\eqref{eq:chain2}$ の鎖の極限であるとは、任意の $D'$ と $\pi_n' : D' \rightarrow D_n$ に対して、$\forall n.\ \pi_n' = i_n^\circ \circ \pi_{n+1}'$ が成り立つならば $\forall n.\ \pi_n \circ k = \pi_n'$ となる $k : D' \rightarrow D$ がただ一つ存在することである。これを示すために一つ補題を証明しておく。

補題:
$\forall n.\ \pi_n' = i_n^\circ \circ \pi_{n+1}'$ となるような $D'$ と $\pi_n'$ が与えられた時、$j_n \circ \pi_n'$ は上昇列であって
\[
\pi_m \circ \bigsqcup_n j_n \circ \pi_n' = \pi_m'
\]となる。これは $D' = D, \pi_n' = \pi_n$ の場合でも成り立つ。


証明:
この証明の概要は輪講担当者の奥村がこのカンペから拾ってきた。まず
\begin{equation}\label{eq:pi_expand}
\pi_n =  i_n^\circ \circ \pi_{n+1} \hspace{4ex}
\pi_n' =  i_n^\circ \circ \pi_{n+1}' \hspace{4ex}
j_n = j_{n+1} \circ i_n\end{equation}である。これらを利用すると
\begin{align*}
j_n \circ \pi_n' &=  j_{n+1}\circ i_n \circ i_n^\circ \circ \pi_{n+1} \\
&\sqsubseteq j_{n+1} \circ \pi_{n+1} & (\because i_n \circ i_n^\circ \sqsubseteq \operatorname{id})
\end{align*}つまり $j_n \circ \pi_n'$ が上昇列であることが分かり、さらに、$m \le n$ ならば
\begin{align}
\pi_m \circ j_n \circ \pi_n' &= i_m \circ i_{m+1} \circ \cdots \circ i_{n-1} \circ \pi_{n} \circ j_n \circ \pi_n' & \notag \\
&= i_m \circ i_{m+1} \circ \cdots \circ i_{n-1} \circ \pi_n' \notag \\
&= \pi_m' \label{eq:pi_j_pi}
\end{align}となる事も分かる。従って、任意の $m$ について
\begin{align*}
\pi_m \circ \bigsqcup \{j_n \circ \pi_n' : n \ge 0\} &= \pi_m \circ \bigsqcup \{j_n \circ \pi_n' : n \ge m\}  & (j_n \circ \pi_n' \text{は上昇列だから}) \\
&= \bigsqcup \{\pi_m \circ j_n \circ \pi_n' : n \ge m \} \\
&= \bigsqcup \{\pi_m' : n \ge m\} & \text{\eqref{eq:pi_j_pi} より} \\
&= \bigsqcup \{\pi_m'\} = \pi_m'
\end{align*}となる。
(補題終わり)

ここで $k = \bigsqcup_n j_n \circ \pi_n'$ とする。補題によりこれは well-defined であり、しかも全ての $n$ について
\[
\pi_n \circ k =  \pi_n \circ \bigsqcup_m j_m \circ \pi_m' = \pi_n'
\]である。従って、条件を満たす $k$ が最低一つは存在する。逆に $\forall n.\ \pi_n \circ k =  \pi_n'$ が成り立つならば、
\begin{equation}\label{eq:pi_k_j_pi}
j_n\circ \pi_n \circ k = j_n \circ \pi_n'
\end{equation}である。補題により右辺が上昇列なので両辺が上昇列となり、上限を取ることが出来る。補題で $D' = D$ とするとどの $n$ についても $\forall n.\ \pi_n \circ \bigsqcup_m j_m \circ \pi_m = \pi_n$ つまり
\[
\pi_n \left(\left(\bigsqcup_m j_m \circ \pi_m\right)\,(x_0,x_1,\ldots)\right) = \pi_n (x_0,x_1,\ldots) = x_n
\]
なので、$\bigsqcup_m j_m \circ \pi_m = \operatorname{id}$。従って、$\eqref{eq:pi_k_j_pi}$ の両辺の上限を取ると
\[
k = \operatorname{id} \circ k = \bigsqcup_n j_n \circ \pi_n \circ k = \bigsqcup_n j_n \circ \pi_n'
\]となり、条件を満たす $k$ は一意であることが示せた。よって $D$ は $\eqref{eq:chain2}$ の極限である。

論文にもある通り、上記の論証は $i_n$ や $j_n$ の性質の内、$F$ が保存するものしか使っていないので $F(D,D)$ は
\[
F\,(D_0,D_0) \underset{\underset{F\,(i_0, i_0^\circ)}{\leftharpoondown}}{\overset{F\,(i_0^\circ,i_0)}{\rightharpoonup}}
F\,(D_1,D_1) \underset{\underset{F\,(i_1, i_1^\circ)}{\leftharpoondown}}{\overset{F\,(i_1^\circ,i_1)}{\rightharpoonup}}
F\,(D_2,D_2) \underset{\underset{F\,(i_2, i_2^\circ)}{\leftharpoondown}}{\overset{F\,(i_2^\circ,i_2)}{\rightharpoonup}}
\cdots
\]の極限である。しかしこの鎖はそのまま $\eqref{eq:chain2}$ の鎖なので、$D$ も $F(D,D)$ も同じ鎖 $\eqref{eq:chain2}$ の極限である。極限は一意なので $i : F(D,D) \cong D$ が存在し、この同型射は $D' = F(D,D)$ と置いた時の $k$ と一致する。[注3]

したがって、
\[
F(j_n, \pi_n)\circ i^{-1} = F(j_n, \pi_n) \circ k = \pi_n
\] (論文は極限ではなく余極限を使っているので $F$ の引数と $i$ の位置が左右逆になっている。今更直すのは面倒なのでこのままにする。)となり、簡単な記号操作で
\[
\forall n.\ j_{n+1} \circ \pi_{n+1} = i\circ F(j_n \circ \pi_n, j_n\circ \pi_n)\circ i^{-1}
\] が示せる。ここで $j_0 \circ \pi_0 = \bot$ なので
\[
\operatorname{id} = \bigsqcup_n j_n \pi_n = \bigsqcup_n \delta^n\,\bot = \operatorname{fix}\,\delta
\](ただし $\delta\,  f = \ i\circ F(f, f)\circ i^{-1}$) となり $i, D$ は最小であることが示せた。

三行まとめ

  • 最小不動点 $i,D$ は $F$ を⊥な対象と⊥な関数に繰り返し適用した領域 $D_n$ の極限として得る。
  • $F$ を繰り返して適用して出てきた射は $D_n \rightarrow D_{n+1}$ の埋め込みになるため、逆向きの射を射影という形で求められるので profunctor の $F$ を繰り返し適用できる。
  • 極限 $D$ は $D_n$ から一つずつ近似値を選んで出来た列全ての集合。
次回は 定理 3.4 から。

[注1] 因みに $f^\circ$ を陽に与えることも出来る。
\[
f^\circ\,x = \max\{y : f\,y \sqsubseteq x\}
\]$\max$ は当然存在すれば一意であり、存在しないならば $f$ は埋め込みではない。これが射影になることの証明は読者への課d(ry
この事を利用すると、埋め込みではない関数の例が簡単に見つけられる。例えば
\begin{align*}
f : &\text{Bool}_\bot \rightarrow \text{()} \times \text{()} \\
f\,\text{True} &= (\text{()}, \bot) \\
f\,\text{False} &= (\bot, \text{()}) \\
f\,\bot &= (\bot, \bot)
\end{align*}は $\max\{ y: f\,y \sqsubseteq (\text{()}, \text{()})\}$ が存在しないので射影を持たない。

[注2] この鎖が well-defined であるには、全ての $n$ について $i_n^\circ$ が定義されている、つまり $i_n$ が埋め込みである必要がある。まず $\bot : \varnothing_\bot \rightarrow F\,(\varnothing_\bot, \varnothing_\bot)$ が埋め込みである事は容易に分かる。また、任意の埋め込み $f$ について $F(f^\circ, f)$ も埋め込みであり、$(F\,(f^\circ, f))^\circ = F\,(f, f^\circ)$ となる:
\begin{align*}
F\,(f^\circ, f)\circ F\,(f,f^\circ) &= F\,((f^\circ, f) \circ (f, f^\circ)) & (\text{関手は合成を保存}) \\
&= F\,(f\circ f^\circ, f \circ f^\circ) & (\text{積圏での合成の定義}) \\
&\sqsubseteq F\,(\operatorname{id}, \operatorname{id}) & (F\text{は単調}) \\
&= \operatorname{id} & (\text{関手はidを保存})
\end{align*}二行目では、左成分は反変なので合成した関数の左右が逆になる事に注意。逆の合成も同様にして $\operatorname{id}$ になることが示せる。したがって、$n$ についての帰納法で $i_n$ も埋め込みであることが分かる。

[注3]$k$ は $D$ と $D'$ によって変化するので、それぞれ区別をつけるため $k_{D' \Rightarrow D} : D' \rightarrow D$ と表記することにする。$D$ も $F(D,D)$ も極限なので $k_{D \Rightarrow F(D,D)}$ と $k_{F(D,D) \Rightarrow D}$ が存在する。これらの合成、例えば $k_{D \Rightarrow F(D,D)} \circ k_{F(D,D) \Rightarrow D}$ は $k_{D \Rightarrow D}$ の条件を満たすので $k_{D \Rightarrow D}$ と一致しなくてはならない。しかし $\operatorname{id}$ もまた $k_{D \Rightarrow D}$ の条件を満たすので $k_{D \Rightarrow F(D,D)} \circ k_{F(D,D) \Rightarrow D} = \operatorname{id}$ となる。逆の合成も同様。

Sunday, December 8, 2013

ガチ勢になるための圏論勉強会 第一回 まとめ

Partake で発表したガチ勢になるための圏論勉強会 第一回では A.Pitts の Relational Properties of Domains の第一節と第三節を読んだ (第二節は本文を読んでからのほうが意味が分かりそうなので後回しした) ので、それのまとめ。というか分量的に言えばでっかい注釈。

ところで blogger で脚注を書いてそこに本文からリンクを貼るの自動化する方法知ってる人が居たら教えて下さい。この記事では全部手打ちしてるので…


第一節: この論文の目的と範囲

この論文の本題は再帰的に定義されたデータ型に機械的に表示 (denotation) を与える方法を確立すること、それからその表示を元にして、そのデータ型を扱うプログラムについて帰納法や余帰納法と言った証明テクニックを使うことを正当化する事。 具体例は論文では与えられていないが、こういう話だと考えられる。例えば OCaml で
type int_list = Nil | Cons of int * int_list
という定義があった時、これは有限の整数のリスト全てを含む集合 (型) であって、この型を使った関数
let rec map f = function
  | Nil -> Nil
  | Cons (x,xs) -> Cons (f x, map f xs)
let id x = x 
などについてmap id xsが常にxsと等価であるとかそういう事実を示すには普通に帰納法を使えば良い[注1]int_listNil に有限回 Cons をつけて作ったデータ全ての集合で、かつそれ以外のデータを含まないのだから、map id Nil = Nilmap id xs = xs ならば map id (Cons (x,xs)) = Cons (x,xs) を示すという具合だ。(以下、必要に応じて(::), [] などの糖衣構文を使う。)

しかしこのやり方は遅延データ構造には使えない。Haskell で
type IntList = Nil | Cons Int IntList
と書けばこれは無限リストも含むので、上記のような Nil から始めてうんたらかんたらという帰納法は Nil を含まないリストを取りこぼしてしまう。そもそもこういう型にはどういうデータが含まれていてどういうデータが含まれていないのだろう? [1,2,3,...] ++ [42]のように無限に続いたリストの後に、おまけのように[42]がくっついているようなデータは含まれていると考えたほうがいいのだろうか?[注2] 同様の問題は OCaml で関数や lazy を使って遅延リストをエンコードした場合にも起きる。

この Pitts の論文では、こうした再帰的に定義された型に対して、遅延が含まれていてもいなくてもその型に含まれるデータ全体の集合と、そのデータ型についてあれこれ証明する時に使えるテクニックを systematic に導出する方法を与える。このテクニックにより computational adequacy の証明なども簡単に行えるようになる。

第三節: 領域方程式の最小解

今回カバーした部分はセットアップ部分なのでそれほど難解な内容は無い。再帰的なデータ型は $\alpha \cong \Phi\,\alpha$ という領域方程式の最小解と解釈する。例えば整数のリストは $\alpha \cong 1 + (\text{Int} \times \alpha)$ を満たす集合 $\alpha$ [注3]。$\Phi$ は $(+),(\times),(\rightarrow)$ を組み合わせて作るが、これらの領域構築子は次のように正格・非正格のバリエーションがある。以下、$\mathbf{Cpo}_\bot$ は⊥を含む完備部分順序 (= pointed cpo = cppo) とそれらの間の正格連続関数からなる圏。全ての射 $f$ について $f\,\bot =\bot$ が要請されることに注意。また、これらの関手は全て局所連続と言って、射への作用を $\operatorname{Hom}(A,B)$ に制限した物がどの $A,B$ についても連続関数になる。

Lifting 関手 $-_{\bot} : \mathbf{Cpo}_\bot \rightarrow \mathbf{Cpo}_\bot$

新たな最小限 $\bot$ を付け足す。この関手を射 $f$ に適用してできる射 $f_\bot$ は
\begin{align*}
f_\bot\,\bot &= \bot \\
f_\bot\,x &= f\,x & \text{($\bot$ 以外)}
\end{align*}

積関手 $(\times), (\otimes) : \mathbf{Cpo}_\bot \times \mathbf{Cpo}_\bot \rightarrow \mathbf{Cpo}_\bot$

普通の集合論的なデカルト積 $A\times B = \{ (a,b) : a \in A, b \in B \}$ に $(a,b) \sqsubseteq (x,y) \Longleftrightarrow a \sqsubseteq x \land b \sqsubseteq y$ という順序を入れると $(\bot_A,\bot_B)$ を最小元に持つ cppo になる。$(a, \bot_B)$ や $(\bot_A, b)$ が $(\bot_A,\bot_B)$ と別物の扱いで、$(,)$ が非正格な構築子になる。ただし Haskell の (A,B) 型はデカルト積ではなくその lift $(A\times B)_\bot$ と一致する。この関手を射 $(f,g)$ に適用してできる射 $f\times g$ は
\[
(f\times g)\,(x,y) = (f\, x, f\, y) \] 非正格性により引数が $(x,y)$ の形をしていると仮定している事に注意。
一方潰れた積 (smash product) の $(\otimes)$ は $(,)$ 構築子を正格にとるため、$(a, \bot_B)$, $(\bot_A, b)$, $(\bot_A, \bot_B)$ を全部一つの $\bot$ に潰す。それ以外はデカルト積と一緒。OCaml の a * b は $A\otimes B$ になる。$f\otimes g$ は
\begin{align*}
(f \otimes g)\,(x,y) &= (f\,x, g\,y) \\
(f \otimes g)\,\bot &= \bot \end{align*}

和関手 $(+), (\oplus) : \mathbf{Cpo}_\bot \times \mathbf{Cpo}_\bot \rightarrow \mathbf{Cpo}_\bot$

集合論的な非交和 $A\uplus B = \{\operatorname{inl}\,a : a \in A\} \cup \{\operatorname{inr}\,b : b \in B\}$ は $\operatorname{inl}\,a$ と $\operatorname{inr}\,b$ を一切比較不可能にするような順序で完備部分順序になるが、それだと⊥を持たないので新たに付け足す: \[ A+B = (A\uplus B)_\bot \]これは $\operatorname{inl}\,\bot$ や $\operatorname{inr}\,\bot$ が $\bot$ とは別になるので $\operatorname{inl}, \operatorname{inr}$ が非正格になり、Haskell の Either A B と一致する。射への作用は \begin{align*}
(f + g )\,(\operatorname{inl}a) &= \operatorname{inl}(f\,a) \\
(f + g )\,(\operatorname{inr}b) &= \operatorname{inr}(g\,b) \\
(f + g)\,\bot &= \bot \end{align*} 一方予め $A$ と $B$ からそれぞれの⊥を消した集合 $A_\downarrow = A - \{\bot_A\}$ と $B_\downarrow$ を作り、それの非交和に改めて最小元を付け足すと構築子 $\operatorname{inl}$, $\operatorname{inr}$ を正格にとる潰れた和 (coalesced sum) ができる。
\[ A\oplus B = (A_\downarrow \uplus B_\downarrow)_\bot
\] OCaml の variant は $A \oplus B$。射への作用は
\begin{align*}
(f \oplus g )\,(\operatorname{inl}a) &= \left\{\begin{array}{ll}\operatorname{inl}\,(f\,a) & (f\,a \neq \bot) \\ \bot & (f\,a = \bot)\end{array}\right\} = \operatorname{inl}_\bot(f\,a) \\
(f \oplus g )\,(\operatorname{inr}b) &= \left\{\begin{array}{ll}\operatorname{inl}\,(g\,a) & (g\,a \neq \bot) \\ \bot & (g\,a = \bot)\end{array}\right\} = \operatorname{inr}_\bot(g\,b) \\
(f \oplus g)\,\bot &= \bot \end{align*} 注意: Pitts はなぜか $(+)$ の方だけ避けている。ひょっとしたら今後出てくる定理が当てはまらない場合があるのかも知れない。$(+)$ の射への作用は局所連続性は持つが、非正格である。

関数空間関手 $(\rightarrow), (\mathrel{-\kern{-1ex}\circ}) : \mathbf{Cpo}_\bot^\text{op} \times \mathbf{Cpo}_\bot \rightarrow \mathbf{Cpo}_\bot$

$A \rightarrow B$ は $A$ から $B$ への正格とは限らない連続関数全体の集合で、順序は $f \sqsubseteq g \Leftrightarrow \forall x.\ f\,x \sqsubseteq g\,x$ (point-wise ordering) で $\lambda \_.\,\bot$ を最小元に持つ。$\bot$ と $\lambda \_.\bot$ を同一視することに注意。Haskell では関数型をパターンマッチで分析できないため $\bot$ と $\lambda \_.\bot$ を区別する手段が無いので、A -> B の表示はそのまま $A \rightarrow B$ になる。
関数空間関手の射 $(f,g) : (A,B) \rightarrow (C,D)$ への作用は \begin{align*} (f \rightarrow g) &: (A \rightarrow B) \rightarrow (C \rightarrow D)\\ (f \rightarrow g) &= g \circ - \circ f \end{align*} となる。正格関数空間 $A \mathrel{-\kern{-1ex}\circ} B$ は $A \rightarrow B$ を正格関数だけに制限したもの。それ以外は $(\rightarrow)$ と一緒。


さて、上記の関手を組み合わせてできた $\Phi$ が与えられた時 $\alpha \cong \Phi\,\alpha$ なる cppo $\alpha$ は大抵複数あるが、データ型の解釈では特に「最小」の解が求められる。直観的には [1,2,3,...] ++ [42] のように計算に携わらない「ゴミ」が混じったデータを排除するという事だ。最小性により解が一意に定まるし、また計算結果について証明する時に意味のない区別を排除する事にもなる。[注4]
Pitts は「最小性の定義はいくつかある」と書いているが、単に集合として最小 (i.e. $(\subseteq)$ について最小) でいいのかどうかは書いていない。それでもいいのだけど射以外の概念を持ちだした定義なので圏論的に筋が悪いという事かも知れない。
ともかく射のみによる圏論的な最小性の定義を模索するのだが、ここで一つ問題がある。例えば $\Phi\,\alpha = \alpha \rightarrow \alpha$ の場合、$\Phi$ は引数 $\alpha$ を反変にも共変にも使うので $\mathbf{Cpo}_\bot$ からの関手にならない。そこで $\Phi$ の引数を共変位置と反変位置で別の引数に分けて、profunctor (この用語の和訳を誰かプリーズ) $\hat{\Phi}$ にする。例えば \[ \Phi\,\alpha = \alpha \oplus (\alpha \rightarrow \alpha \otimes \text{Int}) \] なら別々の引数 $\alpha^-$, $\alpha^+$ を用意して \[ \hat{\Phi}\,(\alpha^-, \alpha^+) = \alpha^+ \oplus (\alpha^- \rightarrow \alpha^+ \otimes \text{Int}) \] とする。こうして作った $\hat{\Phi} : \mathbf{Cpo}_\bot^\text{op} \times \mathbf{Cpo}_\bot \rightarrow \mathbf{Cpo}_\bot$ に対して $i : \hat{\Phi}\,(D,D) \cong D$ となるような $D$ が存在すればそれは当然、元の領域方程式 $\Phi\,\alpha \cong \alpha$ の解になる。こういう $i,D$ の対を不変性 (invariant)、特に $D$ を不変対象 (invariant object) と呼ぶ。この $\hat{\Phi}$ に対して最小性は次のように定義できる。
定義3.2 $\hat{\Phi} : \mathbf{Cpo}_\bot^\text{op} \times \mathbf{Cpo}_\bot \rightarrow \mathbf{Cpo}_\bot$ を、射に対する作用が連続な関手とする。不変性 $i : F\,(D,D) \cong D$ について $\operatorname{fix}\,(\lambda f.\ i\circ \hat{\Phi}\,(f,f)\circ i^{-1})$ が恒等関数である時、$i,D$ は最小であるという。但し $\operatorname{fix}$ は (上記の関数空間のところで定義された) 関数同士の順序に対して最小であるような不動点を求める関数。

この定義は $\hat{\Phi}$ を(遅延)リスト型を生成する関手 $\hat{\Phi}\,(\alpha^-, \alpha^+) = 1 + (\text{Int} \times \alpha^+)_\bot$ に置き換えて考えると分かりやすい。$\delta := (\lambda f.\ i\circ \hat{\Phi}\,(f,f)\circ i^{-1})$ とすると、 \begin{align*} \delta\,f\,[] &= [] \\ \delta\,f\,(x:y) &= i(f\,(\operatorname{inr}(x,y))) \end{align*} つまりリスト型の引数の中からリスト型のフィールドを探してそこに $f$ を適用するという関数になる。詳細には $i^{-1}$ でリスト型を $(+), (\uplus), -_\bot$ を使った表現にバラし、その結果に $f$ を fmap しているという事になる。この調子で $\delta^n\,\bot$ を展開すると \[ \begin{array}{lclll} \delta\,\bot\,[] &=& [] \\ \delta\,\bot\,(x:y) &=& i\,\bot &=& \bot \\ \delta^2\,\bot\,(x:y) &=& i(\operatorname{inr}(x,\delta\,\bot\,y)) &=& x:\bot \\ \delta^2\,\bot\,(x:y:z) &=& i(\operatorname{inr}(x,\delta\,\bot\,(y:z))) &=& x:y:\bot \\ \delta^3\,\bot\,(x:y:z) &=& i(\operatorname{inr}(x,\delta\,\bot\,y:z)) &=& x:y:\bot \\ \delta^3\,\bot\,(x:y:z:w) &=& i(\operatorname{inr}(x,\delta^2\,\bot\,(y:z:w))) &=& x:y:z:\bot \\ &\vdots& \end{array} \] という具合で、$\delta^n\,\bot$ は長さ $n$ の prefix を取り、それ以降は⊥で置き換える関数になる[注5]。$\operatorname{fix}\delta$ はそれの極限だから、 \begin{align*} \operatorname{fix}\delta\,\bot\,(x_1:x_2:x_3:\cdots) &= \bigsqcup\{\bot, (x_1:\bot), (x_1:x_2:\bot), \ldots \} \\ &= x1:x_2:x_3:\cdots \end{align*} となる。つまり、入力リストに終端があるならそこまでコピーし、終端がないなら先頭から有限ステップで到達できる全要素をコピーするのでこれらの入力に対し恒等関数になる。一方、前出の [1,2,3...] ++ [42] という、無限遠に続きを持つリストは有限 prefix 全ての最小上限ではないので、このデータを含む集合は $\alpha \cong 1 + (\text{Int} \times \alpha)_\bot$ の最小解にならない。同様の理由で [1..] ++ [42] というプログラムが生成するデータは[1..]と同じ物にならざるを得ない。これは両者を区別するような関数が Haskell 内で実装不可能であるという直観に合致する。
ここでは非正格な $(+),(\times)$ を使ったが、正格な $(\oplus),(\otimes)$ を使うと 有限リストが出来る。具体的には $\delta^n$ の返り値を構築するときの $\operatorname{inr}$ が正格なので、入力リストの長さが $n$ 未満でない限り戻り値全体が⊥になる。
定理3.3はこうした最小性を満たす解が常に存在すると主張している。

三行まとめ

  • 再帰データの領域は $(+),(\times),(\rightarrow)$ からなる関手 $\Phi$ に対して $i : D \cong \Phi\,D$ なる最小の $i,D$ の $D$
  • ただし $(+),(\times),(\rightarrow)$ にはそれぞれ正格版と非正格版があり、しかも一般には $\Phi(\alpha^-, \alpha^+)$ と反変位置・共変位置を分けないと関手にならない
  • $\operatorname{fix}(\lambda f.\ i\circ \operatorname{fmap}f \circ i^{-1}) = \operatorname{id}$ なら最小
多分次は定理 3.3 の証明から。

注1: OCaml でも let rec x = Cons (0, x) とかすれば無限リストが作れるがここでは無視する。

注2: 混乱のないように書いておくと、そういうリストは存在しないと考えるべき。Haskell で [1..] ++ [42]と書いた時に生成されるデータは[1..]とだけ書いた時にできるデータと同じだ。[1..]の部分は有限時間で辿り終える事ができないので、++[42]の部分はプログラムの実行に一切影響を与えない。したがって表示意味論的には++[42]は消える(無視される)。

注3: ここで 1 というのは値が一種類しか無い型 (OCaml でいう unit、Haskell では ()) で、variant は和、複数引数のコンストラクタは積とみなしている。こうした $\alpha$ に関する方程式を領域方程式と呼ぶ。

注4: 例えば [1,2,3,...] ++ [42] というデータを含まない解を採用しておけば [1..] ++ [42] というコードと [1..] というコードの意味 (表示; 返り値) が一致するので、f [1..] が何かの仕様を満たすことが分かった時、それをわざわざ f ([1..] ++ [42]) について証明し直さなくて良い。

注5: 一般には入力を深さ $n$ まで探索してそれより深い位置に出現する $\alpha$ を $\bot$ しか含まない型に置き換える。

Monday, May 27, 2013

TeX Wiki の英訳

先日の LaTeX のフォント設定の話が TeX Wiki からリンクされたみたい。向こうのほうがシステムを限定しない範囲では詳しい。(先日の自分のポストは現在の Ubuntu 上の quick fix という位置づけ)
そのページに「誰か英訳して」って書いてあったから英訳した。新規ページを作るにはユーザー登録がいるみたいなので、ここに書いとく。一応 PukiWiki の書式を真似たけど、プレビューできてないので正しくフォーマットできてるかは不明。

訳しながら気になったというかわからんかった点:
  • \CJKfamily と \CJKencfamily の違いは?
  • NFSS って何? そういう convention でいいの?
  • CJK 環境内部で他の言語を使った時の話なのか、CJK 環境外部に影響を及ぼすという話なのか?
  • 「ソースファイルのエンコーディングは、フォントエンコーディングと同じものが、 使用されます」は「フォントエンコーディングのエンコーディングは、ソースファイルと同じものが、 使用されます」の間違い?
  • inputenc の説明が全体的によく分からん…
  • 「インストール」の節のTTフォントをOTFに偽装するだの何だの言う話は日本語からしてよく分からなかったので、直訳風味。
  • 最初のサンプルをインストール無しでコンパイルしようとしたけど、どうすればいいのかよく分からんかった。単に展開すれば現在ディレクトリから辿って各種ファイルを見つけてくれるのかと思いきゃそんな事は無いようで。Directory hierarchy を完全に潰して全部のファイルを同一ディレクトリにぶち込んでみたけど dvipdfm にこんな事言われて失敗する (latex は通る):
dvipdfm UTF8-noembed-CJK                                                                                             
UTF8-noembed-CJK.dvi -> UTF8-noembed-CJK.pdf
[1
kpathsea: Running mktexpk --mfmode / --bdpi 600 --mag 1+0/600 --dpi 600 sungu5b
mktexpk: don't know how to create bitmap font for sungu5b.
mktexpk: perhaps sungu5b is missing from the map file.
kpathsea: Appending font creation commands to missfont.log.

** WARNING ** Could not locate a virtual/physical font for TFM "sungu5b".
** WARNING ** >> There are no valid font mapping entry for this font.
** WARNING ** >> Font file name "sungu5b" was assumed but failed to locate that font.
** ERROR ** Cannot proceed without .vf or "physical" font for PDF output...

Output file removed.

正直これ以上やる気無いので誰か他の人頑張って下さい。 
 
* [[The CJK package for LaTeX:http://cjk.ffii.org/]]

(This note was translated from an incomplete version as of 2013-05-26.)

ASCII Inc.'s pTeX is a TeX distribution for processing Japanese, but it
contains extensions to both the TeX typesetter and the DVI engine that make
certain tools like dvisvgm and dvipng incompatible.

This note explains how to use CJK LaTeX, which allows you to process Chines,
Japanese, and Korean (CJK) text solely by macros, without modifications to TeX
proper.  CJK characters are unfortunately rendered as bitmap fonts, but as long
as you can live with that, this arrangement lets you keep using standard TeX
and related tools like you always used to.  Other caveats include that the CJK
package (unlike pTeX) doesn't handle vertical text flow and line breaking rules
very well, but on the upside it can process Chinese and Korean text via UTF-8
encoding.  It seems to be used widely outside of Japan for mixing short
snippets of Asian text into English documents.

The CJK package, like inputenc, changes the category code of bytes that have
their 8-th bit set, so that TeX sources containing multibyte characters can be
compiled by standard (8-bit enabled) LaTeX.  It is not compatible with pLaTeX
which interprets multibyte characters as characters rather than as macros.  The
basic usage is

>\usepackage{CJK}~
...~
\begin{CJK}{encoding}{family}~
...~
\end{CJK}
<

The "encoding" part can be UTF-8 EUC-JP, Shift_JIS, GB2312, Big5, EUC-KR,
x-EUC-TW (CNS 11643), and various other encodings.  The following is a more
complete table of major supported encodings.

|CENTER:Encoding|CENTER:TeX Name|CENTER:TFM Encoding|h
|Big5|Bg5|c00|
|GB2312|GB|c10|
|EUC-JP|JIS|c40|
|Shift_JIS|SJIS|c40|
|JIS X 0212 (EUC-JP)|JIS2|c50|
|EUC-KR|KS|c60|
|UTF-8|UTF8|c70|

The TeX Name column shows the name that should be specified in the second
argument to \begin{CJK} in the TeX source.  TFM encoding is a parameter
required to build an fd file.  As you may haved guessed from the explanation so
far, TeX can handle source code that mixes different encodings in a single
file.  However, in practice it's probably easier to edit if you separate
different encodings into separate files and assemble them by \input as
necessary.  In particular, keeping Big5 and Shift_JIS encodings in separate
files is imperative because these encodings contain characters whose trailing
bytes conicide with special characters like "\", "{", and "}" that need to be
preprocessed away to avoid confusing TeX, like:

 \begin{CJK}{JIS}{}
 \input{euc-jp-text1}%
 \CJKenc{Bg5}%
 \ifx\VTeXversion\undefined%
 \immediate\write18{bg5conv < big5-text.raw > big5-text.tex}%
 \fi\input{big5-text}%
 \input{euc-jp-text2}
 \end{CJK}

The "family" part specifies the font family.  If you leave it blank, TeX
selects the "song" family by default.  This default can be changed with
\CJKfamily or \CJKencfamily.  Note the family does not completely specify the
font.  The font that TeX actually accesses during typesetting is determined by
the "(TFM encoding)(family).fd" files following the NFSS convention.  For
example, if the TeX file specifies the song family, TeX will select
cyberbXX.tfm specified in c70song.fd if the TeX source is UTF-8, or select
jsso12XX.tfm specified in c40song.fd if the TeX source is EUC-JP, and so on.


**Extensions

The CJK package distribution contains several extension packages and examples.
Here we explain the CJKutf8 package, which is probably the most important one.
Chinese and Japanese (and to some extent Korean) text have the unique property
that lines can be broken almost anywhere.  The CJK package implements this
liberal line breaking rule, which can cause inappropriate line breaks when
other languages are mixed into the CJK environment.  This is a bit like how
pTeX incorrectly hyphenates English documents written in full-width
alphanumeric characters.  The font encoding determines hyphenation rules,
kerning, and ligature, so to correctly process non-CJ languages inside the CJK
environment, we have to arrange for the right font encoding to be loaded
outside (prior to?) the CJK environment.  CJKutf8 does just that.  To explain
how this works, I need to tell you about the inputenc package first.

***The inputenc Package

The big change that LaTeX2e made from LaTeX2.09 was the adoption of NFSS2.
This protocol made the font encoding an attribute that the user specifies
separately from all other aspects of the font.  As a result, the minimal
complete source code in LaTeX2e is
>\documentclass{...}~
\usepackage[...]{fontenc}~
\usepackage[...]{inputenc}~
\begin{document}~
...~
\end{document}
<
For backwards compatibility (with LaTeX2.09), OT1 is used if no fontenc is
given, and the source file's encoding is used as the font encoding.  A source
file that doesn't load these packages cannot be said to be fully compliant to
LaTeX2e's conventions, even if it suits your needs.

inputenc.sty itself only sets the character class of character with the 8th bit
set to active and to raise an error whenever the source code uses them.  To use
these activated characters in the TeX source, they have to be redefined to
macros that generate the right character in the right encoding.  The option to
inputenc specifies the file to do this redefinition.  The UTF8 option is
available starting with the Feb 9, 2004 version of LaTeX2e.

\usepackage[UTF8]{inputenc}

But writing this in the preamble is not enough to enable all UTF-8 encoded
characters.  When inputenc is given the UTF8 option, it goes through all font
encodings loaded in the preamble (scanning all the way up to the last line
preceding the document body) and for each encoding XXX reads in XXXenc.dfu and
enables redefinitions of characters defined in that file.  Characters that are
not defined in any of those files remain undefined and attempts to use them
results in an error.

Currently, the standard distribution contains the following dfu files.
>lcyenc.dfu~
ly1enc.dfu~
omsenc.dfu~
ot1enc.dfu~
ot2enc.dfu~
t1enc.dfu~
t2aenc.dfu~
t2benc.dfu~
t2cenc.dfu~
ts1enc.dfu~
x2enc.dfu
<
utf8enc.dfu combines all of the files above.  Languages that can be written in
these font encodings are typeset in UTF-8 with exactly the same hyphenation,
kerning, and ligature as when they are typeset with some other encodings.

So, currently Unicode support in standard LaTeX, with no additional packages,
works as follows.

-LaTeX provides complete support for Unicode source files encoded in UTF-8 (not limited to the BMP).
-Theoretically, any language that satisfies the following conditions can be properly typeset from a UTF-8 source file as long as an appropriate font encoding and dfu file are prepared.
--A line is composed of horizontally listed glyphaemes (i.e. characters), and lines are listed from top to bottom.
--Each line has enough "space" (a white space or similar entity) with a flexible width where the line can be broken.  (So for Chinese and Japanese, there is an implicit space in this sense between (almost) every pair of characters.)

*** CJKutf8 パッケージ

This package does a lot of things under the hood, but its interface is
straightforward.  It reads in inputenc, tries to hijack everything inside the
CJK environment and process it using inputenc, and reverts to the CJK
environment whenever inputenc fails.  
 \documentclass{article}
 \usepackage[T1]{CJKutf8} % The font encoding can be specified in the option.
 
 \begin{document}
 \begin{CJK}{UTF8}{min}
 % Write something in UTF-8.  Hyphenation is properly handled if you specify
 % the right language with babel or the like.
 UTF-8で何か文章を書く。babel等でハイフネーションの言語を指定すれば、正しく組版される。
 \end{CJK}
 \end{document}

*Installation
**TeX

You first need a working LaTeX installation.  Additionally, you need the macro
files from [[CTAN:languages/japanese/CJK/]] (under the directory named
cjk-4.x.x/; it may be archived in a zip or tarball) and the font metric (TFM)
files.  The default font settings that come with the CJK package are compatible
with dvips and pdflatex, but this also means its suboptimal for use with
dvipdfmx.  This section explains how to write a custom font definition.  The
TFM used in standard TeX (which doesn't include nonstandard extensions like
those of pTeX or Omega) can describe up to only 256 glyphs per TFM file.  This
is insufficient to handle Chinese characters or other large character sets, so
in CJK a single font is distributed across multiple files.  That might sound
scary, but you can easily generate those TFM files from any TTF font using
ttf2tfm.
> ttf2tfm [TTF] [TFM stem]@[SFD name]@

If you have a TTC file which combines multiple TrueType faces into one font,
you can use the -f option to choose which face you want.  If you're generating
cyberbXX.tfm the [TFM stem] is cyberb, and for jsso12XX.tfm it's jsso12.  [SFD
name] determines how to split into subfonts.  Which SFD is needed depends on
the font's CMap encoding and the TeX source code's encoding, but for recent
TrueType fonts you should use one that starts with "U".  If you are planning to
use full-width characters exclusively, you can also just copy an existing TFM
file to a different name and use that instead.  (The TFM files contained in the
samples below was made this way, so if you typeset half-width alphanumeric
characters with those files you'll get pretty ugly results.)  For instance, if
you have a document written in EUC-JP/Shift_JIS, you want to use a TFM file
whose stem is foo, and refer to that font as the "bar" family, you do ttf2tfm
baz foo@UJIS@ to create f0001.tfm–foo35.tfm.  Then you have to write
c40bar.fd, which should contain at least \DeclareFontFamily{C40}{bar}{}
\DeclareFontShape{C40}{bar}{m}{n}{<-> CJK * foo}{} If you put those files in
somewhere LaTeX can find them, your LaTeX source should compile as expected.
\documentclasss{article} \usepackage{CJK}
 
 \begin{document}
 \begin{CJK}{JIS}{bar}
 % Write your Japanese text here in EUC-JP.
 ここにEUC-JPで日本語の文章を書きます。
 \end{CJK}
 \begin{CJK}{SJIS}{bar}
 % Write your Japanese text here in Shift_JIS.
 % You may have to preprocess this block if you use certain characters.
 ここにShift_JISで日本語の文章を書きます。%
 しかし、もしかすると、このブロックだけ%
 プリプロセッサーを通さないと%
 \LaTeX のコンパイルが通らないかも知れません。
 \end{CJK}
 \end{document}

To process Shift_JIS or Big5, you'll also need to install the preprocessors
sjisconv and bg5conv.

**DVI Driver

pdflatex is slated to officially support the CJK package in the near future,
but for now the only ways to generate decent PDFs with CJK are VTeX
(commercial) and dvipdfmx.  Here we will focus on dvipdfmx.
>By "decent" we mean that the non-decent PDFs require the fonts to be split in accordance with the TFM files.

The only things you need to set up are the mappings between the DVI file's TFM
and PDF file's fonts.
> DVI files do not contain any information about glyph appearances.  They only specify the size and position of each character and which TFM that information comes from.  The job of a DVI driver is to attach glyph shapes extracted from the fonts.  This means it needs a mapping between TFM and fonts.  Without this mapping, most DVI drivers tries to generate a bitmap font on its own.  Currently, pTeX generates an error and dies at this point, which signals the user that there's something wrong with the installation.  But if the CJK package is fully installed, the driver often succeeds in generating bitmaps for default fonts, which causes many people to not notice the problem and keep using a half-broken installation.  The samples below use newly defined TFMs and show how to map them to real fonts.

dvipdfmx has many files (called map files) that map TFM to fonts inside PDF
files, but most of them are shared with dvipdfm, so they can handle only those
8-bit fonts that dvipdfm can understand.  So this mapping has to be added to
the dvipdfmx-specified map file called cid-x.map.  (Details will be added
later.)

***When Using Non-existent (CFF, CID-keyed) OpenType Fonts
dvipdfmx knows about the following fonts.
|CENTER:|||c
|~Language|CENTER:Character Set|CENTER:Font Name|h
|~Japanese|Adobe-Japan1|Ryumin-Light|
|~|~|GothicBBB-Medium|
|~|~|HeiseiMin-W3|
|~|~|HeiseiKakuGo-W5|
|~|Adobe-Japan1-2|HeiseiMin-W3-Acro|
|~|~|HeiseiKakuGo-W5-Acro|
|~|Adobe-Japan1-4|KozMinPro-Regular-Acro|
|~|~|KozGoPro-Medium-Acro|
|~Simplified Chinese|Adobe-GB1|STSong-Light|
|~|Adobe-GB1-2|STSong-Light-Acro|
|~|Adobe-GB1-4|AdobeSongStd-Light-Acro|
|~Traditional Chinese|Adobe-CNS1|MSung-Light|
|~|~|MHei-Medium|
|~|Adobe-CNS1-0|MSung-Light-Acro|
|~|~|MHei-Medium-Acro|
|~|Adobe-CNS1-4|AdobeMingStd-Light-Acro|
|~Korean|Adobe-Korea1|HYSMyeongJo-Medium|
|~|~|HYGoThic-Medium|
|~|Adobe-Korea1-0|HYSMyeongJo-Medium-Acro|
|~|~|HYGoThic-Medium-Acro|
|~|Adobe-Korea1-2|AdobeMyungjoStd-Medium-Acro|

So if you specify these font names in a cid-x.map entry, which looks like
> [TFM stem]@[SFD name]@ [CMap name] [Font file name]

you'll get a PDF that doesn't embed those fonts, even if the fonts aren't on
dvipdfmx's search path.  [CMap name] is the mapping from the encoding that
results from applying SFD, to the ordering CID (translator note: I have no idea
what this is talking about; this goes for much of the subsequent discussion).
[SFD name] is usually the same as the SFD name you passed in to ttf2tfm when
you created the TFM file.  But you can something like the following instead,
too.
 jsso12@UJIS@ UniJIS-UCS2-H HeiseiMin-W3-Acro
This entry above collects the characters in jsso12XX.tfm and decodes them to Unicode, and maps them to the glyphs in Adobe-Japan1.
 jsso12@SJIS@ RKSJ-H HeiseiMin-W3-Acro
This collects the characters in jsso12XX.tfm and decodes them into Shift_JIS, then maps them to the glyphs in Adobe-Japan1.
 jsso12@SJIS@ 90ms-RKSJ-H HeiseiMin-W3-Acro
This also goes through Shift_JIS, but uses the mapping from Windows-31J (Microsoft Windows Standard Japanese Character Set).  Some characters will deploy different variants than the above.
 jsso12@SJIS@ 78-RKSJ-H HeiseiMin-W3-Acro
This uses glyphs conforming to the example glyph shapes in JIS C 6226-1978 (JIS X 0208:1978).

PDF that contain non-embedded fonts can be rendered on some systems with
different substitute fonts.

***When Using Existing OpenType (CFF, CID-keyed) Fonts
This is almost the same as in the previous section, but the [Font file name]
has to specify a font that exists on dvipdfmx's search path.
By default the font will be embedded, but a "!" before the
[Font file name] prevents embedding.
Embedding is also suppressed when [Font file name] is followed by ",Bold",
",Italic", or ",BolItalic".
***Using TrueType Fonts as OpenType (CFF, CID-keyed)
For TrueType fonts, there is no set order in which glyphs are listed, so 
accesses to glyphs must go through the font file's CMap table.  If
the character set of the CMap file specified in [CMap name] is one of Adobe's
standard character sets, the TrueType font can be embedded as if it's a CID font
using the standard mapping from Unicode.  However, glyphs that do not exist in
Unicode are usually not included in TrueType fonts, and even if they are, they
are inaccessible.  If the character set of the CMap file specified in
[CMap name] is not a standard character set from Adobe, you can emulate e.g. the
Adobe-Japan1 supplement 4 set by adding "/AJ14" after the font name.
Generally speaking, you should use this technique whenever you use a TrueType
font without embedding it.

***Using TrueType Fonts
To access a TrueType font using a CMap table, use the cid-x.map entry
> [TFM stem]@[SFD name]@ unicode [Font file name] [options]
The SFD should start with a "U", indicating that the TFM encoding should be
mapped to Unicode.
>
 -w option
Given when the TrueType font will be used for vertical text.
 -w 0
Horizontal text (default)
 -w 1
Vertical text

>
 -p option
Used to access characters that lie outside of Unicode's BMP (Basic Multilingual Plane)
 -p 0
Access the BMP (default)~
In other words, the code points 0x0000–0xFFFF are mapped to characters with those exact code points.
 -p 1
Access the SMP (Supplementary Multilingual Plane).
The characters needed in TeX are usually ancient scripts.
The code points 0x0000–0xFFFF are slid over by 0x10000 and mapped to
characters in the code point range 0x10000–0x1FFFF.
 -p 2
Access the SIP (Supplementary Ideographic Plane).
This includes Chinese characters that did not fit in the BMP.
The code points 0x0000–0xFFFF are slide over by 0x20000 and mapped to
characters in the code point range 0x20000–0x2FFFF.

If, for some reason, you must access a TrueType font's glyph in the order they
are listed, without going through a CMap, you can do so by specifying a CMap
that has the encoding Adobe-Identity.  However, the CMap file must not be named
"Identity-H" or "Identity-V".

*Examples
The following examples require the files from [[CTAN:languages/japanese/CJK/]].
You should be able to install and use them as given, but to try them out without
installing, you should create an empty temporary directory (folder) and copy
everything there.  Then rename all the dvipdfm/config/cid-x.map-add.* in the
example to cid-x.map.  If you want to install, you should append the contents of
those files to the system's cid-x.map file.

+ &ref(http://oku.edu.mie-u.ac.jp/~okumura/texfaq/archive/CJK-LaTeX-UTF8-noembed.tar.bz2,Render different variants of the same kanji from a TeX file written in UTF-8);
--Known problems:
---There are some parts whose intentions are unclear on each page.
+ &ref(http://oku.edu.mie-u.ac.jp/~okumura/texfaq/archive/CJK-LaTeX-localEncoding-vertical.tar.bz2,Vertical text); also contains settings needed to use JIS X 0213 with Shift_JIS
--Known problems:
---The TFM files included in this archive can only handle full-width characters
---The archive has no fdx files for using horizontal-script fonts to render vertical script, so punctuation appears incorrect in the vertical text mode of CJKvert.sty (this shouldn't be a problem if you have a genuine vertical-script font).
+ &ref(http://oku.edu.mie-u.ac.jp/~okumura/texfaq/archive/CJK-LaTeX-SIP.tar.bz2,Using the Supplementary Ideographic Plane); dvipdfmx (20070409 or newer) is required to build a PDF file from this example.  It also uses proprietary fonts.  In case you don't have them, &ref(http://oku.edu.mie-u.ac.jp/~okumura/texfaq/archive/CJK-LaTeX-SIP.pdf,here's a pre-built PDF) for your reference.
--Known problems
---An old dvipdfmx has a bug that prevents it from handling this example properly (fixed in dvipdfmx-20070409)
---Two fonts are defined in the c70usong.fd file. This should be split into c70usong.fd and c70usong2.fd, or otherwise we can't use SIP characters at the beginning of the document.
---It uses proprietary fonts.  cid-x.map should be rewritten to use [[HAN NOM FONTs:http://www.viethoc.org/article.php?sid=98&mode=threaded&order=0&thold=0]].  (But boy, does Han Nom's design look like SimSun!)
---Lots of other errors that you can spot by searching the Web about this example's usage of CJK's features.
---In CJK 4.6.0, you need to add the kind of code you see in this example's preamble in order to use non-BMP characters.  But on the other hand, the development version (translator note -- as of when?) of CJK clashes with this code.

Let us know if you want to see any other examples!  Of course, new examples and
corrections to this wiki page are welcome too.

Saturday, May 25, 2013

Ubuntu で pLaTeX を使わずに日本語を書く

日本語で LaTeX を使う方法をググると pLaTeX の情報ばっかり山のように出てきますが、pLaTeX は
  • 英語文書と発行するコマンドの流れが違う (pdflatex 一本 vs. platex + dvipdfmx)
  • hyperref などのパッケージがエラーを出して使えない
  • 日本語以外使えず、もし他の言語が使いたくなったら詰む
などの割と致命的な欠陥があるので、使いたくありません。特に普段は英語ばっかり打ってて一部の文書でちょろっと日本語を入れたいというような使い方をしているので、最初のはかなり面倒です。二番目に関しても hyperref ぐらいなら専用の別パッケージがあるようですが、専用パッケージが必要な事がある時点で御免被りたいところです (どうせその内また他のパッケージで同じ問題が起こって、その時は専用パッケージが用意されてなくて詰むに決まってるから)。

そんなわけで通常の (pdf)latex で CJK を入力する方法を探してみた所、CJK.sty というそのまんまのパッケージがある事を知りました。が。こいつ、Ubuntu Raring Ringtail だと latex-cjk-common だか何だかに付いてくるんですがフォントのセットアップがさっぱりされないのでネットで見つかるテスト文書はほとんど全て組版が失敗しました。具体的には これ とか これ とかですが、指示通り
\documentclass{article}
\usepackage{CJK}
\begin{document}
\begin{CJK*}{UTF8}{song}
这是一个测试
\end{CJK*} (this is a test)
\end{document}
とか書いて pdflatex に食わせても
! Undefined control sequence.
try@size@range ...extract@rangefontinfo font@info 
                                                  <->@nil <@nnil 
とか言われてちゃんと組版できません。TeX は "Undefined control sequence" とか嘘こいてますが、これはフォントがちゃんと設定されてない事によるエラーで、フォントを指定している "song" の部分をインストールされてるフォントに変更すればとりあえず表示されます。例えば私の環境では
$ dpkg -l | grep latex-cjk
ii  latex-cjk-chinese      4.8.3+git2012062 amd64            Chinese module of LaTeX CJK
rc  latex-cjk-chinese-arph 1.22             all              traditional Chinese KaiTi fonts for CJK
rc  latex-cjk-chinese-arph 1.22             all              traditional Chinese KaiTi fonts for CJK
ii  latex-cjk-chinese-arph 1.22             all              traditional Chinese KaiTi fonts for CJK
rc  latex-cjk-chinese-arph 1.22             all              traditional Chinese KaiTi fonts for CJK
ii  latex-cjk-common       4.8.3+git2012062 amd64            LaTeX macro package for CJK (Chinese/Japanese/Kor
ii  latex-cjk-japanese     4.8.3+git2012062 amd64            Japanese module of LaTeX CJK
ii  latex-cjk-japanese-wad 0.20050817-16    all              type1 and tfm DNP Japanese fonts for latex-cjk
rc  latex-cjk-korean       4.8.3+git2012062 all              Korean module of LaTeX CJK
rc  latex-cjk-thai         4.8.3+git2012062 all              Thai module of LaTeX CJK
$ ls /usr/share/texmf/tex/latex/CJK/UTF8
UTF8.bdg  UTF8.enc    c70gbsn.fdx  c70goth.fdx  c70maru.fdx  c70min.fdx  zh-Hans.cpx
UTF8.chr  c70gbsn.fd  c70goth.fd   c70maru.fd   c70min.fd    ja.cpx      zh-Hant.cpx
という具合で、c70gbsn.fd というのに目を付けて song を gbsn に変更すれば上の中国語がちゃんと出ました。ちなみにフォントの fd 情報を置けるディレクトリは /usr/share/texmf/tex/latex/CJK/UTF8 だけではなくて /usr/share/texmf/tex/latex 以下ならどこでもいいようです。

で、一応日本語フォントの c70maru.fdx や c70min.fdx も入っていて song を maru や min に変更すれば日本語も出ることは出るのですが、どうも字型が気持ち悪いフォントばかりです。このフォントでいいよという人はこれで設定終了でいいかも知れませんが、私はもっとまともなフォントが欲しかったので北大の Jan Paul さんとか言う人のページを参考に IPA フォントを設定しました。基本的にはリンク先の長ったらしい指示に従うだけですが、一部「どこにあるんだよそのファイル!(怒)」みたいな部分もあったのでここで詳述。全部 root でやります
  1. IPA フォント自体は fonts-ipafont-gothic と fonts-ipafont-mincho 入れとけばおk
  2. TFM ファイル を落として展開、中身は全部 /usr/share/texmf/fonts/tfm に適当なディレクトリ掘って放り込みます。
  3. Font descriptor とかいうの を落として展開、中身は全部 /usr/share/texmf/tex/latex に適当なディレクトリ掘って放り込みます。
  4. /etc/texmf/fonts/map/ttf2pk/ttfonts.map というファイルを作って
    ipam@UJIS@ ipam.ttf
    ipamp@UJIS@ ipamp.ttf
    ipam-uni@Unicode@ ipamp.ttf
    ipamp-uni@Unicode@ ipamp.ttf
    ipag@UJIS@ ipag.ttf
    ipagp@UJIS@ ipagp.ttf
    ipag-uni@Unicode@ ipagp.ttf
    ipagp-uni@Unicode@ ipagp.ttf
    
    と書きます。この /etc/texmf 以下のディレクトリはデフォルトでは存在しないので、自分で作ること。man page にもどこにも載ってないこのステキなディレクトリは ttf2pk を strace して見つけました。最悪ですね。
  5. /usr/share/texmf/web2c/texmf.cnf を開いて MKTEXPK = 1 という行を追加しておきます。625 行目らへんに %MKTEXPK = 0 という行が既に有ると思うのでそれを改変するのがいいでしょう。
一応発行するコマンドを並べて置いときますが、一瞬たりともテストしてないのであしからず。
# 予め root になって /tmp とかどーでもいいファイルおける場所に移動しておく
apt-get install latex-cjk-common latex-cjk-japanese fonts-ipafont-gothic fonts-ipafont-mincho unzip
mkdir tmp
cd tmp
wget http://www-alg.ist.hokudai.ac.jp/~jan/IPA-Jap-Fonts-tfm.zip
unzip IPA-Jap-Fonts-tfm.zip
mkdir /usr/share/texmf/fonts/tfm/ipa
mv *.tfm /usr/share/texmf/fonts/tfm/ipa/
wget http://www-alg.ist.hokudai.ac.jp/~jan/IPA-Jap-Fonts-fd.zip
unzip IPA-Jap-Fonts-fd.zip
mkdir /usr/share/texmf/tex/latex/ipa
mv *.fd /usr/share/texmf/tex/latex/ipa/
mkdir -p /etc/texmf/fonts/map/ttf2pk/
cat > /etc/texmf/fonts/map/ttf2pk/ttfonts.map <<EOF
ipam@UJIS@ ipam.ttf
ipamp@UJIS@ ipamp.ttf
ipam-uni@Unicode@ ipamp.ttf
ipamp-uni@Unicode@ ipamp.ttf
ipag@UJIS@ ipag.ttf
ipagp@UJIS@ ipagp.ttf
ipag-uni@Unicode@ ipagp.ttf
ipagp-uni@Unicode@ ipagp.ttf
EOF
cd ..
これで
\documentclass{article}
\usepackage{CJK}
\begin{document}
\begin{CJK}{UTF8}{ipam}
やっと pLaTeX に頼らずに日本語が出せた…
\end{CJK} The CJK environment doesn't insert newlines.
\end{document}
っていう TeX ファイルを pdflatex に食わせるとこんな PDF が出来るはずです。ipam の部分を ipag にすればゴシック体になります。正直まだあんまり綺麗とは言い難いですが、もういいでしょう。お疲れ様。


もう TeX のこういうフォント周りの汚さには本当にうんざりしますが、何とか出せることは出せました。…はあ。

Wednesday, May 1, 2013

整数計画法で「≠」は表現不可能なのか?

注: この話の文脈が分かってる人は「分かってる事」の節まで飛ばすのが吉。
x,y が次の条件を全て満たすとき、\(143x + 60y\) の最大値を求めよ:
\[
120x + 210y \le 15000\\
110x + 30y \le 4000\\
x + y \le 75\\
x \ge 0\\
y \ge 0
\]↑こんな風に、線形不等式を満たすよう線形式 (ここでは143x + 60y) の最大値や最小値を求める問題を線形計画問題 (linear program, LP) といい、特に変数が全て整数値を取るという条件で解く物を整数計画問題 (integer linear program, ILP) と言う。ILP は NP 完全問題であり、他の NP 完全問題と同じく
  • もの凄く沢山の「制約を満たすアレコレを見つけよ」式の問題が ILP に帰着できる
  • 一般に速く解く方法は知られていない、多分存在しない
  • でも経験的に、実際に起きるケースでは大抵速く解けるソルバが充実してる
という特徴がある。特に ILP 自身が足し算を含むので、足し算を含む問題は ILP に帰着させやすい (カックロとか、何かのコストの合計を最小化する問題とか)。

ここ数日、この ILP で「否等式」とでも呼べばいいのか、$x \neq y$ という形の制約を一般に扱うことが出来るかどうか考えてたんだけど、手詰まりになったので、分かってること、分かってないこと、考えたことを一旦ここにまとめました。何かわかる方はコメントお願いします。

問題

ILP では、制約式は全て
\[
a_1x_1 + a_2x_2 + \cdots + a_n x_n \le c
\]
の形の non-strict な線形不等式 (ここで $a_i$ と $c$ は (整数) 定数で $x_i$ は変数) に制限されてるので、何か問題を ILP に帰着させる時は「不等式ではない制約を如何にして不等式で表現するか」に腐心することになる。

例えば $x = y$ と書きたければ $x \le y, y \le x$ と二つの式に分割する。$x < y$ は $x \le y - 1$ に置き換え、「$x_1,x_2,\ldots,x_n$ の内ただひとつが 1 に等しく、残りは全部 0」というような排他条件は $0 \le x_i \le 1$ という条件に加えて $x_1 + x_2 + \cdots + x_n = 1$ (この = は更に二つの不等号にバラす) で表す。

このように線形不等式は結構色んな制約を表現することが出来るんだけど、このノリで否等式 $x \neq y$ を不等式に翻訳しようとすると途端に詰まるのだ。話を簡単にするため変数の値を一つ 0 で固定して $x \neq 0$ を表現することを考えてみよう。この式を満たす整数の集合は $\mathbb{Z}-\{0\}$。これは穴が空いた(一次元の)図形なので、明らかに線形不等式の集まりで定義できる集合ではない。

一般に、n 個の変数についての連立線形不等式を満たす点の集合は、$\mathbb{R}^n$ 上で解いた場合は凸多胞体 (注: 多角形とか多面体みたいに真っ直ぐな面で区切られた図形の n 次元版) を成す。ILP では $\mathbb{Z}^n$ 上で解くので、凸多胞体に含まれる格子点全ての集合が不等式の解の集合になる。ただし、普通多胞体と言えば有限の大きさを持った閉じた図形を指すけど、ここで言う多胞体は無限に大きい物も含む。例えば $\mathbb{R}^2$ で $0 \le x \le 1, 0 \le y$ を満たす $(x,y)$ の集合は普通多角形とは言わないけど、ここでは直線で囲まれてるので多角形に含める。

しかしながら $\mathbb{Z}-\{0\}$ というのは -1,1 を含むのにその内分点の 0 を含まないので、明らかに連立線形不等式の解ではない。要するに否等式は非線形の制約なので、線形の制約に変換するのが難しいのだ。

これが、単に「難しいから、自分が思いつかないだけ」なのか、「そもそも不可能」なのかというのがこの記事で問いたい問題。形式化するならこんな感じ。

問: $x$ を含むいくつかの変数について整数係数の連立線形不等式があり、その連立不等式の整数解から $x$ の値だけを抜き出した集合が $\mathbb{Z}-\{0\}$ である。このような連立線形不等式は存在するか。

分かってる事: 凸性だけではダメ

さて、無論「$\mathbb{Z}\setminus\{0\}$ は凸ではないので線形不等式では表せない、ハイ終わり」で済むのかと言えばそうは問屋が卸さない。卸してくれるならこんな記事書かない。なぜなら例えば $x \neq 0$ は表せなくても $x \neq 0 \land -2 \le x \le 2$ なら表せるから。この制約の解は $[-2..2]-\{0\}$ と、穴の空いた集合になるけど、補助変数 $y$ を使えば
\[ y \le \frac{1}{3}x + \frac{2}{3} \\
    y \ge\frac{1}{3}x  + \frac{1}{3} \\
    0 \le y \le 1 \]
という制約で表せる。この連立不等式の整数解は $(-2,0), (-1,0), (2,1), (1,1)$ の四点で、$x$ はちゃんと $[-2..2]-\{0\}$をカバーする。

幾何的に考えると、n 個の変数の制約式を k 個の補助変数を使って表すという事はつまり
  • n+k 次元の多胞体を選んで
  • それを n 次元に射影する
事に相当するけど、今しがた見たように $\mathbb{Z}^{n+k}$ から $\mathbb{Z}^n$ への射影では ($\mathbb{R}^{n+k}$ から $\mathbb{R}^n$ への射影とは違って) 凸図形が凸でない図形の影を持つことがある。だから $\mathbb{Z}-\{0\}$ が凸図形でないというのは一変数の線形不等式で表せない理由であって、補助変数を使っても表せない理由にはならない。

分かってる事: 補助変数一つでは足りない

補助変数を一つしか使わずに $x \neq 0$ を表すことは不可能である事は割と簡単に証明できる。泥臭いけど。仮に $x,y$ という二つの変数を使った連立線形不等式が $x \neq 0$ を表せたとする、つまり連立不等式の解の集合を $S ⊆ \mathbb{Z}^2$ とすると、$S$ を $x$ 軸上に射影した時の影 $\operatorname{proj}_x(S)$ が $\mathbb{Z}-\{0\}$ だと仮定する。

その連立不等式を実数の範囲で解いた時の解の集合を $S' ⊆ \mathbb{R}^2$ とすると、$S'$ は(非有界)凸多角形で $S'$ の中の格子点の集合が $S$ と一致する。$S$ は y 軸の左にも右にも点を持つので、$S'$ もそうでなくてはならない。しかも $S'$ は凸図形なので y 軸と交わる。ここで \[
l = \inf \{ y | (x,y) \in S' \cap (\mbox{$y$ 軸}) \} \\
u = \sup \{ y | (x,y) \in S' \cap (\mbox{$y$ 軸}) \}
\] とすると、$l,u \not\in \mathbb{Z}$ でかつ $\lfloor u \rfloor = \lfloor l \rfloor$ である。さもなくば $(0,l)$ と $(0,u)$ の間に格子点が含まれ、これを $S'$ が凸性より含んでしまうからである。

よって $l,u$ は有限である。$(0,l)$ と $(0,u)$ は $S'$ の境界に含まれるので、それぞれどれかの不等式を最適化する点でなくてはならない。つまり連立不等式の中に、変数を左辺、定数を右辺に集めると \[
 a_l x + b_l y \le c_l \\
 a_u x + b_u y \le c_u
\] となる二つの不等式が含まれていて、これらの $\le$ を = に置き換えて得られる式の表す直線 $L_l, L_u$ がそれぞれ $(0,l)$ と $(0,u)$ を含む。

さて、もし$L_l,L_u$ が平行であるとすると、これらは共通して有理数の傾き $-a_l/b_l$ を持つ。従ってこれらの直線と $x = b_l$ との交点の y 座標は $l - a_l$ と $u - a_l$ であり、これらの座標はいずれも整数ではなく floor が同じである。よって $(b_l, l - a_l)$ と $(b_l, u - a_l)$ の間には格子点が含まれず、$b_l \not\in \operatorname{proj}_x(S)$ となり $\operatorname{proj}_x (S) = \mathbb{Z}-\{0\}$ と矛盾する。一方、$L_l,L_u$ は平行でないならどこかで交わる。ここでは y 軸の右で交わったとしよう。$S'$ はその交点より右には一つも点を持たないので、 $S$ も交点より大きな x 座標の点を持たないという事になる。これは $\operatorname{proj}_x (S) = \mathbb{Z}-\{0\}$ と矛盾する。

補助変数二つにすると頭が爆発する

で、まあ当然ここまでの証明を三次元以上に拡張できないかと考えたわけですよ。ところが三次元の時点でどうもうまく行かない。まず $z = z_0 (\in \mathbb{Z})$ という形の任意の平面について、二次元の場合と同じ論証で $+x$ 方向か $-x$ 方向に一定距離以上行けば一定間隔で $S'$ と格子点を共有しない y 軸方向の直線がある事が示せる。だから $z=z_0$ 平面が $\operatorname{proj}_x(S)$ に貢献する部分集合は右か左かが一定距離以降一定間隔で歯抜けになっている。

歯抜けが始まる距離は上で言う $L_l,L_u$ の式の左辺の係数だけを含む式で上から抑えられ ($|u-l| < 1$ を使う。詳細は略)、歯抜けの間隔は y の係数の絶対値なので、いずれの数値も高々 $O((\mbox{不等式の個数})^2)$ 程度しかバリエーションが無い。従って全部の公倍数とかを取ってしまえばどの $z=z_0$ 平面でも歯抜けが始まる距離と、どの平面でも歯抜けが最低一回は起きる間隔が計算できるだろう…と思った。

が。よく考えたら $z = z_0$ では $+x$ 方向でだけ歯抜けが起きるけど $z = z_0 + 1$ では $-x$ 方向でだけ歯抜けが起きるという可能性が残っている。もしそうならこの2つの平面のカバーする $\operatorname{proj}_x(S)$ を合わせると $\operatorname{proj}_x(S)$ が全部カバーできてしまうかも知れない。

多分、そういうことが起きないという事を $S'$ の凸性を使って示すんだと思うんだけど、どうしたらそんな事が示せるのか分からない。手詰まり。←今ここ

ググった結果

ILP で否等式を扱う方法を調べようと "integer linear programming disequality" とか "GLPK 'not equal' " とかでググると次のような情報が見つかる:
予め $|x| < u$ となるような定数の上限 $u$ が分かっているならば、$x \neq 0$ は 補助変数 $b,s_1,s_2$ を用いて次のように表せる:\[ s_1 + s_2 \ge 1 \\  0 \le b \le 1 \\ 0 \le s_1 \le u b \\ 0 \le s_2 \le u (1-b) \]
出典1 Re: [Help-glpk] [GLPK] not-equal constraints
出典2 How to specify an unequal constraint with an Integer Linear Programming (ILP) solver 

理路が若干違うけど、まあ「補助変数一つでは足りない」のとこで書いた方法と大体一緒。上限がわからない場合は使えない。
CPLEX ソルバでは indicator constraint という拡張機能を使えばこんな風に表現できるよ! \[0 \le b \le 1 \\ b = 0 \rightarrow x < 0 \\ b = 1 \rightarrow x > 0 \] (訳注: ($\rightarrow$) は "ならば" を表す CPLEX の拡張語彙。)
出典 Question : how to express the constrain "not equal to" effciently

ILP の範囲逸脱してんじゃねーか!
いやまあ、実用上は非常にありがたい機能で、どれぐらいソルバのパフォーマンスへの影響を抑えられるか興味あるんだけども、
  • 主に私が使ってる GLPK にはそんな機能は無い
  • 「可能なのか?」という数学的な興味に対する答えにはなってない
ので今一つ不服。

というわけで、$x$ の上限が分からない場合 $x \neq 0$ を表す方法は載ってないみたい。なので否等式を表す方法は存在しないか、知られてないかのどっちかだと思うのだけど、どっちなのかは不明。

まとめ

整数計画法で否等式 $x \neq y$ を線形不等式に直すことは可能か知りたい。これはまだ解決してない。ただし $|x - y|$ の上限が分かってるなら線形不等式にすることは出来る。

上限がわかっていない場合、補助変数一つを使った不等式で表すことは不可能。三次元以上でも不可能かどうかは今のところ不明。

引越し

はてなダイアリーから引っ越してきました。はてなの方は一応消されるまで残しますが、コメントとかもらっても多分気づかないので唯の過去ログだと思って下さい。