Re: Occurs-check in the unification (" =:= ")
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
This archive was generated by hypermail 2.3.0
: Do Feb 01 2024 - 07:15:05 CET