- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

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

Date: Mon, 4 Jan 1999 14:15:02 +0100

David Sacher wrote:

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 Aug 05 2021 - 07:15:03 CEST
*