Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: Konrad Slind <slind@de.tu-muenchen.informatik>
To: info-hol@edu.uidaho.cs.ted
Subject: BETA_CONV
Message-Id: <93Jan11.044747met.8121@sunbroy14.informatik.tu-muenchen.de>
Date: Mon, 11 Jan 1993 04:47:46 +0100


(I sent this out earlier, but mis-spelt the mailing list address twice.)

Ching Tsun asks

> Why does BETA_CONV perform the renaming shown below at all?

I think the answer is that the hol88 implementation of subst, used to
implement BETA_CONV, will rename binding occurrences as it moves through
them, if there is another variable in the scope with the same name. The
renaming scheme also takes account of the incoming free variables, i.e.,
if "(\v.M) N" is the beta-redex, the free variables of N. I can't get
hol88 to run locally, so I can't test it, but you might try something
like

   BETA_CONV "(\y (x:*) (x:*). T) 1"

If my supposition is correct, hol88 should rename the inner binding
occurrence of x. Also try

    BETA_CONV "(\x (y:*). T) (y:bool)"

This behaviour is not a bug, more like a feature induced by the
difficulty of writing an efficient "subst" primitive, but it can be
aggravating.

No spurious renaming occurs in hol90, by the way. For example, none
of Ching Tsun's examples renamed in hol90. 

I am curious as to why Ching Tsun didn't need to add more type
information to get the terms to parse: sticky_types = true?

Konrad.