証明と推論の機械化

1

証明と推論の機械化

久木田水生

2

計算・推論の機械化

• 計算の分野では古くから，ある問題に対して解を求めるための機械的な 手続き（アルゴリズム）が発見され，使われてきた．

• 演繹的推論に関しては，形式的論理学の発展により， 20 世紀初頭には

，例えば命題論理や一階述語論理の恒真式の判定や，形式的体系で の証明を構成するためのアルゴリズムが発見された．

• 一方，帰納的な推論，仮説生成的推論に関しても，ベーコンやニュート ン，ミルなどによって，その方法論が提案されてきた．

• 1980 年代以降，コンピュータの発展とともに，帰納推論を行う機械学習

システムが著しく発展した．

• 本発表では導出原理に基く，一階述語論理の定理判定アルゴリズムと

，そのコンピュータによる実装を紹介する．

• 最後に導出原理を応用して作られた論理プログラミング，そしてさらにそ

の帰納推論，仮説推論への応用について簡単に触れる．

3

例）　ユークリッドの互除法

• 以下は，二つの自然数の最大公約数を求める手続きで，「ユ ークリッドの互除法（ Euclidean algorithm ）」として知られて いる．

• 1. m, n に与えられた自然数を入力して 2 に進む．

• 2. q := mod(n, m) と置く． 3 に進む．

• 3. q = 0 ならば手続きを終了する，そうでなければ 4 に進む．

• 4. n := m, m := q と置く． 2 に戻る．

※ mod(n, m) は n を m で割った余りを表す．

• 手続きを終了した時点の m の値が，入力された二つの自然 数の最大公約数である．

（→

EuclideanAlgorithm.java

4

例）　割り算のための「書き換えアルゴリズム」

(Terese [2003])

• 「 n 」は「 S(S(...S(0)...)) 」（ S が n 個現れる）の略記とする．

• 初期状態：　 quot(n, m) 　（ただし n >= 0, m > 0 ）

• 終了状態：　 n 　（ただし n >= 0 ）

• 規則 1 ：　 minus(n, 0) → n

• 規則 2 ：　 minus(S(n), S(m)) → minus(n, m)

• 規則 3 ：　 quot(0, S(n)) → 0

• 規則 4 ：　 quot(S(n), S(m)) → S(quot(minus(n,

m),S(m)))

5

割り算のための「書き換えアルゴリズム」

• quot(4, 2)

 S(quot(minus(3, 1), 2))

 S(quot(minus(2, 0), 2))

 S(quot(2, 2))

 S(S(quot(minus(1, 1), 2)))

 S(S(quot(minus(0, 0), 2)))

 S(S(quot(0, 2)))

 S(S(0)) = 2

6

例）　ルイス・キャロルの論理ゲーム

（ Carrol [2005])

ルイス･キャロルは三段論法的推論を行う次のようなゲームを考えた．

下図の

X

x

Y

y

M

m

XYm Xym

xYm xym

xYM xyM XYM XyM

例えば左上外側の区画は

X

Y

M

その区画に対象が存在しないとき

，そこには灰色のコマを置く．

その区画に対象が存在するとき赤 いコマを置く．

7

ルイス・キャロルの論理ゲーム

XYm Xym

xYm xym

xYM xyM XYM XyM

次の二つの前提が与えられたとし よう．

1

X

m

2

Y

m

2

Y

m

，そこに対象が存在しないことを 表す灰色のコマを置く．

8

ルイス・キャロルの論理ゲーム

XYm Xym

xYm xym

xYM xyM XYM XyM

１　ある

X

m

２　すべての

Y

m

次に１の前提を考慮する．

X

m

XYm

Xym

9

ルイス・キャロルの論理ゲーム

XYm Xym

xYm xym

xYM xyM XYM XyM

１　ある

X

m

２　すべての

Y

m

しかし

XYm

Xym

10

ルイス・キャロルの論理ゲーム

