Ken Dickey wrote: > On Friday 24 October 2008 11:07:25 David Van Horn wrote: >> Ken Dickey wrote: >>> I have not yet found a sorted? predicate used in an induction >>> loop. >> There is an implicit use here (adapted from HtDP), by appealing to fact >> that (sorted? null) is #t. >> >> (define (sort alon) >> (cond >> [(null? alon) null] >> [else (insert (car alon) (sort (cdr alon)))])) >> >> David > > No. The induction is on the length of the list with the termination > condition > that the list is empty.
This would suffice for a termination proof, but but how do you prove correctness? That is, that for all lists of numbers, alon, (sort alon) is in fact sorted? The base case of this induction proof relies on the fact that (null? alon) implies (sorted? alon). The inductive case relies on a lemma that inserting into a sorted list results in a sorted list. If the empty or singleton list are not considered sorted, the proof will not go through. David _______________________________________________ r6rs-discuss mailing list [email protected] http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss
