[SCL] alternate notions for vocabulary and interpretation

[Robert E. Kent]

I have been thinking about the example '(((f a) a) a)' discussed in the SCL
Core Semantics and have been playing around with the following alternate
definition of vocabulary and interpretation. An additional motivation is to
define an abstract (text-independent) notion of vocabulary and
interpretation.

The vocabulary of any SCL text T is a sextuple
(ON, RN, FN, OT, RT, FT)
where ON is the set of names of T in object position,
where RN is the set of names of T in relation position,
where FN is the set of names of T in function position,
where OT is the set of terms of T in object position,
where RT is the set of terms of T in relation position, and
where FT is the set of terms of T in function position,
satisfying
any elementary term in OT is in ON,
any elementary term in RT is in RN, and
any elementary term in FT is in FN
and
for any composite term (t, t1, ... tn) in OT or RT or FT
t is in FT and ti is in OT for 1 <= i <= n.

A bare interpretation of this vocabulary has
a nonempty set U called the universe and three maps
int : ON --> U,
rel : RN --> rel(U), and
fun : FN --> fun(U).

A folded interpretation is a bare interpretation with three extended maps
int* : OT --> U,
rel* : RT --> rel(U), and
fun* : FT --> fun(U),
and two folds
relation : RU --> rel(U) with RU a subset of U and
function : FU --> fun(U) with FU a subset of U,
where
if x is in both ON and RN 
then int(x) is in RU and relation(int(x)) = rel(x),
if x is in both ON and FN 
then int(x) is in FU and function(int(x)) = fun(x),
and where
int* restricts to int for elementary terms in OT,
rel* restricts to rel for elementary terms in RT,
fun* restricts to fun for elementary terms in FT,
and
for any composite term (t, seq) in OT
the value of fun*[t] applied to the sequential extension int*[seq]
is int*[(t, seq)],
for any composite term (t, seq) in RT
the value of fun*[t] applied to the sequential extension int*[seq] 
is some z in RU and rel*[(t, seq)] = relation[z], and
for any composite term (t, seq) in FT
the value of fun*[t] applied to the sequential extension int*[seq] 
is some y in FU and fun*[(t, seq)] = function[y].

Robert E. Kent
rekent at ontologos.org