Shape Expressions 1.0 Definition

1. Introduction

The Shape Expressions Language (ShEx) is used to specify formal constraints on the content of RDF graphs and are intended to be used to validate RDF documents, communicate expected graph patterns for interfaces and to generate forms and validation code. ShEx can be used to:

• Describe the contents of an RDF graph
• Express invariants about an RDF triple store
• Define a predicate that can be tested against an RDF graph instance
• Define a set of rules that can be used to generate forms, validation code and other constructs in specific target languages

Information about the use, grammar and syntax of ShEx can be found at http://www.w3.org/2013/ShEx/. This document describes the formal semantics of the ShEx language using the Z specification language, beginning with a Z specification of the characteristics of an RDF Graph that are referenced by ShEx.

The output from ExtractZed.xsl produces text parsable with fuzz -d .

Display LaTeX for Z notation (or press 'z')

2 The RDF Data Model in Z

The formal definition for an RDF graph in RDF 1.1 Concepts and Abstract Syntax[RDF11-CONCEPTS]:

“An RDF graph is a set of RDF Triples”

“An RDF triple consists of three components:

• the subject, which is an IRI or a blank node
• the predicate, which is an IRI
• the object, which is an IRI, a literal or a blank node”

“... IRIs, literals and blank nodes are distinct and distinguishable.”

provides a definition in Z:

\begin{zed}
Graph == \power Triple
\end{zed}
        

The ShEx language treats IRIs and blank nodes as primitive types, which are defined as Z free types:

\begin{zed}
[IRI, BlankNode]
\end{zed}
        

The ShEx language can express constraints on both the type and content of literals, which are modeled separately:

“A literal in an RDF graph consists of two or three elements:

• a lexical form, being a Unicode string...
• a datatype IRI, being an IRI
• if and only if the datatype IRI is
  http://www.w3.org/1999/02/22-rdf-syntax-ns#langString, a non-empty language tag as defined in [BCP47]. The language tag MUST be well-formed according to section 2.2.9 of [BCP47].”

This is modelled by String and LanguageTag as free types:

\begin{zed}
[String, LanguageTag]
\end{zed}
        

\begin{zed}
TypedLiteral \defs \\
\t1	[lexicalForm:String ; dataType:IRI | \\
\t2		dataType \neq XSD\_String]
\also
PlainLiteral \defs \\
\t1	[lexicalForm:String ; dataType:IRI; langTag:LanguageTag | \\
\t2		dataType = XSD\_String]
\also
RDFLiteral ::= pl \ldata PlainLiteral \rdata | tl \ldata TypedLiteral \rdata
\end{zed}
        

“IRIs, literals and blank nodes are collectively known as RDF terms

RDFTerm ::=

iri《IRI》|

literal《RDFLiteral》|

bnode《BlankNode》

\begin{zed}
RDFTerm ::= \\
\t1	iri \ldata IRI \rdata | \\
\t1	literal \ldata RDFLiteral \rdata | \\
\t1	bnode \ldata BlankNode \rdata
\end{zed}
        

\begin{schema}{Triple}
   s,p,o:RDFTerm
\where
   iri \entryFor s \in IRI \lor bnode \entryFor s \in BlankNode \\
   iri \entryFor p \in IRI \\
   iri \entryFor o \in IRI \lor bnode \entryFor o \in BlankNode \lor literal \entryFor o \in RDFLiteral
\end{schema}
        

\begin{gendef}
   triplesForSubject:RDFTerm \fun Graph \fun Graph
\where
   \forall subj:RDFTerm; g:Graph @ triplesForSubject~subj~g = \{t:g | t.s = subj \}
\end{gendef}
		

\begin{gendef}
   triplesForObject:RDFTerm \fun Graph \fun Graph
\where
   \forall obj:RDFTerm; g:Graph @ triplesForObject~obj~g = \{t:g | t.o = obj \}
\end{gendef}
		

\begin{axdef}
XSD\_String:IRI \\
SHEX\_IRI:IRI \\
SHEX\_BNODE:IRI \\
SHEX\_LITERAL:IRI \\
SHEX\_NONLITERAL:IRI
\end{axdef}
        

3 Shape Expression Evaluation

A Shape Expression Schema is a collection of labeled rules where exactly one rule in the collection is identified as the outermost or “starting” rule. In addition, any rule that is referenced within the Schema is also itself a member of the Schema Formally:

Schema
rules:Label⇸Rule
start:Label
start∈ domrules
∀ r:ranrules •
(r∈ rangroup⇒ (group⋅r).rule∈ domrules)∧
(r∈ ranand⇒ ran(and⋅r)⊆ domrules)∧
(r∈ ranxor⇒ ran(xor⋅r)⊆ domrules)∧
(r∈ ranarc∧ (arc⋅r).valueSpec∈ ranvalueRef⇒
(valueRef⋅(arc⋅r).valueSpec)∈ domrules)

\begin{schema}{Schema}
   rules:Label \pfun Rule \\
   start:Label
\where
   start \in \dom rules \\
\forall r:\ran rules @ \\
\t1 (r \in \ran group \implies (group \entryFor r).rule \in \dom rules) \land \\
\t1 (r \in \ran and \implies \ran (and \entryFor r) \subseteq \dom rules) \land \\
\t1 (r \in \ran xor \implies \ran (xor \entryFor r) \subseteq \dom rules) \land \\ 
\t1 (r \in \ran arc \land (arc \entryFor r).valueSpec \in \ran valueRef \implies \\
\t2 (valueRef \entryFor (arc \entryFor r).valueSpec) \in \dom rules)
\end{schema}
		

While existing ShEx implementations define a rule Label as being either an IRI or a BlankNode, the type of Label does not impact the evaluation semantics. For our purposes, we can simply define it as a separate free type:

\begin{zed}
[Label]
\end{zed}
		

The validity of a given RDF Graph is determined by taking the start Rule of a ShEx Schema and a reference IRI and evaluating the validity of the Rule against the supplied graph.

Formally, the evaluate function takes a Schema, a Graph and a reference IRI and, if the start Rule in the Schema, in the context of the starting Schema and graph, returns either nomatch (z) or pass (p) then the function returns pass. In all other cases, the function returns fail (f ).

\begin{gendef}
   evaluate:Schema \fun Graph \fun IRI \fun OptValidity
\where
\forall s:Schema; g:Graph; i:IRI; v:OptValidity; ec:EvalContext | \\
\t1 ec.graph = g \land ec.schema = s @ \\
\t2		evaluate ~s ~g ~i = \\
\t3			\IF evalRule ~ec ~ (iri~ i)~ (s.rules~ s.start) \in \{\nomatch, \pass\} \\
\t3			\THEN \pass \ELSE \fail
\end{gendef}
        

4 Rule Evaluation

A ShEx Rule is a set of constraints that can be evaluated against a reference RDFTerm in the context of a given Schema and RDF Graph:

\begin{zed}
EvalContext \defs [schema:Schema; graph:Graph]
\end{zed}
		

Formally, the evalRule function takes an EvalContext, a reference RDFTerm and a Rule and returns one of the following:

• Pass (p) - the supplied Graph satisfied the evaluation Rule
• Fail (f ) - the supplied Graph did not satisfy the evaluation Rule
• Nomatch (z) - an optional GroupRule was encountered and there were no matching triples
• None (∅) - an ArcRule was encountered with a minimum cardinality of 0 and there were no matching triples
• Error(ε) - an XorRule was evaluated and two or more components passed the evaluation.

\begin{zed}
OptValidity ::= \pass | \fail | \nomatch | \none | \error \\
\end{zed}
        

• ArcRule – selects the subset of the graph having the reference RDFTerm as the subject and matching predicates and and validates the resulting objects
• RevArcRule – selects the subset of the graph having the reference RDFTerm as the object and matching predicates and and validates the resulting subjects
• GroupRule – identifies a Rule and declares it as optional and/or describes a set of external Actions to be evaluated if the inner Rule passes.
• AndRule – identifies a set of Rules, all of which must pass when evaluated against the supplied Graph and EvalContext
• XorRule – identifies a set of Rules, exactly one of which must pass when evaluated against the supplied Graph and EvalContext

\begin{zed}
Rule ::= \\
\t1	arc \ldata ArcRule \rdata | \\
\t1 rarc \ldata RevArcRule \rdata | \\
\t1 group \ldata GroupRule \rdata | \\
\t1 and \ldata AndRule \rdata | \\
\t1 xor \ldata XorRule \rdata \\
\end{zed}
        

\begin{gendef}
   evalRule:EvalContext \fun RDFTerm \fun Rule \fun OptValidity
