プログラム意味論

横内寛文

関数型プログラムの理論書という感じである。
この分野が、論理学というものであることを初めて知った。そして、「岩波現
代数学」シリーズには論理学はない。論理学は数学ではないのだろうか。

結構いいかげん。誤植もそれなり。

表示的意味論の考え方

カテゴリーの匂いが漂っている。

ラムダ計算の基礎

なかなか慣れないで括弧の対応だの、変数の意味だの、一瞬記号の並びはかけ
算か、と思ったり、ウロウロするが、むしろhaskellで考えれば簡単なのであった。
 true=λxy.x
 false=λxy.y
 fst=λx.xtrue
 snd=λx.xfase
 [M,N]=λx.xMN
といった定義で、
 snd[M,N] は、Nにリダクションする(という表現で正しいか)。のに対応して、
let true=(\x y -> x)
    false=(\x y -> y)
    fst=(\x -> x true)
    snd=(\x -> x false)
    kakko=(\x y -> (\a -> a x y))
    m=(\x -> "M")
    n=(\x -> "N")
in (snd (kakko m n)) 1
で、"N"が返る。という感じ。

一行で書けば、
((\x -> x (\z y -> y)) (\a -> a (\b -> "M") (\b -> "N"))) 1
こんな感じ。

((\x -> x (\z y -> y)) (\a -> a (print "M") (print "N")))
とすると最後のダミーの引数がいらない。

ちなみに
((\x -> x $ (\z y -> y)) $ (\a -> (a $ (\b -> "M")) $ (\b -> "N"))) 1
とも書ける。

.(ピリオド)でもいいかな、とか思ってしまって、試行錯誤。

false=(\x y -> y) で、false M N = N である。
false M N は、false . M . N  ではない。なぜかと言うと、
false . (\a->1)  を考えると、
=(\x y->y) . (\a -> 1) だから、 x->(y->y) . a->Num なので、
結果は、a->(y->y) つまり、
=(\a->(\y->y))
だから、
((\x y->y) . (\a -> 1) . (\b -> 2)) とかすると、 
=((\a->(\y->y)) . (\b -> 2))
これは、b->Num と、 a->(y->y)の合成で、b->(y->y)が残る。したがって、
=(\b->(\y->y))
これはさらに引数を2個とって、2個目をそのまま返す関数。
ということで、全然だめ。

trueの方は、
((\x y->x) . (\a->1) . (\b->2))
=((\a->(\y->1)) . (\b->2))
=(\b->(\y->1))
なので、引数を2つとって、1を返す。(こっちは正しいかも、と思える動作を
する)。

ということで悩んだ。そもそも関数の引数になっていると思って、括弧だけで
グルーピングすると悩まない。

途中面倒になって飛ばす。

領域理論の基礎

証明はジャンジャン飛ばす。

有向集合とは、半順序集合Dの空でない部分集合で、
a∈X, b∈X なら、
a⊑c かつ b⊑c
なる、c∈Xが存在する。

CPO (complete partially ordared set,完備半順序集合)は、半順序集合Dで、
(1)Dは最小元を持つ。
(2)Dの任意の有効部分集合XについてXの上限⊔X が存在する。

(1)は実は必要ない。

単調関数とは、D, D'を半順序集合とし、f:D→D'について、
a∈D, b∈D' で、
a⊑b ⇒ f(a)⊑f(b)

連続関数とは、D, D'をcpoとし、f:D→D'について、
Dの任意の有向集合 X について、{f(x)|x∈X}の上限が存在して、
f(⊔X)=⊔X{f(x)|x∈X}

つまり、上限の関数は、関数値の上限を返す。

関数型言語の意味論

不動点がわからなくなる。

μf:σ→τ.(λx:σ.M)
例えば、

f=F[f]
のように再帰的に定義されている、という意味で、例えば、
fact(x)=1           (x=0)
       =x*fact(x-1) (x>0)
