曖昧表現、一様化、同一視

曖昧表現は:

  1. 名前・記号の借用 例: G = (G, *, 1)
  2. 省略 例: G = (G, *)
  3. 名前・記号の多義的使用〈オーバーロード〉

曖昧表現の解決は、データベース検索。検索条件はパターンマッチ問題〈ユニフィケーション問題〉となる。パターンマッチ問題を解いて曖昧表現を解決する。データベース検索には次の種類がある。

  1. 一意検索: 結果が一意的でないと失敗。
  2. 候補検索: 結果があれば成功、ないと失敗。
  3. 選択検索: 結果があると適当に一個選ぶ。ないと失敗。

検索は、名前空間構造と密接に関係している。基本はコアージョン・データベースで、コアージョン・データベースの一部に増強データベース〈インスタンス・データベース〉がある。コアージョンは型変換子だが、型変換子のデータベースへの登録は、アドホック登録とパラメトリック登録がある。

曖昧表現の利用と解決は本来の構造記述とは独立で自由に導入・削除ができるべき

一様化の例として、総称引数 < >、インデックス引数 [ ]、通常引数を全部同等に扱うこと。

同一視の例として、カリー同型による同一視、自明指数同型(A ≒ A^1)による同一視、左右の単位律子による同一視などがある。証明無関心〈proof irrelevance〉も同一視。