Re: Occurs-check in the unification (" =:= ")

From: Michael Hanus <hanus_at_informatik.rwth-aachen.de>
Date: Mon, 4 Jan 1999 14:15:02 +0100

David Sacher wrote:
> The following question arised reading curry's operational semantics in
> the report.
>
> Consider the 6th transition rule in figure 2 on page 53 (x =:=
> c(e1,...,e_n)):
> Obviously we mustn't avoid x \in vars(c(e_1,...,e_n)) to achive
> completeness. On the other hand I'm in doubt if the suggested
> occurs-check is correct.
> A critical goal could be: x =:= c (I x) where I is the identity, c a
> unary constructor and x a variable. If the occurs-check is correct, this
> goal has to fail. The operational semantics treats this goal as follows.

Dear David,

thanks for the example which shows a small but important mistake
in the current description of the transition rules for constraint
solving. You are completely right, the 6th transition rule must
be corrected as follows: the partial instantiation of x must
be also done in the right-hand side of the equation which is missing
in the current version. Usually, this is implicitly done by variable
binding in the implementation which is the reason why I haven't seen
this mistake. Thus, the correct rule is as follows:

-------------------------------------------------------------------------------
Eval[x=:=c(e_1,...,e_n)] => {\sigma [] y_1=:=\sigma(e_1)&...&y_n=:=\sigma(e_n)}

where x \not\in cv(c(e_1,...,e_n)), \sigma = {x|->c(y_1,...,y_n)}
and y_1,...,y_n are fresh variables.

I'll correct it in the next version.

Best regards,

Michael
Received on Mo Jan 04 1999 - 14:19:00 CET