XYm Xym

xYm xym

xYM xyM XYM XyM

１　ある

X

m

２　すべての

Y

m

最後に

M

m

M

m

また

M,m

11

ルイス・キャロルの論理ゲーム

XY Xy

xY xy

１　ある

X

m

２　すべての

Y

m

図から読み取れる結論は

ある

X

y

ということになる．

12

ルイス・キャロルの論理ゲーム

また次のような前提が与えられたとする．

XYm Xym

xYm xym

xYM xyM XYM XyM

1

X

M

2

M

Y

１から，

X

m

，そこに対象が存在しないことを 表す灰色のコマを置く．

13

ルイス・キャロルの論理ゲーム

XYm Xym

xYm xym

xYM xyM XYM XyM

1

X

M

2

M

Y

2

M

y

，そこに対象が存在しないことを 表す灰色のコマを置く．

14

ルイス・キャロルの論理ゲーム

XYm Xym

xYm xym

xYM xyM XYM XyM

1

X

M

2

M

Y

最後に

M

m

境界の両方に灰色のコマがある 区画（ここでは右上）にだけコマを 残す．

15

ルイス・キャロルの論理ゲーム

XY Xy

xY xy

1

X

M

2

M

Y

最後に

M

m

境界の両方に灰色のコマがある 区画（ここでは右上）にだけコマを 残す．

M

m

16

ルイス・キャロルの論理ゲーム

XY Xy

xY xy

1

X

M

2

M

Y

図から読み取れる結論は，

　　すべての

X

Y

ということになる．

17

ルイスキャロルの論理ゲーム

• ルイス･キャロルの論理ゲームは，論理的な推論を，

一定のルールに従って行うゲームとして表現してい る．

• このゲームの図やコマの配置，そしてそれを操作す るルールは私たちの知識や推論をモデル化したもの であると言うことができる．

• 最初の図とコマの配置が前提を表し，最後の図とコ

マの配置が結論を表現している．

18

例）　トートロジーをチェックするアルゴリズム

• 以下はエルブランによって発見された，論理式の 書き換えアルゴリズムである (Terese [2003]) ．

• 規則 1 ：　 p q ⇒ 　→　 p ・ q + p + 1

• 規則 2 ：　 p q ∨ 　→　 p ・ q + p + q

• 規則 3 ：　￢ p 　→　 p + 1

• 規則 4 ：　 p + 0 　→　 p

• 規則 5 ：　 p + p 　→　 0

• 規則 6 ：　 p ・ 0 　→　 0

19

トートロジーをチェックするアルゴリズム

• 規則 7 ：　 p ・ 1 　→　 p

• 規則 8 ：　 p ・ p 　→　 p

• 規則 9 ：　 p ・ (q + r) 　→　 p ・ q + p ・ r

• 規則 10 ：　・と + に関する結合律，および交換律

• この規則に従って論理式を書き換え， 1 で終了する

とき，そしてそのときに限り，最初の式はトートロジ

ーである．

20

トートロジーをチェックするアルゴリズム

• p ∨ ￢ p

 p ・￢ p + p + ￢ p

 p ・￢ p + p + (p + 1)

 p ・￢ p + (p + p) + 1

 p ・￢ p + 0 + 1

 p ・￢ p + 1

 p ・ (p + 1) + 1

 p ・ p + p + 1

 (p + p) + 1

 0 + 1

 1

21

AI による自動証明の試み

• ある推論を遂行するためのアルゴリズムを確立することによ って，その推論を機械的な手続きにすることができる．

• そこに十分な工学的技術が加わることで，推論の自動化が 可能になる．

• このような試みの一環は，論理学の定理の自動証明という 形で， 1950 年代頃から行われるようになった．

• AI に関する研究集会，ダートマス会議（ 1956 ）では，

Whitehead & Russell, Principia Mathematica の定理を証 明する Logic Theorist というプログラムが Newell, Simon, Shaw によって発表された．

