UNIVERSIDADE da MADEIRA
Departamento de Matemática e Engenharias
FUNDAMENTOS LÓGICOS E ALGÉBRICOS DA PROGRAMAÇÃO
Licenciaturas em Engenharia Informática, Ensino de Informática e Matemática
2º Semestre 2005/2006
Folha de exercı́cios nº 8
Especificações Algébricas. LOTOS - Álgebra de Dados
Definição (Assinatura): Uma assinatura é um par < S, Σ >, onde:
• S é um conjunto finito, não vazio, de sı́mbolos de espécie, designados por géneros.
• Σ : Ω → S∗ × S
Ω = C ∪ OP , em que C, OP são conjuntos disjuntos:
– C é um conjunto de constantes, ou construtores, que verificam a condição f irstΣ(c) =<>,
em que f irst indica a primeira componente de um par ordenado.
– OP é um conjunto de operações, que verificam a condição f irstΣ(op) 6=<>.
1. Considere a assinatura dos números naturais, definida da seguinte forma no LOTOS:
sorts
opns
N at
0 : → N at
succ : N at → N at
+ , ∗ : N at, N at → N at
Determine os conjuntos S, C, OP e Σ desta assinatura.
Definição (Álgebra): Dada uma assinatura < S, Σ >, uma Σ-álgebra A é um par < AS , AΩ >,
em que:
• A cada espécie s ∈ S corresponde um comjunto portador AS (s).
• A cada operação σ : S1 × S2 × · · · × Sn →
| Sσ está associada uma função com entradas e
saı́das nos conjuntos portadores correspondentes
AΩ (σ) : AS (S1 ) × AS (S2 ) × · · · × AS (Sn ) →
| AS (Sσ ).
1
2. Considere a assinatura definida da seguinte forma no LOTOS:
sorts
opns
Bool
true, f alse : → Bool
not : Bool → Bool
and , or : Bool, Bool → Bool
(a) Determine os os conjuntos S, C, OP e Σ desta assinatura.
(b) Apresente duas interpretações distintas para esta assinatura, i.e., indique duas
Σ-álgebras diferentes correspondentes a esta assinatura.
3. Considere a assinatura seguinte, onde se incluem as operações de igualdade e desigualdade
de números naturais:
sorts
opns
N at, Bool
0 : → N at
succ : N at → N at
+ , ∗ : N at, N at → N at
true, f alse : → Bool
not : Bool → Bool
and , or : Bool, Bool → Bool
eq , ne : N at, N at → Bool
Sendo x, y e 0, respectivamente duas variáveis e uma constante de espécie N at e definindo
ΞS = {x, y} dê exemplos de:
(a) Σ-termos da espécie N at.
(b) Ξ-termos de cada uma das espécies N at e Bool.
(c) Termos TΣ∪Ξ de cada uma das espécies N at e Bool.
Equações: Dada uma assinatura < S, Σ > e um conjunto de variáveis Ξ, as equações possuem
a forma (∀Ξ)t1 = t2 , onde t1 e t2 são dois termos da mesma espécie (i.e., t1 , t2 ∈ (TΣ∪Ξ )s ).
Portanto, uma equação é uma fórmula da lógica de predicados de primeira ordem com um único
predicado, a igualdade.
4. Escreva as equações para cada uma das espécies (Bool e N at) da assinatura do exercı́cio
anterior.
Definição (Equação condicional): Dada uma assinatura < S, Σ > e um conjunto de variáveis
ΞS , uma equação condicional é um triplo de termos TΣ∪Ξ . Um dos termos é obrigatoriamente
de espécie Bool e os outros dois termos devem ser da mesma espécie.
2
5. Escreva as equações condicionais para a assinatura especificada abaixo:
sorts
opns
Set, Element, Bool
{} : → Set
Insert, Remove : Element, Set → Set
eq , ne : Element, Element → Bool
eqns
f orall x, y : Element, s : Set
of sort Set
Insert(x, Insert(x, s)) = Insert(x, s);
Insert(x, Insert(y, s)) = Insert(y, Insert(x, s));
Remove(x, {}) = {};
6. Defina o isomorfismo entre as duas álgebras iniciais que apresentou no exercı́cio 2 − (b).
7. (Substituição de um termo) Considerando os conjuntos X = {x, w} e Y = {y}, o termo
2 ∗ x ∗ w + 1 e a função h = {w 7→ 3 + y}, indique a que é igual a fórmula (2 ∗ x ∗ w + 1)X
h .
Definição (Derivação): Dados dois termos t0 , t1 ∈ TΣ∪Ξ da mesma espécie s, t1 deriva t0 ,
t0 ⊢ t1 se for aplicada uma das seguintes regras de cálculo equacional:
(1) Reflexividade: ⊢ (∀X)t = t
(2) Simetria: (∀X)t = t′ ⊢ (∀X)t′ = t
(3) Transitividade: (∀X)t = t′ , (∀X)t′ = t′′ ⊢ (∀X)t = t′′
′
X
(4) Congruência: (∀X)t = t′ ⊢ (∀XY )tX
h = th em que h : X → TΣ∪X∪Y .
Substituição de variáveis por outros termos podem ser efectuadas em simultâneo nos dois
lados da equação.
′
X
(5) Eliminação de quantificadores: (∀X)t = t′ ⊢ (∀Y )tX
h = th em que h : X → TΣ∪Y e
Y ⊆ X.
Variáveis podem ser eliminadas em simultâneo nos dois lados da equação.
8. Considerando as equações da espécie N at que apresentou no exercı́cio 4. e a equação de
comutatividade da soma (∀m, n)m + n = n + m, prove que 0 + Succ(0) ∗ 0 = 0.
Tipos de dados: No LOTOS, um tipo de dados é identificado pelas espécies e pelas equações.
Os tipos de dados são definidos segundo as seguintes regras sintácticas:
Tipo dados
::=
Lista typ
Par formais
::=
::=
type Id typ is Lista typ
Par formais Espécies Equações
endtype
ǫ | Id typ {Id typ}*
ǫ
3
A lista de espécies Lista typ, indicada após a palavra chave is, importa as definições de
espécies e de equações de outros tipos de dados.
Um novo tipo de dados pode ser criado pela simples alteração dos identificadores de um tipo
de dados já existente.
Tipo dados
::=
Actualização
::=
type Id typ is Lista typ Actualização
sortnames {Id esp for Id esp}+
opnnames {Id oper for Id oper}+
endtype
renamedby
9. Defina o tipo de dados F lag a partir da alteração dos identificadores do tipo de dados
Bool (alterar true para set, f alse para clear, not para toggle).
Parametrização de tipos: Quando existem tipos de dados que contêm operações com as
mesmas propriedades, diferindo apenas nas espécies (por exemplo as listas de inteiros e de
booleanos), é útil definir um tipo de dados parametrizado, da seguinte forma:
Par formais
::=
formalsorts {Id esp for Id esp }+
formalopns {Id oper for Id oper}+
As espécies e operações formais devem ser actualizados com espécies e operações concretas:
Actualização
::=
actualizedby Id typ using
10. Consideremos o caso particular de uma lista, designada por pilha, em que o último elemento
é inserido no topo da pilha.
type Queue is
f ormalsorts Element
f ormalopns e0 : → Element
sorts Queue
opns
create : → Queue
add : Element, Queue → Queue
top : Queue → Element
eqns
f orall x, y : Element, q : Queue
of sort Element
top(create) = e0;
top(add(x, q)) = x;
top(add(y, add(x, q))) = top(add(y, q));
endtype
A partir deste tipo de dados, defina o tipo de dados N atQueue que representa uma pilha
de naturais (a espécie formal Element e a operação e0 devem ser actualizados, respectivamente, pela espécie N at e pelo construtor 0).
4