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

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

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/~sacherReceived on Wed Dec 30 1998 - 12:15:00 CET

*
This archive was generated by hypermail 2.3.0
: Mon Sep 23 2019 - 07:15:04 CEST
*