¥³¥ó¥Ó¥Í¡¼¥¿ÏÀÍý

コンビネータ論理

日本ユニシス株式会社 川辺治之

適用系

適用系とは、集合_Cに、それぞれの要素xとy （このとおりの順序）に対して(xy)と表記される 要素を割り当てる演算を合わせたものである。 コンビネータ論理では，左から順に括弧を復元す るものと考えて，括弧を省略することが多い．し たがって，xyzは，(x(yz))ではなく((xy)z)の省 略形である．また，xyzwは，(((xy)z)w)の省略 形である．

合成条件

A, B, C

を任意の要素とするとき，すべ

ての要素

x

に対して

Cx = A(Bx)

となる

ならば，

C

は

A

に

B

を結合させるという．

すべての

A

と

B

に対して，

A

に

B

を結合

させるような

C

があるならば，合成条件

が成り立つという．

M

：モッカー

モッカー（

mocker

，マネシツグミ）また

は複製子は、は、次の条件を満たすコン

ビネータ

M

である．

M x = xx

M = SII = S(SKK)(SKK)

M x = SIIx = Ix(Ix) = xx

不動点

要素

y

は，

xy = y

となるならば，要素

x

の不動点と呼ばれる．

すべての要素

A

が不動点をもつためには，

次の

2

条件が成り立てば十分である．

C1:

合成条件

C2:

モッカー

M

が存在する．

証明

C

を、

A

に

M

を結合させる要素とする．

したがって，すべての要素

x

に対して，

Cx = A(M x)

となる．しかし，

M x = xx

なので，すべての

x

に対して

Cx = A(xx)

である．ここで，

x

を

C

とすると，

CC = A(CC)

となり， これは，

CC

が

A

の不動点であることを示している．

すなわち、

C

が

x

に

M

を結合させるなら

K

：ケストレル

削除子，または，ケストレル（

kestrel,

チョウゲンボウ）は、次の条件を満たす

コンビネータ

K

である．

S

：スターリング

スターリング（

starling

，ホシムクドリ）

は、次の条件を満たすコンビネータ

S

で

ある．

I

：恒等コンビネータ

恒等コンビネータとは，すべての

x

に対

して条件

Ix = x

を満たすような要素

I

の

ことである．

I = SKK

Ix = SKKx = Kx(Kx) = x

B

：ブルーバード

ブルーバード（

bluebird

，ルリツグミ）は、

次の条件を満たすコンビネータ

B

である．

Bxyz = x(yz)

B = S(KS)K

Bxyz = S(KS)Kxyz = KSx(Kx)yz

C

：カーディナル

カーディナル（

cardinal

，コウカンチョウ）

は、次の条件を満たすコンビネータ

C

で

ある．

Cxyz = xzy

C = S(BBS)(KK)

Cxyz = S(BBS)(KK)xyz

= BBSx(KKx)yz = B(Sx)Kyz

= Sx(Ky)z = xz(Kyz) = xzy

T

：スラッシュ

スラッシュ（

thrush

，ツグミ）は、次の条

件を満たすコンビネータ

T

である．

T xy = yx

T = CI

T xy = CIxy = Iyx = yx

R

：ロビン

textbf

ロビン（

robin

，コマツグミ）は，次

の条件を満たすコンビネータ

R

である．

Rxyz = yzx

R = BBT

Rxyz = BBT xyz = B(T x)yz

V

：ヴィレオ

ヴィレオ（

vireo

，モズモドキ）は，次の

条件を満たすコンビネータ

V

である．

V xyz = zxy

V = BCT

実現可能な項

t

が

x

1

, x

2

, . . . , x

n

の中の変数だけから構

成され，

Ax

1

x

2

· · · x

n

= t

の成り立つよう

な要素

A

が適用系

C

に含まれるならば，

x

1

, x

2

, . . . , x

n

を引数とするコンビネータ

A

は項

t

を実現するという．

第

1

不動点定理

任意の実現可能な項

t(x, x

₁

, . . . , x

_n

)

に対

して，条件

Γ x

₁

· · · x

_n

= t(Γ, x

₁

, . . . , x

_n

)

を

証明

A

は項

t

を実現するコンビネータとする．

すなわち，

Axx

1

· · · x

n

= t(x, x

1

, . . . , x

n

)

である．

Γ

を

A

の不動点とすると，

Γ x

₁

· · · x

_n

= AΓ x

₁

· · · x

_n

= t(Γ, x

₁

, . . . , x

_n

)

となる．すなわち，

Γ x

1

· · · x

n

= t(Γ, x

1

, . . . , x

n

)

である．

命題コンビネータ

t

としてケストレル

K

を用い，

f

としてコ

ンビネータ

KI

を用いる．

