Re: [Core] new safeness condition

Axel Polleres wrote:
> 
> Sandro Hawke wrote:
>>> Looks sound, but implies that finiteness is no longer is requested.
>>> Was that what was agreed? (Am just catching up with reading minutes)
>>
>> My sense of the group was that everyone present prefered to give up on
>> finiteness, but we told that you had an argument for it, so we wanted to
>> wait until we'd at least heard that argument.  (Something about datalog
>> implementations, I think.)
>>
>>      -- Sandro
> 
> In principle, bottom-up evaluation is only possible if a finite Herbrand
> universe is guaranteed. 

Not true. The naive fixpoint computation will simply not terminate

> I know at least 2 implementations, probably more
> that would choke on unbound usage of built-ins a la
> 
>   a(X).

I assume you mean a(1)?

>   a(X+1) :-  a(X).
> 
> I mean, these engines would just not be able to handle those kind of
> rules. That's the simple argument.

Could you explain why?

Your ruleset is the same as:

a(1).
a(Y) :- a(X), add(Y,X,1).

And (u,b,b) is a completely reasonable binding pattern for an add/3
built-in predicate. Given two integers, you can compute their addition.


Best, Jos

> Obviously, these engines could handle
> 
>   a(Y) :-  a(X), Y = X+1, HU(Y).
> 
> but I see that this is restrictive. It is just question of what then
> core compliance means. I thought that there was some agreement that Core
> should be something like safe datalog, i.e. something that could be
> handled both with bottom-up and top-down engines.
> 
> Axel
> 

-- 
                         debruijn@inf.unibz.it

Jos de Bruijn,        http://www.debruijn.net/
----------------------------------------------
Many would be cowards if they had courage
enough.
  - Thomas Fuller

Received on Monday, 26 January 2009 17:26:19 UTC