Groups | Search | Server Info | Login | Register

Groups > comp.specification.z > #368

Re: assertions about parts of schema

Show all headers | View raw

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.

Back to comp.specification.z | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

assertions about parts of schema David Lamb <dalamb@cs.queensu.ca> - 2013-03-30 16:02 -0400
  Re: assertions about parts of schema phil.clayton@lineone.net - 2013-04-02 14:01 -0700
    Re: assertions about parts of schema David Lamb <dalamb@cs.queensu.ca> - 2013-04-02 21:17 -0400
      Re: assertions about parts of schema phil.clayton@lineone.net - 2013-04-03 14:29 -0700
        Re: assertions about parts of schema phil.clayton@lineone.net - 2013-04-03 15:34 -0700
          Re: assertions about parts of schema phil.clayton@lineone.net - 2013-04-03 23:41 -0700
        Re: assertions about parts of schema David Lamb <dalamb@cs.queensu.ca> - 2013-04-04 17:08 -0400
          Re: assertions about parts of schema phil.clayton@lineone.net - 2013-04-04 15:01 -0700
            Re: assertions about parts of schema David Lamb <dalamb@cs.queensu.ca> - 2013-04-04 20:37 -0400

csiph-web