We can go on a mystic journey and treat this definition as it is, a definition. Cryptic? This means equational reasoning, i.e. reasoning through equations, i.e. definitions. Here's what I mean. You have
(define (y s lis)
(cond
((null? lis) '() )
((equal? s (car lis)) lis)
(else (y s (cdr lis)))))
We can re-write this as two equations,
y s lis = lis , if (null? lis) || (equal? s (car lis))
= y s (cdr lis) , otherwise
Here y s lis
stands for "the result of Scheme call (y s lis)
" and so on.
Clearly we have two cases. One is base case, another describes a reduction step. Re-writing again,
y s lis = y s (cdr lis) , if (not (null? lis)) && (not (equal? s (car lis)))
= lis , otherwise
This is practically in English now. So while lis
is not null, and its car
isn't s
, we proceed along to its cdr
, and so on and so forth until either we hit the list's end, or its car
is s
, and then we stop. So when we've found s
, we return the list, otherwise the list is exhausted and the empty list is returned. This is otherwise known as member
in Common Lisp. R5RS Scheme's member
, as well as Racket's, returns #f
when no x
is found in the list.
Where is the equational reasoning here, you ask? In treating the RHS as the answer, and re-applying the same set of rules for each reduction step. For example:
y x [a,b,x,c,d,e] ; A
= y x [b,x,c,d,e] ; by 1st rule ; B
= y x [x,c,d,e] ; by 1st rule ; C
= [x,c,d,e] ; by 2nd rule ; D
When we get to apply the 2nd rule, we arrive at the end of the reduction chain, i.e. we get our answer. The result of the Scheme call corresponding to A
will be the same as the Scheme call's corresponding to B
, or C
, or finally D
:
(y x (cons a (cons b (cons x z)))) ==
(y x (cons b (cons x z))) ==
(y x (cons x z)) ==
(cons x z)
What's so mystic about it, you ask? Here probably not much; but usually what that means is that by assuming the meaning of a function, and by interpreting the RHS through it, we arrive at the meaning of the LHS; and if this is the same meaning, that is our proof for it. Induction is kind of magical. For more involved examples see How to recursively reverse a list using only basic operations?.
Incidentally structural recursion is also known as folding, so your function is really
y s lis = para (λ (xs x r) (if (equal? x s) xs (r))) '() lis
using one type of folding, paramorphism, with explicit laziness,
para f z lis = g lis
where
g xs = z , if (null? xs)
= f xs (car xs) (λ () (g (cdr xs))) , otherwise