[SCL] (abstract) vocabulary redux

[Robert E. Kent]

Here is a sharpened definition of an (abstract) SCL vocabulary.

For any name-set N, the term-set trm(N) is the fixpoint solution of the set
operator F(X) = N + (X x seq(X)) consisting of the sum of N and the binary
Cartesian product between the set X and the set of X-sequences. As the
fixpoint solution, the term-set trm(N) comes equipped with two injections
into it: an element map from the name-set N and an application map from the
binary Cartesian product between the set trm(N) and the set of
trm(N)-sequences. The image of the element map is called the set of
elementary N-terms. These are the N-terms that are just names. The image of
the application map is called the set of composite N-terms. These are the
N-terms of the form (t, seq) for N-term t and N-term sequence seq.

For any name-set N, an (abstract) vocabulary V is a triple (O, R, F), where
O is a subset of N-terms, and R and F are subsets of O. The set of N-terms O
is partitioned into two subsets O = elem(O) + comp(O), where elem(O) is the
set of elementary N-terms in O and comp(O) is the set of composite N-terms
in O. We make the following requirements.

1. elem(O) = N; that is, all of the names in N are used in O. This means
that the inclusion map of N into O is the pullback of the element map of N
into the term-set trm(O) along the inclusion map of O into the term-set
trm(N).

2. comp(O) = O - elem(O) = O - N; that is, the set of composite terms of
O are the terms of the form (t, seq) for N-term t and N-term sequence seq.
Hence, the inclusion map of comp(O) into the set of terms trm(O) factors
through the binary Cartesian product between the set of terms trm(N) and the
set of trm(N)-sequences. That is, there is an injective map from comp(O) to
this product. We make the requirement: the composition of this injective map
with the (two) product projections factor through F and the set seq(O) of
sequences of O, respectively. This means that from comp(O) there are two
surjective maps to F and to seq(O), respectively. Call these maps the
function and sequence selectors. They are important for defining
interpretations.

Robert E. Kent
rekent at ontologos.org