のような階乗関数みたいの。fを求めようとすると、F[f]の中のfを求める必要
があり、無限に続く、かというとそういう意味ではない。fact(0)=1のように、
いきなり停止する場合もあるし、
fact(3)=3*fact(2)=3*2*fact(1)=3*2*1*fact(0)=3*2*1*1
のように停止する場合もある。もちろん、条件の与えかたが悪いと、停止せず、
未定義となる。たとえば、fact(1.5)とか、fact(-1)。(factの定義をxが非自
然数の場合にもそのまま使うとして)。

不動点というと、f(x)=x のような、変換によって動かない値、のようなイメー
ジがあるが、この場合変換によって動かないのは、関数。有限回の再帰では、
有限値 x に対してしかx!を与えない関数であるが、極限で不動点まで行くと、
任意の自然数に対して、x!を与え、かつ、F[f∞]してもf∞を返す。

μf:σ→τ.(λx:σ.M)
のように、型を変える関数の例は、
f :: Int -> [Char]
f x | x==0   = ""
    | x>0    = "."++(f (x-1))

のような式である。
これを、muにあたる記法で抽象的に定義することは、Haskellではできないの
か。
(\mu.f x -> F f) 10
みたいに、
(\mu.f x -> | x==0 = "";f x| x>0  = "."++(f (x-1))) 10
なんてことができるとおもしろそうなような、より判らなくなりそうな気もする。
(\x ->  let f y | y==0 = "";f y | y>=1 = "."++(f (y-1));in f x) 10
これがオッケーなので、いいのかな。

letrec x:σ<= M in N       は、(λx:σ.N)(μx:σ.M)                と書ける。
letrec f(x:σ):τ<= M in N は、(λf:σ→τ.N)(μf:σ→τ.λx:σ.M) と書ける。

例えば、schemeでは、factは、
(letrec ((fact (lambda (x) (if (=  x 0) 1 (* x (fact (- x 1))))))) 
 (fact 10))
と書ける。これが、letrecの2番目の使われかた。1番の使われかたは、
letrecを、letの引数のスコープにletの引数が含まれる、という意味と読んで、
scheme的の例を書けば、
(letrec ((x 2) (y (* x x))) y)
となる。これだと、let*でもよい。結局letrecは、自分自身の名前までアクセ
スできる、という点がポイントか。

haskellでは、letの引数スコープにもとからletの引数が入っているので、
let fact x | x==0 = 1
    fact x | x>=1 = x*(fact (x-1))
in fact 10
でよいのであった。つまり、haskellのletは、letrecなのか。そうか話が逆だ。
haskellはletrecを使わないとμが表現できないのじゃなく、μ記法の代りに
letrecを導入したんだ。

しっかし、書いてある証明達が、どこまでノントリビアルなのかわからん。つー
か、どの定理を読んでも、そりゃそうだろうと思えてしまう。(良くない傾向
だ)。

カテゴリ理論の基礎

この章を読みたかったからこの本を借りたわけで、よむ。
集合が要素に基いて考えるのと対称的に、カテゴリ論では、射に基づいて考え
る。なるほど。

カテゴリSetについて。
(1)Setの対象はすべての集合。
(2)Setの射はすべての関数。
(3)SetがAからBへの関数のとき、dom(f)=Aかつcod(f)=Bと定義する。
合成射、恒等射は、関数の合成、恒等関数。

(1)の時点で、私はわからなくなってしまう。全ての集合ってのはなんだ？
例えば、整数の範囲でとりあえず考えることにして、
{0}とか、{1}とか、{0,1}とか、{0,1,2,3}とか、{5,9,1,5}が対象なのか？
さらに、整数の範囲で、なんて限定するのもおかしくて、{整数}とか、{実数}
とか、{複素数}もSetの対象なのか？それどころか、{(x,y)}とか、{多角形}と
か、{人類}とか、も「すべての集合」に入ってそうな気がする。
とりあえず、整数くらいに限定することにして、
f=x^2みたいのを考えると、
f:A→B
に対応するのは、
x^2:{整数}→{0か正整数}
という射である。でいいのかなあ。部分カテゴリ
x^2:{-1,0,1,2}→{0,1,4}
という射でもある。

