Re: formal definition for list operations

[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