typically specified via the collection of values of the
type; for instance, the type natural
is introduced in terms of the
collection {naturals}. This exploits the special handling I give to types in my
specification for denotations of formulaic
collections delimited with {
and }.
A relation is a formal description of a predicate
involving two unresolved names (i.e. a
two-name relationship),
canonically left
and right. If (denotations for) values x and y
are substituted in place of the two names, x in place
of left and y in place
of right, the predicate becomes
a statement
: if this statement is true, we say that the relation
(describing the predicate) relates x to y
, otherwise not.
In so far as a relation, r, relates some value, x, to some value, y, I
describe x as a left value
of r and y as a right value
of r.
Example: left is an ancestor
of right
is a predicate of the canonical form;
if I am substituted for right and one of my
(living) ancestors is substituted for left, the
statement is true; so the associated relation relates each of my (living)
ancestors to me. Everyone (except Adam and Eve) is a right value of this
relation: every parent is a left value of it.
A
collection is a relation subsumed by the universal identity (: x←x :),
i.e. a relation which relates x to y only if x and y are the same value (and
typically subject to some further restriction on this value). A collection is
synonymous with (and encodes, as a relation) a predicate involving only one
unresolved name (a
one-name relationship). If C is
a collection and relates x to x, then x is said to be in
C (as a special
case of a general reading of fixed
points) and x is described as a member of
C.
See {relations}, above. The
template relation relates
left to right
matches a great many sub-texts of
what I've written: in each, relation denotes a
relation describing some two-name relationship, of
which left and right
denote a left value and a right value, respectively.
See {mappings} above.
Written by Eddy.