.
.

.

.
..

.

余論理式，再帰型，循環的言語
久木田水生
minao.kukita@gmail.com

科学哲学コロキアム
2011 年 7 月 30 日

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

1 / 81

背景:

Greg Restall の余論理式.
論理と計算の対応とギャップ
目的:

Restall の余論理式のアイディアを紹介し，それが直観的に何であるか，どのような点で有用であるかを考える．
余論理式のアイディアを改良する．
余論理式に対してどのような証明論が適切であるかを考える．
余論理式と自己言及的言明の関係について論じる．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

2 / 81

概要.
. .1 余論理式.
. .2 論理と計算の関係.
. .3 再帰型としての余論理式.
. .4 証明体系.
. .5 循環的言語としての余論理式

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

3 / 81.
. .1 余論理式.
. .2 論理と計算の関係.
. .3 再帰型としての余論理式.
. .4 証明体系.
. .5 循環的言語としての余論理式

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

4 / 81

ストリーム

余論理式は計算機科学におけるストリームの概念の応用である．
ストリームに関しては次の三つの観点で捉えることが出来る．
集合論的（静的）
計算的（動的）
圏論的（両方）久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

5 / 81

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

.
.

.

.
Deﬁnition
..
Q
ω (=
集合
A
が与えられたとき，Stream(A)=An∈ω A = (ω → A)).
.
..
Stream(A) は次の等式を満たすことに注意せよ．
Stream(A) ' A × Stream(A)

従って任意の S ∈ Stream(A) は a ∈ A と S 0 ∈ A のペア (a, S 0 ) として表すことが出来る．このとき a を S のヘッド，S 0 を S のテールと呼び，それぞれ head(S)，tail(S) によって表す．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

6 / 81

hS

S GG
GG
zz
z
GG
zz
GG
z
z
G#
|z

htS

