Groups | Search | Server Info | Login | Register


Groups > comp.specification.z > #370

Re: assertions about parts of schema

X-Received by 10.224.157.1 with SMTP id z1mr2727141qaw.8.1365057672300; Wed, 03 Apr 2013 23:41:12 -0700 (PDT)
X-Received by 10.49.132.70 with SMTP id os6mr467750qeb.4.1365057672279; Wed, 03 Apr 2013 23:41:12 -0700 (PDT)
Path csiph.com!v102.xanadu-bbs.net!xanadu-bbs.net!news.glorb.com!ca1no28628657qab.0!news-out.google.com!ef9ni1849qab.0!nntp.google.com!ca1no28628651qab.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups comp.specification.z
Date Wed, 3 Apr 2013 23:41:12 -0700 (PDT)
In-Reply-To <3aa3f63b-cb64-4de2-a9ca-79fbc596d85a@googlegroups.com>
Complaints-To groups-abuse@google.com
Injection-Info glegroupsg2000goo.googlegroups.com; posting-host=86.132.178.141; posting-account=v7gx3AoAAABfjb9m5b7l_Lt2KVEgQBIe
NNTP-Posting-Host 86.132.178.141
References <kj7g95$vfe$1@dont-email.me> <01418bc9-dcb9-4915-9781-1dfd1c2a6c04@googlegroups.com> <kjfvqi$6qp$1@dont-email.me> <505bd5c0-c9e3-4dab-87bb-bb43ab2d9944@googlegroups.com> <3aa3f63b-cb64-4de2-a9ca-79fbc596d85a@googlegroups.com>
User-Agent G2/1.0
MIME-Version 1.0
Message-ID <346da566-2ee8-42fe-ae39-e5bb3b32447b@googlegroups.com> (permalink)
Subject Re: assertions about parts of schema
From phil.clayton@lineone.net
Injection-Date Thu, 04 Apr 2013 06:41:12 +0000
Content-Type text/plain; charset=UTF-8
Content-Transfer-Encoding quoted-printable
Xref csiph.com comp.specification.z:370

Show key headers only | View raw


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\})

Back to comp.specification.z | Previous | NextPrevious 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