• このプログラムは PM の第 2 章に挙げられた 52 個の定理のう

ち， 32 個の証明を見つけることができた．

22

節形論理

• Robinson [1965] は，一階述語論理の式が充足不 可能であることを判定するための手続きを与えた．

• ここでは節形論理（ clausal form logic ）という特殊な 論理体系が採用される．

• この手続きは，実際にその式が充足不可能であると きは有限のステップで判定結果を出す．

• 式が充足可能である場合には手続きが終了しない

こともある．

23

節形論理：構文論と解釈（命題論理）

• 原子式，およびその否定をリテラルという．

• リテラルの有限集合（空でもよい）を節という．

• 節集合 { C1 ， ... ， Cn } は ( C1) ... ∨ ∧ ∧ （∨ Cn)

という連言標準形の論理式と同一視される．

• 任意の論理式はそれと論理的に同値な連言標準形を持つこ とに注意．

※節 {L1, ..., Ln} に対して∨ {L1, ..., Ln} は L1 ... L3 ∨ ∨ という論理 式を表す．

∨

※ { } は矛盾⊥を表す．空節を□によって表す．

24

節形論理：導出原理（命題論理）

• リテラル L と L* に対して，一方が他方の否定であると き， L と L* は相補的であるという．

• 節 C と節 D がそれぞれ，相補的なリテラル L ， L* を含 むとき， (C － {L}) (D ∪ － {L*}) を， C と D からのリゾルベ ントと呼ぶ．

• 導出原理： C1 ， C2 は節， C は C1 と C2 からのリゾルベ ントであるとする．このとき， C １と C2 から節 C を導出 してよい．

• 節集合 X に， X に含まれる任意の二つの節から導出

可能なすべての節を加えた節集合を R(X) と表す．

25

節形論理：導出原理（命題論理）

• R ⁰ (X) = X ， R ⁿ⁺¹ (X) = R(R ⁿ (X)) 　と表す．

• 任意の節集合 X = {C1, C2, ... , Cn} （ n >= 0 ）に対し て c(X) は論理式 ( C1) ( C2) ... ( Cn) ∨ ∧ ∨ ∧ ∧ ∨ を表す ものとする．

• 定理（導出原理の完全性）

ある n>=0 に対して　□∈ R ⁿ (X) であるのは c(X) が充

足不可能であるとき，そしてそのときに限る．

26

節形論理：導出原理（命題論理）

• 例）　 X = { {-p1, p2}, {-p2, p3}, {p1}, {-p3} } とする．

このとき以下の導出が可能．

□

{-p1, p2} {p1}

{-p2}

{p2}

{-p2, p3} {-p3}

27

節形論理：導出原理（命題論理）

• 例）　 X = { {p1, p2}, {p1, -p2}, {-p1, -p3}, {p2, p3}, {-p2, p3} } とする．このとき以下の導出が可能．

{p1, p2} {p1, -p2}

{-p1, -p3} {p2, p3} {-p1, -p3} {-p2, p3}

{-p1, p2} {-p1, -p2}

{-p1}

{p1}

□

(→RefutationTest1.java)

28

節形論理：構文論と解釈（述語論理）

• 項：

– 変数，定数は項である．

– n 項関数に対して，引数として n 個の項の配列を与 えたものは項である．

• 原子式： n 項述語に対して，引数として n 個の項の配 列を与えたものは原子式である．

• リテラル：原子式，およびその否定はリテラルである

．

• 節：リテラルの有限集合を節という．

• 相補的なリテラル：命題論理の場合と同様．

29

節形論理：構文論と解釈（述語論理）

• 節集合 {C1,... , Cn} に現れる変数を v1,... , vm とする とき， X は全称冠頭連言標準形の論理式

∀ v1... vm(( C1) ... ( Cn)) ∀ ∨ ∧ ∧ ∨ と同一視される．