x
xx
xx
x
x
{xx

tS GG

ht 2 S

GG
GG
GG
G#

ww
ww
w
w
{w
w

t 2S F

FF
FF
FF
F"

x
xx
xx
x
x
|x

ht 3 Sh = head
久木田水生 (minao.kukita@gmail.com)

t 3S D

DD
DD
DD
D"

t 4S

t = tail

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

科学哲学コロキアム

7 / 81

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

Stream(A) は次のようにも定義される．
.1. S ∈ Stream(A) ならばある a ∈ A と S 0 ∈ Stream(A) に対し.
て s = (a, S 0 )．
.
.. 任意の集合 X と x 0∈ X に対して，ある a ∈ A と x 0 ∈ X が2存在して x = (a, x ) が成り立つならば X ⊆ Stream(A)．

このような定義を余帰納的定義と呼ぶ．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

8 / 81

参考：帰納的定義

データ型 A 上のリストの集合 List(A) の帰納的定義と比較しよう．
List(A) は次のように定義される．
.1. () ∈ List(A)．
.. a ∈ A，L ∈ List(A) ならば (a, L) ∈ List(A)．
2.3. 任意の集合 X に対して，() ∈ X でありかつすべての a ∈ Aとすべての x ∈ X に対して (a, x) ∈ X が成り立つならばList(A) ⊆ X ．

.
.
.

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

9 / 81

ストリームの定義

A 上のストリームを定義するにはヘッドとテールを指定すれば良い．
例えば
ones = (1 : ones)
によって (1, 1, 1, . . . ) というストリームを定義できる．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

10 / 81

例

名前
ones
nats
facts
Fibs

定義
(1:ones)(0:(s+ ones nats))(1:(s* (tail nats) facts))(1:1:(s+ Fibs (tail Fibs)))

出力1, 1, 1, 1, 1, 1, . . .
0, 1, 2, 3, 4, 5, . . .
1, 1, 2, 6, 24, 120, . . .
1, 1, 2, 3, 5, 8, . . .

ただし s+と s*はそれぞれ，二つのストリームの対応する構成要素同士を加えるあるいは掛けた値のストリームを出力する演算．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

11 / 81

1

s*
L 6

*0

66
66
66
66*1
66
66
1
6

facts

久木田水生 (minao.kukita@gmail.com)

+0
/ s+
K 55
55
55
55+1
55
55
55
0



/ onesnats

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

科学哲学コロキアム

12 / 81ストリーム：計算的観点から.
Deﬁnition.
..
データ型 A 上のストリームとは，マシン M = (Q, q0 , δ) である．ただしここで：Q はマシンの内部状態の集合，
q0 ∈ Q は初期状態，
δ : Q → A × Q は状態 q から原子データ a と状態 q 0 のペアへの関数．
.

.

.
..

δ(q) = ha, q 0 i が意味するのは，状態 q にある M は a を出力して，次の状態 q 0 に移行するということである．このとき a と q 0 をそれぞれ q の
head，tail と呼ぶ．特に q0 の head と tail を，M の head と tail と呼ぶ．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

13 / 81注意
A 上の任意のストリーム M = (Q, q0 , δ) と q ∈ Q に対して，
M0 = (Q, q, δ) もまたストリームである．
逆に A 上の任意のストリーム M = (Q, q0 , δ) と a ∈ A に対して，
M0 = (Q ∪ p, p, δp7→(a,q0 ) ) もまた A 上のストリームである．ただし
ここで p ∈/ Q ，δp7→(a,q0 ) は½
δp7→(a,q0 ) (q) =(a, q0 ) q = p のとき
δ(q)それ以外のときによって定義される関数．
このような M0 を (a, M) と表すことにしよう．
従って私たちは任意のストリーム M = (Q, q0 , δ) を (a : M0 ) として表すことが出来る．ただしここで δ(q0 ) = (a, q1 )，M = (Q, q1 , δ) とする．
久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

14 / 81例

データ型として自然数 N を考える．

Q = {q}q0 = qδ(q) = (1, q)によって定義される M = (Q, q0 , δ) は 1, 1, 1, 1, 1, . . . という出力を出し続けるマシンである．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

15 / 81ストリーム：圏論的観点から.
Deﬁnition.
..
Stream(A) 終 FA 余代数，すなわち圏 FA -CoAlg における終対象である．
ただし FA : Set → Set は
FA X = A × X , FA f = h1A , f i
によって定義される関手であり，FA -CoAlg は次の対象と射からなる圏：.
..

射：dom(f ) から dom(g ) への関数 α で，g ◦ α = FA α ◦ f を満たす
ものを f から g への射とする．
.

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム.

対象：Set における関数 f : X → FA X ．

16 / 81具体的に言えば Stream(A) = hhead, taili : Aω → A × Aω ．

Stream(A) の要素や演算の多くはこの終対象への媒介射として定義でき
る．たとえば
ones: Stream(ω)ω ×O ω ω ohidω ,[[h1,!i]]i

hhead,taili

ωω o久木田水生 (minao.kukita@gmail.com)

ω ×O 1h1,!i[[h1,!i]]

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

1

科学哲学コロキアム

17 / 81interleave: Stream(A) × Stream(A) → Stream(A)A ×O Aω ohidA ,[[φ]]i

A × (Aω × Aω )O

hhead,taili

Aω o

φ

[[φ]]

Aω × Aω

ただし φ = hhead ◦ fst, hsnd, tail ◦ fstii.

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

18 / 81余論理式（cf. Restall, forthcoming）
n 項結合子の集合 Σn （n `≥ 0）が与えられているとしよう（n = 0 の場合
は原子文の集合）．Σ = n≥0 Σn とする．
.
Deﬁnition.
..
Σ 上の余論理式の集合 TΣ は以下の条件を満たす集合として定義される．
.. γ ∈ TΣ ならば，ある σ ∈ Σn と γ1 , γ2 , . . . , γn ∈ TΣ に対して
1.

γ = hσ : hγ1 , γ2 , . . . , γn ii．
..2 任意の集合 X と x ∈ X に対して，ある σ ∈ Σn と x1 , x2 , . . . , xn ∈ Xが存在して x = hσ : hx1 , x2 , . . . , xn ii が成り立つならば X ⊆ TΣ ．

γ = hσ : hγ1 , γ2 , . . . , γn ii であるとき，σ を γ のヘッド，γk (0 ≤ k ≤ n) をγ
. のテールと呼び，それぞれ head(γ), tailk (γ) によって表す．
..
.

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム.

.

19 / 81余論理式

直観的には余論理式は，各ノードが S の要素でラベル付けされた無限木である．ただし各ノードが持つ子ノードの個数はそのノードがラベルとして持つ結合子のアリティに等しい．

Σ にはアリティ0 の結合子（つまり原子式）も含まれるため，余論理式は有限木である場合もある．このとき余論理式は通常の論理式である．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

20 / 81余論理式：別な定義.
Deﬁnition..
余論理式はマシン M = (Q, q0 , δ) である．ただし.

Q は状態の集合，
q0 は初期状態`
δ : Q → Σ × n≥0 Q n は状態 q から列 (σ, p1 , p2 , . . . , pn ) への関数．
ただしここで σ ∈ Σn ，pk ∈ Q

M. が有限であると言われるのは Q が有限の場合である．
..

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム.

.

δ(q0 ) = (σ, p1 , p2 , . . . , pn ) であるとき，σ を M のヘッド，pk (1 ≤ k ≤ n)
をテールと呼び，それぞれ head(M), tailk (M) によって表す．

21 / 81余論理式：別の定義.

.
Deﬁnition.
..
余論理式は FΣ -CoAlg における終対象である．ただし FΣ : Set → Set は
次のように定義される関手：aaFΣ X =
Σ × X n FΣ f =hidΣ , f n i
n≥0
n≥0
.
..
.
`
`
具体的にはこれはは n≥0 hhead, tail1 , . . . , tailn i : n≥0 (TΣ → Σ × TΣn )．
ただし TΣ は上記の無限木の集合.

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

22 / 81例→ と ∧ は 2 項結合子とする．このとき以下は余論理式である．
Q = {?}, q0 = ?, δ(?) = h→, ?, ?i.
Q = {], \}, q0 = ], δ(]) = h→, \, \i, δ(\) = h∧, ], ]i.

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

