余論理式，再帰型，循環的言語

.

. . . .

. . 余論理式，再帰型，循環的言語

久木田水生

[email protected]

科学哲学コロキアム

2011

7

30

背景

:

Greg Restall

.

目的

:

Restall

か，どのような点で有用であるかを考える．

余論理式のアイディアを改良する．

余論理式に対してどのような証明論が適切であるかを考える．

余論理式と自己言及的言明の関係について論じる．

概要

. . ¹ .

. . ² .

. . ³ .

. . ⁴ .

. . ⁵ .

. . ¹ .

. . ² .

. . ³ .

. . ⁴ .

. . ⁵ .

ストリーム

余論理式は計算機科学におけるストリームの概念の応用である．

ストリームに関しては次の三つの観点で捉えることが出来る．

集合論的（静的）

計算的（動的）

圏論的（両方）

ストリーム：集合論的観点から

. Definition .

.

. . . .

. .

A

Stream(A) = A ^ω (= Q

n ∈ ω A = (ω → A)).

Stream(A)

Stream(A) ' A × Stream(A)

従って任意の

S ∈ Stream(A)

a ∈ A

S ⁰ ∈ A

(a, S ⁰ )

a

S

S ⁰

S

head(S )

tail(S)

S

||zzz zzz zz

## G

G G G G G G G G

hS tS

