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

From: David Sacher <sacher_at_informatik.uni-muenchen.de>
Date: Wed, 30 Dec 1998 12:10:37 +0100

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

This archive was generated by hypermail 2.3.0 : Do Dez 12 2019 - 07:15:06 CET