23 / 81? → ? の構文木

→D?

久木田水生 (minao.kukita@gmail.com)

zz
zz
z
z
}zz

DD
DD
DD
D!

?

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

科学哲学コロキアム

24 / 81? → ? の構文木

u
uu
uu
u
u
zuu

?→?

久木田水生 (minao.kukita@gmail.com)

→I

II
II
II
II
$

?→?

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

科学哲学コロキアム

24 / 81? → ? の構文木

→E

yy
yy
y
y
|y
y

?

→
nnn
n
n
n
nnn

wnnn

久木田水生 (minao.kukita@gmail.com)

?

EE
EE
EE
E"

→ PP


?

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

PPP
PPP
PPP
P'

?

科学哲学コロキアム

24 / 81? → ? の構文木

?→?

→
ll
lll
l
l
l
lll
ulll


久木田水生 (minao.kukita@gmail.com)

u
uu
uu
u
u
zu
u

→I

II
II
II
II
$

?→?

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

→ RR


?→?

RRR
RRR
RRR
RRR
)

?→?

科学哲学コロキアム

24 / 81? → ? の構文木

→E

yy
yy
y
y
|y
y

?
..
.

m →
mmm
m
m
m
mmm

vmmm
→
→
{
{
{{
{{
{{
{{
{
{


}{{
}{{

EE
EE
EE
E"

→ QQ


→C

QQQ
QQQ
QQQ
QQ(

CC
CC
CC
C!


→C

CC
CC
CC
C!


?

?

?

?

?

?

?

..
.

..
.

..
.

..
.

..
.

..
.

..
.

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

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

0→

久木田水生 (minao.kukita@gmail.com)

%

?

y

1

→

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

科学哲学コロキアム

25 / 81.
Deﬁnition.
..
0
R ⊆ TΣ × TΣ が TΣ 上の bisimulation であるのはすべての M, M ∈ TΣに対して½
head(M) = head(M0 )0
MRM ⇒tailn (M)Rtailn (M0 )余論理式 M, M0 ∈ TΣ が bisimilar であると言われるのは，ある
0.bisimulation R に対して MRM が成り立つときである．
..
.
bisimilar な二つの余論理式は観察に対して等しい，すなわち私たちはそれらの振る舞いを観察することによって区別することが出来ない.

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム.

が成り立つときである．

26 / 81例

次の二つの余論理式は bisimilar である．

M = ({q}, q, δ)，ただし δ(q) = (→, q, q)
M0 = ({q 0 , q 00 }, q 0 , δ 0 )，ただし δ 0 (q 0 ) = (→, q 00 , q 00 )，δ 0 (q 00 ) = (→, q 0 , q 0 )．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

27 / 81論理式と余論理式の対は，同種の双対的な概念の一例である．
代数
帰納法
リスト
論理式

⇐⇒
⇐⇒
⇐⇒
⇐⇒

余代数
余帰納法
ストリーム
余論理式

従って余論理式について考えるのは自然なステップであるように思われる．
しかし以下の質問もまた自然である．
それは何らかの意味を持つのか？
それは何らかの文脈で有用なのか？

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

28 / 81

—「然り」
余論理式の一部は再帰型と見なすことが出来る．
それらは論理と計算の間のギャップを埋めることが出来る.

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

29 / 81.
. .1 余論理式.
. .2 論理と計算の関係.
. .3 再帰型としての余論理式.
. .4 証明体系.
. .5 循環的言語としての余論理式

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

30 / 81Curry-Howard 同型

論理

型付き λ 計算命題論理
一階述語論理二階命題論理命題→-I (∀-I)→-E (∀-E)
証明
正規化

久木田水生 (minao.kukita@gmail.com)

⇐⇒
⇐⇒
⇐⇒
etc.
⇐⇒
⇐⇒
⇐⇒
⇐⇒
⇐⇒
etc.

単純型付き λ 計算
依存型理論
多態型理論
型
抽象
関数適用
項
縮約

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

科学哲学コロキアム

31 / 81

Howard Curry 靴店

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

32 / 81

論理と計算の違い
かくして次のクリシェが生まれた：「証明を構成することはプログラムを書くことである」
しかしこの逆は真ではない：「プログラムを書くことは証明を構成することではない」

Cf. Nordström et al. Programming in Martin-Löf Type Theory:
型理論においては，正しいことが証明できるプログラムを開発するとともに，プログラミングのタスクの仕様を書くことが出来る．従って型理論はプログラミング言語以上のものであって，
プログラミング言語ではなく，むしろ LCF や PL/CV のような形式化されたプログラミング論理と比較されるべきである．
久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

33 / 81ラムダ・キューブ

λ2

yy
yy
y
y
yy

z
zz
zz
z
zz

λ→

λω

ww
ww
w
ww
ww

λC

λP2

λω

λPω

λP

w
ww
ww
w
ww

これらはすべて強正規化可能であり，従って Turing 完全ではない．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

34 / 81一方，実際のプログラミング言語のほとんどは強正規性を持たない．
停止しないプログラムの例：

while (now.isToday()) {System.out.print();}
この while のような構文は特に再帰的関数の定義のために必要である．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

35 / 81以下の定義がどのように働くか考えよう：½
1
if n = 0
f (n) =n ∗ f (n − 1) otherwise
ここで行っているのは以下のように定義されるファンクショナル
Φ : (N + N) → (N + N) の最小不動点を求めることである，と言われる：½
1
if n = 0
Φ(f )(n) =n ∗ f (n − 1) otherwise
ただし N + N は自然数上の部分関数の集合．
しかしこのようなファンクショナルの最小不動点はどのようにして求められるのか？

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

36 / 81Curry の不動点コンビネータ

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

37 / 81.

.
Deﬁnition.
..
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))))∴ M(YM) =β YM.

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

38 / 81

不動点演算子を使った階乗の定義（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久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

39 / 81.
..

Y （もしくは任意の項の最小不動点を計算する何らかの他のメカニズム）を備えた λ→ は Turing 完全である．
.

.

以下の事実に注意
.
Fact
.
..
Y は β 正規形を持たない，よって強正規性を持ついかなる純粋型シ
ステム λ? に対しても 6`λ? Y : σ ．

従ってそのようなメカニズムが論理（型付き λ 計算）とプログラミング
言語を分ける大きな要因の一つである．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

40 / 81.
. .1 余論理式.
. .2 論理と計算の関係.
. .3 再帰型としての余論理式.
. .4 証明体系.
. .5 循環的言語としての余論理式

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

41 / 81反射的領域.
Deﬁnition..
型 D が反射的領域であるのは，項 φ : D → (D → D) と
ψ : (D → D) → D が存在して.

が成り立つときである．ただしここで idD→D : (D → D) → (D → D) は(D
. → D) 上の恒等関数．
..
.

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム.

φ ◦ ψ = idD→D

42 / 81反射的領域.
Deﬁnition..
反射的領域に対する規則：

.
..

fold

M:D
φM : D → D

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

久木田水生 (minao.kukita@gmail.com)

unfoldreﬂexive identity.

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

科学哲学コロキアム.

M:D→DψM : D.

43 / 81Y コンビネータの構成

Y ombinator
x:D
unfoldx : D D
x:D
unfoldy:D D
xx : Dx : D D
x:Dy (xx) : D
y:D D
xx : Dy (xx) : D
xD :y (xx) : D D
foldDx :y (xx) : D D(xD :y (xx)) : D(xD :y (xx))( (xD :y (xx))) : D
y D!D :(xD :y (xx))( (xD :y (xx))) : (D D) D

!

!

!

!

x:D

!

!

! !

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

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

rec t.τ
という形式の型表現である．ただし τ は型表現，t は型変数である．
大雑把に言って rec t.τ は次の等式を満たす型表現である．

rec t.τ = τ [rec t.τ /t]
反射的領域 D は rec t.t → t によって定義される.

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

45 / 81

型表現.
Deﬁnition.
..
型変数の集合 TVar が与えられているものとする（t によって任意の型変数を表す）．型表現の集合 TExp は以下の文法で定義される：

ただしσ ∈ Σn ．
.
..

.

.

τ ::= t | (σ, τ1 , . . . , τn ) | rec t.τ

.

.
Deﬁnition.
..
0
型表現が余論理式的であるのは，それが閉じていてかつ rec t.t という部
分表現を含まないときである（t = t 0 であるか否かを問わず）．余論理式.的な表現の集合を TExp0 によって表す．
..
.
久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

46 / 81

有限の余論理式を余論理式的型表現に変換させる関数 F : TΣﬁn → TExp0
を以下のように定義する：
有限の余論理式 M = hQ, q0 , δi を考える．Q = {qk : 0 ≤ k ≤ n} とし
よう．
Sk = (σk , ti(k,1) , . . . , ti(k,mk ) )とする．ただしここで δ(qk ) = (σk , qi(k,1) , . . . , qi(k,mk ) ) であり，各0 ≤ k ≤ n, 0 ≤ j ≤ mk に対して ti(k,j) は異なる型変数とする．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

47 / 81Ŝk (0 ≤ k ≤ n) を帰納的に以下のように定義する：
Ŝn = rec tn .Sn
Ŝk−1 = rec tk−1 .(Sk−1 [Ŝn /tn ] . . . [Ŝk /tk ])Ŝ0 を F M の値とする．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

48 / 81例えば次の余論理式 M = hQ, q0 , δi を考えよう：

Q = {q0 , q1 , q3 },δ(q0 ) = h→, q1 , q2 i,δ(q1 ) = h∧, q2 , q0 i,
δ(q2 ) = h∨, q0 , q1 i.
F を M に適用することで，次が得られる：
rec t0 .(rec t1 .(rec t2 .(t0 ∨t1 )∧t0 ) → rec t2 .(t0 ∨rec t1 .(rec t2 .(t0 ∨t1 )∧t0 )))久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

49 / 81S2 = t0 ∨ t1
S1 = t2 ∧ t0
S0 = t1 → t2Ŝ2 = rec t2 .(t0 ∨ t1 )S1 [Ŝ2 /t2 ] = rec t2 .(t0 ∨ t1 ) ∧ t0
S0 [Ŝ2 /t2 ] = t1 → rec t2 .(t0 ∨ t1 )Ŝ1 = rec t1 .(rec t2 .(t0 ∨ t1 ) ∧ t0 )S0 [Ŝ2 /t2 ][Ŝ1 /t1 ] = rec t1 .(rec t2 .(t0 ∨ t1 ) ∧ t0 ) →rec t2 .(t0 ∨ rec t1 .(rec t2 .(t0 ∨ t1 ) ∧ t0 ))Ŝ0 = rec t0 .(rec t1 .(rec t2 .(t0 ∨ t1 ) ∧ t0 ) →rec t2 .(t0 ∨ rec t1 .(rec t2 .(t0 ∨ t1 ) ∧ t0 )))久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

50 / 81

注意

Sk の順序が結果に影響するかもしれない．例えば上記の Ŝ0 の構成において，S2 ではなく S1 から変換の手続きを始めるならば結果は
rec t0 .(rec t1 .(rec t2 .(t0 ∨rec t1 .(t2 ∧t0 ))∧t0 ) → rec t2 .(t0 ∨rec t1 .(t2 ∧t0 )))であり

rec t0 .(rec t1 .(rec t2 .(t0 ∨t1 )∧t0 ) → rec t2 .(t0 ∨rec t1 .(rec t2 .(t0 ∨t1 )∧t0 )))ではない．しかしこの違いは後に述べる理由から無視できる．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

51 / 81余論理式的型表現を有限の余論理式に変換する手続き G : TExp0 → TΣﬁnを定義しよう．
`∗ : TExp0 → n≥0 Σ × (TExp0 )n を次のように定義する：(σ, τ1 , . . . , τn )∗ = (σ, τ1 , . . . , τn )(rec t.τ )∗ = (τ [rec t.τ /t])∗

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

52 / 81TΣ は終対象なので，以下のダイアグラムを可換にする[[∗]] : TExp0 → TΣ が一意的に存在する：
Σ × TΣO × TΣ ohidΣ ,[[∗]],[[∗]]i

Σ × TExp0 × TExp0
O∗

hhead,tail0 ,tail1 i

TΣ o

[[∗]]

TExp0

この [[∗]] を G と呼ぼう．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

53 / 81

.

.
Lemma
.
..
S0 , S1 , S2 は t0 , t1 , t3 のみを型変数として含む型表現であり，rec を含まないものとする．θ は（空かもしれない）連続的置換とし，その構成要素の各々は [rec ti .Si θ0 /ti ] という形式であるとする．このときG (rec t0 .S0 [rec t1 .S1 θ1 /t1 ][rec t2 .S2 θ2 /t2 ]) と00
.G (rec t0 .S0 [rec t1 .S1 θ1 /t1 ][rec t2 .S2 θ2 /t2 ]) は bisimilar である．
..
.
証明. 通常の余帰納法による．
¤この結果によって上記の注意が正当化される．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

54 / 81

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

.
.
¤

.

.
Proposition..
任意のM ∈ TΣﬁn に対して，M と GF (M) は bisimilar である．
.
..
証明. 上記の補題を用いて，余帰納法で示される．

55 / 81上記の結果に基づいて，私たちは余論理式を TΣﬁn に制限することを提案する．
この制限には以下のような利点がある：
有限の手段で捉えられないような余論理式を排除する．
計算とプログラミング言語との関わりで重要性を持つ余論理式のみを考えることが出来る．
既に存在している意味論と証明システムを利用できる．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

56 / 81.
. .1 余論理式.
. .2 論理と計算の関係.
. .3 再帰型としての余論理式.
. .4 証明体系.
. .5 循環的言語としての余論理式

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

57 / 81Abramsky “Domain theory in logical form” (1991) は領域理論の言語の「論理的解釈」を定式化している．
この言語には，→（関数空間），×（直積），⊕（融合積），P （Plotkin
冪領域），rec（再帰型）などの，領域理論における通常の型コンストラ
クタが含まれる．
私たちはこの言語を余論理式の証明のために利用することが出来る．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

58 / 81

証明体系

単純性のために Σ = {→, ∧} としよう．
命題論理の自然演繹に加えて，各余論理式 M = hQ, q0 , δi に対して次の規則を採用する：M : δ(q)
rec-I
foldM
q (M) : q

M:q
rec-E
unfoldM
q (M) : δ(q)私たちは δ(q) が (σ, q 0 , q 00 ) を表すものとして記号を乱用している．ただしここで δ(q) = (σ, q 0 , q 00 ).

M が証明されるのはその初期状態が証明されるときである．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

59 / 81例

Q = {q0 , q1 , q2 }δ(q0 ) = q1 → q2 , δ(q1 ) = q2 → q0 , δ(q2 ) = q0 → q1 ,(x : q1 )-Iy:x : q0 q1
re -I
fold(y:x) : q2-I
x:fold(y:x) : q1 q2
re -I
fold(x:fold(y:x)) : q0

! !
! !

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

60 / 81

例

Curry のパラドクス
Q = {q0 , q1 }δ(q0 ) = q0 ∧ q0 , δ(q1 ) = q1 → q0

(x : q1 )unfoldq1 (x) : q1 ! q0
(x : q1 )unfoldq1 (x)x : q0
unfoldq1 (x) : q1 ! q0
(x : q1 )xxq1 :(unfoldq1 (x)x) : q1 ! q0
unfoldq1 (x)x : q0x
re -I
unfoldq1 (xq1 :(unfoldq1 (x)x)) : q1
xq1 :(unfoldq1 (x)x) : q1 ! q0
(xq1 :(unfoldq1 (x)x))(unfold q1 (xq1 :(unfoldq1 (x)x))) : q0
(x : q1 )

re -E

re -E

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

61 / 81注意

この体系は有限の余論理式が自己言及的な文として理解され得るということを示唆する．
証明に際しては，証明の外で余論理式を特定する必要がある．そのためこの体系は純粋に構文論的でないように思われるかもしれない．
しかし有限の余論理式に関する限り，この特定は構文論的な仕方で出来る（それは let を使った構文と同じようなものである）．
証明の中には正規化できないものがある．
余論理式の間の bisimulation 関係は必ずしも証明可能を保存しない．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

62 / 81.
. .1 余論理式.
. .2 論理と計算の関係.
. .3 再帰型としての余論理式.
. .4 証明体系.
. .5 循環的言語としての余論理式

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

63 / 81

循環的言語Leitgeb and Hieke “Circular languages” (2004) は「自己適用的表現」と「自己包含的表現」を許すような言語に対する公理系を与えている．
彼らはここで循環的でない言語の公理系 AppI と循環的な言語の公理
系 AppCI を定式化する．
余論理式は AppCI のモデルになる．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

64 / 81

公理系 AppI

AppI は語彙としてアトムの集合 {ai }i∈Ind ，

2 項関数記号 seq，app，
1 項述語 atomic，object，formulaを持つ．直観的に言って seq は対象から列を形成し，app は式を対象に適用する操作を表す．これらの結果はともに object になるが，formulaになるのは app の結果だけである．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

65 / 81

公理系 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 ).

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

66 / 81

公理系 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 )).

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

67 / 81

公理系 AppI

Atomic Axiom (Scheme):
Atoms:
atomic(ai ) ∧ ai 6= aj .

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

68 / 81

公理系 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))).

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

69 / 81

公理系 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])).
（Φ と Ψ は任意の一階の式を表す）

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

70 / 81

公理系 AppI

公理系 AppI は自己適用の任意の事例――例えば P(P)――を含んでいる．
しかし AppI は自己包含の事例――例えば α = P(α)――を含まない．
そこで帰納的な対象と式の構成についての公理を余帰納的な構成に置き換えた公理系 AppCI が考えられる．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

71 / 81

公理系 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) →(atomic(z)∨∃x, y (formula(x) ∧ object(y ) ∧ z = app(x, y )))).

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

