[SCL] (abstract) vocabulary redux

[Pat Hayes]

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

Yes, but this style of presentation is WAY too, er, sharp for the 
intended audience. We need to produce a document that can be read and 
understood by software developers.

Thanks for your efforts, though.

Pat

>
>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
>
>
>
>_______________________________________________
>SCL mailing list
>SCL at philebus.tamu.edu
>http://philebus.tamu.edu/mailman/listinfo/scl


-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes at ihmc.us       http://www.ihmc.us/users/phayes