[Gotttzsche]

i dont understand the identity function that uses just C and S. :(

C x y = x

S x y z = (x z) (y z)

\I = (S C C)

so uh... that would evaluate to (\z (C z) (C z)), right? and then to (\z z z)? but then you got z twice. what does that even mean? applying z to z?

[fexl]

Oh I love questions like these, thanks!

You went off the rails because you replaced (C z) with z. That is not a valid equivalence. (C z) does not equal z. But (C z) applied to anything else does equal z. So in particular, (C z) (C z) equals z.

Here's how the reduction sequence goes:

  : S C C z
  = (C z) (C z)
  = z

If you think about it, that second C can be replace with anything and it still works:

  : S C anything z
  = (C z) (anything z)
  = z

That C there simply "holds on" to its first argument, and then when it encounters any second argument, it ignores it completely and yields up the thing it was holding onto.

[eru]

I z = (S C C) z = (C z) (C z) = C z _ = z

Where _ stands for a value that doesn't matter.

And actually for any x we have S C x == I.

[fexl]

Yes, I like that expository technique of using "_".

Often when I develop a Fexl function I actually use "_" as a placeholder for "something I haven't implemented yet". So if I'm doing something with a list, I might say:

  list
    _
    \head\tail _

And then I just go back and replace each "_" with an implementation of that particular case. In doing so, I might create new "_" slots ("holes"), which I then implement, and then I repeat this process until no more holes appear. It's a really good "case analysis" approach to programming.

For example I used this approach to implement an associative key-value map structure which uses nested lists, where a list at level N branches on the Nth character of the key, so it's a radix-style algorithm but without splitting the keys into pieces:

    # Helper function.

    \map_put == (\map\pos\key\val
        map             
            (item (pair key (pair val end)) map)
            \head\tail
            head \top_key\top_node

            # Do a three-way comparison of key char at pos
            # with the top key char at that pos.

            long_compare (string_at key pos) (string_at top_key pos)

                # key char is less than top key char
                (item (pair key (pair val end)) map)

                # key char equals top key char
                (
                top_node \top_val\top_map
                \new_head =
                    (
                    string_compare key top_key
                        (pair key (pair val
                            (map_put top_map (long_add pos 1) top_key top_val)))
                        (pair key (pair val top_map))
                        (pair top_key (pair top_val
                            (map_put top_map (long_add pos 1) key val)))
                    )
                item new_head tail
                )

                # key char is greater than top key char
                (item head (map_put tail pos key val))
        )   
    
    # The actual function (map_put key val).  This just
    # calls the helper function with position 0 to start.
    # I should probably re-order the helper function so
    # pos is the last argument, then I can define this
    # function simply as \map_put = (map_put 0).

    \map_put = (\map\key\val map_put map 0 key val)

[eru]

Thanks!

By the way, if you like SKI calculus, you would have loved this year's ICFP programming contest.

[fexl]

Also, you'd be surprised at how self-application can actually mean something. Consider how a recursive function is defined using the Y combinator, which is governed by this rule:

  Y F = F (Y F)

OK now that's not exactly self-application yet, but now let's dig into the Y combinator a bit and see how it can be defined in terms of a Q combinator:

  Y = S Q Q

Now what is Q you ask? It can be defined as a lambda expression this way:

  \Q = (\x\y x (y y))

Aha! There's a self-application for you. See how y is applied to itself there.

Now let's use the abstraction algorithm to convert Q into combinators step by step, removing the variables:

  \Q = (\x\y x (y y))
  \Q = (\x S (\y x) (\y y y))
  \Q = (\x S (C x) (S (\y y) (\y y)))
  \Q = (\x S (C x) (S I I))
  \Q = (S (\x S (C x)) (\x S I I))
  \Q = (S (S (\x S) (\x C x)) (C (S I I))
  \Q = (S (S (C S) C)) (C (S I I))

OK that was kind of fun but all I did was demonstrate that Q can be defined in terms of S and C. That's actually somewhat irrelevant. The main point is to demonstrate that when you apply the Y combinator to an arbitrary function, you can in effect get recursion. So let's follow the reduction sequence:

  : Y F
  = S Q Q F
  = (Q F) (Q F)
  = Q F (Q F)
  = F ((Q F) (Q F))
  = F (S Q Q F)
  = F (Y F)

Now let's show how you can actually remove self-reference from a recursive function. Consider this recursive definition of the function which appends two lists:

  \append == (\x\y x y \h\t cons h; append t y)

Now as it turns out, the "==" in Fexl is merely a short-hand which does this for you:

  \append = (Y \append \x\y x y \h\t cons h; append t y)

That's actually a non-recursive definition of append there. Consider the body of the function by itself:

  (Y \append \x\y x y \h\t cons h; append t y)

There are no free variables in that. The inner call to "append" actually refers to the \append when encloses it. So you actually have a fully closed form function there which calls itself.

You can look at it this way, separating that inner function out and calling it F:

  \F = (\append \x\y x y \h\t cons h; append t y)
  \append = (Y F)

So if we actually apply that function to two lists, it goes like this:

  : append x y
  = Y F x y
  = F (Y F) x y
  = F append x y
  = (\x\y x y \h\t cons h; append t y) x y
  = x y \h\t cons h; append t y

And then it proceeds from there depending on what x is. It's amazing stuff, being able to defined a fully closed-form function which somehow manages to reach out and call itself. :)

[fexl]

Now on another topic which I find interesting, consider how the abstraction algorithm (conversion to combinators) can be simplified with the use of two helper functions L and R:

  \L = (\x\y\z (x z) y)  # send z to left side only
  \R = (\x\y\z x (y z))  # send z to right side only

Of course these can be defined in terms of S and C but I just implement them directly in the interpreter for efficiency.

Now let's abstract the Q definition using L and R in addition to S and C where possible:

  \Q = (\x\y x (y y))
  \Q = (\x R x (\y y y))
  \Q = (\x R x (S I I))
  \Q = (L (\x R x) (S I I))
  \Q = (L R (S I I))

That's much more compact than just using S and C alone.