（以降では，

t

は

K

の省略形であり，

f

は

KI

の省略形であ

る．

）

t

と

f

を命題コンビネータと呼ぶ．

任意のコンビネータ

x

と

y

に対して，そ

れらが命題コンビネータであるかどうか

にかかわらず，

txy = x

かつ

f xy = y

と

なる。

N

：否定コンビネータ

条件

N x = xf t

を満たす否定コンビネー

タ

N

が必要になる．

V

をヴィレオ（

V xyz = zxy

）として，

N

を

Vf t

とすると，

N x = Vf tx = xf t

と

なる．

このとき，

（

t = K

なので）

N t = tf t = f

であり，

（

f = KI

なので）

N f = f f t = t

となる．したがって，

p

が

t

であっても

f

であっても，

N p =

∼p

となる．

連言コンビネータ

cxy = xyf

となるような連言コンビネー

タ

c

を求めたい．

R

をロビン（

Rxyz = yzx

）として，

c

を

Rf

とすると，

cxy = Rf xy = xyf

となる．

ctt = Rf tt = ttf = t

ctf = Rf tf = tf f = f

cf t = Rf f t = f tf = f

選言コンビネータ

dxy = xty

となるような選言コンビネー

タ

d

を求めたい．

T

をスラッシュ（

T xy = yx

）として，

d

を

T t

とすると，

dxy = T txy = xty

となる．

dtt = T ttt = ttf = t

dtf = T ttf = ttf = t

df t = T tf t = f tt = t

df f = T tf f = tf f = f

含意コンビネータ

R

をロビン（

Rxyz = yzx

）として，含意

コンビネータ

i

を

Rt

とする．すると，

ixy = Rtxy = xyt

なので，

ipq = p

⊃ q

と

なる．

itt = Rttt = ttt = t

itf = Rttf = tf t = f

if t = Rtf t = f tt = t

同値コンビネータ

exy = xy(N y)

となるような同値コンビ

ネータ

e

を求めたい．

このために，

e

を

CSN

とすると

CSN xy = SxN y = xy(N y)

となる．

このとき，

epq

は

p

≡ q

と同じ値になる．

ett = CSN tt = tt(N t) = t

etf = CSN tf = tf (N f ) = f

ef t = CSN f t = f t(N t) = f

ef f = CSN f f = f f (N f ) = t

σ

：後者コンビネータ

σ

を後者コンビネータ

Vf

（これは

V (KI)

である）とする．

0

を恒等コンビネータ

I

とし，

1

を

σ0

，

2

を

σ1

というように，

n + 1 = σn

とする．

コンビネータ

0, 1, 2, . . .

を，数値コンビ

ネータ（数項）という。

0, 1, 2, . . .

はすべて相異なる．

（証明は

算術コンビネータ

コンビネータAは，すべてのnに対して， An = mとなる数mが存在するならば，1型の算 術コンビネータと呼ばれる． コンビネータAは，すべてのnとmに対して， An m = pとなる数pが存在するならば，2型の算 術コンビネータと呼ばれる． 一般に，コンビネータAは，すべての数x1, . . . , xnに対して，Ax1· · · xn = yとなる数yが存在す るならば，n型の算術コンビネータと呼ばれる．

Z

：ゼロ試験子

T

をスラッシュ（

T xy = yx

）として，

Z

を

T t

とする．

0 = I

かつ

σ = Vf

であるこ

とから

Z0 = T t0 = 0t = It = t

となる．したがって，

Z0 = t

である．

また、

Zn + 1 = T tn + 1 = n + 1t = σnt

数値コンビネータの前者

n

+

_{= σn}

_なので，

_{P (σn) = n}

_{となるコン}

ビネータ

P

を求めたい．

（

n

+

は

n + 1

の省

略形である。）

T

をスラッシュ（

T xy = yx

）として，

P

を

T f

とすると，

P (σn) = T f (σn) = σnf = Vf nf = f f n = n

となる．

再帰的関数性

任意の項f (y1, . . . , yn)とg(x, z, y1, . . . , yn)に対し て，コンビネータΓ で，すべての数項x, y₁, . . . , y_nに対して Γ 0 y₁· · · yn = f (y₁, . . . , y_n) Γ x y₁· · · yn = g((P x), (Γ (P x)y₁· · · yn), y₁, . . . , y_n) となるようなものが存在する。 不動点定理によって，次の条件によって定義され るコンビネータΓ が存在する。 · · · y

性質コンビネータ

すべての数

n

に対して，

Γ n = t

または

Γ n = f

となるようなコンビネータ

Γ

を性

質コンビネータという。

