Gazâlî’nin Filozofları Eleştirmesi: - Metodik Şüphecilikte Aklın Yeri:

İKİNCİ BÖLÜM GAZÂLÎ’YE GÖRE AKLIN DEĞERİ VE SINIRLILIĞ

II. Metodik Şüphecilikte Aklın Yeri:

II.I. Gazâlî’nin Filozofları Eleştirmesi:

Esta se¸c˜ao fornece exemplos que ilustram constructos da linguagem CASL para o uso em es- pecifica¸c˜oes arquiteturais: defini¸c˜oes de especifica¸c˜oes arquiteturais, declara¸c˜oes de unidades, defini¸c˜oes unidades, especifica¸c˜oes de unidades, e express˜oes de unidades.

Epeciﬁca¸c˜oes Arquiteturais: Uma defini¸c˜ao de uma especifica¸c˜ao arquitetural especi- fica algumas unidades e como compor essas unidades, por exemplo:

arch spec IMP-NAT-LIST

units N : NAT ; F : NAT _{→ LIST [NAT ]}

result F[N]

Um modelo da especifica¸c˜ao arquitetural acima consiste de uma unidade N, uma fun¸c˜ao de unidade F, e a unidade F[N], que ´e ela mesma um modelo da especifica¸c˜ao estruturada LIST[NAT].

Declara¸c˜oes de Unidades : Uma declara¸c˜ao de unidade d´a o nome e o tipo de uma unidade que est´a sendo desenvolvida. Quando o tipo ´e uma especifica¸c˜ao ordin´aria, a unidade ´e um modelo ordin´ario dela; quando o tipo ´e um tipo fun¸c˜ao, a unidade ´e uma fun¸c˜ao de modelos ordin´arios (compat´ıveis) para modelos ordin´arios que estendem os argumentos. Alguns exemplos de declara¸c˜ao unidade s˜ao:

N : NAT

L : LIST[NAT] given N

F : NAT_{→ LIST[NAT]}

A forma de declara¸c˜ao usando ‘given’ fornece uma declara¸c˜ao impl´ıcita de uma fun¸c˜ao unidade que ´e aplicada somente uma vez `a unidades importadas para a implementa¸c˜ao da unidade declarada (no exemplo acima a unidade importada ´e N enquanto que a declarada ´e L). Se a declara¸c˜ao de F acima fosse substitu´ıda pela de L ent˜ao uma implementa¸c˜ao da especifica¸c˜ao arquitetural ainda envolveria uma fun¸c˜ao que retornaria uma implementa¸c˜ao de LIST[NAT] estendendo qualquer implementa¸c˜ao N de NAT.

Deﬁni¸c˜oes de Unidades: Uma defini¸c˜ao de unidade d´a nome a uma unidade que pode ser obtida de unidades pr´evias (na mesma especifica¸c˜ao arquitetural), possivelmente envolvendo adapta¸c˜ao (fitting), “hidding”, tradu¸c˜ao, etc:

L = F[N]

L = F[N ﬁt . . .]hide. . .

As express˜oes no lado direito das defini¸c˜oes de unidades s˜ao da mesma forma que aquelas usadas para especificar a unidade resultante de uma especifica¸c˜ao arquitetural.

Especiﬁca¸c˜oes de Unidades: Uma defini¸c˜ao de especifica¸c˜ao de unidade nomeia um tipo de unidade permitindo que ele seja reus´avel. Por exemplo:

unit spec GEN − LIST = NAT → LIST [NAT ]

Uma declara¸c˜ao de unidade pode ent˜ao referenciar uma especifica¸c˜ao de unidade, e.g: F : GEN-LIST.

Especifica¸c˜oes arquiteturais por si s´o tamb´em podem ser usadas como especifica¸c˜oes de unidades.

Express˜oes de Unidades: As v´arias formas de express˜ao de unidades assemelham-se as especifica¸c˜oes estruturadas:

• aplica¸c˜ao ( para argumentos compat´ıveis): F[N], F[N ﬁt . . .] • abstra¸c˜ao: λN : NAT • . . . N . . .

• composi¸c˜ao (de unidades compat´ıveis): N and C

Entretanto, a semˆantica das express˜oes de unidades envolvem opera¸c˜oes sobre os modelos individuais, em vez de opera¸c˜oes sobre classes inteiras dos modelos. Em particular, a com- posi¸c˜ao (amalgama¸c˜ao) de modelos requer que qualquer s´ımbolo comum seja interpretado do mesmo modo. Note que abstra¸c˜ao ´e necess´aria para permitir especifica¸c˜oes arquiteturais, cujo resultado s˜ao fun¸c˜oes entre unidades.

3.5.4 Exemplo

O seguinte exemplo ilustra uma defini¸c˜ao de especifica¸c˜ao arquitetural (que referencia as especifica¸c˜oes ordin´arias LIST, CHAR, and NAT, assumindo a declara¸c˜ao dos sorts Elem e List[Elem], Char, and Nat, respectivamente):

arch spec CN-LIST units C : CHAR;

N : NAT ;

F : ELEM _{→ LIST [ELEM ]}

result F [C ﬁt Elem _{→ Char] and F [N ﬁt Elem → Nat]}

3.6 Especiﬁca¸c˜oes de Bibliotecas

As bibliotecas em CASL s˜ao formadas pela coleta de: deﬁni¸c˜oes de especiﬁca¸c˜oes estru- turadas, vis˜oes, especiﬁca¸c˜oes arquiteturais, e especiﬁca¸c˜oes de unidades. Al´em disso, as bibliotecas podem referir-se `as especifica¸c˜oes definidas em outras bibliotecas.