モノイドは集合MとM上の2項演算*と、元eが与えられており、
a*(b*c)=(a*b)*c
a*e=a=e*a
であるような集合である。

直積
A={0,1,2}
B={2,3,4}
<a,b>∈AxB
π1:AxB→A  を射影が定義されているとする。
π1(<a,b>)=a
ということで、Setの中には、<a,b>も含まれている、ということがやっぱり前
提なのであった。
任意の対象Cから、Aへの射
C={-1,0,1}, f(x)=x+1
f:C→A
g(x)=x+3
g:C→B
に対して、fと、π1・p、gとπ2・p が可換になるような射pが唯一存在する。
p=<f,g> でよい。
これが直積。

直和とは、
A={0,1,2}
B={2,3,4}
に対して、i1(x)=<0,x>, i2(x)=<1,x>が定義されていて、
任意のC、例えば{-1,0,1}に対して、
f:a-1 : A→C
g:b-3 : B→C
があるとき、p・i1と、fが可換になる、p・i2とgが可換になるpが唯一存在す
る。
 p(<x,y>)|x==0 =y-1
         |x==1 =y-3
かなあ。
直積は、直和か？直積だったら、i1(x)がi2(x)の情報なしには決まらないのか。
直和は、直積か？
直和は、
  π1(<x,y>)|x==0 =y
            |x==1 =0 ?  undefにすべきか？
  π2(<x,y>)|x==1 =y
            |x==0 =0 ?  undefにすべきか？
 に対して、
 p=<0,y>か<1,y>、あ、一意には定義できない。そうか、直積と直和はそういう
関係か。

equalizer
A→Bなる射fとgに対して、
  i    f,g
C → A → B
f・i=g・i
が成立し、かつ、
   h   f,g
C'→ A → B
f・h=g・h
なる別の射に対して、
  p
C'→C
i・p=h
なる射pが唯一存在する。

例えば、Num→Numに対して、f=x^2と、g=2*x のとき、
C={0,2}で、iは包含写像。
0^2=2*0=0
2^2=2*2=4
たとえば、C'={0}に対してもf・i=g・iだが、C'→Cを包含写像とすれば、
C'→C→A
とできる。
f-g という写像を考えると、(f-g)・i=0で、iはf-gのKernelになっている。

coequalizerは、矢印を反対にすればよいだが、equalizerより単純じゃなくて、
{0}
{1,2}
{4}
{6,9}
{8,16,64,32**2,...}= {a_n|a_0=8,a_n=(an-1/2)^2}
{10,25}
{12,36,18**2,...}={a_n|a_0=12,a_n=(an-1/2)^2}
などと分類して、代表元なり、インデックスへの写像とすればいいように思う。
Num/{a_n=(an-1/2)^2}でいいのかな。
これ以上分類を粗くすると、別の h・f=h・g なる、hからの写像ができない。
これは、Coker(f-g)ってことでいいのかな。
x〜y if x=f(z) かつ y=g(z) あるいはx=g(z) かつy=f(z)。
g(f-1(g(f-1(x))))みたいのを簡潔に表記するにはどうしたらよいのだ。
という同値関係で割ったものだな。

cpoを対象とするカテゴリCPOで、
{_|_, 0,1,2}, とかに対して、半順序を、<=で入れる。
カテゴリCPOでは、(この本の定義からは)よくわからんが、最小元を全部の対
象で共有しなければならないらしいので、全ての対象が _|_ は含むとするら
しい。

直積を持つカテゴリCにおいて、対象Aから、Bへの巾対象とは、
App: B^A × A → B を伴った対象B^Aで、
任意の対象Cと射f: C×A→Bについて
          App
B^A × A  →  B
↑Cur(f)×id  ↑f
C×A ----------

を可換にする射 Cur(f): C→B^Aが唯一存在する。というような、B^Aのことで
ある。

