Groups | Search | Server Info | Login | Register

Groups > comp.specification.z > #369

Re: assertions about parts of schema

Show all headers | View raw

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...

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