assertions about parts of schema

[David Lamb]

I have a situation that corresponds roughly to:

\begin{schema}{Small} x1: ...; xn: ... \end{schema}
\begin{schema}{Big}
Small \\
... \end{schema}

\begin{schema}{Other}
v1: Big;
v2: Big
\where
% v1's variables defined in Small equal v2's variables defined in small
\end{schema}

However, I don't know how to write the assertion in the comment. It
seems to me I ought to be able to use \project and perhaps \theta
somehow but I've not understood those portions of Z well enough, and
keep getting syntax errors in fuzz with various things I try. I'd rather
not resort to
v1.x1 = v2.x2 \land ... \land v1.xn = v2.xn

Any suggestions?

[phil.c...@lineone.net]

Assuming you meant to say

v1.x1 = v2.x1 \land ... \land v1.xn = v2.xn
^

(note difference indicated by ^) then how about just writing

v1 = v2

[David Lamb]

On 02/04/2013 5:01 PM, phil.c...@lineone.net wrote:
>
> Assuming you meant to say
>
> v1.x1 = v2.x1 \land ... \land v1.xn = v2.xn
> ^
>
> (note difference indicated by ^) then how about just writing
>
> v1 = v2

I goofed in failing to point out that Big introduces its own variables
w1...wm which shouldn't be part of the comparison.

[phil.c...@lineone.net]

On Wednesday, April 3, 2013 2:17:20 AM UTC+1, David Lamb wrote:
> I goofed in failing to point out that Big introduces its own variables
>
> w1...wm which shouldn't be part of the comparison.

I should have spotted that the ellipsis was part of the signature in schema Big.

With Standard Z, schemas really are sets whose elements are bindings. This makes things easier because e.g. {v1} is a schema (containing a single binding). So you could write

({v1} ⨡ S) = ({v2} ⨡ S)

To avoid concerns about v1 and v2 not satisfying the predicate in S, i.e. concerns that ({vi} ⨡ S) = {}, I would recommend writing

({v1} ⨡ σ S) = ({v2} ⨡ σ S)

where σ (sigma) is a function that gives the signature of its schema argument, i.e. removes the predicate, which you can define as follows, as in [1]:

σ[X] == λ S : ℙ X ⦁ X

Using σ would also make proof easier.

Alternatively, you could write

(μ {v1} ⦁ θS) = (μ {v2} ⦁ θS)

which avoids σ.

No doubt there are other ways to write this in Standard Z, possibly less ugly ways. For Spivey Z, I don't believe that the above ideas work because a schema reference cannot be of the form {b} for some binding b. I can't think of a solution for Spivey Z.

However, all that said, given that you want to link the Small parts of the Big schema, perhaps it is worth defining

\begin{schema}{Big}
s : Small \\
... \end{schema}

Then you can just say

v1.s = v2.s



1. http://www-users.cs.york.ac.uk/susan/bib/ss/zpattern/383.pdf
Chapter 12, page 110.

[phil.c...@lineone.net]

On Wednesday, April 3, 2013 10:29:51 PM UTC+1, phil.c...@lineone.net wrote:
> For Spivey Z, I don't believe that the above ideas work because a schema reference cannot be of the form {b} for some binding b. I can't think of a solution for Spivey Z.

In fact, thinking some more, one can write the schema {b} in Spivey Z as

{Big | θBig = b}

so, following previous suggestions, I think you could write

(\{Big | \theta Big = v1\} \project \sigma Small) = (\{Big | \theta Big = v2\} \project \sigma Small)

assuming

\begin{zed}
\sigma [X] == (\lambda S : \power X @ X)
\end{zed}

or (with a little massaging)

(\mu Big | \theta Big = v1 @ \theta Small) = (\mu Big | \theta Big = v2 @ \theta Small)

Nicer answers on a postcard...

[phil.c...@lineone.net]

On Wednesday, April 3, 2013 11:34:53 PM UTC+1, phil.c...@lineone.net wrote:
> In fact, thinking some more, one can write the schema {b} in Spivey Z as
>
>
>
> {Big | θBig = b}

Provided b ∈ Big. Given this, the benefit of using σ probably goes.

> so, following previous suggestions, I think you could write
>
> (\{Big | \theta Big = v1\} \project \sigma Small) = (\{Big | \theta Big = v2\} \project \sigma Small)

To be valid Spivey, I think that should have been:

([Big | \theta Big = v1] \project \sigma Small) = ([Big | \theta Big = v2] \project \sigma Small)

Perhaps better still, with no \mu or \project:

(\{Big | \theta Big = v1 @ \theta Small\}) = (\{Big | \theta Big = v2 @ \theta Small\})

[David Lamb]

On 03/04/2013 5:29 PM, phil.c...@lineone.net wrote:
> On Wednesday, April 3, 2013 2:17:20 AM UTC+1, David Lamb wrote:
>> I goofed in failing to point out that Big introduces its own variables
>>
>> w1...wm which shouldn't be part of the comparison.
>
> I should have spotted that the ellipsis was part of the signature in schema Big.
>
> With Standard Z, schemas really are sets whose elements are bindings. This makes things easier because e.g. {v1} is a schema (containing a single binding).

Thanks for all your help. I'll eventually need to upgrade to Standard Z
and tools that process it, but for now am using Spivey.

So you could write
>
> ({v1} ⨡ S) = ({v2} ⨡ S)

Thurderbird isn't displaying the character before the S properly for me.
What symbol is it?

[phil.c...@lineone.net]

On Thursday, April 4, 2013 10:08:56 PM UTC+1, David Lamb wrote:
> On 03/04/2013 5:29 PM, phil.c...@lineone.net wrote:
>
> > On Wednesday, April 3, 2013 2:17:20 AM UTC+1, David Lamb wrote:
>
> >> I goofed in failing to point out that Big introduces its own variables
>
> >>
>
> >> w1...wm which shouldn't be part of the comparison.
>
> >
>
> > I should have spotted that the ellipsis was part of the signature in schema Big.
>
> >
>
> > With Standard Z, schemas really are sets whose elements are bindings. This makes things easier because e.g. {v1} is a schema (containing a single binding).
>
>
>
> Thanks for all your help. I'll eventually need to upgrade to Standard Z
>
> and tools that process it, but for now am using Spivey.

You're welcome. I use ProofPower for all my Z work as it provides high-assurance proof support that is programmable.

> So you could write
>
> >
>
> > ({v1} ⨡ S) = ({v2} ⨡ S)
>
>
>
> Thurderbird isn't displaying the character before the S properly for me.
>
> What symbol is it?

Schema projection, i.e. \project. Did the other symbols all appear ok?

[David Lamb]

On 04/04/2013 6:01 PM, phil.c...@lineone.net wrote:
> On Thursday, April 4, 2013 10:08:56 PM UTC+1, David Lamb wrote:
>> On 03/04/2013 5:29 PM, phil.c...@lineone.net wrote:
>>

>>> With Standard Z, schemas really are sets whose elements are bindings. ...

>>
>> Thanks for all your help. I'll eventually need to upgrade to Standard Z
>> and tools that process it, but for now am using Spivey.
>
> You're welcome. I use ProofPower for all my Z work as it provides high-assurance proof support that is programmable.

Thanks! I'll look into installing it.

>> So you could write
>>> ({v1} ⨡ S) = ({v2} ⨡ S)
>>
>> Thurderbird isn't displaying the character before the S properly for me.
>> What symbol is it?
>
> Schema projection, i.e. \project. Did the other symbols all appear ok?

Yes, all else was fine, including theta.