Re: if then else

bart demoen wrote:
On Fri, 22 Feb 2008 21:41:45 -0800, student wrote:


p(L0,L1,L2) :-
( L0 = [] -> L2 = L1 ;
( L1 = [] -> L2 = L0 ;
L0 = [X0|X0s],
L1 = [X1|X1s],
L2 = [X0,X1|X2s],
p(X0s,X1s,X2s) )).

beats

p([],L1,L2) :- !, L2 = L1.
p(L0,[],L2) :- !, L2 = L0.
p([X|L0],[Y|L1],[X,Y|L2]) :- p(L0,L1,L2).

hands down. In fact, I suspect it would be a nontrivial exercise to
rigorously prove that the latter actually means what the former clearly
and explicitly says.

Sorry, but I think that it is a really trivial exercise to prove the
equivalence of both pieces of code.



Relabeling the two predicates p1 and p2, respectively, you claim that
it is a really trivial exercise to prove that, for all X, Y, and Z,

|- 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?


Secondly, the cut in the first rule of the second definition is red,
which to my mind raises the question, is it even possible to write a
definition that is logically equivalent to the first and uses only pure
Prolog {Horn-like) clauses but does not use any red cuts?

If agree that the usage of the predicate is ++? , I would say that
p(L1,L2,L3) :- L1 = [], L2 = L3.
p(L1,L2,L3) :- L1 = [_|_], L2 = [], L3 = L1. p(L1,L2,L3) :- L1 = [X1|R1], L2 = [X2|R2], L3 = [X1,X2|R3], p(R1,R2,R3).
comes pretty close to being logically equivalent, with only pure Prolog
(Horn-like) clauses and no red cuts. Would you agree to that ?



Of course. (I may have had in mind to ask if all red cuts can be
eliminated by such means.)


Thirdly, I think it should be pointed out that the subset of Prolog
that is supported by Staerk's LPTP system[*] includes '(P->Q;R)', which
means that even if you never use LPTP to prove theorems about your
Prolog definitions, you can safely assume that you are on [sound] logical
grounds if do you use '(P->Q;R)'

I think you give some extra power to "is supported by Staerk's LPTP system".
Ask Staerk whether "X is supported by your LPTP system" means that the
construction has a logical meaning.
I bet that it does when the if-part is ground enough only.


"Extra power" sounds like something one might say about a new laundry
detergent. I can use LPTP to prove theorems about 'p1/3 (above), but I
can't use LPTP to prove theorems about 'p2/3'. Aside from any
differences in their respective compiled codes stemming from the matters
being discussed in this thread, that to me makes 'p1' vastly preferable
to 'p2'. At bottom, readable specifications and specifications about
which things can be rigorously proved seem to me to amount to pretty much the same thing.


All of which makes me wonder, given '(P->Q;R)', is there any
compelling need -- other than perhaps the practical need to support
legacy Prolog source codes -- to continue to support the cut?

Find out what Lee Naish wrote about cuts, if-then-else and snip.


Thank you for reminding me.

billh
.

Relevant Pages

  • Re: if then else
    ... I suspect it would be a nontrivial exercise to ... definition that is logically equivalent to the first and uses only pure ... Prolog {Horn-like) clauses but does not use any red cuts? ... compelling need -- other than perhaps the practical need to support ...
    (comp.lang.prolog)
  • Re: Thinking Recursion
    ... >>This is probably the third time I've tried to learn Prolog over the last ... It is a fact that the boundary condition of appending occurs when the ... if we want to talk about Prolog programs we need to agree on how ... and LPTP represents Prolog clauses as variable-free ...
    (comp.lang.prolog)
  • Re: Prolog compiler for Windows XP.
    ... Quintus Prolog, ECLiPSe, or CProlog. ... notes were written, while SWI has. ... I am not sure it is the responsibility of Mr Staerk to accommodate every Prolog compiler in existence. ... But I do not think that Jan Wielemaker has the responsability of making sure that LPTP runs unchanged in all future versions of SWI. ...
    (comp.lang.prolog)
  • Re: if then else
    ... definition that is logically equivalent to the first and uses only pure ... Prolog {Horn-like) clauses but does not use any red cuts? ... I think it should be pointed out that the subset of Prolog ... compelling need -- other than perhaps the practical need to support ...
    (comp.lang.prolog)
  • Re: Prolog compiler for Windows XP.
    ... The system specific file swi.pl for instanc contains a definition of initialization/1 which is a static predicate in SWI. ... Just doing the test from the LPTP INSTALL file shows many more of such errors - all because the promised "it runs on SWI" in the LPTP README is simply not really true. ... effort Staerk has put into making that true; not to the relative strength of the two Prolog systems involved. ... excellence as Gnu Prolog. ...
    (comp.lang.prolog)