🚀 go-pugleaf

In the following, I'll use the following notation:

   P = \power, < ... > = \langle ... \rangle, Z = \num

On page 125 of Spivey's "The Z Notation, A Reference Manual" (1st edition),
disjoint is declared as:

   disjoint _ : P (I \pfun P X)

Laws given for disjoint include:

   disjoint <A,B> \iff A \cap B = \empty

On page 62 of the manual, the type rules for function application are
given as:

   In the expression E_1 E_2, the sub-expression E_1 must have type
   P (t_1 \cross t_2), and E_2 must have type t_1, for some types
   t_1 and t_2.  The type of the whole expression is then t_2.

Suppose A and B are of type P t.  Then, <A,B> is of type P (Z \cross P t).
For disjoint <A,B> to be well typed:

   t_1 = P (Z \cross P t)

   P (t_1 \cross t_2)  = P ( (P (Z \cross P t)) \cross t_2) =
      P (I \pfun P X) = P (P (I \cross P X)) for some I and X

Letting I = Z and X = t almost works, but what about the "\cross t_2"?
Since disjoint <A,B> appears to return either true or false, it seems
that t_2 must be {true,false}.

By equating a set and its characteristic function, I can see how "disjoint Y"
could be viewed as being equivalent to "Y \in disjoint".

The type rules given for \in are that if E_1 has type t in "E_1 \in E_2",
then E_2 must have type P t.  So, the requirement for "<A,B> \in disjoint"
to be well typed is:

   P P (Z \cross P t) = P (P (I \cross P X)) for some I and X

So, choosing I = Z and X = t makes it work out alright.

Is there some place I'm missing in the reference manual where it says that:

   E_1 E_2 == E_2 \in E_1 when E_2 has type t and E_1 has type P t, and
   E_1 E_2 == "apply E1 to E2" when E_2 has type t and E_1 has type
               P (t \cross t_2)

Can someone clear this up?

Todd Fine
fine@sctc.com