Article View: comp.specification.z
Article #71Re: Boolean Valued Functions?
From: Steve King
Date: Sun, 30 Aug 1992 15:48
Date: Sun, 30 Aug 1992 15:48
31 lines
1444 bytes
1444 bytes
In article <1992Aug29.214201.28617@sctc.com> fine@sctc.com (Todd Fine) writes:
>
>On page 125 of Spivey's "The Z Notation, A Reference Manual" (1st edition),
>disjoint is declared as:
>
> disjoint _ : P (I \pfun P X)
>
>On page 62 of the manual, the type rules for function application are
^^^^^^^^^^^^^^^^^^^^
>given as:
> (rest deleted)
>Todd Fine
>fine@sctc.com
Here's the problem: in the *predicate* disjoint <A,B>, you're not dealing
with function application, but with an object (`disjoint') from the
syntactic category Pre-Rel, together with its expression.
All is clear on p73 of ZRM (1st edition).
On p48, you can see that disjoint is given as the only example of the
syntactic category Pre-Rel.
I haven't checked it, but I'd hope that all the types will work properly now.
Steve King
Programming Research Group
Oxford University Computing Laboratory
11 Keble Rd
Oxford OX1 3QD
Technical Details
Message-ID:
<1992Aug30.154848.12403@client66.client66.comlab>Path:
arc1-ca.pugleaf.net!sparky!uunet!math.fu-berlin.de!news.netmbx.de!Germany.EU.net!mcsun!uknet!comlab.ox.ac.uk!kingReferences:
<1992Aug29.214201.28617@sctc.com>Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!sparky!uunet!math.fu-berlin.de!news.netmbx.de!Germany.EU.net!mcsun!uknet!comlab.ox.ac.uk!king From: king@client66.comlab (Steve King) Newsgroups: comp.specification.z Subject: Re: Boolean Valued Functions? Message-ID: <1992Aug30.154848.12403@client66.client66.comlab> Date: 30 Aug 92 15:48:48 GMT References: <1992Aug29.214201.28617@sctc.com> Organization: Oxford University Computing Laboratory, UK Lines: 31 Originator: king@client66.comlab