🚀 go-pugleaf

In ZRM, a generic constant definition is restricted to having a value
uniquely determined for each possible formal parameter.
Now, I think it is sometimes useful to be able to define a generic
object, without having to state this uniqueness condition.
We could call this object a "generic variable" and any standard generic
constant could be considered a particular instance of a generic variable.

For example, I would like to define basic properties of any partial order
among values of an as-yet-unknown type X with a generic variable
definition

         ===[X]==========================
         |
         |    G  :   X <-> X
         |
         |----------------------
         |
         |    -- reflexivity --
         |    -- antisymmetry --
         |    -- transitivity --
         |___________________________


After defining a generic variable G, we would need to be allowed to add
further constraints about it, by means of a predicate used as a
paragraph, as though G were a common global variable.

For example, I would like to constrain the previously defined generic
variable G to be  total.

  But above all, we would need to be allowed to add constraints about
"any instance" of G, without affecting any other instance of G.

For example, if N is the set of natural numbers, I would like to
constrain the instance G[N]  to be the usual order _<=_ , writing

      G[N]  =  (_<=_)


I am very interested in your opinion about the feasibility of the
extension to Z, and in your knowledge of any literature about it.

Thank you in advance.

address: Donatella Castelli
  IEI - CNR
  via  S. Maria 46, Pisa
  Italy

e_mail:  castelli@iei.pi.cnr.it