{{xxx xxx xxx

## G

G G G G G G G G

htS t ² S

{{www www ww

""

F F F F F F F F

ht ² S t ³ S

||xxx xxx xx

""

D D D D D D D D

ht ³ S t ⁴ S

ストリームの余帰納的定義

Stream(A)

. ^.

. ^{S ∈ Stream(A)}

^{a ∈ A}

^{S 0 ∈ Stream(A)}

s = (a, S ⁰ )

. ^.

.

^X

^{x ∈ X}

^{a ∈ A}

^{x 0 ∈ X}

x = (a, x ⁰ )

X ⊆ Stream(A)

参考：帰納的定義

データ型

A

List(A)

List(A)

. ^.

. ^{() ∈ List(A)}

. ^.

. ^a ∈ A

L ∈ List(A)

(a, L) ∈ List (A)

. ^.

.

^X

^{() ∈ X}

^{a ∈ A}

x ∈ X

(a, x) ∈ X

List(A) ⊆ X

ストリームの定義

A

例えば

ones = (1 : ones)

によって

(1, 1, 1, . . . )

例

名前 定義 出力

ones (1:ones) 1, 1, 1, 1, 1, 1, . . . nats (0:(s+ ones nats)) 0, 1, 2, 3, 4, 5, . . . facts (1:(s* (tail nats) facts)) 1, 1, 2, 6, 24, 120, . . .

Fibs (1:1:(s+ Fibs (tail Fibs))) 1, 1, 2, 3, 5, 8, . . .

ただし

s+

s*

s* ^{*0 //}

*1

66

66 66 66 66

66 66 s+ ^{+0 //}

+1

55

55 55 55 55

55 55 ones

1

facts

1

LL

nats

0

KK

ストリーム：計算的観点から

. Definition .

.

. . . .

.

.

データ型

A

M = (Q, q 0 , δ)

Q

q 0 ∈ Q

δ : Q → A × Q

q

a

q ⁰

δ(q) = h a, q ⁰ i

q

M

a

状態

q ⁰

a

q ⁰

q

head

tail

q 0

head

tail

M

head

tail

注意

A

M = (Q , q ₀ , δ)

q ∈ Q

M ⁰ = (Q, q, δ)

逆に

A

M = (Q, q ₀ , δ)

a ∈ A

M ⁰ = (Q ∪ p, p, δ _{p 7→ (a,q}

₎ )

A

p ∈ / Q

δ _{p 7→ (a,q}

₎

δ _{p 7→ (a,q}

₎ (q) =

½ (a, q ₀ ) q = p

δ(q)

このような

M ⁰

(a, M )

M M ⁰

例

データ型として自然数

N

Q = { q } q ₀ = q δ(q) = (1, q )

によって定義される

M = (Q, q 0 , δ)

1, 1, 1, 1, 1, . . .

ストリーム：圏論的観点から

. Definition .

.

.

.

.

Stream(A)

F _A

F _A -CoAlg

ただし

F _A : Set → Set

F A X = A × X , F A f = h1 A , f i

によって定義される関手であり，

F _A -CoAlg

対象：

Set

f : X → F _A X

射：

dom(f )

dom(g )

α

g ◦ α = F _A α ◦ f

f

g

具体的に言えば

Stream(A) = h head, tail i : A ^ω → A × A ^ω

Stream(A)

る．たとえば

ones: Stream(ω) ω × ω ^{ω oo h id}

^{,[[ h 1,! i ]] i} ω × 1

ω ^ω

h head,tail i

OO

[[ h 1,! i ]] 1

oo

h 1,! i

OO

interleave: Stream(A) × Stream(A) → Stream(A) A × A ^{ω oo h id}

^{,[[φ]] i} A × (A ^ω × A ^ω )

A ^ω

h head,tail i

OO

A ^ω × A ^ω

[[φ]]

oo

φ

OO

ただし

φ = h head ◦ fst, h snd, tail ◦ fst ii .

余論理式（ cf. Restall, forthcoming ）

n

Σ _n

n ≥ 0

n = 0

Σ = `

n≥0 Σ n

. Definition .

.

. . . .

.

.

Σ

T _Σ

. ^.

. ^γ ∈ T _Σ

σ ∈ Σ n

γ 1 , γ 2 , . . . , γ n ∈ T _Σ

γ = h σ : h γ ₁ , γ ₂ , . . . , γ _n ii

. ^.

.

^X

^{x ∈ X}

^{σ ∈ Σ n}

^{x 1 , x 2 , . . . , x n ∈ X}

x = h σ : h x ₁ , x ₂ , . . . , x _n ii

X ⊆ T _Σ

γ = h σ : h γ ₁ , γ ₂ , . . . , γ _n ii

σ

γ

γ _k (0 ≤ k ≤ n)

γ

head(γ), tail k (γ )

余論理式

直観的には余論理式は，各ノードが

S

Σ

0

余論理式：別な定義

. Definition .

.

. . . .

.

.

余論理式はマシン

M = (Q, q ₀ , δ)

Q

q ₀

δ : Q → Σ × `

n ≥ 0 Q ⁿ

q

(σ, p 1 , p 2 , . . . , p n )

ただしここで

σ ∈ Σ _n

p _k ∈ Q

δ(q ₀ ) = (σ, p ₁ , p ₂ , . . . , p _n )

σ

M

p _k (1 ≤ k ≤ n)

head(M), tail k (M)

M

Q

余論理式：別の定義

. Definition .

.

. . . .

.

.

余論理式は

F Σ -CoAlg

F Σ : Set → Set

F _Σ X = a

n ≥ 0

Σ × X ⁿ F _Σ f = a

n ≥ 0

h id _Σ , f ⁿ i

`

n ≥ 0 h head, tail 1 , . . . , tail n i : `

n ≥ 0 (T _Σ → Σ × T _Σ ⁿ )

T _Σ

.

例

→

∧

2

Q = { ? } , q ₀ = ?, δ(?) = h→ , ?, ? i .

Q = { ], \ } , q ₀ = ], δ(]) = h→ , \, \ i , δ(\) = h∧ , ], ] i .

? → ? の構文木

→

}}zzz zzz zz

!! D

D D D D D D D

? ?

? → ? の構文木

→

zzuuu uuu uuu

$$ I

I I I I I I I I

? → ? ? → ?

? → ? の構文木

→

||yyy yyy yy

""

E E E E E E E E

→

wwnnnn nnnn nnnn

→

'' P P P P P P P P P P P P

? ? ? ?

? → ? の構文木

→

zzuuu uuu uuu

$$ I

I I I I I I I I

→

uullll llll llll ll

→

)) R R R R R R R R R R R R R R

? → ? ? → ? ? → ? ? → ?

? → ? の構文木

→

||yyy yyy yy

""

E E E E E E E E

→

vvmmmm mmmm mmmm m

→

