Re: On deriving Prolog predicates: sublist/2

From: KBoy (Kris.BoyenNO_SP_at_Mstudent.kuleuven.ac.be)
Date: 06/03/04 

Date: Thu, 3 Jun 2004 00:33:06 +0200

"bart demoen" <bmd@cs.kuleuven.ac.be> schreef in bericht
news:1086152124.592396@seven.kulnet.kuleuven.ac.be...
> flapper wrote:
>
> > Thus, sublist([],[]).
> > [...]
> > Thus, sublist([X|L1],L2) if sublist(L1,L2),
> > [...]
> > Thus, sublist([X|L1],[X|L2]) if sublist(L1,L2).
> >
> > -----*-----
> >
> > Collecting results,
> >
> > sublist([],[]).
> > sublist([X|L1],L2) :- sublist(L1,L2).
> > sublist([X|L1],[X|L2]) :- sublist(L1,L2).
>
> Very nice. That gives us "correctness" of the three Prolog clauses.
>
> You have left open the question of "completeness": how do we know that
> those three clauses cover everything ? Can you prove that as well ?
>
> Cheers
>
> Bart Demoen
>

I'll give it a try. Not sure if it is totally correct, but I can only learn
from it (if I get respons).

Going to take 2 steps. First I want to show that there are exact 2^n
sublists of a list with length n.
After that, I will show that you can get the same number of different
sublists with the given clauses.

- Step 1:

Take a list with n elements. For every sublist of this list, you can define
a binary number where the bit at place i indicates wether the i-th element
of the list occurs in the sublist.

e.g.: when you have a list [1,2,3,4,5] you can identify the sublist [1,4]
with the number 10010.

Since there are 2^n binary numbers of length n, there are the same number of
sublists of a list of length n

Note that this formula is also correct for the empty list, cause this list
only has one sublist, the empty list itself, and 2^0=1

- Step 2:

we're going to prove by induction that with the given clauses, we get 2^n
different sublists for a list of length n.

> > sublist([],[]).
> > sublist([X|L1],L2) :- sublist(L1,L2).
> > sublist([X|L1],[X|L2]) :- sublist(L1,L2).

* base case n = 0:

only the first clause is valid for the empty list and gives exact one
result, the empty list. So there is 2^0=1 sublist.
Since there is only one, you can say that the results are all different.

* prove for n+1, given that it is valid for n

so we know that for a list of length n, we get 2^n different sublists.

now the valid clauses for length n+1 are the last 2 wich both make use of
the sublist of length n. We know that this one gives 2^n results, so in
total we get 2 * 2^n = 2^(n+1) results.
Since the 2nd clause generates only clauses not containing the (n+1)th
element and the 3rd clause generates only clauses that contain the (n+1)th
element, the 2 clauses won't generate a result the other one generates, and
for a list of of length n, we know they only generate different sublists,
those 2^(n+1) found lists are all different.

* Since it is valid for a list of length 0, and since we know that if it is
valid for a list of length n it is also valid for a list of length n+1, we
can conclude that our clauses generate 2^n different sublists for a list of
length n.

- Since the clauses generate 2^n different sublists, and since this is also
the number of different sublists a list of length n can have, the clauses
must generate all the sublist for any list of any given length, so this set
of clauses is also complete.

Kris

Relevant Pages

  • Re: On deriving Prolog predicates: sublist/2
    ... Not sure if it is totally correct, ... > sublists of a list with length n. ... > sublists with the given clauses. ... > those 2^found lists are all different. ...
    (comp.lang.prolog)
  • all subsets of length k
    ... Say I want to generate all sublists of length k. ... Leave alone the fact that ocaml lists are not lazy, ... let guard b = if b then return else mzero ... bind (fun x -> ...
    (comp.lang.functional)
  • Re: Collecting like-labelled sublists of a list
    ... and collect together the contents of all sublists sharing ... the same label. ... The ordering of the final collected lists is not important, ... ; real time 15 msec ...
    (comp.lang.lisp)
  • Re: Collecting like-labelled sublists of a list
    ... The labelled lists represent partials in spectral analysis data ... Of course you get the sublists in random order, ... Sorry, do you mean the order of the labels, or the order of the elements inside each sublist? ...
    (comp.lang.lisp)
  • append, vp6
    ... Hellow, i'm working with visual prolog 6 ... I'd like to join two lists ...
    (comp.lang.prolog)