A subse¸c˜ao 3.6.2 apresenta os conceitos principais em que as semˆanticas das bibliotecas est˜ao baseadas. Finalmente, a se¸c˜ao 3.6.3 fornece exemplos que ilustram os constructos da linguagem CASL para uso em bibliotecas.

3.6.1 Aspectos Pragm´aticos

Quando as especifica¸c˜oes s˜ao coletadas dentro de bibliotecas, a quest˜ao da visibilidade dos s´ımbolos entre as especifica¸c˜oes aparece. Em CASL, os s´ımbolos dispon´ıveis em uma especiﬁca¸c˜ao s˜ao somente aqueles que ela mesma declara, junto com aqueles declara- dos (e n˜ao escondidos) nas especifica¸c˜oes nomeadas que ela explicitamente referencia. Ent˜ao quando uma especifica¸c˜ao numa biblioteca ´e alterada, ´e imediato localizar-se outras especi- fica¸c˜oes que devem ser afetadas pelas mudan¸cas.

Um outro aspecto afeta a visibilidade de nomes de especifica¸c˜oes. Em CASL, a visibilidade ´e linear : uma especifica¸c˜ao pode somente referir as especifica¸c˜oes de nomes (e vis˜oes) que a precedem na biblioteca. A motiva¸c˜ao para esta restri¸c˜ao ´e em parte metodol´ogica (as bibliotecas ser˜ao apresentadas na forma botton-up), em parte por quest˜oes de implementa¸c˜ao (uma biblioteca pode ser processada sequencialmente), e em parte pela dificuldade em dar uma semˆantica formal satisfat´oria para especifica¸c˜oes mutuamente dependentes.

CASL fornece suporte direto para rever a distribui¸c˜ao de bibliotecas pela Internet. Uma biblioteca registrada recebe um ´unico nome, que ´e usado como referˆencia a partir de outras bibliotecas. Servidores de nomes fornecem a localiza¸c˜ao corrente das bibliotecas registradas (antes que uma biblioteca seja registrada, ela ´e referenciada pela sua URL corrente). Con- troles de vers˜ao s˜ao uma importante preocupa¸c˜ao pragm´atica, e os nomes das bibliotecas CASL incorporam n´umeros de vers˜oes; entretanto, ´e poss´ıvel referir-se a uma biblioteca sem

