🚀 go-pugleaf

Once upon a time, at the same place, I launched an "appel au peuple"
requesting "Folk Theorems" about Prolog Programs Transformations.

I didn't receive as many answers as I expected, so I concluded
that Real Prolog Programmers are not interested in transforming
programs :-).

However, I promised to give the list of all answers, so here it is
(after a bit of editing)

Just a word before the list: during a discussion about 'deterministic
predicates' we discovered that the definition :
	deterministic = 0 or 1 success, with/without side effects
was not accurrate enough. We have to add an additionnal constraint :
	deterministic = 0 or 1 success + no side effects by backtracking.

for example  p :- write(a).			is deterministic

	     q :- true ; (write(a),fail).	is NOT deterministic

(this is a bit related to my recent papers... (advertisement :-) )
--------------------------------------------------------------------
From: scheidhr@cs.uni-sb.de

In article <3266@geocub.UUCP> you write:
|> I'm looking for a collection of 'Folk Theorems' for 
|> Prolog programs. Four such examples :
|> 
|> 1. Two consecutive cuts are redundant
|>    Exemple          p :- a,b,!,!,c,d.
|>  is equivalent t is the compound goal   a,b  .
|> 
|> 4. If a is deterministic 
|>    then you can change the LAST clause of a procedure
|>    like :   p :- a,!,b,c,d.
|>    into :   p :- a,b,c,d.
|> 
|> Thanks a lot
|> 
|> Michel BILLAUD
|> 
What about:

5. If b is deterministic and followed by a !, you can switch them:
     p :- a,...,b,!,c,...     
     p :- a,...,!,b,c,...

Inductively you can show: 

move a cut behind the rightmost nondeterministic goal to the left of
the cut.

4. follows together with 2. from this.

------------------------------------------------------------
From bjr@aipna.ed.ac.uk Sat May 25 12:03:01 1991

Michel --

In article <3266@geocub.UUCP> you write:
# I'm looking for a collection of 'Folk Theorems' for 
# Prolog programs. Four such examples :  [...]
#
# Thanks a lot
# 
# Michel BILLAUD

Many of the "folk theorems" or source-to-source transformations you 
list are in the references which follow. They also have other ones
you might be interested.  My current work in Prolog semantics (last two
references) formally proves the equivalence of these and other transformations.

@inproceedings{Sawamura85,
	author =	"H. Sawamura and T. Takeshima",
	title =		"{Recursive Unsolvability of Determinacy, Solvable Cases of Determinacy and Their Applications to Prolog Optimization}",
	booktitle =	"Proceedings of the Symposium on Logic Programming",
	year =		"1985",
	pages =		"200-207"
}

@article{Debray88,
	author =	"S.K. Debray and P. Mishra",
	title =		"{Denotational and Operational Semantics for Prolog}",
	journal =	"Journal of Logic Programming",
	year =		"1988",
	volume =	"5",
	pages =		"61-91"
}

@inproceedings{Ross91b,
	author =	"B.J. Ross",
	title =		"{Using Algebraic Semantics for Proving Prolog
			 Termination and Transformation}",
	booktitle =	"Proc. UK ALP 91",
	address =	"Edinburgh, Scotland",
	year =		"1991",
	publisher = 	"Springer--Verlag",
	note =          "(forthcoming)"
}

@phdthesis{RossPhD,
	author =	"B.J. Ross",
	title =		"{An Algebraic Semantics of Prolog Control}",
	school =	"Department of Artificial Intelligence, 
			University of Edinburgh",
	year =		"1991",
	address =	"Edinburgh, Scotland",
	note =		"(forthcoming)"
}

-- 
Brian Ross.               	Diet Pepsi rules.
bjr@aipna.ed.ac.uk

------------------------------------------------------------


From csa09@seq1.keele.ac.uk Mon May 27 12:04:26 1991
From: "P." Singleton <csa09@seq1.keele.ac.uk>

If a (deterministic) goal doesn't instantiate its arguments 
any further (perhaps it has useful side-effects), then you 
can replace it by

	\+ \+ goal

which will recover its heap space immediately.

Nota : \+ = not

------------------------------------------------------------

Thanks to all !

Michel



-- 
Michel BILLAUD                 :  billaud@geocub.greco-prog.fr
Departement d'Informatique     :  
IUT "A", Universite Bordeaux I :  phone W: 56.84.57.92  // 56.84.69.22
33405 Talence  (FRANCE)        :        H: 56.36.65.90 (answering mach.)