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: ${\displaystyle {\textit {plant}}}$ and ${\displaystyle {\textit {animal}}}$. Enquanto uma função ${\displaystyle {\textit {mother}}:{\textit {animal}}\longrightarrow {\textit {animal}}}$ faz sentido, uma função similar ${\displaystyle {\textit {mother}}:{\textit {plant}}\longrightarrow {\textit {plant}}}$ usualmente não faz não faz. Lógica polissortida permite um ter termos como ${\displaystyle {\textit {mother}}({\textit {lassie}})}$, mas discartar termos como ${\displaystyle {\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,^[1] 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 ${\displaystyle s_{1}}$ para ser declarado como um subtipo de outro tipo. ${\displaystyle s_{2}}$, usualmente escrevendo${\displaystyle s_{1}\subseteq s_{2}}$ ou sintaxe similar. No exemplo abaixo, é desejável declarar

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

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

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

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

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

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

e assim por diante.

Onde um termo de um tipo ${\displaystyle s}$ é requerido, um termo de qualquer subtipo ${\displaystyle s}$ pode ser fornecido em seu lugar. Por exemplo, assumindo uma declaração de função ${\displaystyle {\textit {mother}}:{\textit {animal}}\longrightarrow {\textit {animal}}}$, e uma declaração constante ${\displaystyle {\textit {lassie}}:{\textit {dog}}}$, o termo ${\displaystyle {\textit {mother}}({\textit {lassie}})}$ é perfeitamente válido e tem o tipo ${\displaystyle {\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 ${\displaystyle {\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 ${\displaystyle p_{i}(x)}$ para cada tipo${\displaystyle s_{i}}$, e um axioma ${\displaystyle \forall x:p_{i}(x)\rightarrow p_{j}(x)}$ para cada declaração de subtipo ${\displaystyle 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.^[2]

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 ${\displaystyle s_{1},s_{2}}$ their intersection ${\displaystyle s_{1}\cap s_{2}}$ ser declarados, para: se ${\displaystyle x_{1}}$ e ${\displaystyle x_{2}}$ é im tipo variável ${\displaystyle s_{1}}$ e ${\displaystyle s_{2}}$, respectivamente, a equação ${\displaystyle x_{1}{\stackrel {?}{=}}x_{2}}$ possui a solução ${\displaystyle \{x_{1}=x,\;x_{2}=x\}}$, onde ${\displaystyle x:s_{1}\cap s_{2}}$.

Smolka generalizou a lógica ordem-sortida para permitir polimorfismo paramétrico. ^[3][4] 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 ${\displaystyle {\textit {list}}(X)}$ pode ser declarado (with ${\displaystyle X}$ sendo um tipo paramétrico como em um template C++), e de uma declaração de subtipo ${\displaystyle {\textit {int}}\subseteq {\textit {float}}}$ a relação ${\displaystyle {\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.^[5] Como um exemplo, asumindo declarações de subtipos ${\displaystyle {\textit {even}}\subseteq {\textit {int}}}$ e ${\displaystyle {\textit {odd}}\subseteq {\textit {int}}}$, uma declaração de termo como ${\displaystyle \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

1. Carlos Caleiro, Ricardo Gonçalves (2006). «On the algebraization of many-sorted logics». Proc. 18th int. conf. on Recent trends in algebraic development techniques (WADT) (PDF). [S.l.]: Springer. pp. 21–36. ISBN 978-3-540-71997-7
2. Walther, Christoph (1985). «A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution» (PDF). Artif. Intell. 26 (2): 217–224. doi:10.1016/0004-3702(85)90029-3
3. Smolka, Gert (novembro de 1988). «Logic Programming with Polymorphically Order-Sorted Types». Int. Workshop Algebraic and Logic Programming. LNCS. 343. Springer. pp. 53–70
4. Smolka, Gert (maio de 1989), Logic Programming over Polymorphically Order-Sorted Types, Univ. Kaiserslautern, Germany
5. Schmidt-Schauß, Manfred (abril de 1988). Computational Aspects of an Order-Sorted Logic with Term Declarations. Col: LNAI. 395. [S.l.]: Springer

Ligações externas

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