Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    text
    copied!<p>The first step is to turn your top-level set of equations for <code>foldl</code> into a lambda expression which uses case analysis, like so:</p> <pre><code>val rec foldl = fn f =&gt; fn b =&gt; fn lst =&gt; case lst of [] =&gt; b | (h::t) =&gt; foldl f (f(h,b)) t </code></pre> <p>Now you can use the same logic as before. Taking as an example the function <code>fn (x, y) =&gt; x * y</code>, we can see that</p> <pre><code>val prod = foldl (fn (x, y) =&gt; x * y) </code></pre> <p>is equivalent to</p> <pre><code>val prod = (fn f =&gt; fn b =&gt; fn lst =&gt; case lst of [] =&gt; b | (h::t) =&gt; foldl f (f(h,b)) t) (fn (x, y) =&gt; x * y) </code></pre> <p>which <a href="http://en.wikipedia.org/wiki/Beta_reduction#Reduction" rel="nofollow">beta-reduces</a> to</p> <pre><code>val prod = fn b =&gt; fn lst =&gt; case lst of [] =&gt; b | (h::t) =&gt; foldl (fn (x, y) =&gt; x * y) ((fn (x, y) =&gt; x * y)(h,b)) t </code></pre> <p>which beta-reduces to</p> <pre><code>val prod = fn b =&gt; fn lst =&gt; case lst of [] =&gt; b | (h::t) =&gt; foldl (fn (x, y) =&gt; x * y) (h * b) t </code></pre> <p>Now since we know from our first definition that <code>prod</code> is equivalent to <code>foldl (fn (x, y) =&gt; x * y)</code>, we can substitute it into its own definition:</p> <pre><code>val rec prod = fn b =&gt; fn lst =&gt; case lst of [] =&gt; b | (h::t) =&gt; prod (h * b) t </code></pre> <p>We can then mentally convert this back to a function defined by equations if we like:</p> <pre><code>fun prod b [] = b | prod b (h::t) = prod (h * b) t </code></pre> <p>That's about what you'd expect, right?</p>
 

Querying!

 
Guidance

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload