Lógica polissortida

A lógica polissortida pode refletir formalmente a nossa intenção de não lidar com o universo como um conjunto homogêneo de objetos, mas particionar isso de uma maneira que é semelhante aos de tipos em linguagens tipadas. Ambos funcionais e assertivas "partes do discurso" na linguagem da logica refletem essa partição tipificada do universo, mesmo no nível de sintaxe: substituição e argumento de passagem só pode ser feito em conformidade, respeitando os "tipos".

Há mais maneiras de formalizar a intenção acima mencionada; a Lógica polissortida é qualquer pacote de informação que o preenche. Na maioria dos casos, são os seguintes dados:

• um conjunto de tipos, S
• uma generalização adequada da noção de assinatura ara ser capaz de lidar com a informação adicional que vem com os tipos.

O universo de discurso de qualquer estrutura dessa assinatura é então fragmentada em subconjuntos dijuntos, um para cada tipo.

Exemplo

Ao refletirmos sobre criaturas biológicas, é útil distinguir dois tipos: ${\textit {plant}}$ and ${\textit {animal}}$. Enquanto uma função ${\textit {mother}}:{\textit {animal}}\longrightarrow {\textit {animal}}$ faz sentido, uma função similar ${\textit {mother}}:{\textit {plant}}\longrightarrow {\textit {plant}}$ usualmente não faz não faz. Lógica polissortida permite um ter termos como ${\textit {mother}}({\textit {lassie}})$, mas discartar termos como ${\textit {mother}}({\textit {my\_favorite\_oak}})$ como sintaticamente mal formado.

Álgebra

A álgebra da lógica polissortida é explicada em um artigo de Caleiro e Gonçalves, que generaliza a lógica algébrica abstrata para o caso polissortido, mas também pode ser usado como material introdutório.

Lógica ordem-sortida

Enquanto Lógica polissortida requer dois diferentes tipos para ter conjuntos universo dijuntos, lógica ordem-sortida permite um tipo $s_{1}$ para ser declarado como um subtipo de outro tipo. $s_{2}$, usualmente escrevendo$s_{1}\subseteq s_{2}$ ou sintaxe similar. No exemplo abaixo, é desejável declarar

${\textit {dog}}\subseteq {\textit {carnivore}}$,

${\textit {dog}}\subseteq {\textit {mammal}}$,

${\textit {carnivore}}\subseteq {\textit {animal}}$,

${\textit {mammal}}\subseteq {\textit {animal}}$,

${\textit {animal}}\subseteq {\textit {creature}}$,

${\textit {plant}}\subseteq {\textit {creature}}$,

e assim por diante.

Onde um termo de um tipo $s$ é requerido, um termo de qualquer subtipo $s$ pode ser fornecido em seu lugar. Por exemplo, assumindo uma declaração de função ${\textit {mother}}:{\textit {animal}}\longrightarrow {\textit {animal}}$, e uma declaração constante ${\textit {lassie}}:{\textit {dog}}$, o termo ${\textit {mother}}({\textit {lassie}})$ é perfeitamente válido e tem o tipo ${\textit {animal}}$. A fim de fornecer as informações de que a mãe de um cão é um cão, por sua vez, uma nova declaração ${\textit {mother}}:{\textit {dog}}\longrightarrow {\textit {dog}}$pode ser emitida; isso é chamado de sobrecarga de funções , semelhante ao Polimorfismo em linguagens de programação.

Lógica ordem-sortida pode ser traduzida em lógica não sortida, usando um predicado unário $p_{i}(x)$ para cada tipo$s_{i}$, e um axioma $\forall x:p_{i}(x)\rightarrow p_{j}(x)$ para cada declaração de subtipo $s_{i}\subseteq s_{j}$. A abordagem inversa foi bem sucedido na prova de teoremas automatizado: em 1985, Christoph Walther poderia resolver um problema, então referência, traduzindo-a na lógica ordem-sortida, portando fazendo isso uma ordem de magnitude, assim como muitos predicados unários se transformaram em tipos.

A fim de incorporar uma lógica classificados ordem em um teorema automatizado prover baseada em cláusulas, uma correspondente algoritmo de unificação ordem-sortida é necessário,que exige que para quaisquer dois tipos declarados $s_{1},s_{2}$ their intersection $s_{1}\cap s_{2}$ ser declarados, para: se $x_{1}$ e $x_{2}$ é im tipo variável $s_{1}$ e $s_{2}$, respectivamente, a equação $x_{1}{\stackrel {?}{=}}x_{2}$ possui a solução $\{x_{1}=x,\;x_{2}=x\}$, onde $x:s_{1}\cap s_{2}$.

Smolka generalizou a lógica ordem-sortida para permitir polimorfismo paramétrico. IEm seu quadro, declarações de subtipo são propagadas para expressões do tipo complexo. Como um exemplo de programação, um tipo paramétrico ${\textit {list}}(X)$ pode ser declarado (with $X$ sendo um tipo paramétrico como em um template C++), e de uma declaração de subtipo ${\textit {int}}\subseteq {\textit {float}}$ a relação ${\textit {list}}({\textit {int}})\subseteq {\textit {list}}({\textit {float}})$ é automaticamente inferida, significando que cada lista de inteiros é também uma lista de tipos float.

Schmidt-Schauß generalizou ordem-sortida para permitir a declaração de termos. Como um exemplo, asumindo declarações de subtipos ${\textit {even}}\subseteq {\textit {int}}$ e ${\textit {odd}}\subseteq {\textit {int}}$, uma declaração de termo como $\forall i:{\textit {int}}.\;(i+i):{\textit {even}}$ permite declarar uma propriedade de adição de inteiros que não pode ser expressada por poliformismo ordinário.

Referências

Primeiros artigos sobre lógica de muitos tipos incluem:

• Gilmore, P.C. (1958). «An addition to "Logic of many-sorted theories"» (PDF). Compositio Mathematica. 13: 277–281 
• A. Oberschelp (1962). «Untersuchungen zur mehrsortigen Quantorenlogik». Mathematische Annalen. 145 (4): 297–333. doi:10.1007/bf01396685. Consultado em 25 de fevereiro de 2015. Arquivado do original em 20 de fevereiro de 2015 
• F. Jeffry Pelletier (1972). «Sortal Quantification and Restricted Quantification» (PDF). Philosophical Studies. 23: 400–404. doi:10.1007/bf00355532 

Ligações externas

• "Many-sorted Logic", the first chapter in Lecture Notes on Decision Procedures by Calogero G. Zarba