Re: if then else

On Sun, 24 Feb 2008 18:38:09 +0000, student wrote:

|- p1(X,Y,Z) <=> |- p2(X,Y,Z)

where '|-' means 'provable using the Prolog Inference Engine (PIE)'.

Can you show me a really trivial proof of this proposition?

Certainly not. I don't know what you mean by the PIE: it is way too
fuzzy for me. So I will definitely not try to prove anything in the
PIE framework.

But I can prove it trivially at the level of any reasonable
specification of if-then-else. Here is a trivial lemma that follows
from any such specification and that you can apply twice to prove what
you think is non-trivial:

p(X) :- q(X), !, r(X').
p(X) :- s(X").

is equivalent to

p(X) :- (q(X) -> r(X') ; s(X")).

[X, X' and X" denote a sequence of arguments, usually denoted by an
overline in very formal writing]

Oh, you might need another very trivial equivalence:

p(X) :- body(X').

is equivalent to

p(Y) :- Y = X, body(X').

where Y is a sequence of distinct variables.


At bottom, readable specifications and specifications about
which things can be rigorously proved seem to me to amount to pretty
much the same thing.

It is the eternal pitfall of the scientific approach (mostly male
approach) to equate distinct concepts: in this case, readability and
provability.
Please try to see that you fell in that trap, that it is unscientific,
and that it is counterproductive.

Both readability and provability are worthwhile qualities and we
should persue them in programming languages and in the programs we
write, but neither of them follows from the other. The hitchhikers
guide through the galaxy is a very readable book, but most of it is
not provable. Dixmier's C*-algebres only contains provable statements,
but I doubt it deserves the adjective readable (I am sure in fact: I
read it).

Moreover, as you are probably aware off - you must have been exposed
to CWA (or stronger versions of a similar principle) - not everything
that LPTP can't prove is unprovable.

Cheers

Bart Demoen


.