Boolean model containing both confusion and junk

192 Views Asked by At

I'm doing a course in Equational Programming, and really new to these materials.

So we got a specification for Booleans:

spec Booleans
    sorts bool
    functions:
        true : -> bool
        false : -> bool
        and : bool # bool -> bool
        or : bool # bool -> bool
        not : bool -> bool
    equations:
        [B1] and(true,x) = x
        [B2] and(false,x) = false
        [B3] not(true) = false
        [B4] not(false) = true
        [B5] or(x,y) = not(and(not(x),not(y)))
end Booleans

Let $\mathfrak{A}$ be a model for specification $((S, \Sigma), E)$, $\mathfrak{A}$ contains junk if $\mathfrak{A}$ contains elements that are not the interpretation of a closed term. A contains confusion if $\mathfrak{A}$ identifies two closed terms t and u, without t = u being derivable from E. Or formally:

"no junk": $\forall a \in A \; s.t. \exists t \in {Ter}_\Sigma \; s.t. \; {eval}_{\mathfrak{A}}(t) \equiv a$

"no confusion" : $\forall t, u \in {Ter}_{\Sigma}({eval}_{\mathfrak{A}}(t) \equiv {eval}_{\mathfrak{A}}(u)) \Rightarrow E \vdash t = u$

Now one of the questions was to give a model for the specification booleans s.t. it would have both confusion and junk (in the same model)

The TA didn't think it possible but couldn't prove it. I've done some googling afterwards and found the book Foundations of Algebraic Specification and Formal Software Development, I couldn't entirely read it (only parts are available online, I'm not rich enough to buy on good faith), apparently in section 2.5.3 (page 57) they claim their spec does have a model containing both junk and confusion.

I simply already don't understand what such a model would be like (containing both confusion and junk), let alone construct a model for the spec above.

With the spec above, is a model with both confusion and junk possible, if not why not?

Any help would greatly be appreciated.

Edit: added definitions of confusion and junk for future reference.

1

There are 1 best solutions below

0
On BEST ANSWER

There is no model with both junk and confusion, assuming I am interpreting those words correctly (I am using the definitions given here). First note that it is easy to deduce from the given equational axioms that every term with no variables must be equal to either $\mathtt{true}$ or $\mathtt{false}$ (B1-B4 tell you how to evaluate $\mathtt{not}$ and $\mathtt{and}$, and then B5 reduces evaluting $\mathtt{or}$ to $\mathtt{not}$ and $\mathtt{and}$). So the only way you can have confusion in a model is if $\mathtt{true}=\mathtt{false}$. But in that case, axioms B1 and B2 together tell you that for any $x$, $x=\mathtt{and}(\mathtt{true},x)=\mathtt{and}(\mathtt{false},x)=\mathtt{false}$. So in any model with confusion, every element is equal to $\mathtt{false}$, so there is no junk.

(In the language of abstract algebra that is probably more familiar to most readers here, what we are proving here is that if $B$ is a Boolean algebra such that the map from the initial Boolean algebra to $B$ is not injective, then the map from the initial Boolean algebra to $B$ is surjective. This is just because the only way it can fail to be injective is if $0=1$ in $B$, which can only happen in the trivial Boolean algebra.)