# Trying to construct a model for this algebraic specification

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

-
Doesn't $f(f(x))=x$ mean that $f(f(a))=f(c)=a$? – Thomas Andrews Dec 21 '11 at 15:54
Yes, I guess it does... Does that prove anything? :) – Linus Dec 21 '11 at 16:00
Only that your definition of a model with $f(c)=C$ is not gonna work. – Thomas Andrews Dec 21 '11 at 16:07
Oh, you're right! That was a typo, though :P – Linus Dec 21 '11 at 16:08
Can the initial model have $f(b)=b$? I don't know this area, but if "initial" is much like "initial" in category theory, then that would mean that every model had $f(b)=b$. Under the definition I'd expect for "initial," your initial model would be something like $\{A,B,C,D\}$ with $f(A)=C$, $f(C)=A$, $f(B)=D$ and $f(D)=B$. Basically, you're need to model $\{a,b,c,f(b)\}$. – Thomas Andrews Dec 21 '11 at 16:25

Ah, okay, I've found definitions:

http://jedidiah.stuff.gen.nz/essays/algebraic_specification.html


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.]

-
YES! Thank you so much! That's really helpful. – Linus Dec 21 '11 at 17:32