Comments to CoFI X, version 0.93

[till@informatik.uni-bremen.de (Till Mossakowski)]

Comments to CoFI X, version 0.93

The splitting of part I into a many-sorted and a sub-sorted
part helps a lot!
I found it rather difficult to follow part III, some more words 
about the intended semantics would help.


1.3. and 3.3. Sentences

In the institution, we need sentences in which all subterms
have assigned a unique sort and all functions and predicates
have assigned a unique profile.
This can be achieved more easily by allowing not only
terms to be qualified by sorts, but also function and
predicate names to be qualified by profiles.


1.4 Satisfaction

Variable assingments are total in the present proposal.
If also partial variable assignments are allowed, the
institution remains equally expressive but the
substitution theory (and thus theorem proving)
becomes simpler (as simple as in the total case).
I see three possibilities:
1. total variable assignments  => the substitutions rule
   has to take into account definedness:
   A(x), D(t)
   ----------
     A(t)

   but the quantifier rules are as in the total case: 

   forall x.A(x)
   -------------
       A(x)

2. partial variable assignments, but quantification is
   over defined values
   ==> Simpler substitution rule
   A(x)
   ---
   A(t)

   but the quantifier rules have now to take care of
   definedness (because free variables have a semantics
   different from bound variables)

   forall x.A(x)
   -------------
   D(x) ==> A(x)

   Open axioms have to state definedness explicitly
   x,y:nat. D(x) /\ D(y) ==> x*y=y*x
   but closed axioms not:
   forall x,y:nat. x*y=y*x

3. partial variable assignments, and quantified variables
   may be undefined as well ==> same semantics for free
   and bound variables, and the simpler substitution
   rule AND simpler quantifier rules (see above)

   But now open and closed axioms have to care about definedness:
   x,y:nat. D(x) /\ D(y) ==> x*y=y*x
   forall x,y:nat. D(x) /\ D(y) ==> x*y=y*x

I prefer 2., because quantifier elimination and introduction
seems to occur less often than substitution, and 2. keeps substitution
simple. Of course, the semantics of open formulas are somewhat 
peculiar, but the axioms written down in the language could be taken to
be closed (or if open, then with semantics due to 1.), 
while open formulas (with semantics due to 2.) merely occur as intermediate
steps in the theorem proving process (but they have to be given
a semantics different to 1. if the simple substitution rule shall be sound). 

References:
D. S. Scott, Identity and Existence in Intuitionistic Logic,
Lecture Notes in Mathematics 753, pages 660-696.

L. Bachmair and H. Ganzinger, Rewrite Techniques for Transitive Relations,
Proc. 9th IEEE Symposium on Logic in Computer Science 1994,
pages 384-393.


Typo: the last symbol of 1.4 should be S', not S.


2.2.3, 2.2.4, 4.2.1, 4.2.2 Atomic formulas and terms

I would prefer to let 
- "well-sortedness" mean that a sort can
   be assigned to all subterms of a term (or a formula),
- "well-formedness" mean that the ambiguity resulting
  from having different such assignments can be resolved,
- "fully sortedness" mean that additionally each function
  and predicate symbol is qualified with a profile.

Then in the language, we may write down well-formed formulas,
the institution consists of fully (sub)sorted formulas being
special well-formed formulas, and well-formed formulas
(from the language) can be translated to fully (sub)sorted formulas
(in the institution) in a way which is unique up to
semantical equivalence.

The study note on subsorting also follows this terminology.


4.1.1 Sorts

I prefer the OBJ 3 approach:

SORT-DECL      ::= sort-decl SORT+
SUBSORT-DECL   ::= subsort-decl SORT+ leq SORT+

which allows to introduce arbitrary subsorting relations
on declared sorts. See the study note on subsorting for arguments.


4.2.2 Terms

>actually, we forbid expansions that insert cast injections
>just anove or below sort annotations

That's consistent with the study note on subsorting,
but while formulating the technical details, (most of) the 
authors of the study note find it easier to drop this
restriction and allow explicit qualification of functions
and predicates by profiles instead. Then the purpose of
this restriction (allowing to determine profiles through
qualifications) is achieved more directly.


4.4 Sort generation, 6.2 Specification expressions

An ID-MAP should allow the user also to select profiles,
but this selection cannot be made in an arbitrary way:
it has to select whole connected components wrt
the overloading relation.
See the study note on subsorting.


5. Structuring Concepts

Parameters may have fixeds parts (why?), but where is
this taken care of in section 6?


6.1 Specification libraries, 6.2 Specification expressions

Consider the extension

spec1= sorts s
spec2= enrich spec1 by 
       opns f:s->s

In a linear-section, this is o.k., while in a cyclic-section,
the empty spec is assigned to spec1 in the first iteration step,
making spec2 ill-formed.

6.3. Parameterized Specifications

PAR-INST is used but not defined.