Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Message-Id: <9201262311.AA15708@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Cc: chou@edu.ucla.cs
Subject: Overloading of constant names
Date: Sun, 26 Jan 92 15:11:07 PST
From: chou@edu.ucla.cs

In HOL, if I have defined:

(1)     neg:num->num = \x.0-x

then I can no longer define:

(2)     neg:bool->bool = \x.~x

But why?  DESCRIPTION says a HOL constant is a (name, type) pair.
Clearly neg:num->num and neg:bool->bool are two different constants.
So why does definition (1) preclude definition (2)?

I'm asking this because I would like to use abstract theories but
found the above naming constraint very annoying.  For instance,
I want to define a type :graph and, for any G:graph, get its
adjacency relation by saying adj(G).  Later I want to talk about
graphs in which edges are weighted, so I want to define another
type :w_graph.  But then, to get the adjacency relation of a
weighted graph WG, I would have to say something like w_adj(WG).
instead of simply adj(WG).  If I want to consider yet another
new type :cw_graph of connected weighted graphs, I would have to
introduce yet another set of constant names.  Is there a way out?

- Ching Tsun