\where
   \forall ec:EvalContext; i:RDFTerm; r:Rule @ evalRule~ec~i~r = \\
\t1 \IF r \in \ran arc \\
\t2 \THEN evalArcRule~ec~i~(arc \entryFor r) \\
\t1 \ELSE \IF r \in \ran rarc \\
\t2 \THEN evalRevArcRule~ec~i~(rarc \entryFor r) \\
\t1 \ELSE \IF r \in \ran group \\
\t2 \THEN evalGroupRule~ec~i~(group \entryFor r) \\
\t1 \ELSE \IF r \in \ran and \\
\t2 \THEN evalAndRule~ec~i~(and \entryFor r) \\
\t1 \ELSE \\
\t2 evalXorRule~ec~i~(xor \entryFor r)
\end{gendef}
        

evalRule':EvalContext→ RDFTerm→ Label→ OptValidity
∀ ec:EvalContext; l:Label • l∈ domec.schema.rules

\begin{gendef}
   evalRule':EvalContext \fun RDFTerm \fun Label \fun OptValidity
\where
   \forall ec:EvalContext; l:Label @ l \in \dom ec.schema.rules
\end{gendef}
		

\begin{schema}{ArcRule}
   filter:PredicateFilter \\
   valueSpec:ObjectSpecification \\
   min, max:\optional[\nat] \\
   actions:\power Action
