(Sorry for my poor English.)
Interesting thread !
For years, I have written several versions of predicate eval
including lambda calculus on top of SWI-Prolog for fun. In order to
keep theoretical soundness of lambda ( beta ) calculus, the eval
refreshes bound variables for every application !
Here are several sample calls for the eval predicate,
where \ for lambda abstraction, \\ for Prolog call,
and @ for application.
?- eval((x\x)@ (y\y), V).
V = y\y
?- eval(((X\X)@ (Y\Y))@ hello, V).
V = hello
?- eval([x,y]\[x,y])@1@2, V).
V = [1, 2]
?- maplist(x\ [x], [a,b,c], V).
V= [[a], [b], [c]]
?- maplist(x\y\(y @ x), [a,b,c], [x\[x], x\[x,x], x\[x,x,x]], V)
V = [[a], [b, b], [c, c, c]]
?- maplist([x,y,z]\\ append(x,z,y), [[a],[b]], [[a,b,c], [b,a,c]], V).
V = [[b, c], [a, c]].
If interested, you can find many more samples at the page
http://web.sfc.keio.ac.jp/~mukai/mathcgi/fpop-sample.html,
which was created by a simple script written in SWI-Prolog
using the eval
I should say the current code of the eval predicate is, of course,
very slow. However, I feel lambda notation in Prolog is handy
and useful for daily use of Prolog where efficiency
does not matter.
Learning about 'apply_macro' library in this thread, now I think the
library can be extended to treat these lambda expressions as macros.
I think so because at least for my purpose, lambda expressions
are just a handy macro which is easily rewritten by hand
into the standard Prolog in a straightforward way.
Kuniaki Mukai
On 2008/04/22, at 8:40, Ulrich Neumerkel wrote:
> On Monday 21 Apr 2008 16:06:27 Samer Abdallah wrote:
>> On 21 Apr 2008, at 14:33, Ulrich Neumerkel wrote:
>>> On Monday 21 Apr 2008 12:48:13 Samer Abdallah wrote:
>>>> ... However, the body can include an explicit existential
>>>> quantification so that, eg
>>>> ?- maplist( \(A):- B^(A=B), [a,b,c,d]).
>>>> succeeds leaving B unbound.
>>>
>>> What about
>>>
>>> ?- B = a, maplist( \(A):- B^(A=B), [a,b,c,d]).
>> ...
>>> which should succeed (or produce an error), since the B at the top
>>> is
>> I'm not sure why you would expect it to succeed - perhaps
>> you are reading the existential quantification differently from
>> me? My interpretation is that the existential quantification
>> is to make it behave exactly like an auxiliary predicate defined
>> in the usual way:
>> aux(A) :- A=B
>> which has the implicit quantification, ie, it means
>> (exists B . A=B) => aux(A)
>
> Yes, so the B outside in B = a must be something different, entirely
> unrelated to the quantified B. It is the same as renaming the
> internal B to B1.
>
> Remark that you will succed for
>
> ?- maplist( \(A):- B^(A=B), [a,b,c,d]), B = a
>
> as well, which would be consistent with the success of
>
> ?- B = a, maplist( \(A):- B^(A=B), [a,b,c,d]).
>
> As we have here a pure program the conjunction G, H should be the same
> as H, G. You might have issues about termination and similar to
> settle, but otherwise there cannot be any differences.
>
> The most sensible would be some static checking, but there the
> difficulties start...
>
> Note that ensuring B being a variable is not sufficient, as it may
> share
> with other variables in conflicting scope.
>
> ------------
> For further info, please visit
http://www.swi-prolog.org/>
> To unsubscribe, send a plaintext mail with "unsubscribe prolog <e-
> mail>"
> in its body to
majordomo@...
------------
For further info, please visit
http://www.swi-prolog.org/To unsubscribe, send a plaintext mail with "unsubscribe prolog <e-mail>"
in its body to
majordomo@...