• 任意の論理式 P に対して，ある全称冠頭連言標準形 の論理式 Q が存在して，

P が充足不可能　⇔　 Q が充足不可能

が成り立つことに注意．

30

節形論理：不一致集合

• 式 P1 と P2 の不一致集合とは，それぞれの式を左か ら見て，最初に異なる記号が現れる箇所から始まる 項を要素として持つ集合である．

• 例）　式 P(v2, f1(v1, c1)) と P(v2, f1(f2(v3), c1)) との 不一致集合は， {v1, f2(v3)} ．

• 式の集合から作られる不一致集合も同様に定義さ れる．

（→

DisagreementSetTest1.java

31

節形論理：置換

• 変数 v と項 t に対して [ ｔ / v] を置換または代入という．

• 任意の表現 E に対して E[t / v] は E に現れる変数 v をすべて t に置き換えて得られる表現を表す．

• 表現の集合 {E1, ..., En} と置換 [t / v] に対して，

{E1, ..., En} [t / v] = {E1[t / v], ..., En[t / v]}

とする．

• 表現 E と置換の集合 θ = { [t1 / v1], ..., [tn / vn] } に対して Eθ は E に現れる v1, ..., vn をそれぞれ t1, ..., tn によって置き 換えて得られる表現を表す．

• このような θ を同時置換（または単に置換）と呼ぶ．

（→SubstituteAtOnceTest1.java

, AvoidVariableClashTest1.java

32

節形論理：置換

• 表現の集合 {E1, ..., En} と同時置換 θ に対して，

{E1, ..., En}θ = {E1θ, ..., Enθ}

とする．

• 同時置換 θ = { [t1 / v1], ..., [tn / vn] } と μ = { [s1 / u1], ..., [sm / um] } に対して， θ ・ μ は集合 { [t1μ / v1], ..., [tnμ / vn], [s1/ u1], ..., [sm / um] } から，ある [ti / vi] に対して vi = uj であるような [sj / uj] をすべて取り除いた集合を表すものと する．

• 任意の同時置換 θ ， μ ， ν に対して，結合律 θ ・ (μ ・ ν) = (θ ・ μ) ・ ν

が成り立つ．

33

節形論理：単一化

• 表現の集合 S と置換 θ に対して， Sθ が単元集合であ るとき， θ を S の単一化子と呼ぶ．また単一化子が存 在するとき， S は単一化可能であるという．

• μ は S の単一化子であり，かつ任意の単一化子 θ に 対して，ある置換 ν が存在して θ= μ ・ ν が成り立つとす る．このとき μ を S の最汎単一化子（ most general

unifier; mgu ）と呼ぶ．

• mgu は一般に複数存在するが， μ と ν がともに S の

mgu だとすると，ある θ と δ が存在して μ ・ θ = ν かつ ν ・

δ = μ が成り立つ．

34

節形論理：単一化アルゴリズム

1. 表現の集合 S を入力する． μ:= { }, D は S の不一致集合とす る．

2. D に変数が含まれていないとき，手続きを終了する．

3. D に含まれる他の項の部分項になっていないような変数が 存在しないとき，手続きを終了する．

4. D に含まれ， D の他の要素の部分項になっていない変数 v と

， v とは異なる D の要素 t を選び出し， μ:= (μ ・ { [t / v] }) と置く

．

5. S:= Sμ とし， D を新たに S の不一致集合とする．

6. D = { } のとき，手続きを終了する．そうでないときは 2 に戻

る．

35

節形論理：単一化定理

• 単一化アルゴリズムが， 2 ， 3 のステップで終了すると き，もとの S は単一化不可能である．

• 6 のステップで終了するとき，もとの S は単一化可能 であり，最後に得られた μ はその単一化子である．

• さらには，この μ は S の最汎単一化子である．

• 定理（単一化定理）

表現の集合 S が単一化可能であるならば， S は最汎 単一化子を持つ．

（→

