Re: Z Errors in Shape Expressions 1.0 Definition

Peter,

You asked:

>> How are you going to handle the non-Z part of the definition?

There are two kinds of non-Z parts of a spec. The first kind is the
precise English restatement of each Z definition. The second kind is
the English-only statement of some aspect of the spec that you decide
not to formalize, typically things like performance, security
considerations, etc. By "English" I, of course, mean any natural
language.

Eric,

You asked:

>>Is it the case that Z typechecks all but the return type of recursive invocations (which you must then test by thinking)?

Z treats functions as sets of ordered pairs, so there is no difference
in the type-checking behavior of inputs and outputs. An output must
always have the type that matches the declared codomain of the
function. e.g. given the declaration

f: X -> Y

then the statement

f(x) = expr

is type-correct if x is a member of the type of X and expr is a member
of the type of Y.

BTW, I never understood the statement that "Z can't handle recursion".
In fact, it can. You first have to declare the function and then add
an axiom that defines the function.

I'll review the ShEx spec and look for where recursion is causing difficulty.

-- Arthur


On Thu, Mar 19, 2015 at 8:40 AM, Peter F. Patel-Schneider
<pfpschneider@gmail.com> wrote:
> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
> Yes, the parts that use evalRule', which include the ValueReference - @
> construct, the AndRule - , construct, the XorRule - | construct, and the
> GroupRule (,) construct.
>
> peter
>
>
> On 03/19/2015 03:29 AM, Eric Prud'hommeaux wrote:
>> * Peter F. Patel-Schneider <pfpschneider@gmail.com> [2015-03-19
>> 01:56-0700]
>>> Arthur,
>>>
>>> How are you going to handle the non-Z part of the definition?
>>
>> Is it the case that Z typechecks all but the return type of recursive
>> invocations (which you must then test by thinking)?
>>
>>
>>> peter
>>>
>>
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v1
>
> iQEcBAEBAgAGBQJVCsPMAAoJECjN6+QThfjzhX4IAMa39MmSN6+Gs2oiiruZ6s06
> WIyQ6uUReC0goptW3DerkGL4bUiqjuHrWjle8SlGzO3JCRLWXW0qw7eBXLyTpwp8
> YK//i9ZkvEtr+bnoPaVYepMHtb13Zr82lRz9fbJvpV+JbBiMFAxhi70gAcP8OCF1
> nfEt0pmagU6oDGoGyNc6CP+HmXFcyxLGa5I4HAfznQlgz0tDpij1IT68aC7TYk4A
> OEpgbA9COlIP0HbkQcqozoDjUfb2UrRlAHr7E0mt5MABZj1a5VzEg7owzFwmqS/M
> p3dpgbdzc8PLPFHQFzLokDxtQ1SxMcWXaKLxau3qm3eCWRoVgaENT3bBpRckomQ=
> =OJro
> -----END PGP SIGNATURE-----

Received on Thursday, 19 March 2015 13:50:58 UTC