These denotational forms build on
my restriction notation for relations,
replacing some uses of : with uses
of | to either induce a relation on the left or
right values of a relation or assert a compatibility between two such
relations facing each other

across a | in
the modified notation.

- ( | relation : [ right ] )
- Let r = (: relation
: [ right ] ). The denoted relation relates a
to c precisely if {i: r relates a to i} subsumes {i: r relates c to i} and
neither is empty. The final condition makes this a relation among the left
values of r; I call it the
**left-relation**of the given (: relation : [ right ] ). - ( [ left ] : relation | )
- Let r = ( [ left ]
: relation :). The denotated relation relates a
to c precisely if {i: r relates i to a} subsumes {i: r relates i to c} and
neither is empty. The final condition makes this a relation among the right
values of r; I call it the
**right-relation**of the given ( [ left ] : relation :).

I'll extend these, below, to allow | in place of the : when left or right (as appropriate) is given; these variants shall add assertions relating relation to the restriction.

Collectively, I describe each of these as
an **end-relation**. Because subsume is transitive and
reflexive, so are end-relations. Consequently, intersecting one with its
reverse necessarily yields an equivalence; I'll refer to these
as **end-equivalences**, variously the left-equivalence and
right-equivalence. When e is an end-relation, I'll refer to values as
e-equivalent if e relates each to the other. Since an end-relation is
reflexive, its values are fixed points, hence in

the end-relation;
thus, for given relation r, {right values of r} = {x in (:r|)} = (r:x←x:)
and {left values of r} = {x in (|r:)} = (:x←x:r).

Prior to 2004/June, I defined these two denotational forms to denote the end-equivalences, rather than end-relations themselves (and a whole lot earlier than that, I used the same forms to denote the end-collections); and defined the conformance notion below in terms of those – there may yet be ghosts of that in texts here. I also transiently had the right-end relation defined reversed during July 2004 – hopefully I've fixed that, though.

I now introduce variations on the restriction denotations above in which
a : between two relations may be replaced with
a | to assert (without changing the relation
denoted) a relationship between the end-relations facing one another

across the |. The asserted relationship is
expressed, for transitive reflexive relations e and c,
as e conforms to c

iff (e:c|) subsumes c and e subsumes (e:c:e)

. Note that neither e nor c
necessarily subsumes the other, all the same. Crucially, any reflexive
transitive c conforms to itself and to {x in c}; and any collection, e, conforms
to c if (e:c|) subsumes c.

- ( [ left ] : [ relation ] | right )
- ( left | [ relation ] : [ right ] )
- ( left | [ relation ] | right )
All three denote the same relation as ([left]:[relation]:[right]), but each adds assertions wherever that uses a : in place of a | in this template.

In the first form, the assertion is that ([left]: [relation] |) conforms to (|right:); in the second form, the assertion is that (| [relation] :[right]) conforms to (:left|); the final form makes both of the given assertions. Likewise …

- ( left | relation | )
Denotes (left:relation|) and asserts that (|relation:) conforms to (:left|).

- ( | relation | right )
Denotes (|relation:right) and asserts that (:relation|) conforms to (|right:).

Note that no provision is made for denotations of form (|r|)

with an unconstrained | at each end.

Examples:

- The conventional idiom of mappings
from U to V

when U and V are collections says that the mapping must accept all members of U, while all its outputs must lie in V; which is tersely expressed by f = (V:f|U), given that U and V are collections; and the collection of such mappings is simply {mapping (V:|U)}. - Finiteness, at least for a collection N, can be expressed by the
equation {mapping (N|:N)} = {monic (N:|N)}, known as
the pigeon-hole principle

. A mapping (N|:N) is given to have only members of N as inputs (right values), and to have all members of N as outputs (left values). When N is finite such a mapping, with only one output per input, can only yield enough outputs if it in fact accepts all members of N as inputs and doesn't map any two to the same output; which is just to say that it is a monic (N:|N). Note that, in general, the reverse of a monic (N:|N) is a mapping (N|:N).