especificar uma dada vers˜ao.

Pode acontecer que o mesmo nome possa ser usado para especifica¸c˜oes em diferentes bibliotecas. Para evitar confus˜ao entre os nomes de bibliotecas locais e remotas, uma es- pecifica¸c˜ao que ´e baseada a partir de uma biblioteca remota pode receber um nome local distinto.

3.6.2 Conceitos Semˆanticos

A semˆantica de uma especifica¸c˜ao em uma biblioteca, ´e uma fun¸c˜ao de um ambiente global que mapeia nomes de especifica¸c˜oes (previamente declarados ou carregados “downloaded”na mesma biblioteca) para suas denota¸c˜oes. O ambiente global no final da biblioteca d´a a semˆantica de toda biblioteca.

Um diret´orio de bibliotecas registrado mapeia nomes de bibliotecas para seus registros URLs. Visto que os nomes incluem n´umeros de vers˜ao, este diret´orio tamb´em d´a acesso a vers˜oes anteriores de bibliotecas.

Finalmente, as semˆanticas daquelas cole¸c˜oes das bibliotecas CASL dependem do estado corrente da Internet, associando URLs ao conte´udo de bibliotecas particulares.

3.6.3 Constructos da Linguagem

Esta se¸c˜ao esbo¸ca alguns exemplos que ilustram os constructos da linguagem CASL para uso em bibliotecas.

Bibliotecas Locais: As especifica¸c˜oes e vis˜oes em uma biblioteca auto-contida s˜ao simplesmente listadas em uma ordem botton-up: um nome tem que ser definido antes de ser

referenciado (visibilidade linear). library NUMBERS

spec NAT = ... spec INT = ...

Bibliotecas Distribu´ıdas: Outras bibliotecas podem referir-se a especifica¸c˜oes em bib- liotecas registradas em outros sites da Internet pela inclus˜ao expl´ıcita de downloadings, opcionalmente fornecendo um nome local diferente para a especifica¸c˜ao remota:

from NUMBERS get NAT , INT

As bibliotecas podem ter diferentes vers˜oes, indicadas por seus nomes, ambos quando definem- se as bibliotecas e quando carrega-se especifica¸c˜oes a partir delas:

library NUMBERS version 0 .7 from NAT version 1 .0 get ...

Se o n´umero de vers˜ao ´e omitido em uma defini¸c˜ao de biblioteca, a vers˜ao ´e implicitamente 0 (zero). A vers˜ao ‘default’ quando se referencia uma biblioteca ´e a que foi registrada com o n´umero de vers˜ao maior.

3.7 Considera¸c˜oes Finais

Neste cap´ıtulo, apresentou-se a linguagem CASL, como uma alternativa atual para o desen- volvimento rigoroso de software - desde a especifica¸c˜ao at´e a implementa¸c˜ao do mesmo. O texto aqui apresentado, como foi mencionado, ´e uma adapta¸c˜ao do artigo de Peter Mosses:“CASL a Guided Tour of its Desig” [9], e tem o prop´osito de ser uma referˆencia

inicial, na l´ıngua portuguˆesa, para os interessados em CASL, bem como tem o papel de tornar essa disserta¸c˜ao auto-contida. Para maiores referˆencias o leitor pode utilizar “CASL. The Common Algebraic Specification Language Summary” [1].

Seguindo a proposta deste trabalho, o pr´oximo cap´ıtulo apresenta uma vers˜ao da igual- dade local intervalar proposta por Santiago em [12], que ´e constru´ıda a partir da no¸c˜ao de igualdade forte em CASL. Com isso, se poder´a acrescentar na biblioteca de tipos b´asicos de CASL intervalos mais a igualdade local, permitindo com que se tenha um tipo para n´umeros reais munido do controle de erros de aproxima¸c˜ao. O cap´ıtulo 5 introduz princ´ıpios de congruˆencia e de indicernibilidade para essa igualdade, por fim o apˆendice A cont´em a especifica¸c˜ao da biblioteca intervalar.