(

自然）数の集合

A

は，性質コンビネータ

Γ

で，

A

に属するすべての

n

に対して

Γ n = t

となり，

A

に属さないすべての

n

に対して

Γ n = f

となるようなものが存

在するならば，計算可能という．

このようなコンビネータ

Γ

は，

A

を計算

するという．

例：偶数の集合

偶数であるという性質は，次の条件を満

たすただ一つの性質である．

•

0

は偶数である．

•

正整数

n

に対して，

n

が偶数であるの

は，その前者が偶数でないとき，そし

てそのときに限る．

Γ x = Zxt(N (Γ (P x)))

関係コンビネータ

n

次の関係コンビネータとは，コンビ

ネータ

A

で，すべての数

k

₁

, . . . , k

_n

に対

して，

Ak

₁

· · · k

_n

= t

または

Ak

₁

· · · k

_n

= f

となるようなもの

そして，そのようなコンビネータ

A

は，

Ak

1

· · · k

n

= t

となるような

n

個組

(k

1

, . . . , k

n

)

すべてからなる集合を計算す

るという．

表現可能性

コンビネータ

Γ

は，すべての数

n

に対し

て，

Γ n = t iff n

∈ A

ならば，数の集合

A

を表現するという

n

̸∈ A

のとき、計算可能性の場合は

Γ n

= f

でなければならないが，表現可能

性の場合は

Γ n

̸= t

であればよい。

ゲーデル数

文は，次の形式をした等式である．

S, K

項

= S, K

項

文のゲーデル数は，

S

を

1

，

K

を

2

，

(

を

3

、

)

を

4, =

を

5

で置き換え，その結果を

十進数として読むことによって得られる

数である．

任意の記号列

X

に対して，

⌈X⌉

は，

X

の

ゲーデル数を指示する数項のことである．

すべての真な文からなる集合

T

をすべての真な文からなる集合とし，

T

0

をすべての真な文のゲーデル数からな

る集合とする．

集合

_T

₀

が計算可能であるか。すなわち，

すべての

n

に対して，

n

∈ T

0

ならば

Γ n = t

であり，

n

̸∈ T

0

ならば

Γ n = f

で

あるようなコンビネータ

Γ

が存在するだ

⊕

：加法コンビネータ

加法演算

+

は，

n + 0 = n

，

n + m

+

= (n + m)

+

によって一意に決

まる．

⊕ n 0 = n

⊕ n m

+

_{= σ(}

⊕ n m)

となるもの、すなわち，任意の

n

と

m

に

対して，

⊕ n m = Zm n(σ(⊕(n(P m))))

が

成り立つような

⊕

が不動点定理によって

存在する．

正則コンビネータ

2

次の関係コンビネータ

A

で，すべての

数

n

に対して，

An m = t

となる数

m

が少

なくとも一つ存在するようなものを考え

る．このようなコンビネータは，正則と

呼ばれることもある．

A

が正則ならば，すべての

n

に対して，

An k = t

となるような最小の数

k

がなけ

最小化原理

A

を任意の正則な

2

次の関係コンビネー

タとするとき，不動点定理によって，次

の条件を満たすコンビネータ

A

₁

が存在

する．

A

1

xy = (Axy)y(A

1

x(σy))

したがって，すべての数

n

と

m

に対して

次の条件が成り立つ。

An m = t

ならば，

A

1

n m = m

An m

= f

ならば，

A

₁

n m = A

₁

n m + 1

最小化子

すべての正則な

2

次の関係コンビネータ

A

に対して，

A

の最小化子と呼ばれるコ

ンビネータ

A

′

で，すべての

n

に対して、

k

を

An k = t

となるような最小の数とす

ると、

A

′

n = k

となるようなものが存在

する。

C

をカーディナル（

Cxyz = xzy

）とし，

A

′

を

CA

1

0

とすればよい。このとき，任

長さ測定子

gxy = Zxf (Zyt(g(P x)(P y)))

とすると、

g

が関係

x > y

を計算し，

⃝e

10

が関数

10

x

を

実現する。

すると，

Bg(

⃝e

10)

は、関係

10

x

> y

を計算

する．

したがって，

C(Bg(

⃝e

10))

は関係

10

y

> x

を計算する．

すなわち，長さ測定子

L

′

を，

C(Bg(

⃝e

10))

の最小化子とすればよい．

連結コンビネータ

任意の数

n

と

m

に対して，

n

∗ m

は，通常

の十進数表記で書いたときに，

（十進数表

記の）

n

の後に（十進数表記の）

m

を続

けた数のこととする。

⊛

を，

⊛ xy = ⊕(⊗ x(

⃝e

10(L

′

y)))y

とする

と、すべての

n

と

m

に対して，

⊛ n m = n ∗ m

となる。（

⊗

は乗法コンビ

ネータ、

⃝

はべき乗コンビネータ、

L

′

は長

数項のゲーデル数

任意の数nに対して，数項nは，ほかの項と同じ ように，ゲーデル数をもつ．n#を数項nのゲーデ ル数とする． たとえば，0はコンビネータIで，SとKを使っ て表すと((SK)K)になり，そのゲーデル数は 3312424である．したがって，0# = 3312424と なる． 1#は，数項1のゲーデル数であり，1 = (σ0)で ある． sをσ（になる項）のゲーデル数とすると，1#は， (σ0)のゲーデル数で，3∗ s ∗ 0# ∗ 4である．

δn = n#_{が成り立つようなコンビネータ δ が存在する。} まず、任意のコンビネータ A と任意の数 k に対して，次の 2 条件を満たすコンビネータ δ が存在することを示す。 1. δ0 = k 2. δn+_{= A(δn)} 条件 2 は δn = A(δ(P n)) と同値であるので、次の条件を満 たすコンビネータ δ は、不動点定理によって存在する。 δx = Zxk(A(δ(P x))) 具体的には、δ は、条件 θyx = Zxk(A(y(P x))) を満たすコ ンビネータ θ の不動点である。 ここで A を，等式 An = 3∗ s ∗ n ∗ 4 を満たすコンビネータ、

∆

：正規化子

すべての

n

に対して

∆n = n

∗ n

#

_が成り

立つようなコンビネータ

∆

を正規化子と

いう。

S

をスターリング（

Sxyz = xz(yz)

）とし

て，

∆

を

S

⊛ δ

とする．このとき，

δn = n

#

_{であることに注意すると}

∆n = S

⊛ δn = ⊛ n(δn) = ⊛ n n

#

_{= n}

∗ n

#

が得られる．

第

2

不動点定理

任意のコンビネータ

A

に対して，

A

⌈X⌉ = X

が成り立つような項

X

が存在

証明

∆

を正規化子として，

X

を

BA∆

⌈BA∆⌉

とする．ブルーバード

B

の定義によって，

BA∆

⌈BA∆⌉ = A(∆⌈BA∆⌉)

が得られる．

任意の

Y

に対して

∆

⌈Y ⌉ = ⌈Y ⌈Y ⌉⌉

とな

る．

（証明は次ページ）したがって，

∆

⌈BA∆⌉ = ⌈BA∆⌈BA∆⌉⌉ = ⌈X⌉

証明（つづき）

nを，X のゲーデル数とする．このとき， n =⌈X⌉なので，∆n = ∆⌈X⌉となる． ∆n = n∗ n#_なので， ∆⌈X⌉ = n ∗ n# が得られる．nはX のゲーデル数なので，nの ゲーデル数と定義したn#は⌈X⌉のゲーデル数で もなければならない．なぜなら，n = ⌈X⌉だから である．したがって，n∗ n#はX⌈X⌉のゲーデル 数であり，

ゲーデル文

文（等式）

X

が真であるのは，

X

のゲー

デル数が数の集合

A

に属するとき，そし

てそのときに限るならば，

X

を

A

のゲー

デル文と呼ぶ。

集合

A

が表現可能ならば，

A

のゲーデル

文が存在する。

証明

n∈ A′ iff n∗ 52 ∈ A となるようなA′は表現可能であり（証明は次ペー ジ）、Γ が集合A′を表現するとする．このとき， 第2不動点定理によって，Γ⌈X⌉ = Xとなるよう なX が存在する． nをX のゲーデル数とすると，n =⌈X⌉である． したがって，Γ n = Γ⌈X⌉である．

証明（続き）

Γ

1

が

f (x)

を実現し，

Γ

2

が

A

を表現すると

仮定する．

Γ = BΓ

₂

Γ

₁

とすると，

Γ

は

f

−1

(A)

を表現する。（

Bxyz = x(yz)

で

ある．

）

Γ n = BΓ

2

Γ

1

n = Γ

2

(Γ

1

n) = Γ

2

f (n)

が成り立つ．したがって，

Γ n = t

となる

のは，

n

∈ f

−1

(A)

であるとき，そしてそ

のときに限る．これは，

Γ

が

f

−1

(A)

を表

現するということである．

計算可能でない集合

すべての真な文のゲーデル数からなる集合_T0は計 算可能でない。 T0の補集合のゲーデル文X があったとすると，X が真になるのは，そのゲーデル数nがT0に属さな いとき，そしてそのときに限る．これは，X が真 となるのは，そのゲーデル数が真な文のゲーデル 数ではないとき，そしてそのときに限ることを意 味するが，それは不可能である． T0の補集合のゲーデル文は存在しないので，T0の 補集合は表現可能ではなく，それゆえ，集合_T0は