[r6rs-discuss] Comparison procedures' number of arguments

[David Van Horn]

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