学習負担の原因となる「記法の多様性」問題と解決法

• 「バベルの塔」問題
• 「アブダクション」問題

バベルの塔 - Wikipedia

神は降臨してこの塔を見「人間は言葉が同じなため、このようなことを始めた。人々の言語を乱し、通じない違う言葉を話させるようにしよう」と言った。このため、人間たちは混乱し、塔の建設をやめ、世界各地へ散らばっていった。

「通じない違う言葉を話すようになり、混乱した」という部分に注目。

一方聖書によるとバベルはヘブライ語のbalal（ごちゃまぜ）から来ているとされる。

「バベルの塔」問題

一般的な言葉の問題：

1. 曖昧性
2. 多義性
3. 同犠牲
4. 不適切性

曖昧性は、論理式による記述で排除する。多義性・同犠牲・不適切性はどうにもならない。

不適切性は完全に諦める。同義性は同義語を明示することで解決する。

• 言葉の定義時に、同義語を列挙する。
• 言葉の使用時に、同義語も併記する。

例：

• A, Bを集合（＝型＝データ型）とするとき、A×Bを{直積 | 積}{ _ | 型 | データ型 | 集合}と呼ぶ。

展開すると、

1. A×Bを直積と呼ぶ。
2. A×Bを直積型と呼ぶ。
3. A×Bを直積データ型と呼ぶ。
4. A×Bを直積集合と呼ぶ。
5. A×Bを積と呼ぶ。
6. A×Bを積型と呼ぶ。
7. A×Bを積データ型と呼ぶ。
8. A×Bを積集合と呼ぶ。

同様に、

• A∩Bを{共通部分 | 積 | 交わり}{ _ | 集合}と呼ぶ。

1. A∩Bを共通部分と呼ぶ。
2. A∩Bを共通部分集合と呼ぶ。
3. A∩Bを積と呼ぶ。
4. A∩Bを積集合と呼ぶ。
5. A∩Bを交わりと呼ぶ。
6. A∩Bを交わり集合と呼ぶ。

すると、次の文は多義性を持つ。

• XはAとBの積集合である。

多義性を次のように解決する。

1. XはAとBの積集合（＝共通部分）である。
2. XはAとBの積集合（＝直積）である。

別な例として、

1. xはインスタンス（＝要素）である。
2. xはインスタンス（＝状態）である。

しかし、微妙な問題がある。

• 変数の型＝変数の値の型

から、

• 変数＝変数の値

という用法があるのは分かるが、

• 変数の集合＝変数の値の集合

ではない。型＝集合 として、

• 変数の集合＝変数の値の型＝変数の型

は成立しない。f(x) = f(y) から x = y は導けない。

一方、等式的変形（＝等式的リーズニング）が許される例：

• 制約＝制限
• 制約＝条件＝制約条件

より

• 制限＝条件＝制限条件

ギュメ記法

多義語の意味を区別するために、多義のどれを意味するかをギュメで示す。

• タプル 普通の意味
• 《タプル》 レコードを意味するとき

同義語併記でも同じ効果がある。

• タプル
• タプル（＝レコード）

語義関係と語義推論

語義とは、言葉の集合と意味の集合のあいだの関係である。

• 語義:言葉の集合→意味の集合 in Rel

文脈とは、言葉の集合と意味の集合のあいだの部分写像である。

• 文脈:言葉の集合→意味の集合 in Partial

文脈が語義に{適合 | 妥当}しているとは、文脈が語義の部分関係になっていること。

語wが：

• 単義語である :⇔ 語義(w) が単元集合
• 多義語である :⇔ 語義(w) が非空・非単元集合

語u, wが：

• 完全同義語である :⇔ 語義(u) = 語義(w)
• 部分同義語である :⇔ 語義(u)∩語義(w) ≠ 空集合

文脈Cを固定すると：

• Cにおいて同義語である :⇔ C(u) = C(w)
• Cにおいて異義語である :⇔ C(u) ≠ C(w)

また、wが

• Cにおいて有意語である :⇔ C(w)が定義されている。
• Cにおいて無意語である :⇔ C(w)が定義されていない。

語の集合をWとして、Wの有限部分集合を語群と呼ぶ。

• 語群Xが有意である :⇔ ∩_w∈X語義(w) が空でない
• 語群Xが無意である :⇔ ∩_w∈X語義(w) が空集合
• 語群Xが一意である :⇔ ∩_w∈X語義(w) が単元集合

語群Xが有意であるとき、X⊆X' となる語群X'で一意なものが存在するとき、語義関係は有限一意化可能と呼ぶ。

言葉に関して次の命題を考える。

1. u ＝ w :⇔ uとwは完全同義である
2. u ≠ w :⇔ uとwは完全同義ではない
3. u ≒ w :⇔ uとwは部分同義である
4. u ＝ w in C :⇔ uとwはCにおいて同義である
5. u ≠ w in C :⇔ uとwはCにおいて異義である
6. X↓ :⇔ Xは有意である
7. X! :⇔ Xは一意である

アブダクション

ピグマリオン・アブダクション

   ∃f.  f:A→B isInj

  -------------------[Injアブダクション]

    A⊆B

   ∃f.  f:A→B isBij

  -------------------[Bijアブダクション]

    A = B

アブダクションの種明かし：

   ∃f.  f:A→B isInj

  -----------------------

   Aim(f), im(f)⊆B

  -----------------------

   let A := im(f) in A⊆B

   ∃f.  f:A→B isBij

  -----------------------

   Aim(f), im(f) = B

  -----------------------

   let A := im(f) in A = B