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.
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.
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 …
Denotes (left:relation|) and asserts that (|relation:) conforms to (:left|).
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:
from U to Vwhen 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)}.
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).
Written by Eddy.