Hi,
I wonder very much about what counts as logical.
So sorry for stepping into the discussion.
Joachim Schimpf schrieb:
> I have no problem with you introducing nonlogical variables,
> just don't call them something they are not.
If I take:
X := E; S
As:
(lambda X.S) E
I would say X is still a logical variable. Although
not free in the full expression (lambda X.S) E, it is
bound by the lambda binder.
Otherwise I would say X behaves inside S as a free
logical variable, in inside E it should not alias with a
variable that is also named X.
Bye
P.S.: Here is some testing, using the Jekejeke
Minlog lambdas:
?- I = f(X,a), I = f(b,Y).
I = f(b,a),
X = b,
Y = a
?- I = f(b,Y), I = f(X,a).
I = f(b,a),
Y = a,
X = b
?- call(I\(I=f(X,a)),f(b,Y)).
X = b,
Y = a
?- call(I\(I=f(b,Y)),f(X,a)).
Y = a,
X = b
Or in Picat:
Picat> I = $f(X,a), I = $f(b,Y).
I = f(b,a)
X = b
Y = a
Picat> I = $f(b,Y), I = $f(X,a).
I = f(b,a)
Y = a
X = b
Picat> I := $f(X,a), I = $f(b,Y).
I = f(b,a)
X = b
Y = a
Picat> I := $f(b,Y), I = $f(X,a).
I = f(b,a)
Y = a
X = b
But somehow Picat seems to stretch the notion of
free variable. In my opinion it should show the I
value for the two last example above, at least under
the lambda interpretation.
I am speculating that Picat doesn't show the free
variables but the most inner variables in the
top-level. Take the following example:
Picat> I = $f(b,Y), I := $f(X,a).
I = f(_91b0,a)
And compare it with the Jekejeke Minlog lambdas:
?- I = f(b,Y), call(I\true,f(X,a)).
I = f(b,Y),
X = b
The Prolog lambdas do show the outer I and not
the inner I.
The above example shows also an error or restriction of
the current Prolog lambdas implementation. The bound I
and the outer I do alias, thats why we get X = b,
although we shouldn't.
The correct usage of the Prolog lambdas would require
a renaming of variables in the continuation so that there
is no clash between free and bound variables. The
correct call is then:
?- I = f(b,Y), call(J\true,f(X,a)).
I = f(b,Y),
So the Picat rewriting is still cool, we cannot
make the error from the previous query.
Bye