ｽﾗｲﾄﾞﾀｲﾄﾙなし

世界共通言語としての
数理言語の提案
博士後期課程３年
小林俊一
求められている世界共通言語
インターネット時代の新しい言語
コンピュータ処理に適した言語
数学的処理に適していて、
曖昧性がない言語
新しい世界共通言語の提案
新しい世界共通言語として
数理言語を提案
新しい世界共通言語の提案
Internet New Esperanto
INE（イーネ）
INE言語（イーネ言語）
関数形言語
ＩＮＥの定式化の必要性
コンピュータ処理・数学的処理
に適した世界共通言語
・どの自然言語にも依存しない
・曖昧性がない
数学的に定式化
ＩＮＥの定式化
Boolean Valued Function (BVF)
集合の分割
述語論理
ＩＮＥの定式化
定式化の証明の正しさを
ワルシャワ大学で開発された
証明検証システムＭＩＺＡＲ
を用いて検証
Journal of FORMALIZED MATHEMATICS
の４つの論文としてまとめた
ＩＮＥ言語の考え方の基本
述語命題関数で文をモデル化
例えば、「私は行く」という文を
「行く（私）」という関数の形で表す
「行く(Ｘ)」と書けば、「Ｘは行く」
を意味する
１変数述語論理
真実「私は行く」「彼は行かない」
述語命題関数「行く（Ｘ）」を用い
「X = 私」を代入
行く（私）=ＴＲＵＥ
「Ｘ = 彼」を代入
行く（彼）=ＦＡＬＳＥ
「行く（Ｘ）」
１変数述語論理
２変数述語論理
「ｘがｙより大きい」という文の場合
「大きい（ｘ）（ｙ）」という関数形で書ける
x,yを定めれば、この関数の値が
TRUE か FALSE かが定まる
「大きい（ｘ）（ｙ）」
２変数述語論理
ＩＮＥ言語の考え方の基本
全ての文を関数形で記述
述語命題関数
TRUE or FALSE を値とする関数
Boole値をとる関数
Boolean Valued Function (BVF)
ＩＮＥの定式化１
関数形
述語命題関数
Boolean Valued Functionとして定式化
証明検証システムＭＩＺＡＲを用いて検証
Boolean Valued Function
BVF(Y) = Funcs(Y,Boolean)
Funcs(A,B) AからBへの写像の全体
Boolean = {TRUE, FALSE}
BVF(Y)の要素の例
1
0
TRUE = 1
FALSE = 0
Y
1
0
Y
Pj(a,x)の定義
1
0
x
Pj(a,x) = a(x)
x における a の値
Y
a ‘<‘ b (a implies b)の定義
1
0
1
Y
0
Y
a ‘<‘ b (a implies b)の定義
限定作用素 all Exist
「全ての」「ある」という表現
全ての人が、全ての本を読む。
全ての人が、ある本を読む。
read(All(book))(All(man))
read(Exist(book))(All(man))
限定作用素 all Exist
「全ての」「ある」という表現
文章表現ではきわめて重要
集合の分割
「全ての」「ある」という表現
文章表現ではきわめて重要
「集合の分割」の考え方を
Boolean Valued Function
に導入
ＩＮＥの定式化２
「全ての」「ある」という表現
「集合の分割」を定式化
証明検証システムＭＩＺＡＲを用いて検証
分割(Partition)とは
空でない集合Y
分割(Partition)とは
PA
空でない集合Y
分割の定義
最小の分割 %I(Y)
空でない集合Y
最大の分割 %O(Y)
空でない集合Y
分割のJoin演算子の定義
Y
Y
PA
PB
Y
PA
ＰＢ
分割のJoin演算子の定義
分割のMeet演算子の定義
Y
Y
PA
PB
Y
PA
ＰＢ
分割のMeet演算子の定義
b is_min_depend PA,PB
b is_a_dependent_set_of PA
Y
分割のJoin,Meet演算子の定理
結合法則
分割全体 PARTITIONS(Y)
PA
PD
PB
PE
集合Yの分割の全体集合
PC
PF
複数の分割のJoin演算子の定義
PA
Ｇ
PB
PC
Ｇ PARTITIONS(Y)
Ｇ = {PA,PB,PC}
複数の分割のJoin演算子
限定作用素を含む述語論理
ある人は全ての本を読む
全ての本はある人に読まれる
x y P x y
y x P x y
という２変数述語論理の数式で記述される
x,yは直交する座標であると考えられる
２変数述語論理
xがyを読む
P(x,y)
3が2を読む
P(3,2)
２変数述語論理
ここでは、例えば
1～4という人が
(人は全部で４人)
1～4という本を読む（本は全部で４冊）
とします
２変数述語論理
y
(4,4)
4 (1,4)
3
3が2を読む
P(3,2)
(3,2)
2
1 (1,1)
1
(4,1)
2
3
4
x
２変数述語論理
y
4
3
TRUE
2
P(3,2)=T
(3,2)
3が2を読む
1
1
2
3
4
x
２変数述語論理
ここでは、例えば
３という人が
1～4という本をすべて読む
と仮定します
２変数述語論理
まず、
３という人
に着目して考えると・・・
２変数述語論理
y
(3,4)
P(3,4)=T
3
(3,3)
P(3,3)=T
2
(3,2)
P(3,2)=T
1
(3,1)
4
3
2
4
1
P(3,1)=T
x
y
２変数述語論理
4
(3,4)
3
(3,3)
2
(3,2)
1
(3,1)
4
3
2
1
P(3,4)=T
P(3,3)=T
P(3,2)=T
P(3,1)=T
y P 3 y =T
x y P x y =T
x
２変数述語論理
次に、
1～４の本
に着目して考えると・・・
y
P(3,4)=T
P(3,3)=T
P(3,2)=T
P(3,1)=T
２変数述語論理
4
(3,4)
3
(3,3)
2
(3,2)
1
(3,1)
4
3
2
1
x
xP
xP
xP
xP
x
x
x
x
4
3
2
1
=T
=T
=T
=T
２変数述語論理
xP
xP
xP
xP
P(3,4)=T
P(3,3)=T
P(3,2)=T
P(3,1)=T
y
x
x
x
x
4
3
2
1
=T
=T
=T
=T
x P x y =T
２変数述語論理
y
y
3
x
x y P x y =T
4
3
2
1
y
x
x P x y =T
ある人は全ての本を読む
全ての本はある人に読まれる
２変数述語論理
y
y
4
3
2
1
y
x
x P x y =T
x
x y P x y =T
3
全ての本はある人に読まれる
ある人は全ての本を読む
ＩＮＥの定式化３
x y P x y
y x P x y
限定作用素を含む２変数述語論理を定式化
証明検証システムＭＩＺＡＲを用いて検証
CompF(PA,G)
B_INF(a,PA)
B_SUP(a,PA) などを定義
ＩＮＥの定式化３
x y P x y
y x P x y
x,yは座標であると考えられる
座標を定義
座標の定義
Ｇ
集合Yの分割の全体集合
PA
PB
PC
PD
PE
PF
座標の定義
Ｇ
PARTITIONS(Y) のとき
Ｇが座標
Ｇ is_a_coordinate
座標の定義
次の
１～３の条件を満たすとき
Ｇ is_a_coordinate
と定義する
座標の定義 (条件１)
Y
G is_a_generating_family_of_partitions
座標の定義 (条件２)
G = {PA,PB,・・・}
PA
A
PB
A
B
A
PA
PB
B
B
G is_an_independent_family_of_partitions
座標の定義 (条件２)
G is_an_independent_family_of_partitions
座標の定義 (条件３)
G = {PA,PB,・・・}
PB
Y
PA
PA
PB
PA
Y
PB = ％Ｏ（Ｙ）
CompF(PA,G)の定義
CompF(PA,G) =
(G
{PA})
限定作用素の定義に必要なため
(All, Exist)
CompF(PA,G)
PB
G is_a_coordinate
G = {PA,PB}の場合
PB
Y
PA
Ｇ = ％Ｉ（Ｙ）
Y
CompF(PA,G) = PB
G is_a_coordinate
CompF(PA,G) G = {PA,PB,PC}の場合
PB
PA
PC
Ｇ = ％Ｉ（Ｙ）
CompF(PA,G)
B_INF(a,PA)の定義
PA
1
0
B_INF(a,PA)
Y
1
0
Y
B_SUP(a,PA)の定義
PA
1
0
B_SUP(a,PA)
Y
1
0
Y
All(a,PA,G), Ex(a,PA,G)の定義
全称作用素 All
All(a,PA,G) = B_INF(a,CompF(PA,G))
存在作用素 Exist
Ex(a,PA,G) = B_SUP(a,CompF(PA,G))
All(a,PA,G)
PA
PB
Ｇ = ％Ｉ（Ｙ）
G is_a_coordinate
G = {PA,PB}の場合
Y
PB
Y
CompF(PA,G) = PB
All(a,PA,G) = B_INF(a,CompF(PA,G))
= B_INF(a, PB)
All(a,PA,G) = B_INF(a,CompF(PA,G))
G = {PA,PB}のとき CompF(PA,G) = PB
PB
1
a
TRUE
0
1
All(a,PA,G) = B_INF(a,PB)
Y
TRUE
Z
Y
All(a,PA,G)
All(a,PA,G)
PB
Y
A
TRUE
G is_a_coordinate
G = {PA,PB}の場合
a
PB TRUE
TRUE
Z
TRUE
TRUE
Pj(All(a,PA,G),Z)=TRUE
x
A
Pj(a,x)=TRUE
Y
G is_a_coordinate
G = {PA,PB}の場合
Ex(a,PA,G)
Ex(a,PA,G)
PB
Y
A
TRUE
a
TRUE
Z
Pj(Ex(a,PA,G),Z)=TRUE
Y
PB
x
A
x
Pj(a,x)=TRUE
２変数述語論理
数学の本で記述される
x y P x y
y x P x y
という２変数述語論理は、BVFでは
Ex(All(a,PA,G),PB,G) ‘<‘ All(Ex(a,PB,G),PA,G)
２変数述語論理
条件
G is_a_coordinate
G = {PA,PB}
PA PB
Ex(All(a,PA,G),PB,G) ‘<‘ All(Ex(a,PB,G),PA,G)
x y P x y
y x P x y
Ex(All(a,PA,G),PB,G)
‘<‘ All(Ex(a,PB,G),PA,G)
全体集合Y
条件
G is_a_coordinate PA
G = {PA,PB}
PA PB
PB
２変数述語論理
y
y
3
x
x y P x y =T
4
3
2
1
x
y
x P x y =T
ある人は全ての本を読む
全ての本はある人に読まれる
Ex(All(a,PA,G),PB,G)
‘<‘ All(Ex(a,PB,G),PA,G)
Ex(All(a,PA,G),PB,G) ‘<‘ All(Ex(a,PB,G),PA,G)
同値（定義）
z Y:
Pj(Ex(All(a,PA,G),PB,G),z) = TRUE
Pj(All(Ex(a,PB,G),PA,G),z) = TRUE
Ex(All(a,PA,G),PB,G)
‘<‘ All(Ex(a,PB,G),PA,G)
z Y:
仮定
Pj(Ex(All(a,PA,G),PB,G),z) = TRUE
結論
Pj(All(Ex(a,PB,G),PA,G),z) = TRUE
Ex(All(a,PA,G),PB,G)
‘<‘ All(Ex(a,PB,G),PA,G)
PB
TRUE
y
PA
A
x
z
A,
x
y
B
x
B : Pj(a,y)=TRUE
仮定 Pj(Ex(All(a,PA,G),PB,G),z) = TRUE
Ex(All(a,PA,G),PB,G)
‘<‘ All(Ex(a,PB,G),PA,G)
PB
z
x
A,
y
TRUE
B
B : Pj(a,y)=TRUE
仮定 Pj(Ex(All(a,PA,G),PB,G),z) = TRUE
Ex(All(a,PA,G),PB,G)
‘<‘ All(Ex(a,PB,G),PA,G)
PB
D
y
z
C,
y
x
PA
C
y
TRUE ?
x
D : Pj(a,x)=TRUE
結論 Pj(All(Ex(a,PB,G),PA,G),z) = TRUE
Ex(All(a,PA,G),PB,G)
‘<‘ All(Ex(a,PB,G),PA,G)
TRUE
PA
z
y
C,
x
D : Pj(a,x)=TRUE
結論 Pj(All(Ex(a,PB,G),PA,G),z) = TRUE
Ex(All(a,PA,G),PB,G)
‘<‘ All(Ex(a,PB,G),PA,G)
仮定
PB
結論
PA
Pj(Ex(All(a,PA,G),PB,G),z) = TRUE
Pj(All(Ex(a,PB,G),PA,G),z) = TRUE
２変数述語論理
y
y
仮定
3
x
x y P x y =T
4
3
2
1
結論
x
y
x P x y =T
２変数述語論理
条件
G is_a_coordinate
G = {PA,PB}
PA PB
Ex(All(a,PA,G),PB,G) ‘<‘ All(Ex(a,PB,G),PA,G)
x y P x y
y x P x y
２変数述語論理
条件
G is_a_coordinate
G = {PA,PB}
PA PB
Ex(All(a,PA,G),PB,G) ‘<‘ All(Ex(a,PB,G),PA,G)
証明検証システムＭＩＺＡＲを用いて検証
２変数述語論理の定理
これ以外の
２変数述語論理の定理
に関しても証明可能
証明検証システムＭＩＺＡＲを用いて検証
INEの短所
1. 人間にとっては、自然言語に
比べて、入力しにくい
2. 理解しにくい
INEの欠点の克服
INEの欠点の克服のため
Writing Aid
と呼ぶツールを開発
Writing Aidとは
1. ＩＮＥの入力・表現ツール
（ＩＮＥを人間が簡単に扱えるように
開発した新しいソフトウェア）
2. 対話型同時多言語生成ツール
3. 翻訳支援ツール
Writing Aidの構成
多言語をリアルタイムに目で見て確認
ユーザ
Graphical User Interface
文章作成
に必要な
様々な情
報
キーボード
マウス
入力
表記情報
構文情報
意味情報
辞書
ＩＮＥ
生成
ルール
言語生成
日本語
英語
デモ
Writing Aid のデモを行います
まとめ
1. 世界共通言語として数理言語を提案
2. 数理言語「INE」を数学的に定式化
3. その定式化の正しさをMizarで検証
4. INEの入力、表現ツールを開発
ご静聴ありがとうございました

Download Report