The PRED-SORT-DEFN declares the first SORT; it declares the
embedding of this as a subsort of the second SORT, which must
already be declared in the local environment; and it asserts that the
values of the subsort are precisely (the projections of) those values
of the variable VAR from the supersort for which the FORMULA holds.
The variable VAR must occur
Note that the only terms of the supersort that are also in the subsort
are explicit projections, expressed using the CAST construct
(described in the next section).
A predicative sort definition PRED-SORT-DEFN determines the
values of a new subsort of a previously-declared sort, by taking just
those values for which a formula holds. It provides an explicit
specification of the values of a subsort, in contrast to the implicit
specification provided by using subsort declarations and overloaded
function symbols.
BASIC-ITEM ::= ... | PRED-SORT-DEFN
PRED-SORT-DEFN ::= pred-sort-defn SORT VAR SORT FORMULA
[TM]
Freely? (Yes)
Discharged:
Seems obvious, but maybe adjust wording.
in the FORMULA, and its scope is
restricted to the FORMULA.
[AT]
Why must VAR occur in FORMULA? I can see no
need for this requirement. After all we might want to define a full
subsort (by the formula true) or an empty subsort (by the
formulae false), or even a subsort that is either full or empty
depending on whether a given sentence (closed formula) is true or
false in a given model.
Discharged:
The variable is not required to occur.
Any other variables occurring in the
FORMULA must be explicitly declared by enclosing quantifications.
[TM]
...unless the subsort and the supersort
are made isomorphic by a subsequent ISO-DECL? Or should this
be forbidden?
(Should be forbidden)
Discharged:
The first sentence is correct, except that "subsequent" makes no
sense because of non-linear visibility. The wording needs to be
adjusted. There is a suggested formulation in
ftp://ftp.brics.dk/Projects/CoFI/Notes/S-4/
but this would need to be adjusted to take account of non-linear
visibility.
CoFI
Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk