lambda abstraction a la Arrows

RE01 Rice Brian T. EM2 BRice@vinson.navy.mil
Mon, 4 Jan 1999 23:06:23 +0300


here's a description of what lambda abstraction means in the arrow system.
we'll start with the classical way of stating a lambda abstraction and
attempt to abstract all the issues which depend on text and separate them
from the concept of the lambda operator.

first, the lambda operator returns an expression given a symbol and an
expression, in the interpretation that i'll use here.  this allows the
concept of function and functor to merge seamlessly into repeated
applications of lambdas, yielding functions with multiple arguments.  the
syntax tree for such an action is a binary one.
the symbol creation aspect of the lambda operator is something that i'll
consider noise with respect to the problem of identifying the meaning of the
expression formed, basically because introducing a symbol with a lambda when
the symbol is already previously used in the system (i mean that the same
text token has already been pushed onto a reader's symbol table) creates a
different operator, despite the textual conflict.  so, the central issue
must be that a symbol is postulated which is invoked within the second part
of the lambda expression in a definite group of places.
i propose that within the Arrow system, the lack of textual symbols would
simply allow us to postulate a new node and then attach it to the invocation
points directly.  of course, this new node is accessible from outside of the
lambda's arguments as 'the input for such-and-such lambda expression'.  so,
the new abstract lambda operator must have internal ordered structure - a
binary one, one ideally suited to the Arrow system.
this view of the lambda operator suggests a simple solution: a lambda would
first involve an arrow from a node to a syntax tree for the expression,
using the representation i discussed for the inference system - a binary
tree of arrows and nodes, with a mapping of the nodes to the symbols used.
it would of course also involve a mapping from the postulated node to the
invocation points within the lambda expression.
the prospect of currying on this form would be a node postulation with an
arrow directed from that node to the next lambda operation.
the lambda symbol itself would be mapped to its invocation points as well,
and a syntax tree could be abstracted easily from this form.  in fact, this
easily integrates into a unified syntax tree with the lambda operator a
binary one.
this still doesn't answer the question of how a new node is to be
postulated, and i don't believe that it matters from this standpoint.

another thing comes to mind:

this talk of the interchangeability of an operator like the lambda
representation i have proposed with an integrated syntax graph recalls the
notion of the abstration operator which took an arrow and mapped it to a
node with two arrows, one from and one to the node which denoted the head
and tail pointers, respectively.  using the inverse of this operator
(conceptually), all syntax trees could be simplified into a
multi-dimensional arrow (a Lisp-style linked list) where each arrow
represented a binary operator, with currying implemented as necessary to
construct operators of higher argument number.  the way that the arrows
would represent operators would be via a mapping from the symbol definitions
to the invocation points.

something which should enlighten things for you a great deal as to how the
system deals with such a complicated system and separate the list structure
from its contents as well as the various mappings is to distinguish any
conceptual group of arrows explicitly for the computer using the
multi-dimensional arrow concept, and to link that arrow to the specification
of the concept.