Igualdade Local Intervalar e CASL

O objetivo deste cap´ıtulo ´e apresentar uma no¸c˜ao alternativa de igualdade para os intervalos de maneira que esta possa ser utilizada dentro de especifica¸c˜oes CASL. Para isso, introduz- se, inicialmente, uma l´ogica que pressup˜oe objetos parcialmente definidos que suporta a linguagem CASL1_{e em seguida define-se a vers˜ao booleana da igualdade local sobre intervalos} que foi proposto em [12]. Isso porque2_{, Santiago [12] fez uma an´alise de que a impossibilidade} de resolver equa¸c˜oes alg´ebricas usando a aritm´etica intervalar reside na no¸c˜ao de igualdade intervalar cl´assica, o que exclui completamente o papel dos intervalos como informa¸c˜ao de n´umeros reais [5].

Assim, surge a necessidade de uma no¸c˜ao auxiliar de igualdade para intervalos capaz de ser expressa em CASL, afim de permitir que eles “simulem”o comportamento alg´ebrico dos n´umeros reais, permitindo que propriedades de sistemas que necessitem de propriedades alg´ebricas dos n´umeros reais possam ser derivadas quando estes s˜ao representados por inter- valos. 1 Veja as sess˜oes 4.1 - 4.3. 2 Veja sess˜oes 4.4 - 4.6. 75

4.1 Igualdade e Existˆencia

Deﬁni¸c˜ao 4.1.1.

A rela¸c˜ao de igualdade ´e uma fun¸c˜ao booleana Eq: A × A → {0,1}, definida por

Eq(a, b) =

1, se a e b “s˜ao os mesmos”; ou 0, caso contr´ario.

e que satisfaz as seguintes propriedades: 1. Eq(a,a) = 1 (Reflexividade);

2. Eq(a,b) _{→ Eq(b,a) = 1 (Simetria);}

3. (Eq(a,b) ∧ Eq(b,c)) → Eq(a,c) = 1 (Transitividade).

para todo a,b e c; onde 1 ´e o maior elemento da ´algebra booleana {0, 1}, ≤.

Pela propriedade de simetria e pelas leis da l´ogica proposicional, pode-se demonstrar que “Eq(a,b)_{→ Eq(b,a) = 1 e Eq(b,a) → Eq(a,b) = 1”; e, portanto de acordo com [11], “Eq(a,b)} ≤ Eq(b,a) e Eq(b,a) ≤ Eq(a,b)”. Assim, pode-se reescrever as propriedades da igualdade como:

Deﬁni¸c˜ao 4.1.2.

1. Eq(a,a) = 1 (Reflexividade); 2. Eq(a,b) = Eq(b,a) (Simetria); e

Toma-se como exemplo a igualdade entre fun¸c˜oes:

“Dado duas fun¸c˜oes f : a → b e g: c → d , f = g se e somente se dom(f) = a = c = dom(g) e para todo x ∈ dom(f),f(x) = g(x)”.

Entretanto, o que acontece quando pretende-se levar em considera¸c˜ao objetos parcial- mente definidos? Toma-se como exemplo a fam´ılia das fun¸c˜oes cont´ınuas reais parcialmente definidas sobre . Em s´ımbolos:

=_{∪{[O → ]|O ∈ U},} (4.1)

onde _{U ´e a topologia euclideana. Neste caso, tem-se que trabalhar com fun¸c˜oes par-} cialmente definidas. Como seria ent˜ao, uma l´ogica capaz de formalizar a rela¸c˜ao entre a existˆencia da fun¸c˜ao e a igualdade entre as mesmas? A resposta seria: uma l´ogica sem presumir a existˆencia dos objetos ou “free-logic”.

Belgede Gazâlî'nin düşünce sisteminde aklın yeri (sayfa 39-42)