(( Q Q Q Q Q Q Q Q Q Q Q Q Q

→

}}{{{ {{{ {{

→

}}{{{ {{{ {{

→

!! C C C C C C C C →

!! C C C C C C C C

? ? ? ? ? ? ? ?

? → ? を表すマシンの状態遷移図

?

→

%%

yy →

. Definition .

.

. . . .

.

.

R ⊆ T _Σ × T _Σ

T _Σ

bisimulation

M , M ⁰ ∈ T _Σ

M R M ⁰ ⇒

½ head(M) = head(M ⁰ ) tail n ( M )Rtail n ( M ⁰ )

余論理式

M, M ⁰ ∈ T Σ

bisimilar

bisimulation R

M R M ⁰

bisimilar

れらの振る舞いを観察することによって区別することが出来ない

.

例

次の二つの余論理式は

bisimilar

M = ( { q } , q, δ)

δ(q) = ( → , q, q)

M ⁰ = ( { q ⁰ , q ⁰⁰ } , q ⁰ , δ ⁰ )

δ ⁰ (q ⁰ ) = ( → , q ⁰⁰ , q ⁰⁰ )

δ ⁰ (q ⁰⁰ ) = ( → , q ⁰ , q ⁰ )

論理式と余論理式の対は，同種の双対的な概念の一例である．

代数

⇐⇒

⇐⇒

⇐⇒

⇐⇒

従って余論理式について考えるのは自然なステップであるように思わ れる．

しかし以下の質問もまた自然である．

それは何らかの意味を持つのか？

それは何らかの文脈で有用なのか？

—

余論理式の一部は再帰型と見なすことが出来る．

それらは論理と計算の間のギャップを埋めることが出来る

.

. . ¹ .

. . ² .

. . ³ .

. . ⁴ .

. . ⁵ .

Curry-Howard 同型

論理 型付き

λ

⇐⇒

λ

⇐⇒

⇐⇒

etc.

命題

⇐⇒

→ -I ( ∀ -I) ⇐⇒

→ -E ( ∀ -E) ⇐⇒

証明

⇐⇒

正規化

⇐⇒

etc.

Howard Curry 靴店

論理と計算の違い

かくして次のクリシェが生まれた：

「証明を構成することはプログラムを書くことである」

しかしこの逆は真ではない：

「プログラムを書くことは証明を構成することではない」

Cf. Nordstr¨ om et al. Programming in Martin-L¨ of Type Theory:

型理論においては，正しいことが証明できるプログラムを開発 するとともに，プログラミングのタスクの仕様を書くことが出 来る．従って型理論はプログラミング言語以上のものであって，

プログラミング言語ではなく，むしろ

LCF

PL/CV

ラムダ・キューブ

λω λC

λ2 y y y y y y y y

λP 2 w w w w w w w w w

λω λP ω

λ → z z z z z z z z

λP

w w

w w

w w

w w

一方，実際のプログラミング言語のほとんどは強正規性を持たない．

停止しないプログラムの例：

while (now.isToday()) {

System.out.print( );

}

この

while

以下の定義がどのように働くか考えよう：

f (n) =

½ 1 if n = 0

n ∗ f (n − 1) otherwise

ここで行っているのは以下のように定義されるファンクショナル

Φ : (N + N) → (N + N)

れる：

Φ(f )(n) =

½ 1 if n = 0

n ∗ f (n − 1) otherwise

N + N

しかしこのようなファンクショナルの最小不動点はどのようにして求め

Curry の不動点コンビネータ

. Definition .

.

. . . .

.

.

x ∈ A

f : A → A

f (x) = x

F : (A → A) → A

f : A → A

f (F (f )) = F (f )

Y

λy.(λx.y(xx))(λx.y (xx ))

M

YM → β M((λx.M (xx ))(λx.M (xx )))

→ β M(M((λx.M (xx ))(λx.M (xx ))))

M (YM ) → β M(M((λx.M (xx ))(λx.M (xx ))))

不動点演算子を使った階乗の定義（

Scheme

(define Y

(lambda (f)

((lambda (x) (f (x x))) (lambda (x) (f (x x)))))) (define (F f)

(lambda (n)

(if (= n 0) 1

(* n (f (- n 1))))))) ((Y F) 5)

>> 120

以下の事実に注意

. Fact

. .

. . . .

.

.

Y

β

λ?

6` λ? Y : σ

Y

λ→

Turing

従ってそのようなメカニズムが論理（型付き

λ

. . ¹ .

. . ² .

. . ³ .

. . ⁴ .

. . ⁵ .

反射的領域

. Definition .

.

. . . .

.

.

型

D

φ : D → (D → D)

ψ : (D → D) → D

φ ◦ ψ = id _{D → D}

が成り立つときである．ただしここで

id _D→D : (D → D) → (D → D)

(D → D)

反射的領域

. Definition .

.

. . . .

.

.

反射的領域に対する規則：

M : D → D

ψM : D ^fold

M : D

φM : D → D ^unfold M : D → D

φ(ψM ) = M : D → D reflexive identity

Y コンビネータの構成

Y ombinator

y:D!D

x:D

unfold

x:D!D x:D

xx:D

y(xx):D

x D

:y(xx):D!D

y:D!D

x:D

unfold

x:D!D x:D

xx:D

y(xx):D

x D

:y(xx):D!D

fold

(x D

:y(xx)):D

(x D

:y(xx))( (x D

:y(xx))):D

y D!D

:(x D

:y(xx))( (x D

:y(xx))):(D!D)!D

久木田水生 ([email protected]) 余論理式，再帰型，循環的言語 科学哲学コロキアム 44 / 81

反射的領域はより一般的な再帰型の概念によって定義することが出来る．

再帰型とは

rec t.τ

という形式の型表現である．ただし

τ

t

大雑把に言って

rec t.τ

rec t.τ = τ [rec t.τ /t]

反射的領域

D

rec t.t → t

.

型表現

. Definition .

.

. . . .

.

.

型変数の集合

TVar

t

TExp

τ ::= t | (σ, τ ₁ , . . . , τ _n ) | rec t.τ

σ ∈ Σ _n

. Definition .

. .

型表現が余論理式的であるのは，それが閉じていてかつ

rec t.t ⁰

0

有限の余論理式を余論理式的型表現に変換させる関数

F : T fin

Σ → TExp ₀

有限の余論理式

M = h Q, q ₀ , δ i

Q = { q _k : 0 ≤ k ≤ n }

S k = (σ k , t _i(k,1) , . . . , t _i(k,m

₎ )

とする．ただしここで

δ(q _k ) = (σ _k , q _i(k,1) , . . . , q _{i (k,m}

₎ )

0 ≤ k ≤ n, 0 ≤ j ≤ m _k

t _{i(k ,j )}

S ˆ _k (0 ≤ k ≤ n)

S ˆ _n = rec t _n .S _n

S ˆ _k−1 = rec t _k−1 .(S _{k −1} [ˆ S n /t n ] . . . [ˆ S _k /t _k ])

S ˆ 0

F M

例えば次の余論理式

M = h Q, q ₀ , δ i

Q = { q ₀ , q ₁ , q ₃ } , δ(q ₀ ) = h→ , q ₁ , q ₂ i , δ(q 1 ) = h∧ , q 2 , q 0 i , δ(q 2 ) = h∨, q 0 , q 1 i.

F

M

rec t ₀ .(rec t ₁ .(rec t ₂ .(t ₀ ∨ t ₁ ) ∧ t ₀ ) → rec t ₂ .(t ₀ ∨ rec t ₁ .(rec t ₂ .(t ₀ ∨ t ₁ ) ∧ t ₀ )))

S 2 = t 0 ∨ t 1

S 1 = t 2 ∧ t 0

S ₀ = t ₁ → t ₂

S ˆ ₂ = rec t ₂ .(t ₀ ∨ t ₁ ) S 1 [ˆ S 2 /t 2 ] = rec t 2 .(t 0 ∨ t 1 ) ∧ t 0

S 0 [ˆ S 2 /t 2 ] = t 1 → rec t 2 .(t 0 ∨ t 1 )

S ˆ ₁ = rec t ₁ .(rec t ₂ .(t ₀ ∨ t ₁ ) ∧ t ₀ ) S ₀ [ˆ S ₂ /t ₂ ][ˆ S ₁ /t ₁ ] = rec t ₁ .(rec t ₂ .(t ₀ ∨ t ₁ ) ∧ t ₀ ) →

rec t 2 .(t 0 ∨ rec t 1 .(rec t 2 .(t 0 ∨ t 1 ) ∧ t 0 ))

注意

S _k

S ˆ 0

S ₂

S ₁

rec t ₀ .(rec t ₁ .(rec t ₂ .(t ₀ ∨ rec t ₁ .(t ₂ ∧ t ₀ )) ∧ t ₀ ) → rec t ₂ .(t ₀ ∨ rec t ₁ .(t ₂ ∧ t ₀ )))

rec t 0 .(rec t 1 .(rec t 2 .(t 0 ∨t 1 )∧t 0 ) → rec t 2 .(t 0 ∨rec t 1 .(rec t 2 .(t 0 ∨t 1 )∧t 0 )))

余論理式的型表現を有限の余論理式に変換する手続き

G : TExp ₀ → T fin

Σ

を定義しよう．

∗ : TExp ₀ → `

n ≥ 0 Σ × (TExp ₀ ) ⁿ

(σ, τ ₁ , . . . , τ _n ) ^∗ = (σ, τ ₁ , . . . , τ _n )

(rec t.τ ) ^∗ = (τ [rec t.τ /t]) ^∗

T Σ

[[ ∗ ]] : TExp ₀ → T _Σ

Σ × T _Σ × T _Σ ^{oo h id}

^{,[[ ∗ ]],[[ ∗ ]] i} Σ × TExp ₀ × TExp ₀

T _Σ

h head,tail

,tail

i

OO

TExp ₀

[[ ∗ ]]

oo

∗

OO

この

[[∗]]

G

. Lemma . .

. . . .

.

.

S 0 , S 1 , S 2

t 0 , t 1 , t 3

rec

θ

[rec t _i .S _i θ ⁰ /t _i ]

G (rec t 0 .S 0 [rec t 1 .S 1 θ 1 /t 1 ][rec t 2 .S 2 θ 2 /t 2 ])

G (rec t 0 .S 0 [rec t 1 .S 1 θ ₁ ⁰ /t 1 ][rec t 2 .S 2 θ ₂ ⁰ /t 2 ])

bisimilar

証明

.

¤

この結果によって上記の注意が正当化される．

. Proposition .

.

. . . .

. .

M ∈ T fin _Σ

M

GF ( M )

bisimilar

証明

.

¤

上記の結果に基づいて，私たちは余論理式を

T fin

Σ

この制限には以下のような利点がある：

有限の手段で捉えられないような余論理式を排除する．

計算とプログラミング言語との関わりで重要性を持つ余論理式のみ を考えることが出来る．

既に存在している意味論と証明システムを利用できる．

. . ¹ .

. . ² .

. . ³ .

. . ⁴ .

. . ⁵ .

Abramsky “Domain theory in logical form” (1991)

「論理的解釈」を定式化している．

この言語には，

→

×

⊕

P

Plotkin

rec

私たちはこの言語を余論理式の証明のために利用することが出来る．

証明体系

単純性のために

Σ = {→ , ∧}

命題論理の自然演繹に加えて，各余論理式

M = h Q, q 0 , δ i

M : δ(q)

fold ^M _q (M ) : q rec-I M : q

unfold ^M _q (M ) : δ(q) rec-E

δ(q)

(σ, q ⁰ , q ⁰⁰ )

δ(q) = (σ, q ⁰ , q ⁰⁰ ).

M

例

Q = { q 0 , q 1 , q 2 }

δ(q ₀ ) = q ₁ → q ₂ , δ(q ₁ ) = q ₂ → q ₀ , δ(q ₂ ) = q ₀ → q ₁ ,

(x:q

1 )

!-I

y:x:q

0

!q

1

re-I

fold(y:x):q

2

!-I

x:fold (y:x):q

1

!q

2

re-I

fold(x:fold (y:x)):q

0

久木田水生 ([email protected]) 余論理式，再帰型，循環的言語 科学哲学コロキアム 60 / 81

例

Curry

Q = { q 0 , q 1 }

δ(q ₀ ) = q ₀ ∧ q ₀ , δ(q ₁ ) = q ₁ → q ₀

(x:q

1 )

re-E

unfold

q1 (x):q

1

!q

0

(x:q

1 )

unfold

q1 (x)x:q

0

x

x q1

:(unfold

q

1 (x)x):q

1

!q

0

(x:q

1 )

re-E

unfold

q1 (x):q

1

!q

0

(x:q

1 )

unfold

q1 (x)x:q

0

x

x q1

:(unfold

q1 (x)x):q

1

!q

0

re-I

unfold

q

1 (x

q1

:(unfold

q

1

(x)x)):q

1

(x q

1

:(unfold

q

1

(x)x))(unfold

q

1 (x

q

1

:(unfold

q

1

(x)x))):q

0

久木田水生 ([email protected]) 余論理式，再帰型，循環的言語 科学哲学コロキアム 61 / 81

注意

この体系は有限の余論理式が自己言及的な文として理解され得ると いうことを示唆する．

証明に際しては，証明の外で余論理式を特定する必要がある．その ためこの体系は純粋に構文論的でないように思われるかもしれない．

しかし有限の余論理式に関する限り，この特定は構文論的な仕方で 出来る（それは

let

証明の中には正規化できないものがある．

余論理式の間の

bisimulation

. . ¹ .

. . ² .

. . ³ .

. . ⁴ .

. . ⁵ .

循環的言語

Leitgeb and Hieke “Circular languages” (2004)

と「自己包含的表現」を許すような言語に対する公理系を与えて いる．

彼らはここで循環的でない言語の公理系

AppI

系

AppCI

余論理式は

AppCI

公理系 AppI

AppI

アトムの集合

{ a _i } i ∈ Ind

2

seq

app

1

atomic

object

formula

を持つ．直観的に言って

seq

app

object

formula

app

公理系 AppI

Identity Axioms:

Seq-Identity:

∀x, y, u, v(seq(x, y ) = seq(u, v) → x = u ∧ y = v ).

App-Identity:

∀ x, y, u, v(app(x , y) = app(u, v) → x = u ∧ y = v).

公理系 AppI

Categorization Axioms:

Atomic-Disjoint-Seq:

∀ x(atomic(x) → ¬∃ y , z (x = seq(y, z ))).

Atomic-Disjoint-App:

∀ x(atomic(x) → ¬∃ y , z (x = app(y, z))).

Seq-Disjoint-App:

∀x, y, u, v(seq(x, y ) 6= app(u, v)).

公理系 AppI

Atomic Axiom (Scheme):

Atoms:

atomic(a _i ) ∧ a _i 6 = a _j .

公理系 AppI

Structural Axioms:

Objects:

∀ z

((atomic(z) → object(z )) ∧

∀ x, y (formula(x) ∧ object(y ) ∧ z = seq(x, y) → object(z )) ∧

∀ x, y (formula(x) ∧ object(y ) ∧ z = app(x, y ) → object(z))).

Formulas:

∀z

((atomic(z) → formula(z)) ∧

∀ x, y(formula(x) ∧ object(y) ∧ z = app(x, y ) → formula(z ))).

公理系 AppI

Induction Axiom (Scheme):

Induction:

∀ z

((atomic(z) → Φ[z]) ∧ (atomic(z ) → Ψ[z ] ∧

∀ x, y (Ψ[x] ∧ Φ[y] ∧ z = seq(x, y) → Φ[z ]) ∧

∀ x, y (Ψ[x] ∧ Φ[y] ∧ z = app(x, y ) → Φ[z ]) ∧

∀ x, y (Ψ[x] ∧ Φ[y] ∧ z = app(x, y ) → Ψ[z]))

→ ∀ z ((object(z) → Φ[z ]) ∧ (formula(z ) → Ψ[z ])).

（

Φ

Ψ

公理系 AppI

公理系

AppI

P (P)

しかし

AppI

α = P(α)

そこで帰納的な対象と式の構成についての公理を余帰納的な構成に 置き換えた公理系

AppCI

公理系 AppCI

Identity Axioms

Categorization Axioms

Atom Axiom

AppI

Structural Axioms

Structural Axioms ^∗ : Objects ^∗ :

∀ z (object(z ) → (atomic(z ) ∨

∃ x, y (formula(x) ∧ object(y ) ∧ z = seq(x, y)) ∨

∃ x, y (formula(x) ∧ object(y ) ∧ z = app(x, y )))).

Formulas ^∗ :

∀ z (formula(z) →

公理系 AppCI

Induction Axiom

Coinduction Axiom (Scheme):

Co-Induction:

∀ z

((Φ[z ] → (atomic(z ) ∨

∃ x, y (Ψ[x] ∧ Φ[y] ∧ z = seq(x, y)) ∨

∃x, y (Ψ[x] ∧ Φ[y] ∧ z = app(x, y ))))

∧ (Ψ[z] →

(atomic(z )∨

∃ x, y (Ψ[x] ∧ Φ[y] ∧ z = app(x, y )))))

→ ∀ z ((Φ[z] → object(z)) ∧ (Ψ[z ] → formula(z ))).

公理系 AppICI

AppCI

T _Σ

AppCI

AppICI

公理系 AppICI

AppICI

アトムの集合

{⊥} ∪ { a _nk : n, k ∈ N }

2

seq

app

1

atomic _⊥

atomic n , object

object _n

n ∈ N

formula

公理系 AppICI

Structural Axioms ^† : Objects ^† :

∀ z ((atomic _⊥ (z ) → object(z)) ∧

∀ x, y (formula(x) ∧ object(z ) ∧ z = seq(x, y) → object(z ))).

Objects n :

∀ z (object ₀ (z ) ↔ atomic _⊥ (z )) ∧

∀ z (object _n+1 (z ) ↔

object(z ) ∧ ∃x , y(formula(x) ∧ object _n (y ) ∧ z = seq(x, y))).

Formulas ^† :

∀ →

公理系 AppICI

Induction Axiom (Scheme) ^† : Induction ^† :

∀z

((atomic _⊥ (z ) → Φ[z ]) ∧

∀ x, y (formula(x) ∧ Φ(z ) ∧ z = seq(x, y) → Φ[z]))

→ ∀z (object(z ) → Φ(z)).

公理系 AppICI

CoInduction Axiom

Coinduction Axiom (Scheme) ^† : Co-Induction ^† :

∀ z

(Ψ[z] → (atomic ₀ (z ) ∨

∃ x, y ∃ n ∈ N(atomic n (x) ∧ Φ(y) ∧ z = app(x, y))))

→ ∀ z (Ψ[z ] → formula(z)).

AppICI のモデル

T _Σ

AppICI

さらに

T _Σ

Solution ^† :

∃ x ₁ , x ₂ , . . . , x _n

(formula(x ₁ ) ∧ · · · ∧ formula(x _n ) ∧

x 1 = f 1 [x 1 , x 2 , . . . , x n ] ∧ · · · ∧ x n = f n [x 1 , x 2 , . . . , x n ])

ただし

f 1 . . . f n ∈ FormulaTerms ^†

FormulaTerms ^†

ObjectTerms ^† /FormulaTerms ^†

. ^.

.

ObjectTerms ₁

FormulaTerms

. ^.

. ^a ⊥ ∈ ObjectTerms ₀

a _0k ∈ FormulaTerms

. ^.

. ^f ∈ FormulaTerms, o ∈ ObjectTerms n ⇒ h f , o i ∈ ObjectTerms n+1

. ^.

. ^{o ∈} ObjectTerms n ⇒ ha nk : oi ∈ FormulaTerms.

まとめ

論理学とプログラミングの間には

Curry-Howard

しかし大きなギャップもある．

それは不動点演算子のようなメカニズムを持てるかどうかという点 である．

余論理式はプログラミング言語の再帰型に対応するものであり，こ のギャップを埋めるものである．

そのようなものとして，余論理式を有限なものに制限することは理 にかなっている．

そのときある種の証明体系が余論理式にも与えることが出来る．

余論理式はまた循環的言語のモデルの一種と捉えることも出来る．