UnificationAlgorithmTest1.java

36

節形論理：導出原理（述語論理）

• 節 C ， D に対して， θ と δ は変数を変数に置き換える置換であ り， Cθ と Dδ に共通の変数は現れないものとする．ある

L Cθ ∈ ， M Dδ ∈ に対して， M* は M の相補的なリテラルであり，

L ， M* が単一化可能であるとする． μ は L と M* の mgu であると する．このとき，節 ((Cθ － {L}) (Dδ ∪ ー {M}))μ を C と D からのリ ゾルベントと呼ぶ．

• 導出原理： C1 ， C2 は節集合， C は C1 と C2 からのリゾルベン トであるとする．このとき， C1 ， C2 から節 C を導出してよい．

• X に， X に含まれる任意の二つの節から導出可能なすべての

節を加えた節集合を R(X) と表す．

37

節形論理：導出原理（述語論理）

• R ⁰ (X) = X ， R ⁿ⁺¹ (X) = R(R ⁿ (X)) 　と表す．

• 任意の節集合 X = {C1, C2, ... , Cn} （ n >= 0 ）に対し て， c(X) は論理式

∀ v1... vn(( C1) ( C2) ... ( Cn)) ∀ ∨ ∧ ∨ ∧ ∧ ∨ を表すもの とする．ただし v1,..., vn は X に現れる変数のすべて であるとする．

• 定理（導出原理の完全性）

ある n>=0 に対して　□∈ R ⁿ (X) であるのは c(X) が充 足不可能であるとき，そしてそのときに限る．

（→

RefutationTest3.java

38

節形論理 : 決定可能性，半決定可能性

• 命題論理の場合は，任意の節集合 X に対してある n >= 0 が存在して，

R

(X) = R

(X) となる．つまりある段階において，それ以上導出原理に よって新しいリゾルベントを導出することができなくなるということである

．従ってこの段階で□∈ R

(X) でなければ c(X) が充足可能であるという ことが分かる．

• 従って，導出原理は命題論理に対する完全な決定手続きになっている．

• 述語論理では， c(X) が充足可能である場合，どの n >= 0 に対しても R

(X) から新しいリゾルベントが導出できる可能性がある．

• 一方 c(X) が充足不可能であるときには必ずある n >= 0 に対して

□∈ R

(X) が成り立つ．

• 従って，導出原理は述語論理に対しては，半決定的な手続きということ になる．

（→

RefutationTest4.java, RefutationTest2.java

39

論理プログラミング

• 節形論理と導出原理は，ある背景知識のもとで，ある問題に 対する解を求めるアルゴリズムに応用されている．それが

Prolog に代表される論理プログラミングである．

• 正のリテラルを一つだけ含む節をホーン節と呼ぶ．正のリテ ラルをそのホーン節の頭という．それ以外の節を本体と呼ぶ

．

• 正のリテラルを含まない節をゴール節という．

• ホーン節のみからなる有限節集合を論理プログラムと呼ぶ．

40

論理プログラミング

• 以下は論理プログラムである． X ， Y ， Z は変数，それ以外の 項は定数であるとする．

{

{ grandparent(X, Y), - parent(X, Z), - parent(Z, Y) }, { parent(john, bob) },

{ parent(john, beth) },

{ parent(jane, peter) },

{ parent(beth, tom) },

{ parent(bob, paul) }

}

41

論理プログラミング

• ユーザは質問を与えることによってこのプログラムを利用す ることができる．例えば先ほどのプログラムに，

?- grandparent(john, paul).

という質問を打ち込むと，インタプリタはゴール節 { - grandparent(john, paul) }

をプログラムに与え，導出原理を適用する．

• □が導出されたらインタプリタは yes を，そうでないときは no を出力する．

• 従ってこの場合は yes が出力される．

42

論理プログラミング

• またユーザは例えば

?- grandparent(john, W).

という質問を打ち込むこともできる．

