多ソート論理

多ソート論理は、宇宙を均質なオブジェクトの集合として扱うのではなく、型付きプログラミングにおける型と同様の方法で宇宙を分割するという私たちの意図を形式的に反映することができます。この論理言語における関数型と断言型の「品詞」は、構文レベルにおいても、この宇宙の型付き分割を反映しています。置換と引数渡しは、「ソート」を尊重して、それに従ってのみ行うことができます。

上記の意図を形式化する方法は様々ありますが、多ソート論理とは、それを満たす情報のパッケージのことです。ほとんどの場合、以下のような形式が用いられます。

• 一種のセット、S
• ソートに伴う追加情報を処理できるようにするための、署名の概念の適切な一般化。

その特徴を持つ構造の議論領域は、種類ごとに互いに素な部分集合に分割される。

生物について考察する際には、2種類の生物を区別することが有用である。${\displaystyle \mathrm {植物} }$そして${\displaystyle \mathrm {動物} }$関数が${\displaystyle \mathrm {母親} \colon \mathrm {動物} \to \mathrm {動物} }$理にかなっている、同様の機能${\displaystyle \mathrm {母} \colon \mathrm {植物} \to \mathrm {植物} }$通常はそうではありません。多ソート論理では、次のような用語を使用できます。${\displaystyle \mathrm {母親} (\mathrm {ラッシー} )}$しかし、次のような用語を捨てる${\displaystyle \mathrm {母親} (\mathrm {私の\_お気に入り\_オーク} )}$構文的に不適切である。

多ソート論理の代数化は、CaleiroとGonçalvesによる論文^{[ 1 ]}で説明されており、抽象代数論理を多ソートの場合に一般化していますが、入門資料としても使用できます。

多ソート論理では、互いに素な宇宙集合を持つために2つの異なるソートが必要であるが、順序ソート論理では1つのソートで十分である。$s1$別の種類のサブタイプとして宣言される$s2$通常は、$s_1\subseteq s_2$または同様の構文。上記の生物学の例では、宣言することが望ましい。

${\displaystyle {\text{犬}}\subseteq {\text{肉食動物}}}$、

${\displaystyle {\text{犬}}\subseteq {\text{哺乳類}}}$、

$\displaystyle {\text{肉食動物}}\subseteq {\text{動物}}}$、

${\displaystyle {\text{哺乳類}}\subseteq {\text{動物}}}$、

${\displaystyle {\text{動物}}\subseteq {\text{生物}}}$、

${\displaystyle {\text{植物}}\subseteq {\text{生物}}}$、

など。図を参照。

何らかの用語が${\displaystyle s}$が必要とされる場合、あらゆる種類の用語${\displaystyle s}$代わりに が提供される場合があります (リスコフの置換原則)。たとえば、関数宣言を想定すると${\displaystyle {\text{母}}:{\text{動物}}\longrightarrow {\text{動物}}}$、そして一定の宣言${\displaystyle {\text{ラッシー}}:{\text{犬}}}$、 用語 $\displaystyle {\text{母}}({\text{娘}})}$完全に有効で、$\displaystyle {\text{動物}}}$犬の母親が犬であるという情報を提供するために、別の宣言 ${\displaystyle {\text{母}}:{\text{犬}}\longrightarrow {\text{犬}}}$発行される可能性があります。これは関数オーバーロードと呼ばれ、プログラミング言語のオーバーロードに似ています。

順序付けされた論理は、単項述語を用いて、順序付けされていない論理に変換することができる。${\displaystyle p_{i}(x)}$各ソートについて$\displaystyle s_{i}}$、そして公理${\displaystyle \forall x(p_{i}(x)\rightarrow p_{j}(x))}$各サブソート宣言について$s_i \subseteq s_j$逆のアプローチは自動定理証明で成功を収めた。 1985年、クリストフ・ヴァルターは、当時のベンチマーク問題を順序ソート論理に変換することで解決し、多くの単項述語をソートに変換することで問題を桁違いに縮小することができた。^{[ 2 ]}

順序ソートされたロジックを節ベースの自動定理証明器に組み込むには、対応する順序ソートされた単一化アルゴリズムが必要であり、これは宣言された任意の 2 つのソートに対して、$s_1,s_2$それらの交差点$\displaystyle s_{1}\cap s_{2}}$宣言も必要となる場合：${\displaystyle x_{1}}$そして${\displaystyle x_{2}}$は、次のような変数です。$s1$そして$s2$それぞれ、方程式${\displaystyle x_{1}{\stackrel {?}{=}}\,x_{2}}$解決策があります${\displaystyle \{x_{1}=x,\;x_{2}=x\}}$、 どこ${\displaystyle x:s_{1}\cap s_{2}}$。

スモルカは、パラメトリック多相性を可能にするために、順序ソート論理を一般化した。^{[ 3 ] [ 4 ]} 彼のフレームワークでは、サブソート宣言は複雑な型式に伝播される。プログラミングの例として、パラメトリックソート${\displaystyle {\text{list}}(X)}$宣言される可能性があります（${\displaystyle X}$C++テンプレートの型パラメータとして、またサブソート宣言から${\displaystyle {\text{int}}\subseteq {\text{float}}}$関係${\displaystyle {\text{list}}({\text{int}})\subseteq {\text{list}}({\text{float}})}$は自動的に推論されるため、整数のリストはすべて浮動小数点数のリストにもなります。

Schmidt-Schaußは、項宣言を可能にするために順序ソート論理を一般化した。^{[ 5 ]} 例として、部分ソート宣言を仮定すると、${\displaystyle {\text{even}}\subseteq {\text{int}}}$そして${\displaystyle {\text{odd}}\subseteq {\text{int}}}$用語宣言${\displaystyle \forall i:{\text{int}}.\;(i+i):{\text{even}}}$通常のオーバーロードでは表現できない整数加算の特性を宣言することを可能にする。

• カテゴリー論理
• 一階述語論理 § 多ソート論理

多ソート論理に関する初期の論文には以下のようなものがある。

• 王浩（1952）。「多ソート理論の論理」。記号論理学ジャーナル。17 （ 2）：105–116。doi：10.2307 /2266241。JSTOR 2266241。 著者の論文集『計算、論理、哲学：エッセイ集』（北京：科学出版社、ドルトレヒト：クルーワー・アカデミック、1990年）に収録。
• ギルモア、PC（1958）。「多ソート理論の論理への補遺」" (PDF) . Compositio Mathematica . 13 : 277–281 .
• A. オーバーシェルプ (1962)。「Untersuchungen zur mehrsortigen Quantorenlogik」。数学アンナレン。145 (4): 297–333 .土井: 10.1007/bf01396685。S2CID 123363080。2015 年 2 月 20 日にオリジナルからアーカイブされました。2013 年 9 月 11 日に取得。 
• F. ジェフリー・ペルティエ (1972). 「ソート量化と制限量化」(PDF) . Philosophical Studies . 23 (6): 400– 404. doi : 10.1007/bf00355532 . S2CID 170303654 . 

• カロジェロ・G・ザルバ著『決定手続きに関する講義ノート』の第1章「多ソート論理」