[<<][compsci][>>][..]

Tue May 11 08:50:46 EDT 2010

## S K combinators and the Reader monad

The S and K combinators form a complete set of combinators that can
encode all lambda terms. The proof consists of a mechanised
transformation T explained in [1]. The trick is in the process of
abstraction elimination in rules 5 and 6.
5. T[λx.λy.E] => T[λx.T[λy.E]] (if x occurs free in E)
6. T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂])
Abstractions provide a means to access values passed in by
applications in "outer shells" of a lambda term using their name.
The S combinator works the other way around, it can be interpreted to
operate on binary trees that correspond to applications, propagating
values to branches of a binary tree. I.e. the S combinator passes
some values "under water".
Starting from lambda terms, this binary tree is created by the T
transform, where each application creates a fork point. Rule 5 makes
sure that each abstraction is directly followed by an application, and
rule 6 eliminates the abstraction by representing it as an S
combinator.
Short: all abstractions can be represented by passing values down
branches of a binary expression tree.
From this perspective it is not surprising that S and K pop up as
(<*>) and return from the Reader (environment) monad.
newtype Reader e a = Reader { runReader :: (e -> a) }
instance Monad (Reader e) where
return a = Reader $ \e -> a
(Reader r) >>= f = Reader $ \e -> (runReader $ f (r e)) e
Compare these to S and K.
The K combinator is a non-tagged version of Reader's return.
k :: a -> e -> a
k x e = x
The S combinator is a non-tagged version of Reader's (<*>)
s :: (e -> a -> b) -> (e -> a) -> e -> b
s x y e = (x e) (y e)
(<*>) :: (Applicative f) => f (a -> b) -> f a -> f b
[1] http://en.wikipedia.org/wiki/Combinatory_logic#Completeness_of_the_S-K_basis
[2] http://en.wikipedia.org/wiki/SKI_combinator_calculus

[Reply][About]

[<<][compsci][>>][..]