89-948 Questions and Answers
Can, besides defining functions from relations as in f(X) :- r(X,Y) &
Y., also relations be defined from functions?
Yes, if a function f is invertible using the .= built-in, a relation r
can be defined easily as follows: r(X,Y) :- Y .= f(X). Suppose f is predefined
invertibly, e.g. by f(a) :& 1. and f(b) :& 2. Now, of course, r
can be called like r(a,What) and r(b,What), binding What to 1 and 2, respectively.
But, since f is defined invertibly (without a cut and without arithmetics
built-ins etc.), r can also be called like r(Which,1) and r(Which,2), via
1 .= f(Which) and 2 .= f(Which) binding Which to a and b, respectively.
The remaining input-output modes of r calls, as in r(a,1) and r(Which,What),
aren't a problem for such an f either. The definition of N-ary relations
from (N-1)-ary functions is analogous for N>2.
Is the non-deterministic inverse binary absolute-value function
g(0) :& 0., g(1) :& -1. , g(1) :& 1. definable in just two
clauses?
Yes, as in the underlying mathematical equation G(1) = {-1,1}, we can represent
the non-deterministically returned finite set {-1,1} by a finite domain
dom[-1,1] and replace the last two clauses by g(1) :& dom[-1,1]. This
version represents g's non-determinism by a closed term instead of enumerating
the two values. If f is defined as the binary absolute-value function,
f(0) :& 0., f(-1) :& 1., f(1) :& 1., then f(g(1)) would via
f(dom[-1,1]) unify with the first
and third clauses, as when using the original g's values via f(-1)
and f(1). Conversely, f is also definable in just two clauses, namely f(dom[-1,1])
:& 1., f(0) :& 0. With the dom-using f and g definitions, X .=
g(f(X)), besides the
trivial solution X = 0, binds X to dom[-1,1], acting as a compact intensional
answer.
How could a function straits be defined, which yields unknown for the
argument scylla, goes into an infinite enumeration of the naturals for the
argument charybdis, and for all other arguments acts like the identity?
straits(scylla) !& unknown.
straits(charybdis) !& naturals(0).
straits(X) !& X.
naturals(N) :& N.
naturals(N) :& naturals(1+(N)).