Questions about ShEx Z specification

I have a question about the ShEx Z specification, related to the
specification of functions.

Are the signatures given for the various function definitions correct? They
definitely seem unidiomatic.

Functions are specified in a Miranda/ML/Haskell style
Z functions only take a single argument;  cartesian products are used for
functions of with more than one argument :

The set X → Y contains all the total functions from X to Y : they relate
each member of X to exactly one member of Y . The notation f (x ) can be
used if f is a function: the value of this expression is that unique
element of Y to which x is related by f . Functions with several arguments
are modelled by letting the set on the left of the arrow be a Cartesian
product: in a sense, they do not have many arguments, but only one, which
happens to be a tuple.

Spivey 1992, p. 27 <http://spivey.oriel.ox.ac.uk/mike/zrm/zrm.pdf>


The definition of triplesForSubject in the ShEX specification only defines
the result of apply the result of triplesForSubject to a graph; it  does
not define the result of calling triplesForSubject on it's only argument
(the RDFTerm).


triplesForSubject : RDFTerm → Graph → Graph
--------------------------------------------------------------------------------------------------

∀ subj : RDFTerm; g : Graph • triplesForSubject subj g = {t : g | t.s =
subj }


If triplesForSubject is intended to be a function returning a function, it
could be defined as:


triplesForSubject : RDFTerm → Graph → Graph
--------------------------------------------------------------------------------------------------

∀ subj : RDFTerm • triplesForSubject subj =  (λ g : Graph • {t : g | t.s =
subj })

If it is only intended to be defined when both the RDFTerm and Graph are
present, the signature could be:


triplesForSubject : RDFTerm × Graph → Graph
--------------------------------------------------------------------------------------------------
∀ subj : RDFTerm; g : Graph • triplesForSubject subj g = {t : g | t.s =
subj }

It's been a long time since I last paid attention to Z, and  as someone who
preferred Hope style function declarations, this may be something I'm
overly sensitive to, but it does suggest that there might not be sufficient
familiarity with Z to make it appropriate for use in this context.

Simon

Received on Sunday, 20 July 2014 17:08:22 UTC