assertions (was: Assocative predicates)
fjh at cs.mu.OZ.AU
Thu Apr 23 13:28:31 AEST 1998
I'm leaning towards `:- assertion' as a better name than `:- pragma assert':
* `assertion' is better than `assert' because
we want to use declarative nouns rather than imperative verbs --
using the imperative verb suggests side effects, and would not
doubt cause some confusion with Prolog's `assert';
* assertions are important enough that they should be a part of
the language proper, not pragmas.
I think we should also allow `:- specification' (or perhaps `:- spec')
with the same semantics as `:- assertion' but with an additional
restriction that the assertion must be of the form `p(Vars) <=> Goal'
or `f(Vars) = Expression <=> Goal' with the `<=> Goal' part optional,
where Vars are distinct variables. That is, a specification is an
assertion that completely specificies the semantics for a particular
predicate or function.
Often the code for a procedure is identical to its specification,
so probably it would make sense to use the specification as the default
implementation if there are no clauses for the procedure.
On 23-Apr-1998, Peter Schachte <pets at students.cs.mu.oz.au> wrote:
> ... I still think there is something to be said for using words people
> recognize like "associative," "commutative," etc. I suppose that can be
> done in comments, but how about allowing users (and the standard library) to
> define properties. Maybe something like
> :- pragma assertion(associative_function(F) = (F(A,F(B,C)) = F(F(A,B),C))).
> :- pragma assertion(associative_predicate(P) = (
> P(A,B,C), P(C,D,E) <=> P(B,C,F), P(A,F,E)
That's a good idea. However, these "properties" are in many ways similar
to ordinary predicates, so I'd prefer a syntax that more closely reflected
this. Indeed, this could almost be done just using ordinary predicates,
without introducing any new construct at all:
:- pred associative_function(func(T1, T2) = T3).
:- specification(associative_function(F) <=>
all [A, B, C] (F(A,F(B,C)) = F(F(A,B),C))).
The only problem with this is that the compiler will complain about
there being no modes for `associative_function'.
One way of working around this would be to use a "not_reached" mode
% na stands for "not applicable"
:- mode na == not_reached -> not_reached.
:- mode associative_function(na) is erroneous.
However, it might be better to have some special syntax for this
Fergus Henderson <fjh at cs.mu.oz.au> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger fjh at 22.214.171.124 | -- the last words of T. S. Garp.
More information about the developers