condict@csd1.UUCP (Michael Condict) (01/14/84)
Whoa... Marcel's problem is not meaningless at all. What he did was express
informally three axioms about the predicate "on", axioms which may be formal-
ized in first-order logic as:
(1) on(a) or on(b)
(2) on(a) implies not on(b)
(3) for all x, on(x) or not on(x)
This is called axiomatizing a predicate and is done all the time in logic.
The meaning of it is that we subsequently want to attempt to prove things
about "on", "a" and "b", using these axioms. We would, if we could successfully
express these axioms in Prolog, not try to prove something like "on(x)", but
rather something like "on(a),on(b)" (which would be refutable). We would
be using Prolog in theorem-prover mode, not as a programming language in-
terpreter that is supposed to compute values for variables.
While it is true that there are often many different relations (the word
relation is usually used to refer to the semantic set of pairs that is
denoted by a predicate symbol) satisfying a set of axioms, in this case
there is exactly one relation, if we restrict it to the domain {a,b}. It is
the relation R such that xRy iff x is the logical negation of y.
The point is that we certainly do not need higher-order logic to make sense
of any of this. Any complete theorem prover for full first-order logic could
prove all the theorems that are a logical consequence of the above axioms.
It is the restriction to Horn-clause logic that makes the problem require
the higher-order/hacking facilities of Prolog.
Michael CondictUReddy%Utah-20@sri-unix.UUCP (01/16/84)
From: Uday Reddy <U Reddy@Utah-20>
Ref: Marcel Schoppers, Prolog Digest, 2, 1, Jan 7, 84
The problem cited by Marcel is an example of what happens if one
tries to translate English into a formal language (here Prolog)
without regard to the semantic objects involved. His problem is
"Suppose you are shown two lamps, 'a' and 'b', and you are told
that, at any time,
1. at least one of 'a' or 'b' is on.
2. whenever 'a' is on, 'b' is off.
3. each lamp is either on or off."
Marcel tried to express these constraints in Prolog, by defining
a predicate 'on'. Such an exercise is meaningless. However you
specify 'on', what answers can you expect for the goal ?- on(X).
Either 'a', or 'b' or both of them. None of these results captures
the constraints above.
What is 'on' anyway? It is a predicate on {a,b}. Do the above
constraints specify what 'on' is ? No. They specify what 'on'
can be. In other words, they specify the properties the predicate
'on' should satisfy. So, what we need is a predicate, say 'valid',
which specifies whether a particular 'on' predicate is valid or
not. It is, clearly, a higher-order predicate. Forgetting about
operational semantics of higher-order logic, it may be specified
as
valid(on) :- (on(a) ; on(b)), (on(a) -> not(on(b)))
Reworking this into Prolog would correspond to what Marcel calls
"dumb-search-and-filter" solution. I wonder what he means by
"dumb". If what you are trying to do is express a set of axioms
and use Prolog to obtain all possible solutions of the axioms,
that is what you get. If you are not satisfied with search-and
filter, you have to do more than merely express a set of axioms.
You have to synthesize an algorithm. Don't expect black magic
from Prolog.
-- Uday Reddylee@munnari.SUN (Lee Naish) (01/31/84)
I'm sure everyone is as tired of this problem as I am, but I wont be able to
sleep until the REAL solution is given. Remember the axioms were
(1) a is on or b is on
(2) if a is on then b is off
(3) a and b are both on or off
The mistake has been to formalize this in terms of a predicate on(X), as
Michael Condict (and others) did:
(1) on(a) or on(b)
(2) on(a) implies not on(b)
(3) for all x, on(x) or not on(x)
There are two solution to these axioms: {on(a)} and {on(b)}. These are two
different predicates, not two solutions to the same predicate ({on(a), on(b)}.
Therefore we cant use first order logic for this statement of the problem.
Later in Micheal's follow up, he stated that there is one relation which
satisfies the axioms:
"the relation R such that xRy iff x is the logical negation of y."
Note that this relation has two arguments, each having the domain {on, off}.
This is the right way to do it. My original solution (in MU-Prolog) follows:
% Here's my first (logical, rather than efficient) switches program.
% To find the valid configurations, use the goal ?- config(A, B).
% The logic should be quite clear - the only possibly confusing bit is
% the if construct. This is available in MU-PROLOG, and is implemented
% soundly. The DEC-10 counterpart, ->, would work if cond2 was executed
% last (the evaluation of MU-PROLOG's if is delayed until the condition is
% ground, but this does not occur in DEC-10).
%
% Lee Naish
% (decvax!mulga!lee)
config(A, B) :-
cond1(A, B),
cond2(A, B),
cond3(A, B).
cond1(on, _).
cond1(_, on).
cond2(A, B) :-
if A = on then
B = off.
cond3(A, B) :-
on_or_off(A),
on_or_off(B).
on_or_off(on).
on_or_off(off).