# End-Relations

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.

## Restrictions and end-relations with assertions

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).
Written by Eddy.