<(\x y->x+y) c, a>
=<(\y->c+y), a>
これにAppをかけると、
App(<(\y->c+y), a>)=(\y->c+y) a = c+a

一方,
(\x y->x+y)(<c,a>)=(\x y->x+y) c a =c+a

なのである。ここで、Cur(\x y->x+y) c は、(\y->c+y) いわゆるカリー化。
巾対象は、カリー化した結果(\y->c+y)。
もっと一般に書けば、(Cur(\x y->f(x,y)) c)  (c∈C)である。

Cとfは任意なのだから、巾対象がもう一つあったとして、Cをもう一つの巾対
象にしても上の可換性は成立。C×A→Bを、kと書く。
Cは巾対象だから、任意の対象として、B^Aを選んで、
          k
C × A    →    B
↑Cur(App)×id ↑App
B^A×A ---------

も成立。
ということで、Cur(k)・Cur(App)=Cur(App)・Cur(k)=id
Cと、B^Aは同型。

limitとは、μ:X→Dをconeとする。任意のcone ν:Y→Dに対して、
ある射 p:Y→Xが存在し、Dの各頂点につき
     p
  X<----Y
μ↓    |ν
   Di←-+

が可換になり、このような、pは唯一である場合の、μをDのlimitと言う。

limitは直積とequalizerが定義できれば、存在する。の証明がわからない。

Πi∈VDi  ---(πcod(e))→ Dcod(e)
  |                                 ↑πe
  +-------------(p)---------→ Πe∈EDcod(e)

これでは、私にはわからないので、

D2 ← D1 → D3
 |          ↑
 +-----------+

なる3点からなる図を考えよう。
V={1,2,3}
E={12,23,13}
cod(e)={2,3,3}
dom(e)={1,2,1}

e=23のとき、
D1×D2×D3 ------(π_3)---→ D3
  |                          ↑π23
  +--------------(p)------→ D2×D3×D3

で、π_eはΠe∈EDcod(e)という直積から、Dcod(e)への
projectionのはずなのだ。だったら、πcod(e)ではなかろうか。
成分で考えよう。
D1={0,1,2}
D2={0,1,2,3,4}
D3={-1,0,1,2,3,4,5,6,7,8,9}
D12=x^2
D23=2x+1
D13=4x-1
<2,4,8>∈D1×D2×D3
π_3(<2,4,8>)=8
<4,8,8>∈D2×D3×D3
π23(<4,8,8>)=8  にならなきゃだめだよなあ。
p(<x,y,z>)=<y,z,z>  かなあ。

もう一つのルートとして、

Πi∈VDi  ---(q)---------→ Πe∈EDcod(e)
  ↓πdom(e)                    ↓πe
Ddom(e)------------(D_e)---→ Dcod(e)

これは、e=23のとき、

D1×D2×D3 ------(q)---→ D2×D3×D3
  ↓π_2                       ↓π23
  D2-----------(D23)--------→ D3

<2,4,8>∈D1×D2×D3
π_2(<2,4,8>)=4
D23(4)=9
q(<x,y,z>)=<D12(x),D23(y),D13(x)>

あ、そうか。で、equalizerを入れて、
<f(y),f(z),f(z)>=<D12(f(x)),D23(f(y)),D13(f(x))>
fを包含写像f(x)=xとして、これを満すのは、
<1,1,3>のみ。
<1,1,3>--(π1)→1
<1,1,3>--(π2)→1
<1,1,3>--(π3)→3

<1,1,3>--(D12・π1)→1
<1,1,3>--(D23・π2)→3
<1,1,3>--(D13・π1)→3
ということで、πi=Dij・πj は成立。
このπ(正確には)、πi・X={<1,1,3>}→Di がlimitである。
π_eの意味は結局よくわからないが、limitの意味はわかった。

関手は、まあ想像通り。

この後6章 領域方程式、7章ラムダ計算の意味論と続くのだが、パスすること
にした。