72 / 81

公理系 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))).

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

73 / 81

公理系 AppICIAppCI はそのままでは TΣ をモデルとして持たない．
AppCI を修正した公理系 AppICI を考える．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

74 / 81

公理系 AppICIAppICI は語彙としてアトムの集合 {⊥} ∪ {ank : n, k ∈ N}，

2 項関数記号 seq，app，
1 項述語 atomic⊥ ，atomicn , object，objectn （ただし n ∈ N ），formulaを持つ．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

75 / 81

公理系 AppICIStructural Axioms† :Objects† :∀z((atomic⊥ (z) → object(z))∧∀x, y (formula(x) ∧ object(z) ∧ z = seq(x, y ) → object(z))).
Objectsn :∀z(object0 (z) ↔ atomic⊥ (z))∧∀z(objectn+1 (z) ↔
object(z) ∧ ∃x, y (formula(x) ∧ objectn (y ) ∧ z = seq(x, y ))).
Formulas† :∀z(formula(z) →∃x, y ∃n ∈ N(atomicn (x) ∧ objectn (y ) ∧ z = app(x, y ))).

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

76 / 81

公理系 AppICIInduction Axiom (Scheme)† :Induction† :∀z((atomic⊥ (z) → Φ[z])∧∀x, y (formula(x) ∧ Φ(z) ∧ z = seq(x, y ) → Φ[z]))→ ∀z(object(z) → Φ(z)).

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

