# Re: formal definition for list operations

From: Sandro Hawke <sandro@w3.org>
Date: Mon, 04 May 2009 19:00:59 -0400

Message-ID: <22769.1241478059@ubehebe>
```
[replying to myself, with more thoughts on this...]

> Ah, here's an idea.  Rather than specifying the semantics of the list
> operations in model theory math English, how about if we do it in RIF
> presentation syntax, for all the list operations which are essentially
> syntactic sugar.  (That is, everything other than get(L, 0) and
> sublist(L, 1), which are car and cdr, respectively.)  That would also
> give people a model to work from, if they wanted to parameterize
> equality.

For example, I think the hardest one is index_of.  Here's a (working)
implementation of index_of in a subset of Prolog that I believe
corresponds to RIF Core.  It would read better in RIF Core syntax
because RIF Core has external functions, and in Prolog I had to use
predicates for first, rest, and numeric-add.  (Although for the
implement-them-yourself builtins, RIF Core users would have to use
predicates, too.)

-- Sandro

================================================================

index_of(L, I, X) :-
index_helper(L, I, X, 0).
index_helper(L, I, [Offset|T], Offset) :-
first(L, I),
O2 is 1 + Offset,
rest(L, R),
index_helper(R, I, T, O2).
index_helper(L, I, T, Offset) :-
first(L, X),
literal_not_identical(I, X),
O2 is 1 + Offset,
rest(L, R),
index_helper(R, I, T, O2).
index_helper([], _, [], _).

% helper stuff.
first([X|_],X).
rest([_|T],T).
literal_not_identical(X, Y) :-
number(X),
number(Y),
X \= Y.
% other literals go here....
literal_not_identical(_, _) :-
fail.

================================================================

?- index_of([], 3, X).
X = [].

?- index_of([3], 3, X).
X = [0]

?- index_of([3,3,3], 3, X).
X = [0, 1, 2]

?- index_of([0,0,3,3,3,0,3], 3, X).
X = [2, 3, 4, 6]

?- index_of([0,0,3,xxxx,3,3,0,3], 3, X).
fail.

The "fail" at the end is because prolog is making a NAF assumption on
index_helper; in RIF BLD, it's like 1+foo:bar -- you can't evaluate it
until/unless foo:bar is equated to a literal.  In RIF Core, ... when
that equating isn't possible, I guess it's safe the throw an error at
that point.

-- Sandro
```
Received on Monday, 4 May 2009 23:01:08 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:47:55 UTC