\where
   (\# min = 1 \land \# max = 1) \implies value~ min \leq value~ max
\end{schema}
		

\begin{gendef}
   evalArcRule:EvalContext \fun RDFTerm \fun ArcRule \fun OptValidity
\where
   \forall ec:EvalContext; s:RDFTerm; ar:ArcRule; sg:Graph | \\ 
\t1 sg = evalPredicateFilter~ar.filter~(triplesForSubject~ s~ ec.graph) @ \\
\t2		evalArcRule~ec~s~ar = \\
\t3 \IF evalCardinality~sg~ar.min~ar.max \neq \pass \\
\t4 \THEN evalCardinality~sg~ar.min~ar.max \\
\t3 \ELSE \IF evalObjectSpecification~ec~ar.valueSpec~sg \neq \pass \\
\t4 \THEN evalObjectSpecification~ec~ar.valueSpec~sg \\
\t3 \ELSE \\
\t4  dispatch~ ar.actions~ sg~ ec 
\end{gendef}
		

\begin{zed}
IRIorStem ::= iosi \ldata IRI \rdata | ioss \ldata IRIstem \rdata \\
PredicateFilter ::= pfIRI \ldata IRIorStem \rdata | pfWild \ldata \power IRIorStem \rdata
\end{zed}
		

\begin{zed}
[IRIstem]
\end{zed}
		

\begin{gendef}
	IRIstemRange:IRIstem \pfun \power IRI
\end{gendef}
		

\begin{gendef}
   evalPredicateFilter:PredicateFilter \pfun Graph \pfun Graph
\where
   \forall f:PredicateFilter; g:Graph @ evalPredicateFilter~ f ~g = \\
\t1 \IF f \in \ran pfIRI \THEN evalIRIorStem~ (pfIRI \entryFor f)~ g \\
\t1 \ELSE evalWild~ (pfWild \entryFor f)~ g
\end{gendef}
		

\begin{gendef}
   evalIRIorStem:IRIorStem \pfun Graph \pfun Graph
\where
   \forall e:IRIorStem; g:Graph @ evalIRIorStem~ e ~g = \\
\t1 \IF e \in \ran iosi \THEN \{t:g | iri \entryFor t.p = iosi \entryFor e \} \\
\t1 \ELSE \{t:g | iri \entryFor t.p \in IRIstemRange~ (ioss \entryFor e) \}
\end{gendef}
		

\begin{gendef}
   evalWild:\power IRIorStem \pfun Graph \pfun Graph
\where
   \forall es:\power IRIorStem; g:Graph @ evalWild ~es ~g = \\
\t1 \{t:g | t \notin \bigcup \{e:es @ evalIRIorStem~e~g\} \}
\end{gendef}
		

\begin{zed}
MatchValue ::= \\
\t1	mviri \ldata IRI \rdata | \\
\t1	mviris \ldata IRIstem \rdata | \\
\t1 mvlit \ldata RDFLiteral \rdata
\also
ObjectSpecification ::= \\
\t1	valueType \ldata IRI \rdata | \\
\t1 valueSet \ldata \power MatchValue \rdata | \\
\t1 osWild \ldata \power MatchValue \rdata | \\
\t1 valueRef \ldata Label \rdata
\end{zed}
		

\begin{gendef}
   evalCardinality:Graph \fun \optional[\nat] \fun \optional[\nat] \fun OptValidity
\where
   \forall g:Graph; min, max:\optional[\nat] @ evalCardinality~g~min~max = \\
   \t1 \IF \# min = 1 \land \# g = 0 \land  value~ min = 0 \\
\t2 \THEN \nomatch \\
\t1 \ELSE \IF \# g = 0 \\
\t2 \THEN \none \\
\t1 \ELSE \IF (\# min = 1 \land \# g < value~ min) \lor \\
\t3 (\# max = 1 \land \# g > value~ max) \\
\t2 \THEN \fail \\
\t1 \ELSE \pass
\end{gendef}
		

\begin{gendef}
   evalObjectSpecification:EvalContext \fun ObjectSpecification \fun Graph \fun \\
\t1 OptValidity
\where
   \forall ec:EvalContext; os:ObjectSpecification; g:Graph @ \\ evalObjectSpecification~ec~os~g = \\
\t1 \IF \forall t:g @ evalObjectSpecificationTriple~ec~os~t.o = \pass \\
\t2		\THEN \pass \\
\t2		\ELSE \fail
\end{gendef}
		

\begin{gendef}
   evalObjectSpecificationTriple:EvalContext \fun ObjectSpecification \fun \\
\t1 RDFTerm \fun OptValidity
\where
   \forall ec:EvalContext; os:ObjectSpecification; n:RDFTerm @ \\
\t1	evalObjectSpecificationTriple~ec~os~n = \\
\t2 \IF os \in \ran valueType \THEN \\
\t3 evalValueType~(valueType \entryFor os)~n \\
\t2 \ELSE \IF os \in \ran valueSet \THEN \\
\t3 evalTermSet~(valueSet \entryFor os)~n \\
\t2 \ELSE \IF os \in \ran osWild \THEN \\
\t3 evalTermWild~(osWild \entryFor os)~n \\
\t2 \ELSE \\
\t3 evalTermReference~ec~(valueRef \entryFor os)~n
\end{gendef}
		

\begin{gendef}
   evalValueType:IRI \pfun RDFTerm \pfun OptValidity
\where
   \forall vt:IRI; n:RDFTerm; l:RDFLiteral @ evalValueType~vt~ n = \\
\t1 \IF vt = SHEX\_IRI \land  n \in \ran iri \THEN \pass \\
\t1 \ELSE \IF vt = SHEX\_BNODE \land  n \in \ran bnode \THEN \pass \\
\t1 \ELSE \IF vt = SHEX\_NONLITERAL \land  (n \in \ran iri \lor n \in \ran bnode) \THEN \pass \\
\t1 \ELSE \IF vt = SHEX\_LITERAL \land  n \in \ran literal \THEN \pass \\
\t1 \ELSE \IF n \in \ran literal \land l = (literal \entryFor n) \land \\
\t2 ((l \in \ran pl \land (pl \entryFor l).dataType = vt) \lor \\
\t2  (l \in \ran tl \land (tl \entryFor l).dataType = vt)) \THEN \pass \\
\t1 \ELSE \fail
\end{gendef}
		

\begin{gendef}
   evalTermSet:\power MatchValue \pfun RDFTerm \pfun OptValidity
\where
   \forall mvs:\power MatchValue; n:RDFTerm @ evalTermSet~mvs~n = \\
\t1	\IF \exists mv:mvs @ \\
\t2 ((mv \in \ran mviri \land n \in \ran iri \land (iri \entryFor n) = mviri \entryFor mv) \lor \\
\t2  (mv \in \ran mviris \land n \in \ran iri \land  \\
\t3 (iri \entryFor n) \in IRIstemRange ~ (mviris \entryFor mv) ) \lor \\
\t2  (n \in \ran literal \land mvlit \entryFor mv = literal \entryFor n)) \\
\t1 \THEN \pass \\
\t1 \ELSE \fail
\end{gendef}
		

\begin{gendef}
   evalTermWild:\power MatchValue \fun RDFTerm \fun OptValidity
\where
   \forall mvs:\power MatchValue; n:RDFTerm @ evalTermWild~mvs~n = \\
\t1 \IF evalTermSet~ mvs~ n = \pass \THEN \fail \ELSE \pass
\end{gendef}
		

\begin{gendef}
   evalTermReference:EvalContext \pfun Label \pfun RDFTerm \pfun OptValidity
\where
\forall ec:EvalContext; vr:Label; n:RDFTerm @ \\ 
\t1	evalTermReference~ec~vr~n = \\
\t2		\IF n \notin \ran literal \THEN evalRule'~ec~n~vr \\
\t2		\ELSE \fail
\end{gendef}
		

\begin{schema}{RevArcRule}
   filter:PredicateFilter \\
   valueSpec:SubjectSpecification \\
   min, max:\optional[\nat] \\
   actions:\power Action
\where
   (\# min = 1 \land \# max = 1) \implies value~ min \leq value~ max
\end{schema}
		

\begin{gendef}
   evalRevArcRule:EvalContext \fun RDFTerm \fun RevArcRule \fun OptValidity
\where
  \forall ec:EvalContext; o:RDFTerm; rar:RevArcRule; og:Graph  | \\ 
\t1 og = evalPredicateFilter~rar.filter~(triplesForObject~ o~ ec.graph) @ \\
\t2		evalRevArcRule~ec~o~rar = \\
\t3 		\IF evalCardinality~og~rar.min~rar.max \neq \pass \\
\t4 			\THEN evalCardinality~og~rar.min~rar.max \\
\t3 		\ELSE \IF evalSubjectSpecification~ec~rar.valueSpec~og \neq \pass \\
\t4 			\THEN evalSubjectSpecification~ec~rar.valueSpec~og \\
\t3 		\ELSE \\
\t4 			 dispatch~ rar.actions~ og~ ec 
\end{gendef}
		

\begin{zed}
SubjectSpecification ::=  \\
\t1	subjectSet \ldata \power MatchValue \rdata | \\
\t1 ssWild \ldata \power MatchValue \rdata | \\
\t1 subjectRef \ldata Label \rdata
\end{zed}
			

\begin{gendef}
   evalSubjectSpecification:EvalContext \fun SubjectSpecification \fun Graph \fun \\
\t1 OptValidity
\where
   \forall ec:EvalContext; ss:SubjectSpecification; g:Graph @ \\ 
\t1	evalSubjectSpecification~ec~ss~g = \\
\t2 	\IF \forall t:g @ evalSubjectSpecificationTriple~ec~ss~t.o = \pass \\
\t2		\THEN \pass \\
\t2 	\ELSE \fail
\end{gendef}
			

\begin{gendef}
   evalSubjectSpecificationTriple:EvalContext \fun SubjectSpecification \fun \\
\t1 RDFTerm \fun OptValidity
\where
   \forall ec:EvalContext; ss:SubjectSpecification; n:RDFTerm @ \\
\t1	evalSubjectSpecificationTriple~ec~ss~n = \\
\t2 	\IF ss \in \ran subjectSet \THEN \\
\t3 		evalTermSet~(subjectSet \entryFor ss)~n \\
\t2 	\ELSE \IF ss \in \ran ssWild \THEN \\
\t3 		evalTermWild~(ssWild \entryFor ss)~n \\
\t2 	\ELSE \\
\t3 		evalTermReference~ec~(subjectRef \entryFor ss)~n
\end{gendef}
			

\begin{zed}
OPT ::= OPTIONAL | REQUIRED
\also
GroupRule \defs [rule:Label; opt:OPT; actions:\power Action ] \\
\end{zed}
		

\begin{gendef}
   evalGroupRule:EvalContext \fun RDFTerm \fun GroupRule \fun OptValidity
\where
\forall ec:EvalContext; i:RDFTerm; gr:GroupRule @ \\
\t1	evalGroupRule~ ec~ i ~ gr = \\
\t2 	\IF evalRule'~ec~i~gr.rule = \none \land gr.opt = OPTIONAL \\
\t3 	\THEN \nomatch \\
\t2 	\ELSE \IF evalRule'~ec~i~gr.rule = \error \land gr.opt = OPTIONAL \\
\t3 	\THEN \fail \\
\t2 	\ELSE \IF evalRule'~ec~i~gr.rule = \pass \\
\t3 	\THEN dispatch~ gr.actions~ \emptyset ~ ec \\
\t2 	\ELSE \\
\t3			evalRule'~ec~i~gr.rule
\end{gendef}
		

\begin{gendef}
   And:OptValidity \fun OptValidity \fun OptValidity
\end{gendef}
		

\begin{zed}
AndRule == \seq_1 Label
\end{zed}
		

\begin{gendef}
   evalAndRule:EvalContext \fun RDFTerm \fun AndRule \fun OptValidity
\where
\forall ec:EvalContext; i:RDFTerm; r:AndRule  @ \\
\t1	evalAndRule~ec~i~r = \\
\t2		foldr~ And~ \nomatch ~ (map~(evalRule'~ec~i)~r)
\end{gendef}
		

\begin{gendef}
   Xor:OptValidity \fun OptValidity \fun OptValidity
\end{gendef}
		

\begin{zed}
XorRule == \seq_1 Label
\end{zed}
		

\begin{gendef}
   evalXorRule:EvalContext \fun RDFTerm \fun XorRule \fun OptValidity
\where
   \forall ec:EvalContext; i:RDFTerm; r:XorRule  @ \\
\t1	evalXorRule~ec~i~r = \\
\t2		foldr~ Xor~ \fail ~ (map~(evalRule'~ ec ~i)~ r)
\end{gendef}
		

5 Action evaluation

The dispatch function allows the evaluation / execution of arbitrary external “Actions”. While the evaluation of an Action can (obviously) have side effects outside the context of the ShEx environment, it must be side effect free within the execution context. In particular, an Action may not change anything in the EvalContext The action dispatcher exists to allow external events to happen. Parameters:

• as - the set of Actions associated with the GroupRule, ArcRule or RevArcRule
• g - the Graph that passed the ArcRule or RevArcRule. Empty in the case of GroupRule
• ec - the EvalContext containing the Schema and Graph

The dispatch function usually returns pass (p) or fail (f ), although there may also be cases for other OptValidity values in certain circumstances. The dispatch function always returns pass (p) if the set of actions is empty.

\begin{zed}
[Action]
\end{zed}
		

\begin{gendef}
   dispatch:\power Action \fun Graph \fun EvalContext \fun OptValidity
\where
   \forall as:\power Action; g:Graph; ec:EvalContext @ \\
\t1 as = \emptyset \implies dispatch~ as~ g ~ec = \pass
\end{gendef}
		

6 Parsing Rules

The semantics of the productions and terminals from the Turtle specification are defined in Turtle Terse RDF Triple Language section 7 Parsing.

The following grammar rules are mapped to the abstract syntax:

7 Appendix

\begin{gendef}[T]
   foldr:(T \fun T \fun T) \fun T \fun \seq T \fun T
\where
   \forall f:T \fun T \fun T; id:T; xs:\seq T @ \\
\t1	foldr~f~id~xs = \\
\t2 	\IF xs = \langle \rangle \THEN id \\
\t2 	\ELSE f~(head~xs)~(foldr~f~id~(tail~xs))
\end{gendef}
		

\begin{gendef}[A,B]
   map:(A \fun B) \fun \seq A \fun \seq B
\where
   \forall f:A \fun B; xs:\seq A @ \\
\t1	map~f~xs = \\
\t2 	\IF xs = \langle \rangle \THEN \langle \rangle \\
\t2 	\ELSE \langle f~(head~xs) \rangle \cat map~f~(tail~xs)
\end{gendef}
		

\begin{syntax}
FreeType ::= constructor \ldata source \rdata
\end{syntax}
		

\begin{axdef}
constructor:source \inj FreeType
\end{axdef}
		

\begin{syntax}
TravelDirections ::= \\
\t1	bus \ldata BusDirections \rdata | \\
\t1	walking \ldata WalkingDirections \rdata
\end{syntax}
		

\begin{syntax}
x \in TravelDirections
\where
\IF x \in \ran bus \THEN bus \entryFor x \ELSE walking \entryFor x
\end{syntax}
		

\begin{gendef}[X, Y]
\_  \entryFor \_ :(X \inj Y) \cross Y \pfun X
\where
\forall f:X \inj Y; y:Y @  \\
\t1	f \entryFor y = (\mu x:\dom f | f~x = y)
\end{gendef}
		

\begin{zed} 
  \optional[T] == \{ s:\power T \mid \# s \leq 1 \} \\
\end{zed}
		

\begin{gendef}[T]
   value:\power T \pfun T
\where
   \forall s:\power T @ value~ s = (\mu e:T | e \in s) 
\end{gendef}