• このときインタプリタはゴール節 { - grandparent(john, W) }

をプログラムに与え，導出原理を適用する．

• □が導出されたらインタプリタは，このゴール節に適用され たすべての同時置換に含まれる置換 [t / W] の t を出力する．

• 従ってこの場合は， tom と paul が出力される．

43

論理プログラミング

• ここで，インタプリタは

grandparent(X, Y) ← parent(X, Z), parent(Z, Y) parent(john, beth)

parent(beth, tom)

- grandparent(john, W)

から，一つには，同時置換 { [john / X], [tom / Y], [beth / Z],

[tom / W] } を施すことによって導出原理により□を導出した

．

• 従って答えの一つは tom になっていた．

• もし最初の質問が ?-grandparent(tom, W) であったらどの

ような代入によっても□は導出されないので，答えは no にな

る．

44

論理プログラミング

• このプログラムを与えられたインタプリタは

?- grandparent(john, peter)

という質問に対しては no を出力する． ゴール節 { - grandparent(john, peter) }

をこのプログラムに加えても，□が導出されないからである．

• これを，質問ではなく，説明されるべき事実として与えるとい うアイディアがある．つまり現在のプログラムに，さらにどの ようなホーン節を加えたら，与えられたゴール節から□が導 出されるかをコンピュータに推論させるのである．

• これはコンピュータによる帰納的推論（ induction ），もしくは

仮説的推論（ abduction ）であるといえる．

45

帰納論理プログラミング，仮説論理プログラミング

• この例では，ゴール節

{ - grandparent(john, peter) } に対しては，

parent(john, jane)

が一つの可能な仮説（の一つ）である．

• 論理プログラミングの枠組みを利用して，導出原理の逆演算 として，帰納的，仮説的推論を行わせるのが，帰納論理プロ グラミング（ inductive logic programming ）や，仮説論理プロ グラミング（ abductive logic programming ）と呼ばれ，近年 発展している AI の分野である．

• ALP ， ILP はエキスパート・システムや機械学習といった AI の

分野で大きな成功を収めている．

46

帰納推論の機械化，帰納論理の実現？

• ベーコンやミルなどは，帰納推論や仮説推論の方法 の定式化を試みた．

• しかし，一般的には，このような推論は，決まったルー ルに基くような論理の問題ではなく，科学的に重要な 法則の発見は科学者の直観によるしかないという見 解が強い．

• 一方 Gillies (1996) は ILP に代表される機械学習シス

テムは，帰納的推論を機械化した成功例であり，歴史

上初めての帰納論理の体系の実現であると評価して

いる．

47

ILP のさらなる応用

• ILP は現在も目覚しい発展を続けている．例えば，次のよう

な研究が現在行われている．

– 述語論理と確率論の統合への応用．

– 遺伝的アルゴリズムの導入．

– 倫理的判断を行うエキスパート・システムへの応用．

• こういったことが，論理や計算の哲学に対するどのようなイン

パクトを持つのかについての判断は，今後の発展を待ちた

い．

48

文献

• Carrol, Lewis (2005).

• Kowalski, R. (1979). Logic for Problem Solving, Elsevier North Holland, Inc. （1992，浦昭二

•

(2002).

,

.

• Gillies, D. (1996). Artificial Intelligence and Scientific Method, Oxford University Press.

• Muggleton, S. (1992). `Inductive Logic Programming', in Muggleton (Ed.), in Inductive Logic Programming, Academic Press (pp. 3-27).

• Muggleton, S. & Buntine, W. (1992). `Machine Invention of First-order Predicates by

Inverting Resolution', in Muggleton (Ed.), Inductive Logic Programming, Academic Press (pp. 261-280).

•

(2005).

