less variables

Harold Boley <boley@informatik.uni-kl.de>
Date:     Tue, 22 Feb 94 22:10:28 MET
From: Harold Boley <boley@informatik.uni-kl.de>
To: cg@cs.umn.edu, interlingua@ISI.EDU
Cc: boley@informatik.uni-kl.de
Subject:  less variables
Organization:  University of Kaiserslautern, DFKI, Germany
Message-id: <9402222210.aa19267@uklirb.informatik.uni-kl.de>
I share Fritz Lehmann's interest in graphs as a way to access entities
(e.g. complex nodes of DRLHs) themselves, 2-dimensionally, rather than
their names (or even copies), at several places where they are needed:
for a *named* entity it becomes non-trivial to locate the entities
'pointing' to it.  On the other hand I've become used to (clause-local)
logical variables, whose unique renaming I perceive as an implicitly
happening ('abstract data type'-like) operation, since resolution
renames program clauses on each use (ideally, like RELFUN's *interpreter*,
mapping "X" to something like "X*1", "X*2"..., not to "_1", "_2" ...).

Concerning the recent discussion on variable elimination, I think we
should not try to systematically eliminate *all* variables used in
temporary lambda expressions (not worth a permanent definition) such
as those in the functional arg of diff's mapcar/maplist in the recent
email by John McCarthy (Lisp). Still, it may be possible to eliminate
*some* variables using a set of 'program-forming operations', including
apply-to-all (a Curried mapcar), (sequential) composition, (parallel)
'construction', and 'condition' of John Backus (FP), with readability,
not ('S,K,I'-combinator-like) minimality, in mind.

In logic (programming), variables occurring more than once in a term
serve the additional role of implicitly enforcing equality constraints
(via unification). So if we replace names of single-occurrence
variables by the don't-care symbol for anonymous variables (Prolog's
"_") we stress their 'context-free' readability. It's hard to get rid
of all variables (e.g. X) in rules, e.g. likes(john,X) :- likes(X,_).

In FIT I've reformulated (tail-recursive) rules such as
(in RELFUN's Prolog-like syntax)

add(0,Y) :-& Y.                      % "& Term." returns instant. Term as value
add(X,Y) :-& add(pred(X),succ(Y)).   % "& Expr." returns evaluat. Expr as value

using 'adapters' as in the second clause of (in extended RELFUN syntax)

add(0,Y) :-& Y.       % first clause still needs variable for lhs-rhs transport
add($pred,$succ) -&.  % "$F" applies F when unifying, "-&." re-evaluates result

for obtaining 'variable-reduced', more concise definitions.

I've completed a RELFUN extension permitting variable-free, anonymous
domains, which can be regarded as ('enumeration') types of anonymous
variables. Perhaps such optional 'first-class' types could also be used
in KIF. For obtaining report RR-94-07, email your snail address to me.

Abstract (RR-94-07):

Languages based on logical variables can regard finite domains, finite
exclusions, and, generally, types as values.  Like a variable can be
bound to a non-ground structure which can be later specialized through
in-place assignment of some inner variables, it can also be bound to,
say, a domain structure which can be specialized later through
`in-place deletion' of some of its elements (e.g. by intersection with
other domain structures).  While finite domains prescribe the elements
of a disjunctive structure, the complementary finite exclusions forbid
the elements of a conjunctive structure. Domains and exclusions can be
values of variables or occur inside clauses as/in terms or within an
occurrence-binding construct (useful to name arbitrary terms).  In a
relational-functional language (e.g., RELFUN) they can also be
returned as values of functions. Altogether, domains and exclusions
become first-class citizens. Because they are completely handled by an
extended unification routine, they do not require delay techniques
needed in (more expressive) constraint systems. Still, their
backtracking-superseding `closed' representation leads to smaller
proof trees (efficiency), and abstracted, intensional answers
(readability).  Anti-unification (for generalization) exchanges the
roles of domains and exclusions.  The operational semantics of
domains, exclusions, and occurrence bindings is specified by a RELFUN
meta-unify function (and implemented in pure LISP).

Author="John Backus",
Title="Can Programming Be Liberated from the {von Neumann} Style?
{A} Functional Style and Its Algebra of Programs",
journal ="CACM",
month =	{August}, 

AUTHOR             = {Harold Boley},
TITLE              = {{Finite Domains and Exclusions as First-Class Citizens}},
BOOKTITLE          = {Fourth International Workshop on
Extensions of Logic Programming,
St. Andrews, Scotland, March 1993, Preprints and Proceedings},
EDITOR             = {Roy Dyckhoff},
NOTE               = {Also available as Research Report RR-94-07, Feb.\ 1994,
DFKI, P.\ O.\ Box 2080, D-67608 Kaisers\-lautern},
PUBLISHER          = {Springer},
SERIES             = {LNAI},
YEAR               = {1994}