1
$\begingroup$

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

  • 0
    (Although I guess I also don't know what "confusion" and "junk" mean, so I might be premature in saying your model for the first part satisfies the conditions.)2011-12-21

1 Answers 1

1

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

  • 0
    YES! Thank you so much! That's really helpful.2011-12-21