I'm studying for an exam on lambda-calculus and algebraic specifications, and I'm having trouble figuring out this problem. I was wondering if anyone here could help??
The given specification:
S: sorts O
Σ: constants
a: -> O
b: -> O
c: -> O
function
f: O -> O
E: equations
[1] f(a) = c
[2] f(f(x)) = x
Now, first off, I'm looking for a model that has three elements and contains confusion, but no junk. Right now I have: A = {A,B,C} , a = A, b = B, c = C, f(a) = C, f(b) = B and f(c) = A. I thought the confusion would arise from f(b) = B = b, but I'm not sure this works...
As a second question, I'm looking for the correct initial model for this specification.
Any help would be greatly appreciated!!
Regards,
Linus
Ah, okay, I've found definitions:
Your model has "confusion" because $f(b)=b$ is an axiom for you model, which isn't true in your original algebraic specification. It doesn't have junk because all its elements correspond only to your constants.
$\{a=A,b=B,c=C,D\}$ and $\mathcal f$ defined to send $A\to C$, $C\to A$, $B\to D$, and $D\to B$, is an initial model. It has no junk because only $D$ doesn't correspond with any of the constants, but $D=\mathcal f(B)$.
On the other hand, this model has no confusion because no expressions in the specification language which is not deducible from the axioms is true for this model.[That seems non-trivial to me to prove, however. It seems more obvious that any expression true for this model will be true for all models.]