• Robinson, J. A. (1965). `A Machine-oriented Logic Based on the Resolution Principle', in Journal of the Association for Computing Machinery, 12, no. 1, (pp. 23-41).

• Terese (2003). Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science 55.

•

•

(2005).

Java

49

付録）　形式的体系 Measures

• 項：

1. ーは Measures の項である．

2. X が Measures の項であるとき， X○ は Measures の項である．

• 従って，ー，－○，ー○○，ー○○○等が Measures の項である．

• 式：　 X ， Y が Measures の項であるとき，

X ｜ Y

は Mesures の式である．

50

形式的体系 Measures

• 公理： ー｜ー

• 導出規則 1 ：　ー○ ⁿ | ー　から　 ー○ ⁿ⁺¹ | ー　を導出し て良い．

• 導出規則 2 ：　ー○ ⁿ | ー○ ^m 　から　 ー○ ⁿ | ー○ ^m+n 　 を導出して良い．

ただし任意の n>0 に対して「 ○ ⁿ 」は○を n 個並べた

記号列を表す．

51

形式的体系 Measures

• 以下は Measures における証明である 1. ー｜ー

2. ー○｜－

3. ー○○｜－

4. ー○○○｜－

5. ー○○○｜－○○○

6. ー○○○｜－○○○○○○

7. ー○○○｜－○○○○○○○○○

52

形式的体系 Measures

• Measures に関して次の性質が成り立つ．

1. ー○ ⁿ | ー○ ^m が Measures の定理ならば， n は m の約数．

2. n が m の約数ならば， ー○ ⁿ | ー○ ^m は Measures の定理．

• 1 は， Measures が自然数（ 0 を含む）上の約数関係

に対して健全であることを， 2 は完全であることを述

べている．

53

形式的体系 Measures

• Measures の健全性と完全性が示されたならば，こ

の体系が決定可能であることは容易に示される．

• 実際，任意の式に対して｜の左に現れる○の数と右 に現れる○の数を数え，前者が後者の約数になって いれば，その式は定理である．そうでなければ，そ の式は定理ではない．

• また任意の Measures の定理に対して，その証明を 構成する手続きも容易に考えられる．

• Measures に対しては，その定理を自動的に証明す

るプログラムが書ける．

54

形式的体系 Measures

• ー○ ⁿ ｜－○ ^kn を証明する手続き

1. 　まず導出規則 1 を n 回適用する．すると ー○ ⁿ ｜－ が得られる．

2. 　次に導出規則 2 を k 回適用する．すると ー ○ ⁿ ｜－○ ^kn が得られる．

（→

Measures.java

55

付録）　「シラキュース問題」

• 次の手続きを「シラキュース・アルゴリズム」と呼ぶ．

1. 正整数 n を受け取る．

2. n = 1 ならば停止する．そうでなければ 3 行目に行く．

3. n が偶数ならば 4 行目，そうでなければ 5 行目に行く．

4. n:= n / 2 として 2 行目に行く．

5. n:= 3*n + 1 として 4 行目に行く．

• この計算では， n の値（メモリ）と，いま実行している命令が 何行目であるかということ（内部状態という）がシステムの 状態を決定する．

(→SyracuseProblem.java)

56

「シラキュース問題」

n = 1 ? input (n)

halt

Is n even?

n:=3n+1

n:=n / 2 true

false

true false

初期状態

停止状態

メモリの状態が

n

内部状態がボックスによって 表わされる．

停止した時には常に

n = 1.

57

「シラキュース問題」

input (n:= 7)

 n:= 3*11 + 1 = 34

 n:= 34/2 = 17

 n:= 3*17 + 1 = 52

 n:= 52/2 = 26

 n:= 26/2 = 13

 n:= 3*13 + 1 = 40

 n:= 40/2 = 20

 　n:= 20/2 = 10

 　n:= 10/2 = 5

 　n:= 3*5 + 1 = 16

 　n:= 16/2 = 8

 　n:= 8/2 = 4

 　n:= 4/2 = 2

 　n:= 2/2 = 1

 　halt.

この計算では正規形は数

1

1

1