Sat Apr 17 12:21:35 EDT 2010

Lambda Calculus for Electrical Engineers

If you look at the lambda calculus, it only ever talks about:

  * variable introduction or abstraction = make a socket

  * variable elimination or application = this plug goes in that socket

The fact that it uses variables is really not that interesting and
largely a consequence of paper being a flat medium.  I.e. the
"essence" of the LC needs to be embedded into something that can be
written on paper as a flattened graph.  First flatten the graph into a
tree by introducing variable names, then flatten the tree to a
sequence of symbols in the usual sense by introducing parenthesis and
precedence rules.

This horrible notation really makes it look bad and hides its true

Something clicked for me when I made this "paper serialization"
explicit in the way I looked at the LC, and seeing its intrinsic
beauty: an LC expression represents a directed a-cyclic graph of
computation modules.

Now _that_ is something that should make a lot of sense to an
electrical engineer thinking of wires and amplifiers.  Morale:

    The idea of "connectedness" that can be expressed by abstraction
    and application is tremendously powerful.

There is one problem however.  Variables in the lambda calculus
represent computations, meaning the only values are other lambda
terms.  In some sense it doesn't exist as there are no primitive
objects that are not computations themselves.  Thies defies intuition,
at least mine.  Computation should map things to things, not
computations to computations, right?

Typed lambda calculi fix this by introducing primitive types, for the
simple reason that without them, terms cannot be annotated with types.

One can argue that the due to the existence of primitives and
computations, the simply typed lambda calculus might be the best way
to introduce the lambda calculus in a more concrete way.