On 31/05/2012 02:57 PM, Invisible wrote:

> Ha! Yes, SEqual{} is already defined. It also doesn't /work/. o_O
>
> The mistake is simple. SEqual{} calls SSubset{}, and SSubset{} has a
> bug.

> In short, I've mixed up "exists" and "for all". Kind of an important
> distinction, that one.
>
> Logic Box of course doesn't /have/ an explicit for-all construct. At
> this point I am uncertain whether I can work around that...

A /correct/ definition for SSubset{} is

SSubset{subset, superset}:
   (subset = End[]) |
   (~head ~tail
     subset = Node[head, tail] &
     SMember{head, superset} &
     SSubset{tail, superset}
   )
;

Before SSubset{} would accept any pair of sets where just one element is 
common to both sets. Now it only works if /all/ of the elements of the 
subset are elements of the superset. (I.e., it works correctly now.)

This in turn causes SEqual{} to function correctly.

It's quite slow, but

   SEqual{List[1, 2, 3], List[3, 1, x]}

does eventually yield x := 2.

QED.

Post a reply to this message