...LISP).
This research was supported by the BMFT under Grants ITW 8902 C4 and 413-5839-ITW9304/3.
...domains.
We will not expand much on further type-like constructs as values, but should note here that certain unary predicates (e.g. woman) could be marked (with a ``$''-prefix) as user-defined sorts (here $woman) that may be assigned to variables, where unification applies to an ordinary value (e.g. mary) or looks up 's glb (e.g. $mother) with another marked predicate (e.g. $parent) in a finite sort lattice.
...repetition-free
In accordance with RELFUN's call-by-value semantics, we also permit active dom (and exc) calls, using round parentheses, which remove repetitions before constructing passive dom (and exc) structures, using square brackets.
...:
Unlike many finite-domain systems, we introduce no special treatment for integer domains here. Conversely, generalizing domain elements beyond arbitrary constants would entail complications in using finite domains: even ground structures as in dom[f[a],f[b]] would suggest that unification with f[X] be successful, non-deterministically binding X to a or b, where in fact the advantage of finite domains is their deterministic behavior, as in dom[a,b] unified with X, just binding X to the entire domain term. Rules for reducing a unification like f[X] is dom[f[a],f[b]] to the deterministic X is dom[a,b], perhaps via f[X] is f[dom[a,b]], would be a challenge for non-constant-element extensions of finite domains.
...failure).
Of course, assigning type-like (e.g. domain or non-ground) structures to variables as initial `non-terminal' values and specializing them to `terminal' values after successful (unifying) type checks is only possible for specializing-assignment (LP) languages: in reassignment (imperative) languages, a variable has to preserve its original type `value' - in a separate `slot' - when assigning a terminal value to it because the type will be needed unchanged on reassigning further terminal values. This prevention of the type-as-value principle, and consequently of type `first-classness', can be construed as one more disadvantage of imperative languages.
...:
One could also use an infix notation like for increased conciseness. If was the sort-marked predicate , would then shorten to . The current implementation still has restrictions wrt the 's allowed in bnds. Section 5.2 will detail on the elimination of occurrence bindings.
......,
Since the last premise may constitute the value of a functional clause, the algorithm below will also work for function definitions.
...``''),
While we may also combine post-typing with the reformulation of an is-domain as a disjunction of solved equalities (cf. in section 3), we can directly apply the algorithm (cf. section 5.1) to any -ary-dom-head clause

to obtain equivalent domless clauses

(for anonymous domains we just omit ``'').
...facts
If some (interactive/automatic) analyzer notices that a certain domain such as dom[canada,mexico,usa] occurs repeatedly in a program, it may be useful to have it defined more globally as a predicate (with a user-provided name) such as america(dom[canada,mexico,usa]) and replace the domain by the predicate name used as a ``$''-marked sort, e.g. in the clause separates(pacific,$america,japan). A comparison of the equivalent notations `dom[. . .]' and `$...' reveals our convention that domains/exclusions do not carry a `typing symbol' such as the ``$'' for sorts: their dom/exc-constructor marks them as types with `built-in' unification behavior; on the other hand, ``$''-less predicate names are just constants unifying with themselves. Domains/exclusions exhibit their built-in properties in all places they are permitted as first-class citizens. Making them passively passable data structures (without list-coding as in appendix A), e.g. for amalgamated object/meta-level programming, is as hard as for logical variables, requiring a kind of quote operator.
...#domexcfunargs>.
In RELFUN the relationalize algorithm can be used to make relational/functional knowledge more accessible to such inductive-LP methods, which we study wrt efforts in knowledge Validation and Exploration by Global Analysis (VEGA).
...fact,
Such a separates enrichment was proposed by Manfred Meyer and Knut Hinkelmann. Thanks also to Otto Kühn, Michael Sintek, and Panagiotis Tsarchopoulos.
...bnd(s).
Thus, while the update of non-ground structures in relational languages leads to bindings of free inner variables, the update of dom and exc structures leads to bindings shadowing previous ones, as known from function calls and let blocks in interpreters for functional languages. In a (WAM) compiler implementation we could get the efficiency of in-place assignment via real in-place deletion/addition of elements of dom/exc structures allocated on the heap.

Harold Boley & Michael Sintek (sintek@dfki.uni-kl.de)