Re: comments on 0.93: variable declarations

[Chris George <cwg@iist.unu.edu>]

Please forgive me if this reply is not relevant to CoFI: I am not
at all up to date and it may have been discussed before.

[I don't think that it has in CoFI - but there are papers by 
Meseguer and Goguen on the topic, e.g., "Initiality, induction,
and computability", in Algebraic Methods in Semantics, CUP, 1985.  
Perhaps the discussion in the message by Till Mossakowski on 5 Oct 
is also relevant?  BTW, would some of you please indicate whether you
agree with Till's recommendation concerning logic or not?  --PDM]

There is a problem in RAISE at least with global quantification of
variables (and the corresponding "forall" construct was removed for
this reason).

"forall" was defined as equivalent to universally quantifying each of
the axioms within its scope (which is also Gianna Reggio's proposal).
Consider the following (and excuse the RSL syntax) which contains two
axioms within the scope of "forall":

  axiom
  forall e : Elem, s : Stack :-

  is_empty(empty) is true,

  is_empty(push(e,s)) is false
  
Any axiom quantified over an empty type is vacuously true.  Hence
if we want in a proof to use the first axiom, which does not mention
"e" or "s", we would need to prove that the types Elem and Stack are
not empty.  This is tedious but possible for Stack (since we have the
constant empty) but typically impossible for Elem because it is a
parameter.    

There is a nice paradox here that in a world where all stacks are
necessarily empty, because nothing can be pushed onto them, it is
impossible to prove it!

So we need to write the example 

  axiom

  is_empty(empty) is true,

  all e : Elem, s : Stack :- is_empty(push(e,s)) is false

(where "all" is the standard universal quantifier).

[So perhaps one could interpret variable declarations as
quantifying only over the variables *used* in each axiom?
Or just leave the axioms open??  --PDM]

Of course, the remark about empty types applies just as well to the
second axiom, but in any proof involving it there are almost certainly
"e" and "s" values around and the problem never arises.

-- 

Regards,
	  Chris George

	  Senior Research Fellow
          International Institute for Software Technology
	  United Nations University (UNU/IIST)
	  P.O.Box 3058
	  Macau

          e-mail: cwg@iist.unu.edu
	  tel: +853 712 930
          fax: +853 712 940
          www: http://www.iist.unu.edu/Ccwg