[BLD] proposed text for interpretations

Michael,

Herewith a proposal for a definition of interpretations with extensible
datatype support. Since you dislike datatype maps so much, I avoided
using them.



Primitive datatypes. Some symbol spaces symsp, called primitive data
types, have a value space, denoted VSsymsp, and a mapping from the
lexical space to the VSsymsp, denoted Lsymsp.
[JB: I think the value space and the lexical-to-value mapping needs to
be defined before the interpretation is defined, because they do not
depend on the interpretation]


Truth values. Interpretations assign a truth value to every formula.

The set of truth values is denoted by TV. For RIF-BLD, TV includes only
two values, t (true) and f (false). (See end note on truth values.)

In RIF, TV has a total or partial order, called the truth order, and
denoted with <t. In RIF-BLD, f <t t, and it is a total order. (See end
note on ordering truth values.)
[JB: I think it is not necessary to intermingle the definition of truth
values with the definition of an interpretation]


Basic semantic structures. Given a set of datatypes DT which includes
all data types supported by RIF, a basic semantic structure, I, is a
tuple of the form <D,IC, IV, IF, IR>, where

* D, called the domain of I, is a non-empty countable set of elements,

* IC is a mapping from Const to elements of D, such that for every
symbol l^^u in Const,

  *   if u is a datatype in DT, then IC(l^^u)=Lu(l),

* IV is a mapping from Var to elements of D,

* IF is a mapping from Const to functions from D* into D (here D* is a
set of all tuples of any length over the domain D), and

* IR is a mapping from Const to partial truth-valued mappings D* → TV.

The equality predicate = is interpreted as identity on D, i.e.: IR(=) is
a truth-valued mapping such as IR(=)(<a,a>) = t for every a ∈ D; it maps
any other pair of elements of D to f. IR(=) is undefined on other
elements of D* (tuples of length other than 2).

.....

Semantic structures and the entailment would also need to be defined
with respect to a set of datatypes DT.
-- 
                         debruijn@inf.unibz.it

Jos de Bruijn,        http://www.debruijn.net/
----------------------------------------------
In heaven all the interesting people are
missing.
  - Friedrich Nietzsche