From csus.edu!decwrl!decwrl!uunet!pipex!uknet!comlab.ox.ac.uk!vnet.IBM.COM Fri Aug  6 07:09:28 1993
Newsgroups: comp.specification.z
Path: csus.edu!decwrl!decwrl!uunet!pipex!uknet!comlab.ox.ac.uk!vnet.IBM.COM
From: ryman@vnet.IBM.COM (Arthur Ryman)
Subject: How Are Implicit Parameters to Generic Constants Inferred?
Message-ID: <19930805.170318.RYMAN@TOROLAB2>
Date: 05 Aug 93 17:03:17 EDT
X-Mailer: mail-news 2.0.3
Lines: 51

From:    Arthur Ryman
Phone:   (416) 448-3077, TIE  778-3077, FAX (416) 448-4414

The ZRM (first edition 3.9.2 p79) states that implicit parameters are
inferred from type information, but this seems wrong since we can use
generic constants with different sets of the same type and get different
constants. For example id {1} = {(1,1)} but 3.9.2 implies id {1} = id Z.

My problem arises with generic relations as in the following simplified
example (which typechecks ok under fuzz).

The following schema depends on a formal paramter:

\begin{schema}{Set}[X]
elements : \power X
\end{schema}

Now define some generic constants:

\begin{gendef}[X]
universe : \power X \\
subset : Set[X] \rel Set[X]
\where
universe = X \\
subset = \{~s1, s2 : Set[X] | s1.elements \subseteq s2.elements~\}
\end{gendef}

Now use the generic constants in a predicate so they get instantiated:

\begin{axdef}
a : Set[\{1, 2\}] \\
b : Set[\{1, 2, 3, 4\}]
\where
a.elements \in universe \\
b.elements \in universe \\
(a, b) \in subset
\end{axdef}

In the predicate we should get the constants universe[{1,2}] on line
one and universe[{1,2,3,4}] on line two. I guess we get the constant
subset[Set[Z]] on line three.

It seems that the inference rule is such that sets are used when there
is no unification necessary, but types are used when unification is
necessary. Is this correct? Is this explained somewhere differently
than the ZRM edition 1?

Sincerely yours,
Dr. A.G.(Arthur) Ryman, Senior Development Analyst, AD Tools
IBM Canada Laboratory, 3G/611/1150/TOR
1150 Eglinton Avenue East, North York, Ontario, M3C 1H7 Canada