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,^[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 $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.^[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 $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. ^[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 ${\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.^[5] 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

↑ 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
↑ 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
↑ Smolka, Gert (novembro de 1988). «Logic Programming with Polymorphically Order-Sorted Types». Int. Workshop Algebraic and Logic Programming. LNCS. 343. Springer. pp. 53–70
↑ Smolka, Gert (maio de 1989), Logic Programming over Polymorphically Order-Sorted Types, Univ. Kaiserslautern, Germany
↑ Schmidt-Schauß, Manfred (abril de 1988). Computational Aspects of an Order-Sorted Logic with Term Declarations. Col: LNAI. 395. [S.l.]: Springer

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

[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

[1]

[2]

[3]

[4]

[5]