🚀 go-pugleaf

[I'm posting this for Marc Gillet.]

------

In <4054@goanna.cs.rmit.oz.au> (Richard A. O'Keefe)  writes :

>I haven't been able to try this in IBM Prolog, but in one Prolog that
>I _have_ got that takes this kind of thing (the arity is part of the
>structure but the function symbol is not) there were two unpleasant
>effects:  first, the wretched thing didn't take the function symbol
>into account when indexing (I am *not* saying that IBM Prolog doesn't,
>not at all, but if you can't rely on the function symbol being _there_
>it's a wee bit tricky to index on it), and second precisely this
>anomaly occurred:
>        f =.. X         -> X = "f"
>        f() =.. X       -> X = "f"
>        T =.. "f"       -> T = f
>but NOT T =.. "f"       -> T = f()

>Why do I have to keep on saying that we want our EPs to satisfy
>SIMPLE laws?  Here are two laws which univ satisfies in Prologs whose
>data structures are based on the usual description of terms in
>first-order logic:

>        if at any instant T1 =.. L1, T2 =.. L2, L1 == L2 would succeed,
>        then at that instant T1 = T2 would succeed.
>       "univ is an isomorphism between terms and certain lists"

>       immediately after doing T1 =.. L1,
>       T2 =.. L1, T2 == T1 would succeed (where T2 is a new variable) and
>       T1 =.. L2, L2 == L1 would succeed (where L2 is a new variable)


In fact these problems don't exist in IBM Prolog.

IBM Prolog has two built-in predicates for =..

1) One called built2 : (T =.. L) is provided for compatibility with
   Edimburgh Prolog.

   This means that T has to be a functor with an atomic name or a
   constant and that functors of arity 0 are not allowed.

   This is the classical Edinburgh =.. and this predicate verifies
   the above properties.

   [You get built2 : (T =.. L) automatically when you are in
    Edinburgh syntax.]

2) The second is built : (T =.. L), in which T can be any
   functor, (including functor with non atomic names and functors
   of arity 0) but cannot be another term (variable excepted) like
   a constant. (It means that :- a =.. X . fails.)
 
   The above properties are equally verified for this predicate,
   because in IBM Prolog, the term X() does NOT unify with X.

   Furthermore :-  _ =..  L . succeeds for ANY non empty list L.

   The only difference is that:
   >       "univ is an isomorphism between terms and certain lists"
   has to be changed into :
     built : ( T =.. L) is an isomorphism between functors and non
     empty lists .

For the indexing, an easy solution is to apply the classical
indexing on the name and arity of a functor for all the
functors with an atomic name, and to not use indexing for the
other functors.  (That is to handle them like variables.)

Best Regards,
 Marc Gillet,