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.
1st derivation step:
Eval[x =:= c (I x)] => { {x->c y} [] y =:= I x }
----------------------------------------------------
{ id [] x =:= c (I x) } => { {x->c y} [] y =:= I x }
As x \not \in cv(c (I x))
2nd derivation step:
Eval[I x] => { id [] x }
-----------------------------------------------------
Eval[y =:= I x] => replace(y =:= I x, 2, { id [] x })
-----------------------------------------------------
{ {x->c y} [] y =:= I x } => { {x->c y} [] y =:= x }
As replace(y=:=I x,2,{id [] x}) = {{x->c y} [] y=:=x}
3rd derivation step:
Eval[y =:= x] => { {y->x} [] success }
---------------------------------------------------------
{ {x->c y} [] y =:= x } => { {x-> c x, y->x} [] success }
(Assuming that no occurs-check is provided during the compositions of
substitutions.)
Reading Loogen/Fraguas/Aratejo:"A Demand Driven Computation Strategy for
Lazy Narrowing" didn't help me either: Solving the above goal will be
succesfully interpreted by the given Prolog-Program also, assuming the
underlying Prolog-System provides no occurs-check (if it would, the
occurs-check in the interpreter would be superfluous, I think).
Hoping not to write complete nonsense
David
--
-------------------------------------------------------------
David Sacher mailto:sacher_at_informatik.uni-muenchen.de
Tel.: 089 / 6789 367 http://www.lrz-muenchen.de/~sacher
Received on Mi Dez 30 1998 - 12:15:00 CET