77 / 81

公理系 AppICICoInduction Axiom は次のものに置き換える．
Coinduction Axiom (Scheme)† :Co-Induction† :∀z(Ψ[z] →
(atomic0 (z)∨∃x, y ∃n ∈ N(atomicn (x) ∧ Φ(y ) ∧ z = app(x, y ))))→ ∀z(Ψ[z] → formula(z)).

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

78 / 81AppICI のモデル

TΣ が AppICI のモデルになることは自明．
さらに TΣ は次の公理を満たす．

Solution† :∃x1 , x2 , . . . , xn
(formula(x1 ) ∧ · · · ∧ formula(xn )∧x1 = f1 [x1 , x2 , . . . , xn ] ∧ · · · ∧ xn = fn [x1 , x2 , . . . , xn ])ただし f1 . . . fn ∈ FormulaTerms † ．FormulaTerms † は次のように定義される．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

79 / 81ObjectTerms † /FormulaTerms †... 変数は ObjectTerms1 と FormulaTerms の両方に属する．
... a⊥ ∈ ObjectTerms0，a0k ∈ FormulaTerms ．
... f ∈ FormulaTerms, o ∈ ObjectTermsn ⇒ hf , oi ∈ ObjectTermsn+1．
... o ∈ ObjectTermsn ⇒ hank : oi ∈ FormulaTerms.
1
2
3
4

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

80 / 81

まとめ

論理学とプログラミングの間には Curry-Howard 同型が成り立つが，しかし大きなギャップもある．
それは不動点演算子のようなメカニズムを持てるかどうかという点である．
余論理式はプログラミング言語の再帰型に対応するものであり，このギャップを埋めるものである．
そのようなものとして，余論理式を有限なものに制限することは理にかなっている．
そのときある種の証明体系が余論理式にも与えることが出来る．
余論理式はまた循環的言語のモデルの一種と捉えることも出来る．

久木田水生 (minao.kukita@gmail.com)

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

科学哲学コロキアム

81 / 81