Re: [Core] new safeness condition

Jos de Bruijn wrote:
> 
> 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

That's what I meant, of course, jos.

>> 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?

Because they wouldn't terminate.

> 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.

I didn't say that I consider this safe in the strong sense. Indeed this 
one has the same problem.

Axel

> 
> 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
>>
> 


-- 
Dr. Axel Polleres
Digital Enterprise Research Institute, National University of Ireland, 
Galway
email: axel.polleres@deri.org  url: http://www.polleres.net/