Re: Thinking Recursion

From: student (nospam_at_a.b.c.dINVALID)
Date: 03/30/05 

Date: Wed, 30 Mar 2005 04:47:37 GMT

> Torkel Franzen wrote:
>
>>
>> append/3 is a direct translation into Prolog of the (only
>> reasonable) recursive definition of list concatenation:
>>
>> []+L=L
>> [X|L1]+L=[X|L1+L]
>>
> > which is how I present it to beginners
>

p.s.

I notice that your equations appear to fit in with LPTP quite
nicely, at least if they are given a functional interpretation
(the following is from the file 'suffix.pr' in the LPTP library):

:- definition_fun(**,2,
  all [l1,l2,l3]: succeeds list(?l1) =>
   (?l1 ** ?l2 = ?l3 <=> succeeds append(?l1,?l2,?l3)),
  existence by lemma(append:existence),
  uniqueness by lemma(append:uniqueness)
).

:- corollary(app:nil,
all l: [] ** ?l = ?l,
[] ** ?l = ?l by uniqueness(**,2)
).

:- corollary(app:cons,
all [x,l1,l2]: succeeds list(?l1) =>
                           [?x|?l1] ** ?l2 = [?x|?l1 ** ?l2],
assume(succeeds list(?l1),
  [succeeds append(?l1,?l2,?l1 ** ?l2) by existence(**,2),
   succeeds append([?x|?l1],?l2,[?x|?l1 ** ?l2]), % by def. append/3.
   succeeds list([?x|?l1]), % by def. list/1.
% succeeds append([?x|?l1],?l2,[?x|?l1] ** ?l2) by existence(**,2)
   [?x|?l1] ** ?l2 = [?x|?l1 ** ?l2] by uniqueness(**,2)],
  [?x|?l1] ** ?l2 = [?x|?l1 ** ?l2]) % q.e.d.
).

% = comments added by me

The TeX output is easier to read.

Proofs, not IFYSWIM.