Assocative predicates

[Lee Naish]

Wow!  I get sick for a few days and there are a squillion articles to
followup to (lucky comp.lang.prolog is as boring as usual).

Re: quantification in assertions

There have now been three different errors concerning the existentially
quantified variables.  People seems to be getting closer to the relationship
between assertions and clauses or collections of them.  Lets make it
explicit: (collections of) clauses are special cases of assertions (they
are special primarily because they have a procedural reading as well as
the declarative reading, and to make this feasible they are restricted
in various ways, particularly having one distinguished positive literal).
Assertions are not a generalisation of (the logic of) goals; they
are a generalisation of clauses.

We allow the clause:

cons(A, As, A.As).

It makes sense that we allow the assertion/specification:

:- assertion cons(A, As, A.As) <==> true.

to mean (declaratively) the same thing, rather than meaning

some [A,As] cons(A, As, A.As).

Fortunately, Fergus has started using implicit universal quantification
in his more recent postings (on type classes :-).


Re: admissibility/preconditions etc

The 'where' syntax supported by some NU-Prolog type checkers was
introduced to allow arbitrary definitions of types, see

@incollection{naish:90,
        author =        {Naish, Lee},
        title  =        {Types and the intended meaning of logic programs},
        pages  =        {189-216},
        booktitle =     {Types in logic programming},
        editor =        {Frank Pfenning},
        publisher =     {MIT Press},
        address =       {Cambridge, Massachusetts},
        year =          {1992},
        comment   =     {Technical Report 90/4, Department of Computer
                        Science, University of Melbourne}
}

There was no intention to distinguish between inputs and output,
preconditions and postconditions etc, though there is some overlap
between this "types" approach and the use of preconditions (see below).

Debugging code with the notion of inadmissibility is discussed in

@TechReport{ddscheme3,
        Author = { Naish, Lee },
        Title = { A three-valued declarative debugging scheme },
        Number = { 97/5 },
        Institution = { Department of Computer Science, University of
                Melbourne },
        Address = { Melbourne, Australia },
        pages = 13,
        Month = {April},
        Year = 1997,
        subcat =  {G4},
        authorcode = {433,13,00,FW,MD,M},
        abstractURL = "http://www.cs.mu.oz.au/~lee/papers/dds3/",
      comment = {Presented at 8th Workshop on
        Logic Programming Environments, Leuven, July 1997}
}

Several different notions of inadmissibility can be supported.  Eg
inadmissibility = ill-typedness in the scheme above.  However, it seems
that a more natural view is inadmissibility = ill-typedness of "input"
arguments  (this might seem procedural but can be given a purely
declarative reading).  For example, if list_merge succeeds with the last
("output") argument not sorted it is rather different to the "inputs"
being unsorted.  A semantics for logic programs, given that intended
interpretations are three-valued, is given in

@TechReport{naish:sem3,
        Author = { Naish, Lee },
        Title = {  A three-valued semantics for Horn clause programs},
        Number = { 98/4 },
        Institution = { Department of Computer Science, University of
                Melbourne },
        Address = { Melbourne, Australia },
        pages = 12,
        Month = {March},
        Year = 1998,
        authorcode = {433,13,00,FW,MD,M},
        abstractURL = "http://www.cs.mu.oz.au/~lee/papers/sem3/"
}

If you look at typical assertions about logic programs you will find
that many of them assume admissibility or well-typedness in the sense
above.  Eg, list_merge is only associative if we restrict attention to
the admissible subset.  The same applies to addition and multiplication!
Here admissibility means the size of the inputs are small enough that
the result can fit into the limited number of bits in the
representation (I assume we are dealing with integers/rationals here).
People have made all sorts of mistakes in claiming certain code
fragments are equivalent when, in general, they are not.  Similarly,
when debugging its very easy to make general assertions which assume
admissibility (eg all [X,Y] some [Z] list_merge(X,Y,Z)).

I think its important to recognise the notion of admissibility when
designing certain aspects of the language.  The meaning of general
assertions should probably be restricted so as to apply to only
admissible atoms.  There should be some way to declare admissibility.
One simple way is to allow special meta predicate(s) admissible
(and/or inadmissible) in assertions.  eg

:- assertion admissible(list_merge(X,Y,Z)) => sorted(X).

This avoids any additional constructs and allows us to get the third
truth value by using just two values in each assertion.  However, 
I think this does belittle the importance of admissibility.  It would be
nice to rethink the semantics of Mercury using three values and give
admissibility more prominence and its own syntactic construct (no, I
won't propose any).

Happy reading:-)

	lee